From 7775afdcc392c4bfc30de234b62166576ade781f Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 4 Dec 2018 10:30:24 -0800 Subject: [PATCH] order lemma Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index bd54707fc..443e316f7 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -1040,6 +1040,8 @@ struct solver::imp { const rooted_mon& bd, const factor& b, const factor& d) { + rational c_over_d = vvr(c) / vvr(d); + SASSERT(abs(c_over_d) == rational(1)); if (c != d) { lpvar i = var(c); lpvar j = var(d); @@ -1048,9 +1050,21 @@ struct solver::imp { if (iv == jv) { mk_ineq(i, -rational(1), j, lp::lconstraint_kind::NE); } else { // iv == -jv + c_over_d = -rational(1); mk_ineq(i, j, lp::lconstraint_kind::NE); } } + + { + lpvar i = var(a); + rational i_fs = flip_sign(a); + lpvar j = var(b); + rational j_fs = flip_sign(b); + auto iv = vvr(a), jv = vvr(b); + SASSERT(iv != jv); + lp::lconstraint_kind cmp = iv < jv? lp::lconstraint_kind::GE : lp::lconstraint_kind::LE; + mk_ineq(i_fs, i, -rational(1) * j_fs, j, cmp); + } } bool order_lemma_on_ac_and_bd_and_factors(const rooted_mon& ac,