mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 19:35:42 +00:00
Code Activity

fix ordered lemma

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-05 12:58:38 -07:00
parent 54ba889b7b
commit 59e8382909
4 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/factorization.h
View file

@ -49,7 +49,7 @@ public:
} }
bool sign() const { return m_sign; } bool sign() const { return m_sign; }
bool& sign() { return m_sign; } bool& sign() { return m_sign; }
rational rsign() const { return m_sign? rational(-1) : rational(1); } rational rat_sign() const { return m_sign? rational(-1) : rational(1); }
}; };

2
src/util/lp/nla_core.cpp
View file

@ -93,7 +93,7 @@ svector<lpvar> core::sorted_rvars(const factor& f) const {
// the value of the factor is equal to the value of the variable multiplied // the value of the factor is equal to the value of the variable multiplied
// by the canonize_sign // by the canonize_sign
rational core::canonize_sign(const factor& f) const { rational core::canonize_sign(const factor& f) const {
return f.rsign() * (f.is_var()? canonize_sign_of_var(f.var()) : m_emons[f.var()].rsign()); return f.rat_sign() * (f.is_var()? canonize_sign_of_var(f.var()) : m_emons[f.var()].rsign());
} }
rational core::canonize_sign_of_var(lpvar j) const { rational core::canonize_sign_of_var(lpvar j) const {

2
src/util/lp/nla_core.h
View file

@ -106,7 +106,7 @@ public:
rational val_rooted(const monomial& m) const { return m.rsign()*val(m.var()); } rational val_rooted(const monomial& m) const { return m.rsign()*val(m.var()); }
rational val(const factor& f) const { return f.rsign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); } rational val(const factor& f) const { return f.rat_sign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); }
lpvar var(const factor& f) const { return f.var(); } lpvar var(const factor& f) const { return f.var(); }

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

@ -180,7 +180,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
mk_ineq(c_sign, a, -d_sign, b.var(), negate(ab_cmp)); mk_ineq(c_sign, a, -d_sign * b.rat_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);