mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 08:23:17 +00:00
Code Activity

do as Lev does

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-03 13:21:43 -07:00
parent 7802e33f37
commit 8d3caa00fe
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_lra.cpp
View file

@ -1396,6 +1396,11 @@ public:
} }
else { else {
/*literal div_ge_0 = */ mk_literal(a.mk_ge(div, zero));
/*literal div_le_0 = */ mk_literal(a.mk_le(div, zero));
/*literal p_ge_0 = */ mk_literal(a.mk_ge(p, zero));
/*literal p_le_0 = */ mk_literal(a.mk_le(p, zero));
// q >= 0 or p = (p mod q) + q * (p div q) // q >= 0 or p = (p mod q) + q * (p div q)
// q <= 0 or p = (p mod q) + q * (p div q) // q <= 0 or p = (p mod q) + q * (p div q)
// q >= 0 or (p mod q) >= 0 // q >= 0 or (p mod q) >= 0
@ -1411,12 +1416,10 @@ public:
mk_axiom(q_le_0, mod_ge_0); mk_axiom(q_le_0, mod_ge_0);
mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero))); mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero))); mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
#if 0 #if 0
// seem expensive // seem expensive
literal div_ge_0 = mk_literal(a.mk_ge(div, zero));
literal div_le_0 = mk_literal(a.mk_le(div, zero));
literal p_ge_0 = mk_literal(a.mk_ge(p, zero));
literal p_le_0 = mk_literal(a.mk_le(p, zero));
mk_axiom(q_le_0, ~p_ge_0, div_ge_0); mk_axiom(q_le_0, ~p_ge_0, div_ge_0);
mk_axiom(q_le_0, ~p_le_0, div_le_0); mk_axiom(q_le_0, ~p_le_0, div_le_0);