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::{self, Write};
14
15use crate::{
16    Constraint, Identifier, KVarDecl, Pred, Sort, Task, Types,
17    smt_fmt::{SmtEncoder, SmtOptions},
18};
19
20/// A flattened Horn clause extracted from the constraint tree.
21struct HornClause<'a, T: Types> {
22    vars: Vec<(&'a T::Var, &'a Sort<T>)>,
23    guards: Vec<&'a Pred<T>>,
24    head: &'a Pred<T>,
25}
26
27fn flatten_constraint<'a, T: Types>(
28    constraint: &'a Constraint<T>,
29    vars: &mut Vec<(&'a T::Var, &'a Sort<T>)>,
30    guards: &mut Vec<&'a Pred<T>>,
31    clauses: &mut Vec<HornClause<'a, T>>,
32) {
33    match constraint {
34        Constraint::ForAll(bind, body) => {
35            vars.push((&bind.name, &bind.sort));
36            let guard_len = guards.len();
37            guards.extend(bind.preds.iter().filter(|a| !a.is_trivially_true()));
38            flatten_constraint(body, vars, guards, clauses);
39            guards.truncate(guard_len);
40            vars.pop();
41        }
42        Constraint::Conj(cstrs) => {
43            for cstr in cstrs {
44                flatten_constraint(cstr, vars, guards, clauses);
45            }
46        }
47        Constraint::Pred(head, _tag) => {
48            if !head.is_trivially_true() {
49                clauses.push(HornClause { vars: vars.clone(), guards: guards.clone(), head });
50            }
51        }
52    }
53}
54
55/// Format a task in the SMT-LIB HORN CHC format.
56pub fn fmt_smt_horn<T: Types>(task: &Task<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
57    write_smt_horn(task, f)
58}
59
60fn write_smt_horn<T: Types>(task: &Task<T>, out: &mut impl Write) -> fmt::Result {
61    let encoder = SmtEncoder::new(&task.data_decls, SmtOptions::HORN);
62    writeln!(out, "(set-logic HORN)\n")?;
63    for line in &task.comments {
64        writeln!(out, ";; {line}")?;
65    }
66    if !task.comments.is_empty() {
67        writeln!(out)?;
68    }
69    for decl in &task.data_decls {
70        encoder.write_datatype_decl(out, decl)?;
71    }
72    for decl in &task.constants {
73        encoder.write_const_decl(out, &decl.name.display().to_string(), &decl.sort)?;
74    }
75    for fun in &task.define_funs {
76        encoder.write_fun_def(out, fun)?;
77    }
78    for kvar in &task.kvars {
79        write_kvar_decl(&encoder, kvar, out)?;
80    }
81    writeln!(out)?;
82
83    let mut clauses = Vec::new();
84    flatten_constraint(&task.constraint, &mut Vec::new(), &mut Vec::new(), &mut clauses);
85    for clause in &clauses {
86        write_assert(&encoder, clause, out)?;
87    }
88    writeln!(out, "\n(check-sat)")?;
89    Ok(())
90}
91
92fn write_kvar_decl<T: Types>(
93    encoder: &SmtEncoder<T>,
94    kvar: &KVarDecl<T>,
95    out: &mut impl Write,
96) -> fmt::Result {
97    write!(out, "(declare-fun {} (", kvar.kvid.display())?;
98    for (i, sort) in kvar.sorts.iter().enumerate() {
99        if i != 0 {
100            out.write_char(' ')?;
101        }
102        encoder.write_sort(out, sort)?;
103    }
104    writeln!(out, ") Bool)")?;
105    Ok(())
106}
107
108fn write_assert<T: Types>(
109    encoder: &SmtEncoder<T>,
110    clause: &HornClause<'_, T>,
111    out: &mut impl Write,
112) -> fmt::Result {
113    write!(out, "(assert ")?;
114    if !clause.vars.is_empty() {
115        write!(out, "(forall (")?;
116        for (var, sort) in &clause.vars {
117            write!(out, "({} ", var.display())?;
118            encoder.write_sort(out, sort)?;
119            write!(out, ")")?;
120        }
121        write!(out, ") ")?;
122    }
123    write!(out, "(=> ")?;
124    match clause.head {
125        Pred::KVar(..) => {
126            write_guard_conjunction(encoder, &clause.guards, out)?;
127            out.write_char(' ')?;
128            encoder.write_pred(out, clause.head)?;
129            out.write_char(')')?;
130        }
131        Pred::Expr(expr) => {
132            if !clause.guards.is_empty() {
133                write!(out, "(and")?;
134                for guard in &clause.guards {
135                    out.write_char(' ')?;
136                    encoder.write_pred(out, guard)?;
137                }
138                out.write_char(' ')?;
139            }
140            write!(out, "(not ")?;
141            encoder.write_expr(out, expr)?;
142            out.write_char(')')?;
143            if !clause.guards.is_empty() {
144                out.write_char(')')?;
145            }
146            write!(out, " false)")?;
147        }
148    }
149    if !clause.vars.is_empty() {
150        out.write_char(')')?;
151    }
152    writeln!(out, ")")?;
153    Ok(())
154}
155
156fn write_guard_conjunction<T: Types>(
157    encoder: &SmtEncoder<T>,
158    guards: &[&Pred<T>],
159    out: &mut impl Write,
160) -> fmt::Result {
161    match guards {
162        [] => out.write_str("true")?,
163        [guard] => encoder.write_pred(out, guard)?,
164        _ => {
165            write!(out, "(and")?;
166            for guard in guards {
167                out.write_char(' ')?;
168                encoder.write_pred(out, guard)?;
169            }
170            out.write_char(')')?;
171        }
172    }
173    Ok(())
174}
175
176pub struct SmtFormatter<'a, T: Types>(pub &'a Task<T>);
177
178impl<T: Types> fmt::Display for SmtFormatter<'_, T> {
179    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
180        fmt_smt_horn(self.0, f)
181    }
182}
liquid_fixpoint/smt_horn.rs

liquid_fixpoint/
smt_horn.rs
