From a3f56f0d95f58037b378c154bf6524e7f8b7b97f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 May 2020 11:21:03 -0700 Subject: [PATCH] revert 'fix' Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_monotone_lemmas.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index 717091f53..68585ca4c 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -46,6 +46,11 @@ void monotone::monotonicity_lemma(monic const& m) { m[i] < val(m[i]) for val(m[i]) < 0 m >= product m[i] for product m[i] < 0 m <= product m[i] for product m[i] > 0 + + Example: + + x <= -2 & y >= 3 => x*y <= -6 + */ void monotone::monotonicity_lemma_gt(const monic& m) { new_lemma lemma(c(), __FUNCTION__); @@ -53,8 +58,6 @@ 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); - if (v.is_neg()) - lemma |= ineq(j, llc::GT, 0); product *= v; } lemma |= ineq(m.var(), product.is_neg() ? llc::GE : llc::LE, product);