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

liquid_fixpoint/
lib.rs
