From 90f5595067605480782840dca92d34ab999848fc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 May 2020 15:38:55 -0700 Subject: [PATCH] fix order lemma bug see 30ce6f20f2b2311c504cd7d30a01b0891d6174f7 Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 2 +- src/math/lp/nla_order_lemmas.cpp | 6 +----- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index f849a9421..fea075d27 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1396,7 +1396,7 @@ lbool core::check(vector& l_vec) { set_use_nra_model(false); - if (l_vec.empty() && !done()) + if (false && l_vec.empty() && !done()) m_monomial_bounds(); if (l_vec.empty() && !done() && need_to_call_algebraic_methods()) diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 77bd16e0f..decc81438 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -213,7 +213,7 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab tout << "ab.size()=" << ab.size() << "\n"; tout << "we should have sign*var_val(m):" << mv << "=(" << rsign << ")*(" << var_val(m) <<") to be equal to " << " val(var(ab[0]))*val(var(ab[1])):" << fv << "\n";); TRACE("nla_solver", tout << "m="; _().print_monic_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout);); - if (mv != fv) { + if (mv != fv && !c().has_real(m)) { bool gt = mv > fv; for (unsigned j = 0, k = 1; j < 2; j++, k--) { new_lemma lemma(_(), __FUNCTION__); @@ -326,8 +326,6 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac, lemma b != val(b) || sign*m <= a*val(b) */ void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) { - if (!c().var_is_int(b) && val(b).is_big()) - return; SASSERT(sign * var_val(m) > val(a) * val(b)); // negate b == val(b) lemma |= ineq(b, llc::NE, val(b)); @@ -339,8 +337,6 @@ void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rationa lemma b != val(b) || sign*m >= a*val(b) */ void order::order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) { - if (!c().var_is_int(b) && val(b).is_big()) - return; TRACE("nla_solver", tout << "sign = " << sign << ", m = "; c().print_monic(m, tout) << ", a = "; c().print_var(a, tout) << ", b = "; c().print_var(b, tout) << "\n";); SASSERT(sign * var_val(m) < val(a) * val(b));