mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-19 17:50:23 +00:00
Code Activity

order lemma

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-04 10:30:24 -08:00 • committed by Lev Nachmanson
parent fc277f5648
commit 7775afdcc3
1 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/util/lp/nla_solver.cpp
View file

@ -1040,6 +1040,8 @@ struct solver::imp {
const rooted_mon& bd, const rooted_mon& bd,
const factor& b, const factor& b,
const factor& d) { const factor& d) {
rational c_over_d = vvr(c) / vvr(d);
SASSERT(abs(c_over_d) == rational(1));
if (c != d) { if (c != d) {
lpvar i = var(c); lpvar i = var(c);
lpvar j = var(d); lpvar j = var(d);
@ -1048,9 +1050,21 @@ struct solver::imp {
if (iv == jv) { if (iv == jv) {
mk_ineq(i, -rational(1), j, lp::lconstraint_kind::NE); mk_ineq(i, -rational(1), j, lp::lconstraint_kind::NE);
} else { // iv == -jv } else { // iv == -jv
c_over_d = -rational(1);
mk_ineq(i, j, lp::lconstraint_kind::NE); 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, bool order_lemma_on_ac_and_bd_and_factors(const rooted_mon& ac,