From 0c91109577ca44f1a4617c1eda347108f9d1b4a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 May 2020 10:11:52 -0700 Subject: [PATCH] order lemmas on also rationals --- src/math/lp/nla_order_lemmas.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 09d62c456..eaa470db5 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -40,8 +40,6 @@ void order::order_lemma() { void order::order_lemma_on_monic(const monic& m) { TRACE("nla_solver_details", tout << "m = " << pp_mon(c(), m);); - if (c().has_real(m)) - return; for (auto ac : factorization_factory_imp(m, _())) { if (ac.size() != 2) continue; @@ -82,6 +80,8 @@ void order::order_lemma_on_binomial(const monic& ac) { */ void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) { + if (!c().var_is_int(x) && val(x).is_big()) + return; SASSERT(!_().mon_has_zero(xy.vars())); int sy = rat_sign(val(y)); new_lemma lemma(c(), __FUNCTION__); @@ -326,6 +326,8 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac, lemma b != val(b) || sign 0 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)); @@ -337,6 +339,8 @@ 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));