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

fix incorrect bound in order-lemma

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-13 14:28:15 -07:00
parent 23c12b75af
commit 5ee9edf46b
6 changed files with 34 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/math/grobner/pdd_solver.cpp
View file

@ -311,6 +311,7 @@ namespace dd {
unsigned v = m_level2var[m_levelp1-1];
equation* eq = nullptr;
for (equation* curr : m_to_simplify) {
SASSERT(curr->idx() != UINT_MAX);
pdd const& p = curr->poly();
if (curr->state() == to_simplify && p.var() == v) {
if (!eq || is_simpler(*curr, *eq))
@ -389,6 +390,16 @@ namespace dd {
retire(eq);
}
void solver::retire(equation* eq) {
#if 0
// way to check if retired equations are ever accessed.
eq->set_index(UINT_MAX);
#else
dealloc(eq);
#endif
}
void solver::pop_equation(equation& eq) {
equation_vector& v = get_queue(eq);
unsigned idx = eq.idx();

2
src/math/grobner/pdd_solver.h
View file

@ -181,7 +181,7 @@ private:
void del_equation(equation& eq) { del_equation(&eq); }
void del_equation(equation* eq);
equation_vector& get_queue(equation const& eq);
void retire(equation* eq) { dealloc(eq); }
void retire(equation* eq);
void pop_equation(equation& eq);
void pop_equation(equation* eq) { pop_equation(*eq); }
void push_equation(eq_state st, equation& eq);

4
src/math/lp/nla_core.cpp
View file

@ -892,10 +892,6 @@ bool core::divide(const monic& bc, const factor& c, factor & b) const {
return true;
}
void core::negate_var_relation_strictly(new_lemma& lemma, lpvar a, lpvar b) {
SASSERT(val(a) != val(b));
lemma |= ineq(term(a, -rational(1), b), val(a) < val(b) ? llc::GT : llc::LT, 0);
}
void core::negate_factor_equality(new_lemma& lemma, const factor& c,
const factor& d) {

1
src/math/lp/nla_core.h
View file

@ -426,7 +426,6 @@ public:
void negate_relation(new_lemma& lemma, unsigned j, const rational& a);
void negate_factor_equality(new_lemma& lemma, const factor& c, const factor& d);
void negate_factor_relation(new_lemma& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b);
void negate_var_relation_strictly(new_lemma& lemma, lpvar a, lpvar b);
bool find_bfc_to_refine_on_monic(const monic&, factorization & bf);

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

@ -227,25 +227,22 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab
}
}
bool order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac, bool k) {
void order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac, bool k) {
const factor c = ac[k];
TRACE("nla_solver", tout << "c = "; _().print_factor_with_vars(c, tout); );
if (c.is_var()) {
TRACE("nla_solver", tout << "var(c) = " << var(c););
for (monic const& bc : _().emons().get_use_list(c.var())) {
if (order_lemma_on_ac_and_bc(rm, ac, k, bc)) {
return true;
}
if (order_lemma_on_ac_and_bc(rm, ac, k, bc))
return;
}
}
else {
for (monic const& bc : _().emons().get_products_of(c.var())) {
if (order_lemma_on_ac_and_bc(rm, ac, k, bc)) {
return true;
}
if (order_lemma_on_ac_and_bc(rm, ac, k, bc))
return;
}
}
return false;
}
void order::generate_ol_eq(const monic& ac,
@ -280,15 +277,19 @@ void order::generate_ol(const monic& ac,
const factor& b) {
new_lemma lemma(_(), __FUNCTION__);
IF_VERBOSE(100, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac
TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout););
IF_VERBOSE(10, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac
<< " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"
<< " a " << "*v" << var(a) << " " << val(a) << "\n"
<< " b " << "*v" << var(b) << " " << val(b) << "\n"
<< " c " << "*v" << var(c) << " " << val(c) << "\n");
// fix the sign of c
// c > 0 and ac >= bc => a >= b
// c > 0 and ac <= bc => a <= b
// 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);
_().negate_var_relation_strictly(lemma, ac.var(), bc.var());
_().negate_var_relation_strictly(lemma, a.var(), b.var());
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 &= ac;
lemma &= a;
@ -298,8 +299,9 @@ void order::generate_ol(const monic& ac,
}
// We have ac = a*c and bc = b*c.
// Suppose ac >= bc, then ac/|c| >= bc/|b|
// Notice that ac/|c| = a*rat_sign(val(c)|, and similar fo bc/|c|.//
// Suppose ac >= bc, then ac/|c| >= bc/|c|
// Notice that ac/|c| = a*rat_sign(val(c)|, and similar fo bc/|c|.
//
bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
const factor& a,
const factor& c,
@ -309,16 +311,14 @@ 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 ((var_val(ac) > var_val(bc) && av_c_s < bv_c_s)
||
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)) {
TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout););
generate_ol(ac, a, c, bc, b);
return true;
} else {
if ((var_val(ac) == var_val(bc)) && (av_c_s != bv_c_s)) {
generate_ol_eq(ac, a, c, bc, b);
}
}
else if ((var_val(ac) == var_val(bc)) && (av_c_s != bv_c_s)) {
generate_ol_eq(ac, a, c, bc, b);
return true;
}
return false;
}

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

@ -34,7 +34,7 @@ private:
bool k,
const monic& rm_bd);
bool order_lemma_on_ac_explore(const monic& rm, const factorization& ac, bool k);
void order_lemma_on_ac_explore(const monic& rm, const factorization& ac, bool k);
void order_lemma_on_factorization(const monic& rm, const factorization& ab);