mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

separate hint literals

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-07-20 10:52:58 -07:00
parent e8a38c5482
commit 3479cdc10b
3 changed files with 41 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/euf_proof.cpp
View file

@ -52,7 +52,7 @@ namespace euf {
* We will here leave it to the EUF checker to perform resolution steps.
*/
void solver::log_antecedents(literal l, literal_vector const& r, th_proof_hint* hint) {
TRACE("euf", log_antecedents(tout, l, r););
TRACE("euf", log_antecedents(tout, l, r); tout << mk_pp(hint->get_hint(*this), m) << "\n");
if (!use_drat())
return;
literal_vector lits;
@ -79,7 +79,7 @@ namespace euf {
}
}
eq_proof_hint* solver::mk_hint(symbol const& th, literal conseq, literal_vector const& r) {
eq_proof_hint* solver::mk_hint(symbol const& th, literal conseq) {
if (!use_drat())
return nullptr;
push(value_trail(m_lit_tail));
@ -87,7 +87,7 @@ namespace euf {
push(restore_vector(m_proof_literals));
if (conseq != sat::null_literal)
m_proof_literals.push_back(~conseq);
m_proof_literals.append(r);
m_proof_literals.append(m_hint_lits);
m_lit_head = m_lit_tail;
m_cc_head = m_cc_tail;
m_lit_tail = m_proof_literals.size();

46
src/sat/smt/euf_solver.cpp
View file

@ -227,20 +227,25 @@ namespace euf {
*/
void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) {
bool create_hint = use_drat() && !probing;
m_egraph.begin_explain();
m_explain.reset();
if (use_drat() && !probing) {
if (create_hint) {
push(restore_vector(m_explain_cc));
m_hint_eqs.reset();
m_hint_lits.reset();
}
auto* ext = sat::constraint_base::to_extension(idx);
th_proof_hint* hint = nullptr;
bool has_theory = false;
if (ext == this)
get_antecedents(l, constraint::from_idx(idx), r, probing);
else {
ext->get_antecedents(l, idx, r, probing);
has_theory = true;
}
if (create_hint && ext != this)
ext->get_antecedents(l, idx, m_hint_lits, probing);
for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) {
size_t* e = m_explain[qhead];
if (is_literal(e))
@ -249,24 +254,43 @@ namespace euf {
size_t idx = get_justification(e);
auto* ext = sat::constraint_base::to_extension(idx);
SASSERT(ext != this);
auto& jst = th_explain::from_index(idx);
sat::literal lit = sat::null_literal;
ext->get_antecedents(lit, idx, r, probing);
has_theory = true;
}
if (create_hint) {
if (is_literal(e))
m_hint_lits.push_back(get_literal(e));
else
m_hint_eqs.push_back(th_explain::from_index(get_justification(e)).eq_consequent());
}
}
m_egraph.end_explain();
if (use_drat() && !probing)
hint = mk_hint(has_theory ? m_smt : m_euf, l, r);
m_egraph.end_explain();
unsigned nv = s().num_vars();
expr_ref_vector eqs(m);
if (create_hint) {
// add negated equalities to hint.
for (auto const& [a,b] : m_hint_eqs) {
eqs.push_back(m.mk_eq(a->get_expr(), b->get_expr()));
set_tmp_bool_var(nv, eqs.back());
m_hint_lits.push_back(literal(nv, false));
++nv;
}
hint = mk_hint(m_euf, l);
}
unsigned j = 0;
for (sat::literal lit : r)
if (s().lvl(lit) > 0) r[j++] = lit;
r.shrink(j);
CTRACE("euf", probing, tout << "explain " << l << " <- " << r << "\n");
CTRACE("euf", create_hint, tout << "explain " << l << " <- " << m_hint_lits << "\n");
DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true););
if (!probing)
log_antecedents(l, r, hint);
for (unsigned v = s().num_vars(); v < nv; ++v)
set_tmp_bool_var(v, nullptr);
}
void solver::get_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing) {
@ -307,7 +331,7 @@ namespace euf {
init_ackerman();
if (!probing && use_drat())
cc = &m_explain_cc;
switch (j.kind()) {
case constraint::kind_t::conflict:
SASSERT(m_egraph.inconsistent());
@ -333,8 +357,8 @@ namespace euf {
bool_var v = ante->bool_var();
lbool val = ante->value();
SASSERT(val != l_undef);
literal ante(v, val == l_false);
m_explain.push_back(to_ptr(ante));
literal ante_lit(v, val == l_false);
m_explain.push_back(to_ptr(ante_lit));
}
break;
}
@ -510,7 +534,7 @@ namespace euf {
bool solver::is_self_propagated(th_eq const& e) {
if (!e.is_eq())
return false;
m_egraph.begin_explain();
m_explain.reset();
m_egraph.explain_eq<size_t>(m_explain, nullptr, e.child(), e.root());

4
src/sat/smt/euf_solver.h
View file

@ -147,6 +147,8 @@ namespace euf {
ptr_vector<expr> m_bool_var2expr;
ptr_vector<size_t> m_explain;
euf::cc_justification m_explain_cc;
enode_pair_vector m_hint_eqs;
sat::literal_vector m_hint_lits;
unsigned m_num_scopes = 0;
unsigned_vector m_var_trail;
svector<scope> m_scopes;
@ -228,7 +230,7 @@ namespace euf {
void log_justification(literal l, th_explain const& jst);
eq_proof_hint* mk_hint(symbol const& th, literal lit, literal_vector const& r);
eq_proof_hint* mk_hint(symbol const& th, literal lit);