mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
Lev Nachmanson
commit
536f4f84bb
28 changed files with 188 additions and 116 deletions
|
|
@ -611,4 +611,19 @@ void emonics::set_propagated(monic const& m) {
|
|||
m_u_f_stack.push(set_unpropagated(*this, m.var()));
|
||||
}
|
||||
|
||||
void emonics::set_bound_propagated(monic const& m) {
|
||||
struct set_bound_unpropagated : public trail {
|
||||
emonics& em;
|
||||
unsigned var;
|
||||
public:
|
||||
set_bound_unpropagated(emonics& em, unsigned var): em(em), var(var) {}
|
||||
void undo() override {
|
||||
em[var].set_bound_propagated(false);
|
||||
}
|
||||
};
|
||||
SASSERT(!m.is_bound_propagated());
|
||||
(*this)[m.var()].set_bound_propagated(true);
|
||||
m_u_f_stack.push(set_bound_unpropagated(*this, m.var()));
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -143,6 +143,7 @@ public:
|
|||
void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}
|
||||
|
||||
void set_propagated(monic const& m);
|
||||
void set_bound_propagated(monic const& m);
|
||||
|
||||
// this method is required by union_find
|
||||
trail_stack & get_trail_stack() { return m_u_f_stack; }
|
||||
|
|
|
|||
|
|
@ -59,6 +59,7 @@ class monic: public mon_eq {
|
|||
bool m_rsign;
|
||||
mutable unsigned m_visited;
|
||||
bool m_propagated = false;
|
||||
bool m_bound_propagated = false;
|
||||
public:
|
||||
// constructors
|
||||
monic(lpvar v, unsigned sz, lpvar const* vs, unsigned idx):
|
||||
|
|
@ -77,6 +78,8 @@ public:
|
|||
void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); }
|
||||
void set_propagated(bool p) { m_propagated = p; }
|
||||
bool is_propagated() const { return m_propagated; }
|
||||
void set_bound_propagated(bool p) { m_bound_propagated = p; }
|
||||
bool is_bound_propagated() const { return m_bound_propagated; }
|
||||
|
||||
svector<lpvar>::const_iterator begin() const { return vars().begin(); }
|
||||
svector<lpvar>::const_iterator end() const { return vars().end(); }
|
||||
|
|
|
|||
|
|
@ -1517,6 +1517,9 @@ void core::add_bounds() {
|
|||
for (lpvar j : m.vars()) {
|
||||
if (!var_is_free(j))
|
||||
continue;
|
||||
if (m.is_bound_propagated())
|
||||
continue;
|
||||
m_emons.set_bound_propagated(m);
|
||||
// split the free variable (j <= 0, or j > 0), and return
|
||||
m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
|
||||
TRACE("nla_solver", print_ineq(m_literals.back(), tout) << "\n");
|
||||
|
|
|
|||
|
|
@ -59,21 +59,20 @@ namespace nla {
|
|||
if (m_delay_base > 0)
|
||||
--m_delay_base;
|
||||
|
||||
if (is_conflicting())
|
||||
return;
|
||||
|
||||
try {
|
||||
if (propagate_bounds())
|
||||
|
||||
if (is_conflicting())
|
||||
return;
|
||||
|
||||
if (propagate_eqs())
|
||||
return;
|
||||
|
||||
|
||||
if (propagate_factorization())
|
||||
return;
|
||||
|
||||
|
||||
if (propagate_linear_equations())
|
||||
return;
|
||||
|
||||
}
|
||||
catch (...) {
|
||||
|
||||
|
|
@ -111,17 +110,9 @@ namespace nla {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool grobner::propagate_bounds() {
|
||||
unsigned changed = 0;
|
||||
for (auto eq : m_solver.equations())
|
||||
if (propagate_bounds(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
|
||||
return true;
|
||||
return changed > 0;
|
||||
}
|
||||
|
||||
bool grobner::propagate_eqs() {
|
||||
unsigned changed = 0;
|
||||
for (auto eq : m_solver.equations())
|
||||
for (auto eq : m_solver.equations())
|
||||
if (propagate_fixed(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
|
||||
return true;
|
||||
return changed > 0;
|
||||
|
|
@ -129,7 +120,7 @@ namespace nla {
|
|||
|
||||
bool grobner::propagate_factorization() {
|
||||
unsigned changed = 0;
|
||||
for (auto eq : m_solver.equations())
|
||||
for (auto eq : m_solver.equations())
|
||||
if (propagate_factorization(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
|
||||
return true;
|
||||
return changed > 0;
|
||||
|
|
@ -165,19 +156,12 @@ 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;
|
||||
}
|
||||
|
||||
|
|
@ -377,73 +361,18 @@ namespace nla {
|
|||
}
|
||||
}
|
||||
|
||||
bool grobner::propagate_bounds(const dd::solver::equation& e) {
|
||||
return false;
|
||||
// TODO
|
||||
auto& di = c().m_intervals.get_dep_intervals();
|
||||
dd::pdd_interval eval(di);
|
||||
eval.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) {
|
||||
if (deps) c().m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
|
||||
else c().m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
|
||||
};
|
||||
scoped_dep_interval i(di), i_wd(di);
|
||||
eval.get_interval<dd::w_dep::without_deps>(e.poly(), i);
|
||||
return false;
|
||||
}
|
||||
|
||||
bool grobner::propagate_linear_equations() {
|
||||
unsigned changed = 0;
|
||||
m_mon2var.clear();
|
||||
for (auto const& m : c().emons())
|
||||
m_mon2var[m.vars()] = m.var();
|
||||
|
||||
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, coeff);
|
||||
for (auto v : vars) {
|
||||
set_var_interval(v, s);
|
||||
di.mul<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.mul<dd::w_dep::with_deps>(coeff, u, 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;
|
||||
// m_solver.display(verbose_stream() << "missed bound\n", e);
|
||||
// exit(1);
|
||||
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;
|
||||
|
|
|
|||
|
|
@ -35,20 +35,14 @@ namespace nla {
|
|||
bool is_conflicting();
|
||||
bool is_conflicting(dd::solver::equation const& eq);
|
||||
|
||||
bool propagate_bounds();
|
||||
bool propagate_bounds(dd::solver::equation const& eq);
|
||||
|
||||
bool propagate_eqs();
|
||||
bool propagate_fixed(dd::solver::equation const& eq);
|
||||
|
||||
bool propagate_factorization();
|
||||
bool propagate_factorization(dd::solver::equation const& eq);
|
||||
|
||||
|
||||
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);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue