mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 02:45:51 +00:00
add facility to check for missing propagations
This commit is contained in:
Nikolaj Bjorner
parent
cafe3acff1
commit
bdac86501d
5 changed files with 109 additions and 11 deletions
|
|
@ -61,6 +61,9 @@ namespace nla {
|
|||
|
||||
}
|
||||
|
||||
// DEBUG_CODE(for (auto e : m_solver.equations()) check_missing_propagation(*e););
|
||||
|
||||
|
||||
if (m_quota > 0)
|
||||
--m_quota;
|
||||
|
||||
|
|
@ -125,11 +128,11 @@ namespace nla {
|
|||
typedef lp::lar_term term;
|
||||
bool grobner::propagate_fixed(const dd::solver::equation& eq) {
|
||||
dd::pdd const& p = eq.poly();
|
||||
//IF_VERBOSE(0, verbose_stream() << p << "\n");
|
||||
if (p.is_unary()) {
|
||||
unsigned v = p.var();
|
||||
if (c().var_is_fixed(v))
|
||||
return false;
|
||||
|
||||
ineq new_eq(v, llc::EQ, rational::zero());
|
||||
if (c().ineq_holds(new_eq))
|
||||
return false;
|
||||
|
|
@ -147,12 +150,19 @@ namespace nla {
|
|||
rational d = lcm(denominator(a), denominator(b));
|
||||
a *= d;
|
||||
b *= d;
|
||||
#if 0
|
||||
c().lra.update_column_type_and_bound(v, lp::lconstraint_kind::EQ, b/a, eq.dep());
|
||||
lp::explanation exp;
|
||||
explain(eq, exp);
|
||||
c().add_fixed_equality(c().lra.column_to_reported_index(v), b/a, exp);
|
||||
#else
|
||||
ineq new_eq(term(a, v), llc::EQ, b);
|
||||
if (c().ineq_holds(new_eq))
|
||||
return false;
|
||||
new_lemma lemma(c(), "pdd-eq");
|
||||
add_dependencies(lemma, eq);
|
||||
lemma |= new_eq;
|
||||
#endif
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -193,15 +203,19 @@ namespace nla {
|
|||
return true;
|
||||
}
|
||||
|
||||
|
||||
void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) {
|
||||
lp::explanation ex;
|
||||
void grobner::explain(const dd::solver::equation& eq, lp::explanation& exp) {
|
||||
u_dependency_manager dm;
|
||||
vector<unsigned, false> lv;
|
||||
dm.linearize(eq.dep(), lv);
|
||||
for (unsigned ci : lv)
|
||||
ex.push_back(ci);
|
||||
lemma &= ex;
|
||||
exp.push_back(ci);
|
||||
}
|
||||
|
||||
|
||||
void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) {
|
||||
lp::explanation exp;
|
||||
explain(eq, exp);
|
||||
lemma &= exp;
|
||||
}
|
||||
|
||||
void grobner::configure() {
|
||||
|
|
@ -280,6 +294,10 @@ namespace nla {
|
|||
}
|
||||
|
||||
bool grobner::is_conflicting(const dd::solver::equation& e) {
|
||||
for (auto j : e.poly().free_vars())
|
||||
if (lra.column_is_free(j))
|
||||
return false;
|
||||
|
||||
auto& di = c().m_intervals.get_dep_intervals();
|
||||
dd::pdd_interval eval(di);
|
||||
eval.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) {
|
||||
|
|
@ -549,4 +567,16 @@ namespace nla {
|
|||
tout << "\n");
|
||||
}
|
||||
|
||||
void grobner::check_missing_propagation(const dd::solver::equation& e) {
|
||||
vector<dd::pdd> eqs;
|
||||
eqs.push_back(e.poly());
|
||||
lbool r = c().m_nra.check(eqs);
|
||||
CTRACE("grobner", r == l_false, m_solver.display(tout << "missed conflict ", e););
|
||||
if (r != l_true)
|
||||
return;
|
||||
r = c().m_nra.check_tight(e.poly());
|
||||
CTRACE("grobner", r == l_false, m_solver.display(tout << "tight equality ", e););
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -41,6 +41,9 @@ namespace nla {
|
|||
bool propagate_factorization(const dd::solver::equation& eq);
|
||||
|
||||
void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq);
|
||||
void explain(const dd::solver::equation& eq, lp::explanation& exp);
|
||||
|
||||
void check_missing_propagation(const dd::solver::equation& eq);
|
||||
|
||||
// setup
|
||||
void configure();
|
||||
|
|
|
|||
|
|
@ -206,14 +206,62 @@ struct solver::imp {
|
|||
}
|
||||
}
|
||||
|
||||
if (r == l_true)
|
||||
return r;
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << "check-nra " << r << "\n";
|
||||
m_nlsat->display(verbose_stream());
|
||||
for (auto const& [v, w] : m_lp2nl) {
|
||||
auto& ls = m_nla_core.lra;
|
||||
if (ls.column_has_lower_bound(v))
|
||||
verbose_stream() << w << " >= " << ls.get_lower_bound(v) << "\n";
|
||||
verbose_stream() << "x" << w << " >= " << ls.get_lower_bound(v) << "\n";
|
||||
if (ls.column_has_upper_bound(v))
|
||||
verbose_stream() << w << " <= " << ls.get_upper_bound(v) << "\n";
|
||||
verbose_stream() << "x" << w << " <= " << ls.get_upper_bound(v) << "\n";
|
||||
});
|
||||
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
lbool check_tight(dd::pdd const& eq) {
|
||||
m_zero = nullptr;
|
||||
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
|
||||
m_zero = alloc(scoped_anum, am());
|
||||
m_lp2nl.reset();
|
||||
m_term_set.reset();
|
||||
add_eq(eq);
|
||||
for (auto const& [v, w] : m_lp2nl) {
|
||||
auto& ls = m_nla_core.lra;
|
||||
if (ls.column_has_lower_bound(v))
|
||||
add_strict_lb(ls.get_lower_bound(v), w);
|
||||
if (ls.column_has_upper_bound(v))
|
||||
add_strict_ub(ls.get_upper_bound(v), w);
|
||||
}
|
||||
|
||||
lbool r = l_undef;
|
||||
try {
|
||||
r = m_nlsat->check();
|
||||
}
|
||||
catch (z3_exception&) {
|
||||
if (m_limit.is_canceled()) {
|
||||
r = l_undef;
|
||||
}
|
||||
else {
|
||||
throw;
|
||||
}
|
||||
}
|
||||
|
||||
if (r == l_true)
|
||||
return r;
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << "check-nra tight " << r << "\n";
|
||||
m_nlsat->display(verbose_stream());
|
||||
for (auto const& [v, w] : m_lp2nl) {
|
||||
auto& ls = m_nla_core.lra;
|
||||
if (ls.column_has_lower_bound(v))
|
||||
verbose_stream() << "x" << w << " >= " << ls.get_lower_bound(v) << "\n";
|
||||
if (ls.column_has_upper_bound(v))
|
||||
verbose_stream() << "x" << w << " <= " << ls.get_upper_bound(v) << "\n";
|
||||
});
|
||||
|
||||
|
||||
|
|
@ -235,6 +283,13 @@ struct solver::imp {
|
|||
m_nlsat->mk_clause(1, &lit, nullptr);
|
||||
}
|
||||
|
||||
void add_strict_lb(lp::impq const& b, unsigned w) {
|
||||
add_bound(b.x, w, false, nlsat::atom::kind::GT);
|
||||
}
|
||||
void add_strict_ub(lp::impq const& b, unsigned w) {
|
||||
add_bound(b.x, w, false, nlsat::atom::kind::LT);
|
||||
}
|
||||
|
||||
void add_lb(lp::impq const& b, unsigned w) {
|
||||
add_bound(b.x, w, b.y <= 0, b.y > 0 ? nlsat::atom::kind::GT : nlsat::atom::kind::LT);
|
||||
}
|
||||
|
|
@ -269,7 +324,8 @@ struct solver::imp {
|
|||
m_lp2nl.insert(v, w);
|
||||
}
|
||||
polynomial::polynomial_ref vp(pm.mk_polynomial(w, 1), pm);
|
||||
return pm.add(lo, pm.mul(vp, hi));
|
||||
polynomial::polynomial_ref mp(pm.mul(vp, hi), pm);
|
||||
return pm.add(lo, mp);
|
||||
}
|
||||
|
||||
bool is_int(lp::var_index v) {
|
||||
|
|
@ -361,6 +417,10 @@ lbool solver::check(vector<dd::pdd> const& eqs) {
|
|||
return m_imp->check(eqs);
|
||||
}
|
||||
|
||||
lbool solver::check_tight(dd::pdd const& eq) {
|
||||
return m_imp->check_tight(eq);
|
||||
}
|
||||
|
||||
bool solver::need_check() {
|
||||
return m_imp->need_check();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -38,10 +38,15 @@ namespace nra {
|
|||
lbool check();
|
||||
|
||||
/**
|
||||
\breif Check feasibility of equalities modulo bounds constraints on their variables.
|
||||
\brief Check feasibility of equalities modulo bounds constraints on their variables.
|
||||
*/
|
||||
lbool check(vector<dd::pdd> const& eqs);
|
||||
|
||||
/**
|
||||
\brief Check if equality is tight.
|
||||
*/
|
||||
lbool check_tight(const dd::pdd& eq);
|
||||
|
||||
/*
|
||||
\brief determine whether nra check is needed.
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -2158,7 +2158,6 @@ public:
|
|||
if (m_nla) {
|
||||
m_nla->propagate();
|
||||
add_lemmas();
|
||||
add_equalities();
|
||||
lp().collect_more_rows_for_lp_propagation();
|
||||
}
|
||||
}
|
||||
|
|
@ -2193,6 +2192,7 @@ public:
|
|||
assume_literal(i);
|
||||
for (const nla::lemma & l : m_nla->lemmas())
|
||||
false_case_of_check_nla(l);
|
||||
add_equalities();
|
||||
}
|
||||
|
||||
bool should_propagate() const {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue