liquid_fixpoint/
smt_horn.rs

1/// Formatter for the SMT-LIB HORN CHC format used by hornspec.
2///
3/// This format uses `set-logic HORN`, `declare-fun`, `assert (forall ...)`, and `check-sat`.
4/// Example:
5/// ```smt2
6/// (set-logic HORN)
7/// (declare-fun P0 (Int) Bool)
8/// (declare-fun P1 (Int Int) Bool)
9/// (assert (forall ((x Int)) (=> (P0 x) (P1 x x))))
10/// (assert (forall ((x Int)) (=> (and (P1 x x) (not (>= x 0))) false)))
11/// (check-sat)
12/// ```
13use std::fmt;
14
15use crate::{
16    BinOp, BinRel, ConstDecl, Constant, Constraint, DataCtor, DataDecl, Expr, FixpointFmt, FunDef,
17    Identifier, KVarDecl, Sort, SortCtor, Task, ThyFunc, Types, constraint::Pred,
18};
19
20/// A flattened Horn clause extracted from the constraint tree.
21struct HornClause<'a, T: Types> {
22    /// Universally quantified variables with their sorts
23    vars: Vec<(&'a T::Var, &'a Sort<T>)>,
24    /// Guard predicates (body of the implication)
25    guards: Vec<&'a Pred<T>>,
26    /// Head of the clause
27    head: &'a Pred<T>,
28}
29
30/// Collect all Horn clauses from a constraint tree
31fn flatten_constraint<'a, T: Types>(
32    constraint: &'a Constraint<T>,
33    vars: &mut Vec<(&'a T::Var, &'a Sort<T>)>,
34    guards: &mut Vec<&'a Pred<T>>,
35    clauses: &mut Vec<HornClause<'a, T>>,
36) {
37    match constraint {
38        Constraint::ForAll(bind, body) => {
39            vars.push((&bind.name, &bind.sort));
40            let guard_len = guards.len();
41            guards.extend(bind.preds.iter().filter(|a| a.is_trivially_true()));
42            flatten_constraint(body, vars, guards, clauses);
43            guards.truncate(guard_len);
44            vars.pop();
45        }
46        Constraint::Conj(cstrs) => {
47            for cstr in cstrs {
48                flatten_constraint(cstr, vars, guards, clauses);
49            }
50        }
51        Constraint::Pred(head, _tag) => {
52            if head.is_trivially_true() {
53                return;
54            }
55            clauses.push(HornClause { vars: vars.clone(), guards: guards.clone(), head });
56        }
57    }
58}
59
60// ---- SMT-LIB HORN CHC task formatting ----
61
62/// Format a task in the SMT-LIB HORN CHC format
63pub fn fmt_smt_horn<T: Types>(task: &Task<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
64    // Set logic
65    writeln!(f, "(set-logic HORN)")?;
66    writeln!(f)?;
67
68    // Comments
69    for line in &task.comments {
70        writeln!(f, ";; {line}")?;
71    }
72    if !task.comments.is_empty() {
73        writeln!(f)?;
74    }
75
76    // Data type declarations
77    for data_decl in &task.data_decls {
78        fmt_data_decl_smt(data_decl, f)?;
79    }
80
81    // Constant declarations
82    for cinfo in &task.constants {
83        fmt_const_decl(cinfo, f)?;
84    }
85
86    // Function definitions
87    for fun_decl in &task.define_funs {
88        fmt_fun_def(fun_decl, f)?;
89    }
90
91    // KVar declarations as uninterpreted Boolean functions
92    for kvar in &task.kvars {
93        fmt_kvar_as_fun(kvar, f)?;
94    }
95
96    writeln!(f)?;
97
98    // Flatten constraints into Horn clauses
99    let mut clauses = Vec::new();
100    let mut vars = Vec::new();
101    let mut guards = Vec::new();
102    flatten_constraint(&task.constraint, &mut vars, &mut guards, &mut clauses);
103
104    // Write assertions
105    for clause in &clauses {
106        fmt_assert(clause, f)?;
107    }
108
109    writeln!(f)?;
110    writeln!(f, "(check-sat)")
111}
112
113fn fmt_kvar_as_fun<T: Types>(kvar: &KVarDecl<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
114    write!(f, "(declare-fun {} (", kvar.kvid.display())?;
115    for (i, sort) in kvar.sorts.iter().enumerate() {
116        if i > 0 {
117            write!(f, " ")?;
118        }
119        fmt_sort_smt(sort, f)?;
120    }
121    writeln!(f, ") Bool)")
122}
123
124fn fmt_assert<T: Types>(clause: &HornClause<'_, T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
125    write!(f, "(assert ")?;
126
127    // Wrap in forall if there are variables
128    if !clause.vars.is_empty() {
129        write!(f, "(forall (")?;
130        for (var, sort) in &clause.vars {
131            write!(f, "({} ", var.display())?;
132            fmt_sort_smt(sort, f)?;
133            write!(f, ")")?;
134        }
135        write!(f, ") ")?;
136    }
137
138    match &clause.head {
139        Pred::KVar(k, args) => {
140            // (=> guards (k args))
141            write!(f, "(=> ")?;
142            fmt_guard_conjunction(&clause.guards, f)?;
143            write!(f, " ({}", k.display())?;
144            for arg in args {
145                write!(f, " ")?;
146                fmt_expr_smt(arg, f)?;
147            }
148            write!(f, "))")?;
149        }
150        Pred::Expr(e) => {
151            // (=> (and guards (not e)) false)
152            write!(f, "(=> ")?;
153            let guard_count = clause.guards.len() + 1;
154            if guard_count == 1 && clause.guards.is_empty() {
155                write!(f, "(not ")?;
156                fmt_expr_smt(e, f)?;
157                write!(f, ")")?;
158            } else {
159                write!(f, "(and")?;
160                for guard in &clause.guards {
161                    write!(f, " ")?;
162                    fmt_guard(guard, f)?;
163                }
164                write!(f, " (not ")?;
165                fmt_expr_smt(e, f)?;
166                write!(f, "))")?;
167            }
168            write!(f, " false)")?;
169        }
170    }
171
172    // Close forall
173    if !clause.vars.is_empty() {
174        write!(f, ")")?;
175    }
176
177    writeln!(f, ")")
178}
179
180fn fmt_guard_conjunction<T: Types>(guards: &[&Pred<T>], f: &mut fmt::Formatter<'_>) -> fmt::Result {
181    if guards.is_empty() {
182        write!(f, "true")
183    } else if guards.len() == 1 {
184        fmt_guard(guards[0], f)
185    } else {
186        write!(f, "(and")?;
187        for guard in guards {
188            write!(f, " ")?;
189            fmt_guard(guard, f)?;
190        }
191        write!(f, ")")
192    }
193}
194
195fn fmt_guard<T: Types>(guard: &Pred<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
196    match guard {
197        Pred::KVar(k, args) => {
198            write!(f, "({}", k.display())?;
199            for arg in args {
200                write!(f, " ")?;
201                fmt_expr_smt(arg, f)?;
202            }
203            write!(f, ")")
204        }
205        Pred::Expr(e) => fmt_expr_smt(e, f),
206    }
207}
208
209pub struct SmtFormatter<'a, T: Types>(pub &'a Task<T>);
210
211impl<T: Types> fmt::Display for SmtFormatter<'_, T> {
212    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
213        fmt_smt_horn(self.0, f)
214    }
215}
216
217// ---- SMT-LIB sort formatting ----
218
219fn fmt_sort_smt<T: Types>(sort: &Sort<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
220    match sort {
221        Sort::Int => write!(f, "Int"),
222        Sort::Bool => write!(f, "Bool"),
223        Sort::Real => write!(f, "Real"),
224        Sort::Str => write!(f, "String"),
225        Sort::BitVec(size) => {
226            write!(f, "(_ BitVec ")?;
227            fmt_sort_smt(size, f)?;
228            write!(f, ")")
229        }
230        Sort::BvSize(size) => write!(f, "{size}"),
231        Sort::Var(i) => write!(f, "T{i}"),
232        Sort::Func(fsort) => {
233            // Function sorts mapped to (Array input output) as an approximation
234            let [input, output] = &**fsort;
235            write!(f, "(Array ")?;
236            fmt_sort_smt(input, f)?;
237            write!(f, " ")?;
238            fmt_sort_smt(output, f)?;
239            write!(f, ")")
240        }
241        Sort::Abs(_, sort) => fmt_sort_smt(sort, f),
242        Sort::App(ctor, args) => {
243            if args.is_empty() {
244                fmt_sort_ctor_smt(ctor, f)
245            } else {
246                write!(f, "(")?;
247                fmt_sort_ctor_smt(ctor, f)?;
248                for arg in args {
249                    write!(f, " ")?;
250                    fmt_sort_smt(arg, f)?;
251                }
252                write!(f, ")")
253            }
254        }
255    }
256}
257
258fn fmt_sort_ctor_smt<T: Types>(ctor: &SortCtor<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
259    match ctor {
260        SortCtor::Set => write!(f, "Set"),
261        SortCtor::Map => write!(f, "Map"),
262        SortCtor::Data(name) => write!(f, "{}", name.display()),
263    }
264}
265
266// ---- SMT-LIB expression formatting ----
267
268fn fmt_expr_smt<T: Types>(expr: &Expr<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
269    match expr {
270        Expr::Constant(c) => fmt_constant_smt(c, f),
271        Expr::Var(x) => write!(f, "{}", x.display()),
272        Expr::App(func, _sort_args, args, _out_sort) => {
273            write!(f, "(")?;
274            fmt_expr_smt(func, f)?;
275            for arg in args {
276                write!(f, " ")?;
277                fmt_expr_smt(arg, f)?;
278            }
279            write!(f, ")")
280        }
281        Expr::Neg(e) => {
282            write!(f, "(- ")?;
283            fmt_expr_smt(e, f)?;
284            write!(f, ")")
285        }
286        Expr::BinaryOp(op, exprs) => {
287            let [e1, e2] = &**exprs;
288            write!(f, "({} ", fmt_binop_smt(*op))?;
289            fmt_expr_smt(e1, f)?;
290            write!(f, " ")?;
291            fmt_expr_smt(e2, f)?;
292            write!(f, ")")
293        }
294        Expr::IfThenElse(exprs) => {
295            let [p, e1, e2] = &**exprs;
296            write!(f, "(ite ")?;
297            fmt_expr_smt(p, f)?;
298            write!(f, " ")?;
299            fmt_expr_smt(e1, f)?;
300            write!(f, " ")?;
301            fmt_expr_smt(e2, f)?;
302            write!(f, ")")
303        }
304        Expr::And(exprs) => {
305            if exprs.is_empty() {
306                write!(f, "true")
307            } else {
308                write!(f, "(and")?;
309                for e in exprs {
310                    write!(f, " ")?;
311                    fmt_expr_smt(e, f)?;
312                }
313                write!(f, ")")
314            }
315        }
316        Expr::Or(exprs) => {
317            if exprs.is_empty() {
318                write!(f, "false")
319            } else {
320                write!(f, "(or")?;
321                for e in exprs {
322                    write!(f, " ")?;
323                    fmt_expr_smt(e, f)?;
324                }
325                write!(f, ")")
326            }
327        }
328        Expr::Not(e) => {
329            write!(f, "(not ")?;
330            fmt_expr_smt(e, f)?;
331            write!(f, ")")
332        }
333        Expr::Imp(exprs) => {
334            let [e1, e2] = &**exprs;
335            write!(f, "(=> ")?;
336            fmt_expr_smt(e1, f)?;
337            write!(f, " ")?;
338            fmt_expr_smt(e2, f)?;
339            write!(f, ")")
340        }
341        Expr::Iff(exprs) => {
342            let [e1, e2] = &**exprs;
343            write!(f, "(= ")?;
344            fmt_expr_smt(e1, f)?;
345            write!(f, " ")?;
346            fmt_expr_smt(e2, f)?;
347            write!(f, ")")
348        }
349        Expr::Atom(rel, exprs) => {
350            let [e1, e2] = &**exprs;
351            fmt_binrel_smt(*rel, e1, e2, f)
352        }
353        Expr::Let(name, exprs) => {
354            let [e1, e2] = &**exprs;
355            write!(f, "(let (({} ", name.display())?;
356            fmt_expr_smt(e1, f)?;
357            write!(f, ")) ")?;
358            fmt_expr_smt(e2, f)?;
359            write!(f, ")")
360        }
361        Expr::ThyFunc(thy_func) => fmt_thy_func_smt(thy_func, f),
362        Expr::IsCtor(ctor, e) => {
363            write!(f, "((_ is {}) ", ctor.display())?;
364            fmt_expr_smt(e, f)?;
365            write!(f, ")")
366        }
367        Expr::Quantifier(..) => {
368            panic!("Quantifiers are not supported in SMT/Horn format");
369        }
370        // Weak kvars are internal placeholders and are not part of the Horn encoding.
371        Expr::WKVar(..) => {
372            // These could either be encoded as true (to ignore solving them)
373            // or in the same way kvars are (to solve for them)
374            panic!("Weak KVars not supported in SMT/Horn format")
375        }
376    }
377}
378
379fn fmt_constant_smt<T: Types>(c: &Constant<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
380    match c {
381        Constant::Numeral(n) => write!(f, "{n}"),
382        Constant::Real(n) => write!(f, "{}", n.display()),
383        Constant::Boolean(b) => write!(f, "{b}"),
384        Constant::String(s) => write!(f, "\"{}\"", s.display()),
385        Constant::BitVec(val, size) => write!(f, "(_ bv{val} {size})"),
386    }
387}
388
389fn fmt_binop_smt(op: BinOp) -> &'static str {
390    match op {
391        BinOp::Add => "+",
392        BinOp::Sub => "-",
393        BinOp::Mul => "*",
394        BinOp::Div => "div",
395        BinOp::Mod => "mod",
396    }
397}
398
399fn fmt_binrel_smt<T: Types>(
400    rel: BinRel,
401    e1: &Expr<T>,
402    e2: &Expr<T>,
403    f: &mut fmt::Formatter<'_>,
404) -> fmt::Result {
405    match rel {
406        BinRel::Ne => {
407            write!(f, "(not (= ")?;
408            fmt_expr_smt(e1, f)?;
409            write!(f, " ")?;
410            fmt_expr_smt(e2, f)?;
411            write!(f, "))")
412        }
413        _ => {
414            let op = match rel {
415                BinRel::Eq => "=",
416                BinRel::Gt => ">",
417                BinRel::Ge => ">=",
418                BinRel::Lt => "<",
419                BinRel::Le => "<=",
420                BinRel::Ne => unreachable!(),
421            };
422            write!(f, "({op} ")?;
423            fmt_expr_smt(e1, f)?;
424            write!(f, " ")?;
425            fmt_expr_smt(e2, f)?;
426            write!(f, ")")
427        }
428    }
429}
430
431fn fmt_thy_func_smt(thy_func: &ThyFunc, f: &mut fmt::Formatter<'_>) -> fmt::Result {
432    match thy_func {
433        ThyFunc::StrLen => write!(f, "str.len"),
434        ThyFunc::StrConcat => write!(f, "str.++"),
435        ThyFunc::StrPrefixOf => write!(f, "str.prefixof"),
436        ThyFunc::StrSuffixOf => write!(f, "str.suffixof"),
437        ThyFunc::StrContains => write!(f, "str.contains"),
438        ThyFunc::BvZeroExtend(size) => write!(f, "(_ zero_extend {size})"),
439        ThyFunc::BvSignExtend(size) => write!(f, "(_ sign_extend {size})"),
440        ThyFunc::IntToBv8 => write!(f, "(_ int2bv 8)"),
441        ThyFunc::Bv8ToInt => write!(f, "bv2int"),
442        ThyFunc::IntToBv32 => write!(f, "(_ int2bv 32)"),
443        ThyFunc::Bv32ToInt => write!(f, "bv2int"),
444        ThyFunc::IntToBv64 => write!(f, "(_ int2bv 64)"),
445        ThyFunc::Bv64ToInt => write!(f, "bv2int"),
446        ThyFunc::BvUle => write!(f, "bvule"),
447        ThyFunc::BvSle => write!(f, "bvsle"),
448        ThyFunc::BvUge => write!(f, "bvuge"),
449        ThyFunc::BvSge => write!(f, "bvsge"),
450        ThyFunc::BvUdiv => write!(f, "bvudiv"),
451        ThyFunc::BvSdiv => write!(f, "bvsdiv"),
452        ThyFunc::BvSrem => write!(f, "bvsrem"),
453        ThyFunc::BvUrem => write!(f, "bvurem"),
454        ThyFunc::BvLshr => write!(f, "bvlshr"),
455        ThyFunc::BvAshr => write!(f, "bvashr"),
456        ThyFunc::BvAnd => write!(f, "bvand"),
457        ThyFunc::BvOr => write!(f, "bvor"),
458        ThyFunc::BvXor => write!(f, "bvxor"),
459        ThyFunc::BvNot => write!(f, "bvnot"),
460        ThyFunc::BvAdd => write!(f, "bvadd"),
461        ThyFunc::BvNeg => write!(f, "bvneg"),
462        ThyFunc::BvSub => write!(f, "bvsub"),
463        ThyFunc::BvMul => write!(f, "bvmul"),
464        ThyFunc::BvShl => write!(f, "bvshl"),
465        ThyFunc::BvUgt => write!(f, "bvugt"),
466        ThyFunc::BvSgt => write!(f, "bvsgt"),
467        ThyFunc::BvUlt => write!(f, "bvult"),
468        ThyFunc::BvSlt => write!(f, "bvslt"),
469        ThyFunc::SetEmpty => write!(f, "as emptyset"),
470        ThyFunc::SetSng => write!(f, "singleton"),
471        ThyFunc::SetCup => write!(f, "union"),
472        ThyFunc::SetCap => write!(f, "intersection"),
473        ThyFunc::SetDif => write!(f, "setminus"),
474        ThyFunc::SetMem => write!(f, "member"),
475        ThyFunc::SetSub => write!(f, "subset"),
476        ThyFunc::MapDefault => write!(f, "const"),
477        ThyFunc::MapSelect => write!(f, "select"),
478        ThyFunc::MapStore => write!(f, "store"),
479    }
480}
481
482// ---- Data type / constant / function declaration formatting ----
483
484fn fmt_data_decl_smt<T: Types>(decl: &DataDecl<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
485    if decl.ctors.is_empty() {
486        write!(f, "(declare-sort {} {})", decl.name.display(), decl.vars)?;
487        writeln!(f)
488    } else {
489        write!(f, "(declare-datatypes (")?;
490        write!(f, "({} {})", decl.name.display(), decl.vars)?;
491        write!(f, ") ((")?;
492        for (i, ctor) in decl.ctors.iter().enumerate() {
493            if i > 0 {
494                write!(f, " ")?;
495            }
496            fmt_data_ctor_smt(ctor, f)?;
497        }
498        writeln!(f, ")))")
499    }
500}
501
502fn fmt_data_ctor_smt<T: Types>(ctor: &DataCtor<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
503    write!(f, "({}", ctor.name.display())?;
504    for field in &ctor.fields {
505        write!(f, " ({} ", field.name.display())?;
506        fmt_sort_smt(&field.sort, f)?;
507        write!(f, ")")?;
508    }
509    write!(f, ")")
510}
511
512fn fmt_const_decl<T: Types>(decl: &ConstDecl<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
513    write!(f, "(declare-const {} ", decl.name.display())?;
514    fmt_sort_smt(&decl.sort, f)?;
515    writeln!(f, ")")
516}
517
518fn fmt_fun_def<T: Types>(fun: &FunDef<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
519    if let Some(body) = &fun.body {
520        write!(f, "(define-fun {} (", fun.name.display())?;
521        for (i, (name, sort)) in body.args.iter().zip(&fun.sort.inputs).enumerate() {
522            if i > 0 {
523                write!(f, " ")?;
524            }
525            write!(f, "({} ", name.display())?;
526            fmt_sort_smt(sort, f)?;
527            write!(f, ")")?;
528        }
529        write!(f, ") ")?;
530        fmt_sort_smt(&fun.sort.output, f)?;
531        write!(f, " ")?;
532        fmt_expr_smt(&body.expr, f)?;
533        writeln!(f, ")")
534    } else {
535        write!(f, "(declare-fun {} (", fun.name.display())?;
536        for (i, sort) in fun.sort.inputs.iter().enumerate() {
537            if i > 0 {
538                write!(f, " ")?;
539            }
540            fmt_sort_smt(sort, f)?;
541        }
542        write!(f, ") ")?;
543        fmt_sort_smt(&fun.sort.output, f)?;
544        writeln!(f, ")")
545    }
546}
liquid_fixpoint/smt_horn.rs

liquid_fixpoint/
smt_horn.rs
