1use crate::{constraint::Constraint, parser::ParsingTypes};
2
3#[cfg(feature = "rust-fixpoint")]
4mod rust_fixpoint {
5 use core::panic;
6 use std::collections::HashMap;
7
8 use z3::{
9 Config, Context, SatResult, Solver, SortKind,
10 ast::{self, Ast},
11 };
12
13 use crate::{
14 constraint::{BinOp, BinRel, Bind, Constant, Constraint, Expr, Pred, Sort},
15 parser::ParsingTypes,
16 };
17 struct Env<'ctx> {
18 bindings: HashMap<String, Vec<ast::Dynamic<'ctx>>>,
19 }
20
21 impl<'ctx> Env<'ctx> {
22 fn new() -> Self {
23 Self { bindings: HashMap::new() }
24 }
25
26 fn insert(&mut self, name: String, value: ast::Dynamic<'ctx>) {
27 self.bindings.entry(name).or_default().push(value);
28 }
29
30 fn pop(&mut self, name: &str) {
31 if let Some(stack) = self.bindings.get_mut(name) {
32 stack.pop();
33 if stack.is_empty() {
34 self.bindings.remove(name);
35 }
36 }
37 }
38
39 fn lookup(&self, name: &str) -> Option<ast::Dynamic<'ctx>> {
40 self.bindings
41 .get(name)
42 .and_then(|stack| stack.last().cloned())
43 }
44 }
45
46 fn const_to_z3<'ctx>(ctx: &'ctx Context, cnst: &Constant<ParsingTypes>) -> ast::Dynamic<'ctx> {
47 match cnst {
48 Constant::Numeral(num) => ast::Int::from_i64(ctx, (*num).try_into().unwrap()).into(),
49 Constant::Boolean(b) => ast::Bool::from_bool(ctx, *b).into(),
50 Constant::String(strconst) => ast::String::from_str(ctx, strconst).unwrap().into(),
51 _ => panic!("handling for this kind of const isn't implemented yet"),
52 }
53 }
54
55 fn atom_to_z3<'ctx>(
56 ctx: &'ctx Context,
57 bin_rel: &BinRel,
58 operands: &Box<[Expr<ParsingTypes>; 2]>,
59 env: &mut Env<'ctx>,
60 ) -> ast::Dynamic<'ctx> {
61 let loperand = expr_to_z3(ctx, &operands[0], env);
62 let roperand = expr_to_z3(ctx, &operands[1], env);
63 if loperand.sort_kind() != roperand.sort_kind() {
64 panic!("Operands must have the same sort");
65 }
66 if !matches!(bin_rel, BinRel::Eq | BinRel::Ne)
67 && !matches!(loperand.sort_kind(), SortKind::Int | SortKind::Real)
68 {
69 panic!("Comparison operators require numeric operands");
70 }
71 match (bin_rel, loperand.sort_kind(), roperand.sort_kind()) {
72 (BinRel::Ne, _, _) => loperand._eq(&roperand).not().into(),
73 (BinRel::Eq, _, _) => loperand._eq(&roperand).into(),
74 (BinRel::Gt, SortKind::Int, SortKind::Int) => {
75 let iloperand = loperand.as_int().expect("already checked");
76 let iroperand = roperand.as_int().expect("already checked");
77 iloperand.gt(&iroperand).into()
78 }
79 (BinRel::Gt, SortKind::Real, SortKind::Real) => {
80 let rloperand = loperand.as_real().expect("already checked");
81 let rroperand = roperand.as_real().expect("already checked");
82 rloperand.gt(&rroperand).into()
83 }
84 (BinRel::Ge, SortKind::Int, SortKind::Int) => {
85 let iloperand = loperand.as_int().expect("already checked");
86 let iroperand = roperand.as_int().expect("already checked");
87 iloperand.ge(&iroperand).into()
88 }
89 (BinRel::Ge, SortKind::Real, SortKind::Real) => {
90 let rloperand = loperand.as_real().expect("already checked");
91 let rroperand = roperand.as_real().expect("already checked");
92 rloperand.ge(&rroperand).into()
93 }
94 (BinRel::Lt, SortKind::Int, SortKind::Int) => {
95 let iloperand = loperand.as_int().expect("already checked");
96 let iroperand = roperand.as_int().expect("already checked");
97 iloperand.lt(&iroperand).into()
98 }
99 (BinRel::Lt, SortKind::Real, SortKind::Real) => {
100 let rloperand = loperand.as_real().expect("already checked");
101 let rroperand = roperand.as_real().expect("already checked");
102 rloperand.lt(&rroperand).into()
103 }
104 (BinRel::Le, SortKind::Int, SortKind::Int) => {
105 let iloperand = loperand.as_int().expect("already checked");
106 let iroperand = roperand.as_int().expect("already checked");
107 iloperand.le(&iroperand).into()
108 }
109 (BinRel::Le, SortKind::Real, SortKind::Real) => {
110 let rloperand = loperand.as_real().expect("already checked");
111 let rroperand = roperand.as_real().expect("already checked");
112 rloperand.le(&rroperand).into()
113 }
114 _ => panic!("Unsupported relation or operand types"),
115 }
116 }
117
118 fn binop_to_z3<'ctx>(
119 ctx: &'ctx Context,
120 bin_op: &BinOp,
121 operands: &Box<[Expr<ParsingTypes>; 2]>,
122 env: &mut Env<'ctx>,
123 ) -> ast::Dynamic<'ctx> {
124 let lhs = expr_to_z3(ctx, &operands[0], env);
125 let rhs = expr_to_z3(ctx, &operands[1], env);
126
127 if lhs.sort_kind() != rhs.sort_kind() {
128 panic!("binary operands must have the same sort");
129 }
130
131 match lhs.sort_kind() {
132 SortKind::Int => {
136 let l: ast::Int<'ctx> = lhs.as_int().unwrap();
137 let r: ast::Int<'ctx> = rhs.as_int().unwrap();
138
139 let res = match bin_op {
140 BinOp::Add => ast::Int::add(ctx, &[&l, &r]),
141 BinOp::Sub => ast::Int::sub(ctx, &[&l, &r]),
142 BinOp::Mul => ast::Int::mul(ctx, &[&l, &r]),
143 BinOp::Div => l.div(&r),
144 BinOp::Mod => l.modulo(&r),
145 };
146 res.into()
147 }
148 SortKind::Real => {
149 let l: ast::Real<'ctx> = lhs.as_real().unwrap();
150 let r: ast::Real<'ctx> = rhs.as_real().unwrap();
151
152 let res = match bin_op {
153 BinOp::Add => ast::Real::add(ctx, &[&l, &r]),
154 BinOp::Sub => ast::Real::sub(ctx, &[&l, &r]),
155 BinOp::Mul => ast::Real::mul(ctx, &[&l, &r]),
156 BinOp::Div => l.div(&r),
157 BinOp::Mod => panic!("modulo is not defined on Real numbers"),
158 };
159 res.into()
160 }
161
162 _ => panic!("arithmetic operators only support Int and Real"),
163 }
164 }
165
166 fn expr_to_z3<'ctx>(
167 ctx: &'ctx Context,
168 expr: &Expr<ParsingTypes>,
169 env: &mut Env<'ctx>,
170 ) -> ast::Dynamic<'ctx> {
171 match expr {
172 Expr::Var(var) => env.lookup(var).expect("error if not present"),
173 Expr::Constant(cnst) => const_to_z3(ctx, cnst),
174 Expr::Atom(bin_rel, operands) => atom_to_z3(ctx, bin_rel, operands, env),
175 Expr::BinaryOp(bin_op, operands) => binop_to_z3(ctx, bin_op, operands, env),
176 Expr::And(conjuncts) => {
177 let booleans = conjuncts
178 .iter()
179 .map(|conjunct| expr_to_z3(ctx, conjunct, env).as_bool())
180 .collect::<Option<Vec<_>>>()
181 .unwrap();
182 let boolean_refs: Vec<&ast::Bool> = booleans.iter().collect();
183 let bool_ref_slice: &[&ast::Bool] = boolean_refs.as_slice();
184 ast::Bool::and(ctx, bool_ref_slice).into()
185 }
186 Expr::Or(options) => {
187 let booleans = options
188 .iter()
189 .map(|option| expr_to_z3(ctx, option, env).as_bool())
190 .collect::<Option<Vec<_>>>()
191 .unwrap();
192 let boolean_refs: Vec<&ast::Bool> = booleans.iter().collect();
193 let bool_ref_slice: &[&ast::Bool] = boolean_refs.as_slice();
194 ast::Bool::or(ctx, bool_ref_slice).into()
195 }
196 Expr::Not(inner) => {
197 expr_to_z3(ctx, &*inner, env)
198 .as_bool()
199 .unwrap()
200 .not()
201 .into()
202 }
203 Expr::Neg(number) => {
204 let zero = ast::Int::from_i64(ctx, 0);
205 let z3_num = expr_to_z3(ctx, &number, env);
206 match z3_num.sort_kind() {
207 SortKind::Int => ast::Int::sub(ctx, &[&zero, &z3_num.as_int().unwrap()]).into(),
208 SortKind::Real => {
209 ast::Real::sub(ctx, &[&zero.to_real(), &z3_num.as_real().unwrap()]).into()
210 }
211 _ => panic!("Negation requires numeric operand"),
212 }
213 }
214 Expr::Iff(operands) => {
215 let lhs = expr_to_z3(ctx, &operands[0], env);
216 let rhs = expr_to_z3(ctx, &operands[1], env);
217 lhs.as_bool().unwrap().iff(&rhs.as_bool().unwrap()).into()
218 }
219 Expr::Imp(operands) => {
220 let lhs = expr_to_z3(ctx, &operands[0], env);
221 let rhs = expr_to_z3(ctx, &operands[1], env);
222 lhs.as_bool()
223 .unwrap()
224 .implies(&rhs.as_bool().unwrap())
225 .into()
226 }
227 Expr::Let(variable, exprs) => {
228 let binding = expr_to_z3(ctx, &exprs[0], env);
229 env.insert(variable.clone(), binding);
230 let res = expr_to_z3(ctx, &exprs[1], env);
231 env.pop(variable.as_str());
232 res
233 }
234 _ => {
235 panic!("handling for this kind of expression is not implemented yet")
236 }
237 }
238 }
239
240 fn pred_to_z3<'ctx>(
241 ctx: &'ctx Context,
242 pred: &Pred<ParsingTypes>,
243 env: &mut Env<'ctx>,
244 ) -> ast::Bool<'ctx> {
245 match pred {
246 Pred::Expr(expr) => expr_to_z3(ctx, expr, env).as_bool().expect(" asldfj "),
247 Pred::And(conjuncts) => {
248 let bools: Vec<_> = conjuncts
249 .iter()
250 .map(|conjunct| pred_to_z3(ctx, conjunct, env))
251 .collect::<Vec<_>>();
252 let bool_refs: Vec<&ast::Bool> = bools.iter().collect();
253 ast::Bool::and(ctx, bool_refs.as_slice()).into()
254 }
255 Pred::KVar(_kvar, _vars) => panic!("Kvars not supported yet"),
256 }
257 }
258
259 fn new_const<'ctx>(ctx: &'ctx Context, bind: &Bind<ParsingTypes>) -> ast::Dynamic<'ctx> {
260 match &bind.sort {
261 Sort::Int => ast::Int::new_const(ctx, bind.name.as_str()).into(),
262 Sort::Real => ast::Real::new_const(ctx, bind.name.as_str()).into(),
263 Sort::Bool => ast::Bool::new_const(ctx, bind.name.as_str()).into(),
264 Sort::Str => ast::String::new_const(ctx, bind.name.as_str()).into(),
265 _ => panic!("unhandled kind encountered"),
266 }
267 }
268
269 fn is_constraint_satisfiable_inner<'ctx>(
270 ctx: &'ctx Context,
271 cstr: &Constraint<ParsingTypes>,
272 solver: &Solver,
273 env: &mut Env<'ctx>,
274 ) -> bool {
275 solver.push();
276 let res = match cstr {
277 Constraint::Pred(pred, _tag) => {
278 solver.assert(&pred_to_z3(ctx, pred, env).not());
279 matches!(solver.check(), SatResult::Unsat)
280 }
281 Constraint::Conj(conjuncts) => {
282 conjuncts
283 .iter()
284 .all(|conjunct| is_constraint_satisfiable_inner(ctx, conjunct, solver, env))
285 }
286
287 Constraint::ForAll(bind, inner) => {
288 env.insert(bind.name.clone(), new_const(ctx, bind));
289 solver.assert(&pred_to_z3(ctx, &bind.pred, env));
290 let inner_soln = is_constraint_satisfiable_inner(ctx, &**inner, solver, env);
291 env.pop(bind.name.as_str());
292 inner_soln
293 }
294 };
295 solver.pop(1);
296 res
297 }
298
299 pub fn is_constraint_satisfiable(cstr: &Constraint<ParsingTypes>) -> bool {
300 let cfg = Config::new();
301 let ctx = Context::new(&cfg);
302 let solver = Solver::new(&ctx);
303 let mut vars = Env::new();
304 is_constraint_satisfiable_inner(&ctx, &cstr, &solver, &mut vars)
305 }
306}
307
308#[cfg(feature = "rust-fixpoint")]
309pub fn is_constraint_satisfiable(cstr: &Constraint<ParsingTypes>) -> bool {
310 rust_fixpoint::is_constraint_satisfiable(cstr)
311}
312
313#[cfg(not(feature = "rust-fixpoint"))]
314pub fn is_constraint_satisfiable(_cstr: &Constraint<ParsingTypes>) -> bool {
315 true
316}