mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
increase build version, better propagation in euf-egraph, handle assumptions in sat.smt
- increase build version to 4.12.1. This prepares updated release for MacOs-11 build on x86 - move literal propagation mode in euf-egraph to a callback and traversal of equivalence class. Track antecedent by newest equality instead of root. This makes equality propagation to literals have similar behavior as in legacy solver and appears to result in a speedup (10% fewer conflicts on QF_UF/QG-classification/qg5/iso_icl478.smt2 in preliminary testing) - fix interaction of pre-processing and assumptions. Pre-processing has to freeze assumption literals so they don't get eliminated. This is similar to dependencies that are already frozen.
This commit is contained in:
Nikolaj Bjorner
parent
c8f197d0ca
commit
7368f9f7d3
22 changed files with 201 additions and 162 deletions
|
|
@ -70,7 +70,7 @@ class sat_smt_solver : public solver {
|
|||
return out;
|
||||
}
|
||||
void append(generic_model_converter& mc) { model_trail().append(mc); }
|
||||
void replay(unsigned qhead) { m_reconstruction_trail.replay(qhead, *this); }
|
||||
void replay(unsigned qhead, expr_ref_vector& assumptions) { m_reconstruction_trail.replay(qhead, assumptions, *this); }
|
||||
void flatten_suffix() override {
|
||||
expr_mark seen;
|
||||
unsigned j = qhead();
|
||||
|
|
@ -237,8 +237,10 @@ public:
|
|||
expr_ref_vector assumptions(m);
|
||||
for (unsigned i = 0; i < sz; ++i)
|
||||
assumptions.push_back(ensure_literal(_assumptions[i]));
|
||||
for (expr* a : assumptions)
|
||||
m_preprocess_state.freeze(a);
|
||||
TRACE("sat", tout << assumptions << "\n";);
|
||||
lbool r = internalize_formulas();
|
||||
lbool r = internalize_formulas(assumptions);
|
||||
if (r != l_true)
|
||||
return r;
|
||||
|
||||
|
|
@ -271,7 +273,8 @@ public:
|
|||
|
||||
void push() override {
|
||||
try {
|
||||
internalize_formulas();
|
||||
expr_ref_vector none(m);
|
||||
internalize_formulas(none);
|
||||
}
|
||||
catch (...) {
|
||||
push_internal();
|
||||
|
|
@ -430,7 +433,7 @@ public:
|
|||
}
|
||||
|
||||
expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) override {
|
||||
lbool r = internalize_formulas();
|
||||
lbool r = internalize_formulas(vs);
|
||||
if (r != l_true) {
|
||||
IF_VERBOSE(0, verbose_stream() << "internalize produced " << r << "\n");
|
||||
return expr_ref_vector(m);
|
||||
|
|
@ -561,7 +564,8 @@ public:
|
|||
|
||||
void convert_internalized() {
|
||||
m_solver.pop_to_base_level();
|
||||
internalize_formulas();
|
||||
expr_ref_vector none(m);
|
||||
internalize_formulas(none);
|
||||
if (!is_internalized() || m_internalized_converted)
|
||||
return;
|
||||
sat2goal s2g;
|
||||
|
|
@ -641,9 +645,9 @@ private:
|
|||
add_assumption(a);
|
||||
}
|
||||
|
||||
lbool internalize_formulas() {
|
||||
lbool internalize_formulas(expr_ref_vector& assumptions) {
|
||||
|
||||
if (is_internalized())
|
||||
if (is_internalized() && assumptions.empty())
|
||||
return l_true;
|
||||
|
||||
unsigned qhead = m_preprocess_state.qhead();
|
||||
|
|
@ -651,7 +655,7 @@ private:
|
|||
|
||||
m_internalized_converted = false;
|
||||
|
||||
m_preprocess_state.replay(qhead);
|
||||
m_preprocess_state.replay(qhead, assumptions);
|
||||
m_preprocess.reduce();
|
||||
if (!m.inc())
|
||||
return l_undef;
|
||||
|
|
|
|||
|
|
@ -63,6 +63,11 @@ namespace euf {
|
|||
};
|
||||
m_egraph.set_display_justification(disp);
|
||||
|
||||
std::function<void(euf::enode* n, euf::enode* ante)> on_literal = [&](enode* n, enode* ante) {
|
||||
propagate_literal(n, ante);
|
||||
};
|
||||
m_egraph.set_on_propagate(on_literal);
|
||||
|
||||
if (m_relevancy.enabled()) {
|
||||
std::function<void(euf::enode* root, euf::enode* other)> on_merge =
|
||||
[&](enode* root, enode* other) {
|
||||
|
|
@ -414,7 +419,6 @@ namespace euf {
|
|||
}
|
||||
bool propagated1 = false;
|
||||
if (m_egraph.propagate()) {
|
||||
propagate_literals();
|
||||
propagate_th_eqs();
|
||||
propagated1 = true;
|
||||
}
|
||||
|
|
@ -435,52 +439,52 @@ namespace euf {
|
|||
return propagated;
|
||||
}
|
||||
|
||||
void solver::propagate_literals() {
|
||||
for (; m_egraph.has_literal() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_literal()) {
|
||||
auto [n, ante] = m_egraph.get_literal();
|
||||
expr* e = n->get_expr();
|
||||
expr* a = nullptr, *b = nullptr;
|
||||
bool_var v = n->bool_var();
|
||||
SASSERT(m.is_bool(e));
|
||||
size_t cnstr;
|
||||
literal lit;
|
||||
if (!ante) {
|
||||
VERIFY(m.is_eq(e, a, b));
|
||||
cnstr = eq_constraint().to_index();
|
||||
lit = literal(v, false);
|
||||
}
|
||||
else {
|
||||
//
|
||||
// There are the following three cases for propagation of literals
|
||||
//
|
||||
// 1. n == ante is true from equallity, ante = true/false
|
||||
// 2. n == ante is true from equality, value(ante) != l_undef
|
||||
// 3. value(n) != l_undef, ante = true/false, merge_tf is set on n
|
||||
//
|
||||
lbool val = ante->value();
|
||||
if (val == l_undef) {
|
||||
SASSERT(m.is_value(ante->get_expr()));
|
||||
val = m.is_true(ante->get_expr()) ? l_true : l_false;
|
||||
}
|
||||
auto& c = lit_constraint(ante);
|
||||
cnstr = c.to_index();
|
||||
lit = literal(v, val == l_false);
|
||||
}
|
||||
unsigned lvl = s().scope_lvl();
|
||||
|
||||
CTRACE("euf", s().value(lit) != l_true, tout << lit << " " << s().value(lit) << "@" << lvl << " " << mk_bounded_pp(a, m) << " = " << mk_bounded_pp(b, m) << "\n";);
|
||||
if (s().value(lit) == l_false && m_ackerman && a && b)
|
||||
m_ackerman->cg_conflict_eh(a, b);
|
||||
switch (s().value(lit)) {
|
||||
case l_true:
|
||||
if (n->merge_tf() && !m.is_value(n->get_root()->get_expr()))
|
||||
m_egraph.merge(n, ante, to_ptr(lit));
|
||||
break;
|
||||
case l_undef:
|
||||
case l_false:
|
||||
s().assign(lit, sat::justification::mk_ext_justification(lvl, cnstr));
|
||||
break;
|
||||
|
||||
void solver::propagate_literal(enode* n, enode* ante) {
|
||||
expr* e = n->get_expr();
|
||||
expr* a = nullptr, *b = nullptr;
|
||||
bool_var v = n->bool_var();
|
||||
if (v == sat::null_bool_var)
|
||||
return;
|
||||
SASSERT(m.is_bool(e));
|
||||
size_t cnstr;
|
||||
literal lit;
|
||||
if (!ante) {
|
||||
VERIFY(m.is_eq(e, a, b));
|
||||
cnstr = eq_constraint().to_index();
|
||||
lit = literal(v, false);
|
||||
}
|
||||
else {
|
||||
//
|
||||
// There are the following three cases for propagation of literals
|
||||
//
|
||||
// 1. n == ante is true from equallity, ante = true/false
|
||||
// 2. n == ante is true from equality, value(ante) != l_undef
|
||||
// 3. value(n) != l_undef, ante = true/false, merge_tf is set on n
|
||||
//
|
||||
lbool val = ante->value();
|
||||
if (val == l_undef) {
|
||||
SASSERT(m.is_value(ante->get_expr()));
|
||||
val = m.is_true(ante->get_expr()) ? l_true : l_false;
|
||||
}
|
||||
auto& c = lit_constraint(ante);
|
||||
cnstr = c.to_index();
|
||||
lit = literal(v, val == l_false);
|
||||
}
|
||||
unsigned lvl = s().scope_lvl();
|
||||
|
||||
CTRACE("euf", s().value(lit) != l_true, tout << lit << " " << s().value(lit) << "@" << lvl << " " << mk_bounded_pp(a, m) << " = " << mk_bounded_pp(b, m) << "\n";);
|
||||
if (s().value(lit) == l_false && m_ackerman && a && b)
|
||||
m_ackerman->cg_conflict_eh(a, b);
|
||||
switch (s().value(lit)) {
|
||||
case l_true:
|
||||
if (n->merge_tf() && !m.is_value(n->get_root()->get_expr()))
|
||||
m_egraph.merge(n, ante, to_ptr(lit));
|
||||
break;
|
||||
case l_undef:
|
||||
case l_false:
|
||||
s().assign(lit, sat::justification::mk_ext_justification(lvl, cnstr));
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -206,7 +206,7 @@ namespace euf {
|
|||
void validate_model(model& mdl);
|
||||
|
||||
// solving
|
||||
void propagate_literals();
|
||||
void propagate_literal(enode* n, enode* ante);
|
||||
void propagate_th_eqs();
|
||||
bool is_self_propagated(th_eq const& e);
|
||||
void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue