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

liquid_fixpoint/
lib.rs
