From 8d3caa00fe0936d431a39cb537d29180c8b967e9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2020 13:21:43 -0700 Subject: [PATCH] do as Lev does Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b69c628c4..071496577 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1396,6 +1396,11 @@ public: } 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 mod q) >= 0 @@ -1411,12 +1416,10 @@ public: 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_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero))); + + #if 0 // 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_le_0, div_le_0);