liquid_fixpoint/
smt_fmt.rs

1//! Shared SMTLIB serialization methods
2
3use std::{
4    collections::HashSet,
5    fmt::{self, Write},
6};
7
8use crate::{
9    BinOp, BinRel, Constant, DataDecl, Expr, FixpointFmt, FunDef, Identifier, Pred, Quantifier,
10    Sort, SortCtor, ThyFunc, Types,
11};
12
13macro_rules! parens {
14    ($out:ident, $body:block) => {{
15        $out.write_char('(')?;
16        $body;
17        $out.write_char(')')
18    }};
19}
20
21fn sexp_list<W, I, F>(out: &mut W, items: I, mut write_item: F) -> fmt::Result
22where
23    W: Write,
24    I: IntoIterator,
25    F: FnMut(&mut W, I::Item) -> fmt::Result,
26{
27    out.write_char('(')?;
28    for (i, item) in items.into_iter().enumerate() {
29        if i != 0 {
30            out.write_char(' ')?;
31        }
32        write_item(out, item)?;
33    }
34    out.write_char(')')
35}
36
37#[derive(Clone, Copy, Default)]
38pub(crate) enum FunctionEncoding {
39    /// Treat functions as... functions.
40    #[default]
41    FirstOrder,
42    /// Turn functions into arrays (what smt_horn did, not sure why)
43    ArrayApproximation,
44}
45
46#[derive(Clone, Copy)]
47pub(crate) enum PredicateEncoding {
48    /// Encode KVars as relations and panic on WKVars (in theory if we wanted it
49    /// to solve the wkvars, we would encode those as relations too).
50    Horn,
51    /// Panic on KVars and replace WKVars with true.
52    Suggestions,
53}
54
55#[derive(Clone, Copy)]
56pub(crate) struct SmtOptions {
57    pub functions: FunctionEncoding,
58    pub predicates: PredicateEncoding,
59}
60
61impl SmtOptions {
62    pub const HORN: Self = Self {
63        functions: FunctionEncoding::ArrayApproximation,
64        predicates: PredicateEncoding::Horn,
65    };
66
67    pub const SUGGESTIONS: Self = Self {
68        functions: FunctionEncoding::FirstOrder,
69        predicates: PredicateEncoding::Suggestions,
70    };
71}
72
73pub(crate) struct SmtEncoder<T: Types> {
74    options: SmtOptions,
75    constructors: HashSet<T::Var>,
76    datatypes: HashSet<T::Sort>,
77}
78
79impl<T: Types> SmtEncoder<T> {
80    pub fn new(data_decls: &[DataDecl<T>], options: SmtOptions) -> Self {
81        let constructors = data_decls
82            .iter()
83            .flat_map(|decl| decl.ctors.iter().map(|ctor| ctor.name.clone()))
84            .collect();
85        let datatypes = data_decls.iter().map(|decl| decl.name.clone()).collect();
86        Self { options, constructors, datatypes }
87    }
88
89    pub fn write_datatype_decl(&self, out: &mut impl Write, decl: &DataDecl<T>) -> fmt::Result {
90        let name = decl.name.display();
91        assert!(!decl.ctors.is_empty(), "datatype `{name}` has no constructors");
92
93        parens!(out, {
94            write!(out, "declare-datatypes (({name} {})) ", decl.vars)?;
95            parens!(out, {
96                if decl.vars > 0 {
97                    parens!(out, {
98                        write!(out, "par ")?;
99                        sexp_list(out, 0..decl.vars, |out, i| write!(out, "T{i}"))?;
100                        out.write_char(' ')?;
101                        self.write_datatype_ctors(out, decl)?;
102                    })?;
103                } else {
104                    self.write_datatype_ctors(out, decl)?;
105                }
106            })?;
107        })?;
108        writeln!(out)?;
109        Ok(())
110    }
111
112    fn write_datatype_ctors(&self, out: &mut impl Write, decl: &DataDecl<T>) -> fmt::Result {
113        sexp_list(out, &decl.ctors, |out, ctor| {
114            parens!(out, {
115                write!(out, "{}", ctor.name.display())?;
116                for field in &ctor.fields {
117                    out.write_char(' ')?;
118                    parens!(out, {
119                        write!(out, "{} ", field.name.display())?;
120                        self.write_sort_in_scope(out, &field.sort, true)?;
121                    })?;
122                }
123            })?;
124            Ok(())
125        })
126    }
127
128    pub fn write_const_decl(
129        &self,
130        out: &mut impl Write,
131        name: &str,
132        sort: &Sort<T>,
133    ) -> fmt::Result {
134        if matches!(self.options.functions, FunctionEncoding::ArrayApproximation) {
135            parens!(out, {
136                write!(out, "declare-const {name} ")?;
137                self.write_sort(out, sort)?;
138            })?;
139            writeln!(out)?;
140            return Ok(());
141        }
142
143        let mut inputs = Vec::new();
144        let mut output = sort;
145        while let Sort::Func(parts) = output {
146            inputs.push(&parts[0]);
147            output = &parts[1];
148        }
149        if matches!(output, Sort::Abs(..))
150            || inputs.iter().any(|sort| matches!(sort, Sort::Abs(..)))
151        {
152            panic!("polymorphic function declaration `{name}`");
153        }
154        if inputs.is_empty() {
155            parens!(out, {
156                write!(out, "declare-const {name} ")?;
157                self.write_sort(out, output)?;
158            })?;
159            writeln!(out)?;
160        } else {
161            self.write_fun_signature(out, name, &inputs, output)?;
162        }
163        Ok(())
164    }
165
166    fn write_fun_signature(
167        &self,
168        out: &mut impl Write,
169        name: &str,
170        inputs: &[&Sort<T>],
171        output: &Sort<T>,
172    ) -> fmt::Result {
173        parens!(out, {
174            write!(out, "declare-fun {name} ")?;
175            sexp_list(out, inputs, |out, sort| self.write_sort(out, sort))?;
176            out.write_char(' ')?;
177            self.write_sort(out, output)?;
178        })?;
179        writeln!(out)?;
180        Ok(())
181    }
182
183    pub fn write_fun_def(&self, out: &mut impl Write, fun: &FunDef<T>) -> fmt::Result {
184        if fun.sort.params > 0 && matches!(self.options.functions, FunctionEncoding::FirstOrder) {
185            panic!("polymorphic function declaration `{}`", fun.name.display());
186        }
187        if let Some(body) = &fun.body {
188            parens!(out, {
189                write!(out, "define-fun {} ", fun.name.display())?;
190                sexp_list(out, body.args.iter().zip(&fun.sort.inputs), |out, (name, sort)| {
191                    parens!(out, {
192                        write!(out, "{} ", name.display())?;
193                        self.write_sort(out, sort)?;
194                    })?;
195                    Ok(())
196                })?;
197                out.write_char(' ')?;
198                self.write_sort(out, &fun.sort.output)?;
199                out.write_char(' ')?;
200                self.write_expr(out, &body.expr)?;
201            })?;
202            writeln!(out)?;
203        } else {
204            let inputs = fun.sort.inputs.iter().collect::<Vec<_>>();
205            self.write_fun_signature(
206                out,
207                &fun.name.display().to_string(),
208                &inputs,
209                &fun.sort.output,
210            )?;
211        }
212        Ok(())
213    }
214
215    pub fn write_sort(&self, out: &mut impl Write, sort: &Sort<T>) -> fmt::Result {
216        self.write_sort_in_scope(out, sort, false)
217    }
218
219    fn write_sort_in_scope(
220        &self,
221        out: &mut impl Write,
222        sort: &Sort<T>,
223        in_datatype_params: bool,
224    ) -> fmt::Result {
225        match sort {
226            Sort::Int => out.write_str("Int")?,
227            Sort::Bool => out.write_str("Bool")?,
228            Sort::Real => out.write_str("Real")?,
229            Sort::Str => out.write_str("String")?,
230            Sort::BitVec(size) => {
231                let Sort::BvSize(size) = &**size else {
232                    panic!("non-constant bit-vector width");
233                };
234                write!(out, "(_ BitVec {size})")?;
235            }
236            Sort::BvSize(_) => {
237                panic!("bit-vector width used as a value sort");
238            }
239            Sort::Var(i) => {
240                write!(out, "T{i}")?;
241            }
242            Sort::Func(parts)
243                if matches!(self.options.functions, FunctionEncoding::ArrayApproximation) =>
244            {
245                parens!(out, {
246                    out.write_str("Array ")?;
247                    self.write_sort_in_scope(out, &parts[0], in_datatype_params)?;
248                    out.write_char(' ')?;
249                    self.write_sort_in_scope(out, &parts[1], in_datatype_params)?;
250                })?;
251            }
252            Sort::Abs(_, inner)
253                if matches!(self.options.functions, FunctionEncoding::ArrayApproximation) =>
254            {
255                self.write_sort_in_scope(out, inner, in_datatype_params)?;
256            }
257            Sort::Abs(..) | Sort::Func(_) => {
258                panic!("higher-rank or function value sort `{sort:?}`");
259            }
260            // If we don't recognize the sort, it is an opaque sort and we fall back to Int.
261            // The Haskell Fixpoint's fappSmtSort (Types/Theories.hs) has the same fallback.
262            // TODO: If/when we patch fixpoint, we should update this to have parity.
263            Sort::App(SortCtor::Data(name), _) if !self.datatypes.contains(name) => {
264                out.write_str("Int")?;
265            }
266            Sort::App(ctor, args) => {
267                if args.is_empty() {
268                    self.write_sort_ctor(out, ctor)?;
269                } else {
270                    parens!(out, {
271                        self.write_sort_ctor(out, ctor)?;
272                        for arg in args {
273                            out.write_char(' ')?;
274                            self.write_sort_in_scope(out, arg, in_datatype_params)?;
275                        }
276                    })?;
277                }
278            }
279        }
280        Ok(())
281    }
282
283    fn write_sort_ctor(&self, out: &mut impl Write, ctor: &SortCtor<T>) -> fmt::Result {
284        match ctor {
285            SortCtor::Set => out.write_str("Set"),
286            SortCtor::Map => out.write_str("Array"),
287            SortCtor::Data(name) => write!(out, "{}", name.display()),
288        }
289    }
290
291    pub fn pred(&self, pred: &Pred<T>) -> Result<String, fmt::Error> {
292        let mut out = String::new();
293        self.write_pred(&mut out, pred)?;
294        Ok(out)
295    }
296
297    pub fn write_pred(&self, out: &mut impl Write, pred: &Pred<T>) -> fmt::Result {
298        match pred {
299            Pred::Expr(expr) => self.write_expr(out, expr),
300            Pred::KVar(kvar, args) => {
301                match self.options.predicates {
302                    PredicateEncoding::Horn => {
303                        if args.is_empty() {
304                            write!(out, "{}", kvar.display())?;
305                        } else {
306                            parens!(out, {
307                                write!(out, "{}", kvar.display())?;
308                                for arg in args {
309                                    out.write_char(' ')?;
310                                    self.write_expr(out, arg)?;
311                                }
312                            })?;
313                        }
314                        Ok(())
315                    }
316                    PredicateEncoding::Suggestions => {
317                        panic!("ordinary KVar in suggestion query")
318                    }
319                }
320            }
321        }
322    }
323
324    pub fn expr(&self, expr: &Expr<T>) -> Result<String, fmt::Error> {
325        let mut out = String::new();
326        self.write_expr(&mut out, expr)?;
327        Ok(out)
328    }
329
330    fn write_weak_kvar(&self, out: &mut impl Write) -> fmt::Result {
331        match self.options.predicates {
332            PredicateEncoding::Suggestions => {
333                out.write_str("true")?;
334                Ok(())
335            }
336            PredicateEncoding::Horn => {
337                panic!("weak KVar in Horn query")
338            }
339        }
340    }
341
342    pub fn write_expr(&self, out: &mut impl Write, expr: &Expr<T>) -> fmt::Result {
343        match expr {
344            Expr::Constant(Constant::Numeral(n)) => write!(out, "{n}")?,
345            Expr::Constant(Constant::Boolean(b)) => write!(out, "{b}")?,
346            Expr::Constant(Constant::Real(n)) => write!(out, "{}", n.display())?,
347            Expr::Constant(Constant::String(s)) => write!(out, "{}", s.display())?,
348            Expr::Constant(Constant::BitVec(value, size)) => write!(out, "(_ bv{value} {size})")?,
349            Expr::Var(var) => write!(out, "{}", var.display())?,
350            Expr::WKVar(_) => self.write_weak_kvar(out)?,
351            Expr::Neg(inner) => self.write_unary(out, "-", inner)?,
352            Expr::Not(inner) => self.write_unary(out, "not", inner)?,
353            Expr::BinaryOp(op, args) => {
354                let op = match op {
355                    BinOp::Add => "+",
356                    BinOp::Sub => "-",
357                    BinOp::Mul => "*",
358                    BinOp::Div => "div",
359                    BinOp::Mod => "mod",
360                };
361                self.write_binary(out, op, &args[0], &args[1])?;
362            }
363            Expr::Atom(BinRel::Ne, args) => {
364                parens!(out, {
365                    out.write_str("not ")?;
366                    self.write_binary(out, "=", &args[0], &args[1])?;
367                })?;
368            }
369            Expr::Atom(rel, args) => {
370                let op = match rel {
371                    BinRel::Eq => "=",
372                    BinRel::Gt => ">",
373                    BinRel::Ge => ">=",
374                    BinRel::Lt => "<",
375                    BinRel::Le => "<=",
376                    BinRel::Ne => unreachable!(),
377                };
378                self.write_binary(out, op, &args[0], &args[1])?;
379            }
380            Expr::Imp(args) => self.write_binary(out, "=>", &args[0], &args[1])?,
381            Expr::Iff(args) => self.write_binary(out, "=", &args[0], &args[1])?,
382            Expr::And(exprs) => self.write_nary(out, "and", exprs, "true")?,
383            Expr::Or(exprs) => self.write_nary(out, "or", exprs, "false")?,
384            Expr::IfThenElse(args) => {
385                parens!(out, {
386                    out.write_str("ite ")?;
387                    self.write_expr(out, &args[0])?;
388                    out.write_char(' ')?;
389                    self.write_expr(out, &args[1])?;
390                    out.write_char(' ')?;
391                    self.write_expr(out, &args[2])?;
392                })?;
393            }
394            Expr::Let(name, args) => {
395                parens!(out, {
396                    out.write_str("let ")?;
397                    parens!(out, {
398                        parens!(out, {
399                            write!(out, "{} ", name.display())?;
400                            self.write_expr(out, &args[0])?;
401                        })?;
402                    })?;
403                    out.write_char(' ')?;
404                    self.write_expr(out, &args[1])?;
405                })?;
406            }
407            Expr::App(fun, _, args, out_sort) => {
408                if matches!(&**fun, Expr::WKVar(_)) {
409                    return self.write_weak_kvar(out);
410                }
411                if args.is_empty() {
412                    self.write_application_head(out, fun, out_sort.as_ref())?;
413                } else {
414                    parens!(out, {
415                        self.write_application_head(out, fun, out_sort.as_ref())?;
416                        for arg in args {
417                            out.write_char(' ')?;
418                            self.write_expr(out, arg)?;
419                        }
420                    })?;
421                }
422            }
423            Expr::ThyFunc(func) => self.write_thy_func(out, *func)?,
424            Expr::IsCtor(ctor, inner) => {
425                parens!(out, {
426                    write!(out, "(_ is {}) ", ctor.display())?;
427                    self.write_expr(out, inner)?;
428                })?;
429            }
430            Expr::Quantifier(quantifier, bindings, body) => {
431                let quantifier = match quantifier {
432                    Quantifier::Exists => "exists",
433                    Quantifier::Forall => "forall",
434                };
435                parens!(out, {
436                    write!(out, "{quantifier} ")?;
437                    sexp_list(out, bindings, |out, (name, sort)| {
438                        parens!(out, {
439                            write!(out, "{} ", name.display())?;
440                            self.write_sort(out, sort)?;
441                        })?;
442                        Ok(())
443                    })?;
444                    out.write_char(' ')?;
445                    self.write_expr(out, body)?;
446                })?;
447            }
448        }
449        Ok(())
450    }
451
452    fn write_application_head(
453        &self,
454        out: &mut impl Write,
455        fun: &Expr<T>,
456        out_sort: Option<&Sort<T>>,
457    ) -> fmt::Result {
458        match fun {
459            Expr::Var(name) if self.constructors.contains(name) && out_sort.is_some() => {
460                parens!(out, {
461                    write!(out, "as {} ", name.display())?;
462                    self.write_sort(out, out_sort.unwrap())?;
463                })?;
464            }
465            Expr::ThyFunc(ThyFunc::SetEmpty | ThyFunc::MapDefault) => {
466                let sort = out_sort.unwrap_or_else(|| {
467                    panic!("empty set or constant array without an output sort")
468                });
469                let name = if matches!(fun, Expr::ThyFunc(ThyFunc::SetEmpty)) {
470                    "emptyset"
471                } else {
472                    "const"
473                };
474                parens!(out, {
475                    write!(out, "as {name} ")?;
476                    self.write_sort(out, sort)?;
477                })?;
478            }
479            other => self.write_expr(out, other)?,
480        }
481        Ok(())
482    }
483
484    fn write_unary(&self, out: &mut impl Write, op: &str, expr: &Expr<T>) -> fmt::Result {
485        parens!(out, {
486            write!(out, "{op} ")?;
487            self.write_expr(out, expr)?;
488        })?;
489        Ok(())
490    }
491
492    fn write_binary(
493        &self,
494        out: &mut impl Write,
495        op: &str,
496        lhs: &Expr<T>,
497        rhs: &Expr<T>,
498    ) -> fmt::Result {
499        parens!(out, {
500            write!(out, "{op} ")?;
501            self.write_expr(out, lhs)?;
502            out.write_char(' ')?;
503            self.write_expr(out, rhs)?;
504        })?;
505        Ok(())
506    }
507
508    fn write_nary(
509        &self,
510        out: &mut impl Write,
511        op: &str,
512        exprs: &[Expr<T>],
513        empty: &str,
514    ) -> fmt::Result {
515        if exprs.is_empty() {
516            out.write_str(empty)?;
517            return Ok(());
518        }
519        parens!(out, {
520            write!(out, "{op}")?;
521            for expr in exprs {
522                out.write_char(' ')?;
523                self.write_expr(out, expr)?;
524            }
525        })?;
526        Ok(())
527    }
528
529    fn write_thy_func(&self, out: &mut impl Write, func: ThyFunc) -> fmt::Result {
530        let name = match func {
531            ThyFunc::StrLen => "str.len",
532            ThyFunc::StrConcat => "str.++",
533            ThyFunc::StrPrefixOf => "str.prefixof",
534            ThyFunc::StrSuffixOf => "str.suffixof",
535            ThyFunc::StrContains => "str.contains",
536            ThyFunc::BvZeroExtend(size) => {
537                write!(out, "(_ zero_extend {size})")?;
538                return Ok(());
539            }
540            ThyFunc::BvSignExtend(size) => {
541                write!(out, "(_ sign_extend {size})")?;
542                return Ok(());
543            }
544            ThyFunc::IntToBv8 => "(_ int2bv 8)",
545            ThyFunc::IntToBv32 => "(_ int2bv 32)",
546            ThyFunc::IntToBv64 => "(_ int2bv 64)",
547            ThyFunc::IntToBv128 => "(_ int2bv 128)",
548            ThyFunc::Bv8ToInt | ThyFunc::Bv32ToInt | ThyFunc::Bv64ToInt | ThyFunc::Bv128ToInt => {
549                "bv2int"
550            }
551            ThyFunc::BvUle => "bvule",
552            ThyFunc::BvSle => "bvsle",
553            ThyFunc::BvUge => "bvuge",
554            ThyFunc::BvSge => "bvsge",
555            ThyFunc::BvUdiv => "bvudiv",
556            ThyFunc::BvSdiv => "bvsdiv",
557            ThyFunc::BvSrem => "bvsrem",
558            ThyFunc::BvUrem => "bvurem",
559            ThyFunc::BvLshr => "bvlshr",
560            ThyFunc::BvAshr => "bvashr",
561            ThyFunc::BvAnd => "bvand",
562            ThyFunc::BvOr => "bvor",
563            ThyFunc::BvXor => "bvxor",
564            ThyFunc::BvNot => "bvnot",
565            ThyFunc::BvAdd => "bvadd",
566            ThyFunc::BvNeg => "bvneg",
567            ThyFunc::BvSub => "bvsub",
568            ThyFunc::BvMul => "bvmul",
569            ThyFunc::BvShl => "bvshl",
570            ThyFunc::BvUgt => "bvugt",
571            ThyFunc::BvSgt => "bvsgt",
572            ThyFunc::BvUlt => "bvult",
573            ThyFunc::BvSlt => "bvslt",
574            ThyFunc::SetEmpty => {
575                panic!("unqualified empty set");
576            }
577            ThyFunc::SetSng => "singleton",
578            ThyFunc::SetCup => "union",
579            ThyFunc::SetCap => "intersection",
580            ThyFunc::SetDif => "setminus",
581            ThyFunc::SetMem => "member",
582            ThyFunc::SetSub => "subset",
583            ThyFunc::MapDefault => {
584                panic!("unqualified constant array");
585            }
586            ThyFunc::MapSelect => "select",
587            ThyFunc::MapStore => "store",
588        };
589        out.write_str(name)?;
590        Ok(())
591    }
592}
liquid_fixpoint/smt_fmt.rs

liquid_fixpoint/
smt_fmt.rs
