liquid_fixpoint/
lib.rs

1//! This crate implements an interface to the [liquid-fixpoint] binary
2//!
3//! [liquid-fixpoint]: https://github.com/ucsd-progsys/liquid-fixpoint
4#![cfg_attr(feature = "nightly", feature(rustc_private))]
5
6#[cfg(feature = "nightly")]
7extern crate rustc_data_structures;
8#[cfg(feature = "nightly")]
9extern crate rustc_macros;
10#[cfg(feature = "nightly")]
11extern crate rustc_serialize;
12#[cfg(feature = "nightly")]
13extern crate rustc_span;
14
15mod constraint;
16#[cfg(feature = "rust-fixpoint")]
17mod constraint_fragments;
18#[cfg(feature = "rust-fixpoint")]
19mod constraint_solving;
20#[cfg(any(feature = "rust-fixpoint", feature = "suggestions"))]
21mod constraint_with_env;
22#[cfg(any(feature = "rust-fixpoint", feature = "suggestions"))]
23mod cstr2smt2;
24mod format;
25#[cfg(any(feature = "rust-fixpoint", feature = "suggestions"))]
26mod graph;
27pub mod parser;
28pub mod sexp;
29pub mod smt_horn;
30
31use std::{
32    collections::{HashMap, hash_map::DefaultHasher},
33    fmt::{self, Debug},
34    hash::{Hash, Hasher},
35    io,
36    str::FromStr,
37};
38#[cfg(not(feature = "rust-fixpoint"))]
39use std::{
40    io::{BufWriter, Write as IOWrite},
41    process::{Command, Stdio},
42};
43
44pub use constraint::{
45    BinOp, BinRel, Bind, Constant, Constraint, DataCtor, DataDecl, DataField, Expr, FlatConstraint,
46    FunSort, Pred, Qualifier, Quantifier, Sort, SortCtor, SortDecl, WKVar,
47};
48use derive_where::derive_where;
49#[cfg(feature = "nightly")]
50use rustc_macros::{Decodable, Encodable};
51use serde::{Deserialize, Serialize, de};
52
53/// Type alias for qualifier assignments used in constraint solving
54pub type Assignments<'a, T> = HashMap<<T as Types>::KVar, Vec<(&'a Qualifier<T>, Vec<usize>)>>;
55
56#[cfg(feature = "rust-fixpoint")]
57use crate::constraint_with_env::ConstraintWithEnv;
58#[cfg(feature = "suggestions")]
59use crate::constraint_with_env::topo_sort_data_declarations;
60
61pub trait Types {
62    type Sort: Identifier + Hash + Clone + Debug + Eq;
63    type KVar: Identifier + Hash + Clone + Debug + Eq;
64    type Var: Identifier + Hash + Clone + Debug + Eq;
65    type String: FixpointFmt + Hash + Clone + Debug + Eq;
66    type Real: FixpointFmt + Hash + Clone + Debug + Eq;
67    type Tag: fmt::Display + FromStr + Hash + Clone + Debug;
68}
69
70pub trait FixpointFmt: Sized {
71    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result;
72
73    /// Returns a type that implements [`fmt::Display`] using this [`FixpointFmt::fmt`] implementation.
74    fn display(&self) -> impl fmt::Display {
75        struct DisplayAdapter<T>(T);
76        impl<T: FixpointFmt> std::fmt::Display for DisplayAdapter<&T> {
77            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
78                FixpointFmt::fmt(self.0, f)
79            }
80        }
81        DisplayAdapter(self)
82    }
83}
84
85pub trait Identifier: Sized {
86    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result;
87
88    /// Returns a type that implements [`fmt::Display`] using this [`Identifier::fmt`] implementation.
89    fn display(&self) -> impl fmt::Display {
90        struct DisplayAdapter<T>(T);
91        impl<T: Identifier> fmt::Display for DisplayAdapter<&T> {
92            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
93                Identifier::fmt(self.0, f)
94            }
95        }
96        DisplayAdapter(self)
97    }
98}
99
100impl Identifier for &str {
101    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
102        write!(f, "{self}")
103    }
104}
105
106impl FixpointFmt for u32 {
107    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
108        write!(f, "{self}")
109    }
110}
111
112impl FixpointFmt for String {
113    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
114        write!(f, "\"{self}\"")
115    }
116}
117
118#[macro_export]
119macro_rules! declare_types {
120    (   type Sort = $sort:ty;
121        type KVar = $kvar:ty;
122        type Var = $var:ty;
123        type String = $str:ty;
124        type Real = $real:ty;
125        type Tag = $tag:ty;
126    ) => {
127        pub mod fixpoint_generated {
128            pub struct FixpointTypes;
129            pub type Expr = $crate::Expr<FixpointTypes>;
130            pub type Constraint = $crate::Constraint<FixpointTypes>;
131            pub type FlatConstraint = $crate::FlatConstraint<FixpointTypes>;
132            pub type KVarDecl = $crate::KVarDecl<FixpointTypes>;
133            pub type ConstDecl = $crate::ConstDecl<FixpointTypes>;
134            pub type FunDef = $crate::FunDef<FixpointTypes>;
135            pub type FunSort = $crate::FunSort<FixpointTypes>;
136            pub type FunBody = $crate::FunBody<FixpointTypes>;
137            pub type Task = $crate::Task<FixpointTypes>;
138            pub type Qualifier = $crate::Qualifier<FixpointTypes>;
139            pub type Sort = $crate::Sort<FixpointTypes>;
140            pub type SortCtor = $crate::SortCtor<FixpointTypes>;
141            pub type SortDecl = $crate::SortDecl<FixpointTypes>;
142            pub type DataDecl = $crate::DataDecl<FixpointTypes>;
143            pub type DataCtor = $crate::DataCtor<FixpointTypes>;
144            pub type DataField = $crate::DataField<FixpointTypes>;
145            pub type Bind = $crate::Bind<FixpointTypes>;
146            pub type Constant = $crate::Constant<FixpointTypes>;
147            pub type Pred = $crate::Pred<FixpointTypes>;
148            pub use $crate::{BinOp, BinRel, Quantifier, ThyFunc, WKVar};
149        }
150
151        impl $crate::Types for fixpoint_generated::FixpointTypes {
152            type Sort = $sort;
153            type KVar = $kvar;
154            type Var = $var;
155            type String = $str;
156            type Real = $real;
157            type Tag = $tag;
158        }
159    };
160}
161
162#[cfg(feature = "suggestions")]
163pub fn qe_and_simplify<T: Types>(
164    constraint: &FlatConstraint<T>,
165    binder_consts: &Vec<ConstDecl<T>>,
166    global_consts: &Vec<ConstDecl<T>>,
167    datatype_decls: Vec<DataDecl<T>>,
168) -> Result<Expr<T>, cstr2smt2::Z3DecodeError> {
169    // let mut consts = self.constants.clone();
170    // consts.extend(free_vars.clone());
171    let datatype_decls = topo_sort_data_declarations(datatype_decls);
172    cstr2smt2::qe_and_simplify(constraint, binder_consts, global_consts, &datatype_decls)
173}
174
175#[cfg(feature = "suggestions")]
176pub fn check_validity<T: Types>(
177    constraint: &FlatConstraint<T>,
178    binder_consts: &Vec<ConstDecl<T>>,
179    global_consts: &Vec<ConstDecl<T>>,
180    datatype_decls: Vec<DataDecl<T>>,
181) -> bool {
182    let datatype_decls = topo_sort_data_declarations(datatype_decls);
183    cstr2smt2::check_validity(constraint, binder_consts, global_consts, &datatype_decls)
184}
185
186#[derive_where(Hash, Clone, Debug)]
187pub struct ConstDecl<T: Types> {
188    pub name: T::Var,
189    pub sort: Sort<T>,
190    #[derive_where(skip)]
191    pub comment: Option<String>,
192}
193
194#[derive_where(Hash, Debug)]
195pub struct FunDef<T: Types> {
196    pub name: T::Var,
197    pub sort: FunSort<T>,
198    pub body: Option<FunBody<T>>,
199    #[derive_where(skip)]
200    pub comment: Option<String>,
201}
202
203#[derive_where(Hash, Debug)]
204pub struct FunBody<T: Types> {
205    pub args: Vec<T::Var>,
206    pub expr: Expr<T>,
207}
208
209#[derive_where(Hash)]
210pub struct Task<T: Types> {
211    #[derive_where(skip)]
212    pub comments: Vec<String>,
213    pub constants: Vec<ConstDecl<T>>,
214    pub data_decls: Vec<DataDecl<T>>,
215    pub define_funs: Vec<FunDef<T>>,
216    pub kvars: Vec<KVarDecl<T>>,
217    pub constraint: Constraint<T>,
218    pub qualifiers: Vec<Qualifier<T>>,
219    pub scrape_quals: bool,
220    pub solver: SmtSolver,
221}
222
223#[derive(Clone, Copy, Hash)]
224pub enum SmtSolver {
225    Z3,
226    CVC5,
227}
228
229impl fmt::Display for SmtSolver {
230    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
231        match self {
232            SmtSolver::Z3 => write!(f, "z3"),
233            SmtSolver::CVC5 => write!(f, "cvc5"),
234        }
235    }
236}
237
238#[derive(Serialize, Deserialize, Debug, Clone)]
239#[serde(
240    tag = "tag",
241    content = "contents",
242    bound(deserialize = "Tag: FromStr", serialize = "Tag: ToString")
243)]
244pub enum FixpointStatus<Tag> {
245    Safe(Stats),
246    Unsafe(Stats, Vec<Error<Tag>>),
247    Crash(CrashInfo),
248}
249
250#[derive(Serialize, Deserialize, Debug, Clone, Default)]
251#[serde(tag = "tag", content = "contents")]
252pub enum LeanStatus {
253    #[default]
254    Invalid,
255    Valid,
256}
257
258#[derive(Serialize, Deserialize, Debug, Clone)]
259#[serde(bound(deserialize = "Tag: FromStr", serialize = "Tag: ToString"))]
260pub struct VerificationResult<Tag> {
261    pub status: FixpointStatus<Tag>,
262    pub solution: Vec<KVarBind>,
263    #[serde(rename = "nonCutsSolution")]
264    pub non_cuts_solution: Vec<KVarBind>,
265    #[serde(default)]
266    pub lean_status: LeanStatus,
267}
268
269#[derive(Serialize, Deserialize, Debug, Clone)]
270pub struct KVarBind {
271    pub kvar: String,
272    pub val: String,
273}
274
275impl KVarBind {
276    pub fn dump(&self) -> String {
277        format!("{} := {}", self.kvar, self.val)
278    }
279}
280
281impl<Tag> FixpointStatus<Tag> {
282    pub fn is_safe(&self) -> bool {
283        matches!(self, FixpointStatus::Safe(_))
284    }
285
286    pub fn merge(self, other: FixpointStatus<Tag>) -> Self {
287        use FixpointStatus as FR;
288        match (self, other) {
289            (FR::Safe(stats1), FR::Safe(stats2)) => FR::Safe(stats1.merge(&stats2)),
290            (FR::Safe(stats1), FR::Unsafe(stats2, errors)) => {
291                FR::Unsafe(stats1.merge(&stats2), errors)
292            }
293            (FR::Unsafe(stats1, mut errors1), FR::Unsafe(stats2, errors2)) => {
294                errors1.extend(errors2);
295                FR::Unsafe(stats1.merge(&stats2), errors1)
296            }
297            (FR::Unsafe(stats1, errors), FR::Safe(stats2)) => {
298                FR::Unsafe(stats1.merge(&stats2), errors)
299            }
300            (FR::Crash(info1), FR::Crash(info2)) => FR::Crash(info1.merge(info2)),
301            (FR::Crash(info), _) => FR::Crash(info),
302            (_, FR::Crash(info)) => FR::Crash(info),
303        }
304    }
305}
306
307#[derive(Debug, Clone)]
308pub struct Error<Tag> {
309    pub id: i32,
310    pub tag: Tag,
311}
312
313#[derive(Debug, Serialize, Deserialize, Default, Clone)]
314#[serde(rename_all = "camelCase")]
315pub struct Stats {
316    pub num_cstr: i32,
317    pub num_iter: i32,
318    pub num_chck: i32,
319    pub num_vald: i32,
320}
321
322impl Stats {
323    pub fn merge(&self, other: &Stats) -> Self {
324        Stats {
325            num_cstr: self.num_cstr + other.num_cstr,
326            num_iter: self.num_iter + other.num_iter,
327            num_chck: self.num_chck + other.num_chck,
328            num_vald: self.num_vald + other.num_vald,
329        }
330    }
331}
332
333#[derive(Serialize, Deserialize, Debug, Clone)]
334pub struct CrashInfo(Vec<serde_json::Value>);
335
336impl CrashInfo {
337    pub fn merge(self, other: CrashInfo) -> Self {
338        let mut v = self.0;
339        v.extend(other.0);
340        CrashInfo(v)
341    }
342}
343
344#[derive_where(Debug, Clone, Hash)]
345pub struct KVarDecl<T: Types> {
346    pub kvid: T::KVar,
347    pub sorts: Vec<Sort<T>>,
348    #[derive_where(skip)]
349    pub comment: String,
350}
351
352impl<T: Types> Task<T> {
353    pub fn hash_with_default(&self) -> u64 {
354        let mut hasher = DefaultHasher::new();
355        self.hash(&mut hasher);
356        hasher.finish()
357    }
358
359    #[cfg(feature = "rust-fixpoint")]
360    pub fn run(&self) -> io::Result<VerificationResult<T::Tag>> {
361        let mut cstr_with_env = ConstraintWithEnv::new(
362            self.data_decls.clone(),
363            self.kvars.clone(),
364            self.qualifiers.clone(),
365            self.constants.clone(),
366            self.constraint.clone(),
367        );
368        Ok(VerificationResult {
369            status: cstr_with_env.is_satisfiable(),
370            solution: vec![],
371            non_cuts_solution: vec![],
372            lean_status: LeanStatus::default(),
373        })
374    }
375
376    #[cfg(not(feature = "rust-fixpoint"))]
377    pub fn run(&self) -> io::Result<VerificationResult<T::Tag>> {
378        let mut child = Command::new("fixpoint")
379            .arg("-q")
380            .arg("--stdin")
381            .arg("--sorted-solution")
382            .arg("--json")
383            .arg("--allowho")
384            .arg("--allowhoqs")
385            .arg(format!("--solver={}", self.solver))
386            .stdin(Stdio::piped())
387            .stdout(Stdio::piped())
388            .stderr(Stdio::piped())
389            .spawn()?;
390        let mut stdin = None;
391        std::mem::swap(&mut stdin, &mut child.stdin);
392        {
393            let mut w = BufWriter::new(stdin.unwrap());
394            // Use compact formatting to reduce overhead when communicating with fixpoint
395            writeln!(w, "{}", format::CompactTask(self))?;
396        }
397        let out = child.wait_with_output()?;
398
399        serde_json::from_slice(&out.stdout).map_err(|err| {
400            // If we fail to parse stdout fixpoint may have outputed something to stderr
401            // so use that for the error instead
402            if !out.stderr.is_empty() {
403                let stderr = std::str::from_utf8(&out.stderr)
404                    .unwrap_or("fixpoint exited with a non-zero return code");
405                io::Error::other(stderr)
406            } else {
407                err.into()
408            }
409        })
410    }
411}
412
413impl<T: Types> KVarDecl<T> {
414    pub fn new(kvid: T::KVar, sorts: Vec<Sort<T>>, comment: String) -> Self {
415        Self { kvid, sorts, comment }
416    }
417}
418
419#[derive(Serialize, Deserialize)]
420struct ErrorInner(i32, String);
421
422impl<Tag: ToString> Serialize for Error<Tag> {
423    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
424    where
425        S: serde::Serializer,
426    {
427        ErrorInner(self.id, self.tag.to_string()).serialize(serializer)
428    }
429}
430
431impl<'de, Tag: FromStr> Deserialize<'de> for Error<Tag> {
432    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
433    where
434        D: serde::Deserializer<'de>,
435    {
436        let ErrorInner(id, tag) = Deserialize::deserialize(deserializer)?;
437        let tag = tag
438            .parse()
439            .map_err(|_| de::Error::invalid_value(de::Unexpected::Str(&tag), &"valid tag"))?;
440        Ok(Error { id, tag })
441    }
442}
443
444#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
445#[cfg_attr(feature = "nightly", derive(Encodable, Decodable))]
446pub enum ThyFunc {
447    // STRINGS
448    StrLen,
449    StrConcat,
450    StrPrefixOf,
451    StrSuffixOf,
452    StrContains,
453
454    // BIT VECTORS
455    BvZeroExtend(u8),
456    BvSignExtend(u8),
457    IntToBv8,
458    Bv8ToInt,
459    IntToBv32,
460    Bv32ToInt,
461    IntToBv64,
462    Bv64ToInt,
463    BvUle,
464    BvSle,
465    BvUge,
466    BvSge,
467    BvUdiv,
468    BvSdiv,
469    BvSrem,
470    BvUrem,
471    BvLshr,
472    BvAshr,
473    BvAnd,
474    BvOr,
475    BvXor,
476    BvNot,
477    BvAdd,
478    BvNeg,
479    BvSub,
480    BvMul,
481    BvShl,
482    BvUgt,
483    BvSgt,
484    BvUlt,
485    BvSlt,
486
487    // SETS
488    /// Make an empty set
489    SetEmpty,
490    /// Make a singleton set
491    SetSng,
492    /// Set union
493    SetCup,
494    /// Set intersection
495    SetCap,
496    /// Set difference
497    SetDif,
498    /// Subset
499    SetSub,
500    /// Set membership
501    SetMem,
502
503    // MAPS
504    /// Create a map where all keys point to a value
505    MapDefault,
506    /// Select a key in a map
507    MapSelect,
508    /// Store a key value pair in a map
509    MapStore,
510}
511
512impl ThyFunc {
513    pub const ALL: [ThyFunc; 44] = [
514        ThyFunc::StrLen,
515        ThyFunc::StrConcat,
516        ThyFunc::StrPrefixOf,
517        ThyFunc::StrSuffixOf,
518        ThyFunc::StrContains,
519        ThyFunc::IntToBv8,
520        ThyFunc::Bv8ToInt,
521        ThyFunc::IntToBv32,
522        ThyFunc::Bv32ToInt,
523        ThyFunc::IntToBv64,
524        ThyFunc::Bv64ToInt,
525        ThyFunc::BvAdd,
526        ThyFunc::BvNeg,
527        ThyFunc::BvSub,
528        ThyFunc::BvShl,
529        ThyFunc::BvLshr,
530        ThyFunc::BvAshr,
531        ThyFunc::BvMul,
532        ThyFunc::BvUdiv,
533        ThyFunc::BvSdiv,
534        ThyFunc::BvUrem,
535        ThyFunc::BvSrem,
536        ThyFunc::BvAnd,
537        ThyFunc::BvOr,
538        ThyFunc::BvXor,
539        ThyFunc::BvNot,
540        ThyFunc::BvUle,
541        ThyFunc::BvSle,
542        ThyFunc::BvUge,
543        ThyFunc::BvSge,
544        ThyFunc::BvUgt,
545        ThyFunc::BvSgt,
546        ThyFunc::BvUlt,
547        ThyFunc::BvSlt,
548        ThyFunc::SetEmpty,
549        ThyFunc::SetSng,
550        ThyFunc::SetCup,
551        ThyFunc::SetMem,
552        ThyFunc::SetCap,
553        ThyFunc::SetDif,
554        ThyFunc::SetSub,
555        ThyFunc::MapDefault,
556        ThyFunc::MapSelect,
557        ThyFunc::MapStore,
558    ];
559}
560
561impl fmt::Display for ThyFunc {
562    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
563        match self {
564            ThyFunc::StrLen => write!(f, "strLen"),
565            ThyFunc::StrConcat => write!(f, "strConcat"),
566            ThyFunc::StrPrefixOf => write!(f, "strPrefixOf"),
567            ThyFunc::StrSuffixOf => write!(f, "strSuffixOf"),
568            ThyFunc::StrContains => write!(f, "strContains"),
569            ThyFunc::BvZeroExtend(size) => {
570                // `app` is a hack in liquid-fixpoint used to implement indexed identifiers
571                write!(f, "app (_ zero_extend {size})")
572            }
573            ThyFunc::BvSignExtend(size) => write!(f, "app (_ sign_extend {size})"),
574            ThyFunc::IntToBv32 => write!(f, "int_to_bv32"),
575            ThyFunc::Bv32ToInt => write!(f, "bv32_to_int"),
576            ThyFunc::IntToBv8 => write!(f, "int_to_bv8"),
577            ThyFunc::Bv8ToInt => write!(f, "bv8_to_int"),
578            ThyFunc::IntToBv64 => write!(f, "int_to_bv64"),
579            ThyFunc::Bv64ToInt => write!(f, "bv64_to_int"),
580            ThyFunc::BvUle => write!(f, "bvule"),
581            ThyFunc::BvSle => write!(f, "bvsle"),
582            ThyFunc::BvUge => write!(f, "bvuge"),
583            ThyFunc::BvSge => write!(f, "bvsge"),
584            ThyFunc::BvUdiv => write!(f, "bvudiv"),
585            ThyFunc::BvSdiv => write!(f, "bvsdiv"),
586            ThyFunc::BvUrem => write!(f, "bvurem"),
587            ThyFunc::BvSrem => write!(f, "bvsrem"),
588            ThyFunc::BvLshr => write!(f, "bvlshr"),
589            ThyFunc::BvAshr => write!(f, "bvashr"),
590            ThyFunc::BvAnd => write!(f, "bvand"),
591            ThyFunc::BvOr => write!(f, "bvor"),
592            ThyFunc::BvXor => write!(f, "bvxor"),
593            ThyFunc::BvNot => write!(f, "bvnot"),
594            ThyFunc::BvAdd => write!(f, "bvadd"),
595            ThyFunc::BvNeg => write!(f, "bvneg"),
596            ThyFunc::BvSub => write!(f, "bvsub"),
597            ThyFunc::BvMul => write!(f, "bvmul"),
598            ThyFunc::BvShl => write!(f, "bvshl"),
599            ThyFunc::BvUgt => write!(f, "bvugt"),
600            ThyFunc::BvSgt => write!(f, "bvsgt"),
601            ThyFunc::BvUlt => write!(f, "bvult"),
602            ThyFunc::BvSlt => write!(f, "bvslt"),
603            ThyFunc::SetEmpty => write!(f, "Set_empty"),
604            ThyFunc::SetSng => write!(f, "Set_sng"),
605            ThyFunc::SetCup => write!(f, "Set_cup"),
606            ThyFunc::SetCap => write!(f, "Set_cap"),
607            ThyFunc::SetDif => write!(f, "Set_dif"),
608            ThyFunc::SetMem => write!(f, "Set_mem"),
609            ThyFunc::SetSub => write!(f, "Set_sub"),
610            ThyFunc::MapDefault => write!(f, "Map_default"),
611            ThyFunc::MapSelect => write!(f, "Map_select"),
612            ThyFunc::MapStore => write!(f, "Map_store"),
613        }
614    }
615}
616
617impl FromStr for ThyFunc {
618    type Err = String;
619    fn from_str(s: &str) -> Result<Self, Self::Err> {
620        match s {
621            "strLen" => Ok(ThyFunc::StrLen),
622            "int_to_bv32" => Ok(ThyFunc::IntToBv32),
623            "bv32_to_int" => Ok(ThyFunc::Bv32ToInt),
624            "int_to_bv8" => Ok(ThyFunc::IntToBv8),
625            "bv8_to_int" => Ok(ThyFunc::Bv8ToInt),
626            "int_to_bv64" => Ok(ThyFunc::IntToBv64),
627            "bv64_to_int" => Ok(ThyFunc::Bv64ToInt),
628            "bvule" => Ok(ThyFunc::BvUle),
629            "bvsle" => Ok(ThyFunc::BvSle),
630            "bvuge" => Ok(ThyFunc::BvUge),
631            "bvsge" => Ok(ThyFunc::BvSge),
632            "bvudiv" => Ok(ThyFunc::BvUdiv),
633            "bvsdiv" => Ok(ThyFunc::BvSdiv),
634            "bvurem" => Ok(ThyFunc::BvUrem),
635            "bvsrem" => Ok(ThyFunc::BvSrem),
636            "bvlshr" => Ok(ThyFunc::BvLshr),
637            "bvashr" => Ok(ThyFunc::BvAshr),
638            "bvand" => Ok(ThyFunc::BvAnd),
639            "bvor" => Ok(ThyFunc::BvOr),
640            "bvxor" => Ok(ThyFunc::BvXor),
641            "bvnot" => Ok(ThyFunc::BvNot),
642            "bvadd" => Ok(ThyFunc::BvAdd),
643            "bvneg" => Ok(ThyFunc::BvNeg),
644            "bvsub" => Ok(ThyFunc::BvSub),
645            "bvmul" => Ok(ThyFunc::BvMul),
646            "bvshl" => Ok(ThyFunc::BvShl),
647            "bvugt" => Ok(ThyFunc::BvUgt),
648            "bvsgt" => Ok(ThyFunc::BvSgt),
649            "bvult" => Ok(ThyFunc::BvUlt),
650            "bvslt" => Ok(ThyFunc::BvSlt),
651            "Set_empty" => Ok(ThyFunc::SetEmpty),
652            "Set_sng" => Ok(ThyFunc::SetSng),
653            "Set_cup" => Ok(ThyFunc::SetCup),
654            "Set_mem" => Ok(ThyFunc::SetMem),
655            "Map_default" => Ok(ThyFunc::MapDefault),
656            "Map_select" => Ok(ThyFunc::MapSelect),
657            "Map_store" => Ok(ThyFunc::MapStore),
658            // TODO: (ck) Fix this?
659            // NOTE: (ck) There isn't a straightforward way to translate
660            // the name of a Z3 node to the BvZeroExtend and BvSignExtend,
661            // so this is a partial parse.
662            _ => Err(format!("Unexpected ThyFunc {}", s)),
663        }
664    }
665}
liquid_fixpoint/lib.rs

liquid_fixpoint/
lib.rs
