logicaffeine_verify/
smtlib.rs

1//! SMT-LIB2 Export
2//!
3//! Export VerifyExpr to standard SMT-LIB2 format readable by Z3, CVC5, Yices, etc.
4
5use crate::ir::{VerifyExpr, VerifyOp, VerifyType, BitVecOp};
6use std::collections::HashSet;
7
8/// Export a VerifyExpr to SMT-LIB2 format.
9pub fn to_smtlib2(expr: &VerifyExpr, declarations: &[(&str, VerifyType)]) -> String {
10    let mut output = String::new();
11    output.push_str("(set-logic ALL)\n");
12
13    // Declarations
14    for (name, ty) in declarations {
15        let sort = type_to_smtlib(ty);
16        output.push_str(&format!("(declare-fun {} () {})\n", name, sort));
17    }
18
19    // Auto-declare any variables not in declarations
20    let mut vars = HashSet::new();
21    crate::equivalence::collect_vars_pub(expr, &mut vars);
22    let declared: HashSet<String> = declarations.iter().map(|(n, _)| n.to_string()).collect();
23    for var in &vars {
24        if !declared.contains(var) {
25            output.push_str(&format!("(declare-fun {} () Int)\n", var));
26        }
27    }
28
29    output.push_str(&format!("(assert {})\n", expr_to_smtlib(expr)));
30    output.push_str("(check-sat)\n");
31    output.push_str("(get-model)\n");
32    output
33}
34
35/// Export an equivalence check to SMT-LIB2 format.
36pub fn equivalence_to_smtlib2(a: &VerifyExpr, b: &VerifyExpr) -> String {
37    let mut output = String::new();
38    output.push_str("(set-logic ALL)\n");
39
40    let mut vars = HashSet::new();
41    crate::equivalence::collect_vars_pub(a, &mut vars);
42    crate::equivalence::collect_vars_pub(b, &mut vars);
43    for var in &vars {
44        output.push_str(&format!("(declare-fun {} () Int)\n", var));
45    }
46
47    let a_smt = expr_to_smtlib(a);
48    let b_smt = expr_to_smtlib(b);
49    output.push_str(&format!("(assert (not (= {} {})))\n", a_smt, b_smt));
50    output.push_str("(check-sat)\n");
51    output
52}
53
54fn type_to_smtlib(ty: &VerifyType) -> String {
55    match ty {
56        VerifyType::Int => "Int".into(),
57        VerifyType::Bool => "Bool".into(),
58        VerifyType::Object => "Int".into(),
59        VerifyType::Real => "Real".into(),
60        VerifyType::BitVector(w) => format!("(_ BitVec {})", w),
61        VerifyType::Array(idx, elem) => {
62            format!("(Array {} {})", type_to_smtlib(idx), type_to_smtlib(elem))
63        }
64    }
65}
66
67fn expr_to_smtlib(expr: &VerifyExpr) -> String {
68    match expr {
69        VerifyExpr::Bool(true) => "true".into(),
70        VerifyExpr::Bool(false) => "false".into(),
71        VerifyExpr::Int(n) => {
72            if *n < 0 { format!("(- {})", -n) } else { n.to_string() }
73        }
74        VerifyExpr::Var(name) => name.clone(),
75        VerifyExpr::Binary { op, left, right } => {
76            let l = expr_to_smtlib(left);
77            let r = expr_to_smtlib(right);
78            let op_str = match op {
79                VerifyOp::Add => "+",
80                VerifyOp::Sub => "-",
81                VerifyOp::Mul => "*",
82                VerifyOp::Div => "div",
83                // Floor division: real division then floor (`to_int` is floor) — exact toward -inf.
84                VerifyOp::FloorDiv => return format!("(to_int (/ (to_real {}) (to_real {})))", l, r),
85                VerifyOp::Eq => "=",
86                VerifyOp::Neq => return format!("(not (= {} {}))", l, r),
87                VerifyOp::Gt => ">",
88                VerifyOp::Lt => "<",
89                VerifyOp::Gte => ">=",
90                VerifyOp::Lte => "<=",
91                VerifyOp::And => "and",
92                VerifyOp::Or => "or",
93                VerifyOp::Implies => "=>",
94            };
95            format!("({} {} {})", op_str, l, r)
96        }
97        VerifyExpr::Not(inner) => format!("(not {})", expr_to_smtlib(inner)),
98        VerifyExpr::Iff(l, r) => format!("(= {} {})", expr_to_smtlib(l), expr_to_smtlib(r)),
99        VerifyExpr::ForAll { vars, body } => {
100            let bindings: Vec<String> = vars.iter()
101                .map(|(n, t)| format!("({} {})", n, type_to_smtlib(t)))
102                .collect();
103            format!("(forall ({}) {})", bindings.join(" "), expr_to_smtlib(body))
104        }
105        VerifyExpr::Exists { vars, body } => {
106            let bindings: Vec<String> = vars.iter()
107                .map(|(n, t)| format!("({} {})", n, type_to_smtlib(t)))
108                .collect();
109            format!("(exists ({}) {})", bindings.join(" "), expr_to_smtlib(body))
110        }
111        VerifyExpr::Apply { name, args } | VerifyExpr::ApplyInt { name, args } => {
112            let arg_strs: Vec<String> = args.iter().map(expr_to_smtlib).collect();
113            if arg_strs.is_empty() {
114                name.clone()
115            } else {
116                format!("({} {})", name, arg_strs.join(" "))
117            }
118        }
119        VerifyExpr::BitVecConst { width, value } => {
120            format!("#x{:0>width$X}", value, width = ((*width + 3) / 4) as usize)
121        }
122        VerifyExpr::BitVecBinary { op, left, right } => {
123            let l = expr_to_smtlib(left);
124            let r = expr_to_smtlib(right);
125            let op_str = match op {
126                BitVecOp::And => "bvand",
127                BitVecOp::Or => "bvor",
128                BitVecOp::Xor => "bvxor",
129                BitVecOp::Not => return format!("(bvnot {})", l),
130                BitVecOp::Shl => "bvshl",
131                BitVecOp::Shr => "bvlshr",
132                BitVecOp::AShr => "bvashr",
133                BitVecOp::Add => "bvadd",
134                BitVecOp::Sub => "bvsub",
135                BitVecOp::Mul => "bvmul",
136                BitVecOp::SDiv => "bvsdiv",
137                BitVecOp::SRem => "bvsrem",
138                BitVecOp::ULt => "bvult",
139                BitVecOp::SLt => "bvslt",
140                BitVecOp::ULe => "bvule",
141                BitVecOp::SLe => "bvsle",
142                BitVecOp::Eq => return format!("(= {} {})", l, r),
143            };
144            format!("({} {} {})", op_str, l, r)
145        }
146        VerifyExpr::BitVecExtract { high, low, operand } => {
147            format!("((_ extract {} {}) {})", high, low, expr_to_smtlib(operand))
148        }
149        VerifyExpr::BitVecConcat(l, r) => {
150            format!("(concat {} {})", expr_to_smtlib(l), expr_to_smtlib(r))
151        }
152        VerifyExpr::Select { array, index } => {
153            format!("(select {} {})", expr_to_smtlib(array), expr_to_smtlib(index))
154        }
155        VerifyExpr::Store { array, index, value } => {
156            format!("(store {} {} {})", expr_to_smtlib(array), expr_to_smtlib(index), expr_to_smtlib(value))
157        }
158        VerifyExpr::AtState { expr, .. } => expr_to_smtlib(expr),
159        VerifyExpr::Transition { from, to } => {
160            format!("(and {} {})", expr_to_smtlib(from), expr_to_smtlib(to))
161        }
162    }
163}
logicaffeine_verify/smtlib.rs

logicaffeine_verify/
smtlib.rs
