mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

log also quantifier generation (besides binding)

Browse source 
We add also logging for quantifier generation.
It is auxiliary information that is of use for diagnostics (axiom profiler).
This commit is contained in:
Nikolaj Bjorner 2022-10-20 17:49:15 -07:00
parent c1b355f342
commit 842e8057bc
7 changed files with 27 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/q_clause.h
View file

@ -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);
}

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

@ -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<size_t**>(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);
}

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

@ -97,7 +97,7 @@ namespace q {
ptr_vector<size_t> 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);

2
src/sat/smt/q_mbi.cpp
View file

@ -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);
}

12
src/sat/smt/q_solver.cpp
View file

@ -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);
}

8
src/sat/smt/q_solver.h
View file

@ -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<sat::literal*>(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;
};

4
src/smt/qi_queue.cpp
View file

@ -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);
}