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

liquid_fixpoint/
lib.rs
