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

increment generation for literals created during E-matching

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-01 10:04:33 +09:00
parent f24ecde35c
commit 30c9cda61e
2 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/q_ematch.cpp
View file

@ -383,7 +383,7 @@ namespace q {
sat::literal_vector lits;
lits.push_back(~j.m_clause.m_literal);
for (unsigned i = 0; i < j.m_clause.size(); ++i)
lits.push_back(instantiate(j.m_clause, j.m_binding, j.m_clause[i]));
lits.push_back(instantiate(j.m_clause, j.m_generation, j.m_binding, j.m_clause[i]));
m_qs.log_instantiation(lits, &j);
euf::th_proof_hint* ph = nullptr;
if (ctx.use_drat())
@ -418,11 +418,12 @@ namespace q {
m_qs.log_instantiation(~c.m_literal, lit);
}
sat::literal ematch::instantiate(clause& c, euf::enode* const* binding, lit const& l) {
sat::literal ematch::instantiate(clause& c, unsigned generation, euf::enode* const* binding, lit const& l) {
expr_ref_vector _binding(m);
for (unsigned i = 0; i < c.num_decls(); ++i)
_binding.push_back(binding[i]->get_expr());
var_subst subst(m);
euf::solver::scoped_generation sg(ctx, generation + 1);
auto sub = [&](expr* e) {
expr_ref r = subst(e, _binding);
//ctx.rewrite(r);

2
src/sat/smt/q_ematch.h
View file

@ -103,7 +103,7 @@ namespace q {
void ensure_ground_enodes(clause const& c);
void instantiate(binding& b);
sat::literal instantiate(clause& c, euf::enode* const* binding, lit const& l);
sat::literal instantiate(clause& c, unsigned generation, euf::enode* const* binding, lit const& l);
// register as callback into egraph.
void on_merge(euf::enode* root, euf::enode* other);