mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

add code for free bounds axiom, but keep it disabled

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-03-16 20:07:14 -07:00
parent 99ec42c0d7
commit 2ecf6dc53c
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_lra.cpp
View file

@ -1172,11 +1172,14 @@ public:
void mk_ite_axiom(expr* n) {
return;
expr* c = nullptr, *t = nullptr, *e = nullptr;
rational b1, b2;
VERIFY(m.is_ite(n, c, t, e));
literal e1 = th.mk_eq(n, t, false);
literal e2 = th.mk_eq(n, e, false);
scoped_trace_stream sts(th, e1, e2);
mk_axiom(e1, e2);
if (!a.is_numeral(t, b1) || !a.is_numeral(e, b2))
return;
auto v = mk_var(n);
auto vi = register_theory_var_in_lar_solver(v);
add_def_constraint_and_equality(vi, lp::GE, std::min(b1, b2));
add_def_constraint_and_equality(vi, lp::LE, std::max(b1, b2));
}
// is_int(x) <=> to_real(to_int(x)) = x