From b2bfb1faea933af69fbaeafb85daf3a2322528c9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 May 2020 17:26:09 -0700 Subject: [PATCH] fix nla_monotone lemmas again Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_monotone_lemmas.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index 68585ca4c..76d549f27 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -49,7 +49,7 @@ void monotone::monotonicity_lemma(monic const& m) { Example: - x <= -2 & y >= 3 => x*y <= -6 + 0 >= x >= -2 & 0 <= y <= 3 => x*y >= -6 */ void monotone::monotonicity_lemma_gt(const monic& m) { @@ -58,6 +58,7 @@ void monotone::monotonicity_lemma_gt(const monic& m) { for (lpvar j : m.vars()) { auto v = c().val(j); lemma |= ineq(j, v.is_neg() ? llc::LT : llc::GT, v); + lemma |= ineq(j, v.is_neg() ? llc::GT : llc::LT, 0); product *= v; } lemma |= ineq(m.var(), product.is_neg() ? llc::GE : llc::LE, product); @@ -68,6 +69,10 @@ void monotone::monotonicity_lemma_gt(const monic& m) { /\_i |m[i]| >= |val(m[i])| => |m| >= |product_i val(m[i])| <=> \/_i |m[i]| < |val(m[i])| or |m| >= |product_i val(m[i])| + + Example: + + x <= -2 & y >= 3 => x*y <= -6 */ void monotone::monotonicity_lemma_lt(const monic& m) { new_lemma lemma(c(), __FUNCTION__);