mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
track instantiations from MBQI in proof logging for new solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d3e6ba9f98
commit
ac5b190a72
|
@ -68,11 +68,21 @@ namespace q {
|
|||
}
|
||||
}
|
||||
m_max_cex += ctx.get_config().m_mbqi_max_cexs;
|
||||
for (auto const& [qlit, fml, generation] : m_instantiations) {
|
||||
for (auto const& [qlit, fml, inst, generation] : m_instantiations) {
|
||||
euf::solver::scoped_generation sg(ctx, generation + 1);
|
||||
sat::literal lit = ctx.mk_literal(fml);
|
||||
euf::th_proof_hint* ph = nullptr;
|
||||
if (!inst.empty()) {
|
||||
ph = q_proof_hint::mk(ctx, inst.size(), inst.data());
|
||||
sat::literal_vector lits;
|
||||
lits.push_back(~qlit);
|
||||
lits.push_back(~lit);
|
||||
m_qs.add_clause(lits, ph);
|
||||
}
|
||||
else {
|
||||
m_qs.add_clause(~qlit, ~lit);
|
||||
}
|
||||
m_qs.log_instantiation(~qlit, ~lit);
|
||||
m_qs.add_clause(~qlit, ~lit);
|
||||
}
|
||||
m_instantiations.reset();
|
||||
if (result != l_true)
|
||||
|
@ -224,10 +234,31 @@ namespace q {
|
|||
TRACE("q", tout << "project: " << proj << "\n";);
|
||||
IF_VERBOSE(11, verbose_stream() << "mbi:\n" << mk_pp(q, m) << "\n" << proj << "\n");
|
||||
++m_stats.m_num_instantiations;
|
||||
unsigned generation = ctx.get_max_generation(proj);
|
||||
m_instantiations.push_back(instantiation_t(qlit, proj, generation));
|
||||
unsigned generation = ctx.get_max_generation(proj);
|
||||
expr_ref_vector inst = extract_binding(q);
|
||||
m_instantiations.push_back(instantiation_t(qlit, proj, inst, generation));
|
||||
}
|
||||
|
||||
expr_ref_vector mbqi::extract_binding(quantifier* q) {
|
||||
if (!m_defs.empty()) {
|
||||
expr_safe_replace sub(m);
|
||||
for (unsigned i = m_defs.size(); i-- > 0; ) {
|
||||
sub(m_defs[i].term);
|
||||
sub.insert(m_defs[i].var, m_defs[i].term);
|
||||
}
|
||||
q_body* qb = q2body(q);
|
||||
expr_ref_vector inst(m);
|
||||
for (expr* v : qb->vars) {
|
||||
expr_ref t(m);
|
||||
sub(v, t);
|
||||
inst.push_back(t);
|
||||
}
|
||||
return inst;
|
||||
}
|
||||
return expr_ref_vector(m);
|
||||
}
|
||||
|
||||
|
||||
void mbqi::add_universe_restriction(q_body& qb) {
|
||||
for (app* v : qb.vars) {
|
||||
sort* s = v->get_sort();
|
||||
|
@ -284,6 +315,7 @@ namespace q {
|
|||
expr_ref_vector fmls(qb.vbody);
|
||||
app_ref_vector vars(qb.vars);
|
||||
bool fmls_extracted = false;
|
||||
m_defs.reset();
|
||||
TRACE("q",
|
||||
tout << "Project\n";
|
||||
tout << fmls << "\n";
|
||||
|
@ -314,16 +346,22 @@ namespace q {
|
|||
fmls_extracted = true;
|
||||
}
|
||||
if (!p)
|
||||
continue;
|
||||
if (!(*p)(*m_model, vars, fmls))
|
||||
return expr_ref(nullptr, m);
|
||||
continue;
|
||||
if (ctx.use_drat()) {
|
||||
if (!p->project(*m_model, vars, fmls, m_defs))
|
||||
return expr_ref(m);
|
||||
}
|
||||
else if (!(*p)(*m_model, vars, fmls))
|
||||
return expr_ref(m);
|
||||
}
|
||||
for (app* v : vars) {
|
||||
expr_ref term(m);
|
||||
expr_ref val = (*m_model)(v);
|
||||
val = m_model->unfold_as_array(val);
|
||||
term = replace_model_value(val);
|
||||
rep.insert(v, term);
|
||||
rep.insert(v, term);
|
||||
if (ctx.use_drat())
|
||||
m_defs.push_back(mbp::def(expr_ref(v, m), term));
|
||||
eqs.push_back(m.mk_eq(v, val));
|
||||
}
|
||||
rep(fmls);
|
||||
|
|
|
@ -66,15 +66,17 @@ namespace q {
|
|||
scoped_ptr_vector<obj_hashtable<expr>> m_values;
|
||||
scoped_ptr_vector<mbp::project_plugin> m_plugins;
|
||||
obj_map<quantifier, q_body*> m_q2body;
|
||||
unsigned m_max_cex{ 1 };
|
||||
unsigned m_max_quick_check_rounds { 100 };
|
||||
unsigned m_max_unbounded_equalities { 10 };
|
||||
unsigned m_max_choose_candidates { 10 };
|
||||
unsigned m_generation_bound{ UINT_MAX };
|
||||
unsigned m_generation_max { UINT_MAX };
|
||||
typedef std::tuple<sat::literal, expr_ref, unsigned> instantiation_t;
|
||||
unsigned m_max_cex = 1;
|
||||
unsigned m_max_quick_check_rounds = 100;
|
||||
unsigned m_max_unbounded_equalities = 10;
|
||||
unsigned m_max_choose_candidates = 10;
|
||||
unsigned m_generation_bound = UINT_MAX;
|
||||
unsigned m_generation_max = UINT_MAX;
|
||||
typedef std::tuple<sat::literal, expr_ref, expr_ref_vector, unsigned> instantiation_t;
|
||||
vector<instantiation_t> m_instantiations;
|
||||
vector<mbp::def> m_defs;
|
||||
|
||||
expr_ref_vector extract_binding(quantifier* q);
|
||||
void restrict_to_universe(expr * sk, ptr_vector<expr> const & universe);
|
||||
// void register_value(expr* e);
|
||||
expr_ref replace_model_value(expr* e);
|
||||
|
|
|
@ -365,6 +365,15 @@ namespace q {
|
|||
}
|
||||
|
||||
q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned n, euf::enode* const* bindings) {
|
||||
auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n));
|
||||
q_proof_hint* ph = new (mem) q_proof_hint();
|
||||
ph->m_num_bindings = n;
|
||||
for (unsigned i = 0; i < n; ++i)
|
||||
ph->m_bindings[i] = bindings[i]->get_expr();
|
||||
return ph;
|
||||
}
|
||||
|
||||
q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned n, expr* const* bindings) {
|
||||
auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n));
|
||||
q_proof_hint* ph = new (mem) q_proof_hint();
|
||||
ph->m_num_bindings = n;
|
||||
|
@ -372,13 +381,13 @@ namespace q {
|
|||
ph->m_bindings[i] = bindings[i];
|
||||
return ph;
|
||||
}
|
||||
|
||||
|
||||
expr* q_proof_hint::get_hint(euf::solver& s) const {
|
||||
ast_manager& m = s.get_manager();
|
||||
expr_ref_vector args(m);
|
||||
sort_ref_vector sorts(m);
|
||||
for (unsigned i = 0; i < m_num_bindings; ++i) {
|
||||
args.push_back(m_bindings[i]->get_expr());
|
||||
args.push_back(m_bindings[i]);
|
||||
sorts.push_back(args.back()->get_sort());
|
||||
}
|
||||
sort* range = m.mk_proof_sort();
|
||||
|
|
|
@ -31,10 +31,11 @@ namespace q {
|
|||
|
||||
struct q_proof_hint : public euf::th_proof_hint {
|
||||
unsigned m_num_bindings;
|
||||
euf::enode* m_bindings[0];
|
||||
expr* m_bindings[0];
|
||||
q_proof_hint() {}
|
||||
static size_t get_obj_size(unsigned num_bindings) { return sizeof(q_proof_hint) + num_bindings*sizeof(euf::enode*); }
|
||||
static size_t get_obj_size(unsigned num_bindings) { return sizeof(q_proof_hint) + num_bindings*sizeof(expr*); }
|
||||
static q_proof_hint* mk(euf::solver& s, unsigned n, euf::enode* const* bindings);
|
||||
static q_proof_hint* mk(euf::solver& s, unsigned n, expr* const* bindings);
|
||||
expr* get_hint(euf::solver& s) const override;
|
||||
};
|
||||
|
||||
|
|
Loading…
Reference in a new issue