mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

fix order lemmas for emons

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-24 14:26:31 -07:00
parent 9d6bf016fc
commit f78a2058fc
2 changed files with 1 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/util/lp/nla_order_lemmas.cpp
View file

@ -168,7 +168,7 @@ void order::generate_mon_ol(const monomial& ac,
add_empty_lemma(); add_empty_lemma();
mk_ineq(c_sign, c, llc::LE); mk_ineq(c_sign, c, llc::LE);
explain(c); // this explains c == +- d explain(c); // this explains c == +- d
negate_var_factor_relation(c_sign, a, d_sign, b); mk_ineq(c_sign, a, -d_sign, b.var(), negate(ab_cmp));
mk_ineq(ac.var(), rational(-1), var(bd), ab_cmp); mk_ineq(ac.var(), rational(-1), var(bd), ab_cmp);
explain(bd); explain(bd);
explain(b); explain(b);
@ -263,14 +263,6 @@ void order::generate_ol(const monomial& ac,
TRACE("nla_solver", _().print_lemma(tout);); TRACE("nla_solver", _().print_lemma(tout););
} }
void order::negate_var_factor_relation(const rational& a_sign, lpvar a, const rational& b_sign, const factor& b) {
rational b_fs = canonize_sign(b);
llc cmp = a_sign*val(a) < b_sign*val(b)? llc::GE : llc::LE;
mk_ineq(a_sign, a, - b_fs*b_sign, var(b), cmp);
}
bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& ac, bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
const factor& a, const factor& a,
const factor& c, const factor& c,

1
src/util/lp/nla_order_lemmas.h
View file

@ -88,6 +88,5 @@ private:
const rational& d_sign, const rational& d_sign,
lpvar d, lpvar d,
llc ab_cmp); llc ab_cmp);
void negate_var_factor_relation(const rational& a_sign, lpvar a, const rational& b_sign, const factor& b);
}; };
} }