mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

try with missed bounds

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-02 10:48:35 -08:00
parent 5c1e7f7112
commit 7eab26e3ef
2 changed files with 42 additions and 0 deletions

40
src/math/lp/nla_grobner.cpp
View file

@ -399,9 +399,49 @@ namespace nla {
for (auto eq : m_solver.equations())
if (propagate_linear_equations(*eq))
++changed;
#if 0
for (auto eq : m_solver.equations())
if (check_missed_bound(*eq))
return true;
#endif
return changed > 0;
}
bool grobner::check_missed_bound(dd::solver::equation const& e) {
auto& di = c().m_intervals.get_dep_intervals();
auto set_var_interval = [&](lpvar j, scoped_dep_interval& a) {
c().m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
};
scoped_dep_interval i(di), t(di), s(di), u(di);
di.set_value(i, rational::zero());
for (auto const& [coeff, vars] : e.poly()) {
if (vars.empty())
di.add(coeff, i);
else {
di.set_value(t, rational::one());
for (auto v : vars) {
set_var_interval(v, s);
di.mul<dd::w_dep::with_deps>(coeff, s, s);
di.add<dd::w_dep::with_deps>(t, s, t);
}
if (m_mon2var.find(vars) != m_mon2var.end()) {
auto v = m_mon2var.find(vars)->second;
set_var_interval(v, u);
di.intersect<dd::w_dep::with_deps>(t, u, t);
}
di.add<dd::w_dep::with_deps>(i, t, i);
}
}
if (!di.separated_from_zero(i))
return false;
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
new_lemma lemma(m_core, "pdd");
lemma &= e;
};
return di.check_interval_for_conflict_on_zero(i, e.dep(), f);
}
bool grobner::propagate_linear_equations(dd::solver::equation const& e) {
if (equation_is_true(e))
return false;

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

@ -47,6 +47,8 @@ namespace nla {
bool propagate_linear_equations();
bool propagate_linear_equations(dd::solver::equation const& eq);
bool check_missed_bound(dd::solver::equation const& eq);
void add_dependencies(new_lemma& lemma, dd::solver::equation const& eq);
void explain(dd::solver::equation const& eq, lp::explanation& exp);