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

liquid_fixpoint/
lib.rs
