mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

additional sign related fix for #4740 https://github.com/Z3Prover/z3/issues/4740#issuecomment-721508240

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-11-10 10:50:06 -08:00
parent 5ace60c812
commit fdedeed7ae
3 changed files with 6 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/monic.h
View file

@ -77,6 +77,8 @@ public:
svector<lpvar>::const_iterator begin() const { return vars().begin(); }
svector<lpvar>::const_iterator end() const { return vars().end(); }
rational rat_sign() const { return m_rsign ? rational(-1) : rational(1); }
};
inline std::ostream& operator<<(std::ostream& out, monic const& m) {

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

@ -262,7 +262,7 @@ void order::generate_ol_eq(const monic& ac,
// ac == bc
lemma |= ineq(c.var(), llc::EQ, 0); // c is not equal to zero
lemma |= ineq(term(ac.var(), -rational(1), bc.var()), llc::NE, 0);
lemma |= ineq(term(sign_to_rat(canonize_sign(a)), a.var(), sign_to_rat(!canonize_sign(b)), b.var()), llc::EQ, 0);
lemma |= ineq(term(a.rat_sign(), a.var(), -b.rat_sign(), b.var()), llc::EQ, 0);
lemma &= ac;
lemma &= a;
lemma &= bc;
@ -288,8 +288,8 @@ void order::generate_ol(const monic& ac,
// c < 0 and ac >= bc => a <= b
// c < 0 and ac <= bc => a >= b
lemma |= ineq(c.var(), val(c.var()).is_neg() ? llc::GE : llc::LE, 0);
lemma |= ineq(term(ac.var(), -rational(1), bc.var()), val(ac.var()) < val(bc.var()) ? llc::GT : llc::LT, 0);
lemma |= ineq(term(a.var(), -rational(1), b.var()), val(a.var()) < val(b.var()) ? llc::GE : llc::LE, 0);
lemma |= ineq(term(rational(1), ac.var(), -rational(1), bc.var()), var_val(ac) < var_val(bc) ? llc::GT : llc::LT, 0);
lemma |= ineq(term(a.rat_sign(), a.var(), -b.rat_sign(), b.var()), val(a) < val(b) ? llc::GE : llc::LE, 0);
lemma &= ac;
lemma &= a;
@ -311,10 +311,6 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
rational c_sign = rational(nla::rat_sign(val(c)));
auto av_c_s = val(a) * c_sign;
auto bv_c_s = val(b) * c_sign;
if (b.sign() != a.sign())
return false;
if (bc.rsign() != ac.rsign())
return false;
if ((var_val(ac) > var_val(bc) && av_c_s < bv_c_s) ||
(var_val(ac) < var_val(bc) && av_c_s > bv_c_s)) {
generate_ol(ac, a, c, bc, b);

2
src/sat/smt/bv_delay_internalize.cpp
View file

@ -179,7 +179,7 @@ namespace bv {
args[i] = n->get_arg(i);
add_unit(eq_internalize(r, arg_value));
}
IF_VERBOSE(0, verbose_stream() << "delay internalize @" << s().scope_lvl() << "\n");
IF_VERBOSE(2, verbose_stream() << "delay internalize @" << s().scope_lvl() << "\n");
return false;
}
if (bv.is_zero(mul_value)) {