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

liquid_fixpoint/
lib.rs
