diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h index e1e31b199..aedb0bc4c 100644 --- a/src/sat/smt/q_clause.h +++ b/src/sat/smt/q_clause.h @@ -125,12 +125,13 @@ namespace q { struct justification { expr* m_lhs, * m_rhs; bool m_sign; + unsigned m_generation; unsigned m_num_ex; size_t** m_explain; clause& m_clause; euf::enode* const* m_binding; - justification(lit const& l, clause& c, euf::enode* const* b, unsigned n, size_t** ev) : - m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_num_ex(n), m_explain(ev), m_clause(c), m_binding(b) {} + justification(lit const& l, clause& c, euf::enode* const* b, unsigned generation, unsigned n, size_t** ev) : + m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_generation(generation), m_num_ex(n), m_explain(ev), m_clause(c), m_binding(b) {} sat::ext_constraint_idx to_index() const { return sat::constraint_base::mem2base(this); } diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 2c5ab80ae..9335c576b 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -104,7 +104,7 @@ namespace q { * is created to ensure the justification trail is well-founded * during conflict resolution. */ - sat::ext_justification_idx ematch::mk_justification(unsigned idx, clause& c, euf::enode* const* b) { + sat::ext_justification_idx ematch::mk_justification(unsigned idx, unsigned generation, clause& c, euf::enode* const* b) { void* mem = ctx.get_region().allocate(justification::get_obj_size()); sat::constraint_base::initialize(mem, &m_qs); bool sign = false; @@ -129,7 +129,7 @@ namespace q { size_t** ev = static_cast(ctx.get_region().allocate(sizeof(size_t*) * m_explain.size())); for (unsigned i = m_explain.size(); i-- > 0; ) ev[i] = m_explain[i]; - auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b, m_explain.size(), ev); + auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b, generation, m_explain.size(), ev); return constraint->to_index(); } @@ -363,7 +363,7 @@ namespace q { if (!is_owned) binding = copy_nodes(c, binding); - auto j_idx = mk_justification(idx, c, binding); + auto j_idx = mk_justification(idx, max_generation, c, binding); if (is_owned) propagate(ev == l_false, idx, j_idx); @@ -387,7 +387,7 @@ namespace q { m_qs.log_instantiation(lits, &j); euf::th_proof_hint* ph = nullptr; if (ctx.use_drat()) - ph = q_proof_hint::mk(ctx, lits, j.m_clause.num_decls(), j.m_binding); + ph = q_proof_hint::mk(ctx, j.m_generation, lits, j.m_clause.num_decls(), j.m_binding); m_qs.add_clause(lits, ph); } @@ -414,7 +414,7 @@ namespace q { void ematch::add_instantiation(clause& c, binding& b, sat::literal lit) { m_evidence.reset(); - ctx.propagate(lit, mk_justification(UINT_MAX, c, b.nodes())); + ctx.propagate(lit, mk_justification(UINT_MAX, b.m_max_generation, c, b.nodes())); m_qs.log_instantiation(~c.m_literal, lit); } diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h index 834c8740d..c04107b3b 100644 --- a/src/sat/smt/q_ematch.h +++ b/src/sat/smt/q_ematch.h @@ -97,7 +97,7 @@ namespace q { ptr_vector m_explain; euf::cc_justification m_explain_cc; - sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b); + sat::ext_justification_idx mk_justification(unsigned idx, unsigned generation, clause& c, euf::enode* const* b); void ensure_ground_enodes(expr* e); void ensure_ground_enodes(clause const& c); diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index cda05ee28..2c9b87c13 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -71,7 +71,7 @@ namespace q { for (auto const& [qlit, fml, inst, generation] : m_instantiations) { euf::solver::scoped_generation sg(ctx, generation + 1); sat::literal lit = ~ctx.mk_literal(fml); - auto* ph = ctx.use_drat()? q_proof_hint::mk(ctx, ~qlit, lit, inst.size(), inst.data()) : nullptr; + auto* ph = ctx.use_drat()? q_proof_hint::mk(ctx, generation, ~qlit, lit, inst.size(), inst.data()) : nullptr; m_qs.add_clause(~qlit, lit, ph); m_qs.log_instantiation(~qlit, lit); } diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index a94008074..ae37b7f07 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -364,10 +364,10 @@ namespace q { } } - q_proof_hint* q_proof_hint::mk(euf::solver& s, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings) { + q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned generation, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings) { SASSERT(n > 0); auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, lits.size())); - q_proof_hint* ph = new (mem) q_proof_hint(n, lits.size()); + q_proof_hint* ph = new (mem) q_proof_hint(generation, n, lits.size()); for (unsigned i = 0; i < n; ++i) ph->m_bindings[i] = bindings[i]->get_expr(); for (unsigned i = 0; i < lits.size(); ++i) @@ -375,10 +375,10 @@ namespace q { return ph; } - q_proof_hint* q_proof_hint::mk(euf::solver& s, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings) { + q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned generation, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings) { SASSERT(n > 0); auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, 2)); - q_proof_hint* ph = new (mem) q_proof_hint(n, 2); + q_proof_hint* ph = new (mem) q_proof_hint(generation, n, 2); for (unsigned i = 0; i < n; ++i) ph->m_bindings[i] = bindings[i]; ph->m_literals[0] = l1; @@ -390,6 +390,9 @@ namespace q { ast_manager& m = s.get_manager(); expr_ref_vector args(m); expr_ref binding(m); + arith_util a(m); + expr_ref gen(a.mk_int(m_generation), m); + expr* gens[1] = { gen.get() }; sort* range = m.mk_proof_sort(); for (unsigned i = 0; i < m_num_bindings; ++i) args.push_back(m_bindings[i]); @@ -398,6 +401,7 @@ namespace q { for (unsigned i = 0; i < m_num_literals; ++i) args.push_back(s.literal2expr(~m_literals[i])); args.push_back(binding); + args.push_back(m.mk_app(symbol("gen"), 1, gens, range)); return m.mk_app(symbol("inst"), args.size(), args.data(), range); } diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index 3a95a00be..153cdc774 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -30,19 +30,21 @@ namespace euf { namespace q { struct q_proof_hint : public euf::th_proof_hint { + unsigned m_generation; unsigned m_num_bindings; unsigned m_num_literals; sat::literal* m_literals; expr* m_bindings[0]; - q_proof_hint(unsigned b, unsigned l) { + q_proof_hint(unsigned g, unsigned b, unsigned l) { + m_generation = g; m_num_bindings = b; m_num_literals = l; m_literals = reinterpret_cast(m_bindings + m_num_bindings); } static size_t get_obj_size(unsigned num_bindings, unsigned num_lits) { return sizeof(q_proof_hint) + num_bindings*sizeof(expr*) + num_lits*sizeof(sat::literal); } - static q_proof_hint* mk(euf::solver& s, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings); - static q_proof_hint* mk(euf::solver& s, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings); + static q_proof_hint* mk(euf::solver& s, unsigned generation, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings); + static q_proof_hint* mk(euf::solver& s, unsigned generation, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings); expr* get_hint(euf::solver& s) const override; }; diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index a1402839d..b3e8429b4 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -306,11 +306,15 @@ namespace smt { } else if (m_context.on_clause_active()) { expr_ref_vector bindings_e(m), args(m); + arith_util a(m); + expr_ref gen(a.mk_int(generation), m); + expr* gens[1] = { gen.get() }; for (unsigned i = 0; i < num_bindings; ++i) bindings_e.push_back(bindings[i]->get_expr()); args.push_back(m.mk_not(q)); args.push_back(instance); args.push_back(m.mk_app(symbol("bind"), num_bindings, bindings_e.data(), m.mk_proof_sort())); + args.push_back(m.mk_app(symbol("gen"), 1, gens, m.mk_proof_sort())); pr1 = m.mk_app(symbol("inst"), args.size(), args.data(), m.mk_proof_sort()); m_instances.push_back(pr1); }