diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 669347d68..9f716d071 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -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); diff --git a/src/sat/smt/q_mbi.h b/src/sat/smt/q_mbi.h index c7dc4a551..2cc5655bf 100644 --- a/src/sat/smt/q_mbi.h +++ b/src/sat/smt/q_mbi.h @@ -66,15 +66,17 @@ namespace q { scoped_ptr_vector> m_values; scoped_ptr_vector m_plugins; obj_map 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 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 instantiation_t; vector m_instantiations; + vector m_defs; + expr_ref_vector extract_binding(quantifier* q); void restrict_to_universe(expr * sk, ptr_vector const & universe); // void register_value(expr* e); expr_ref replace_model_value(expr* e); diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 565b2536b..0a8ca5085 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -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(); diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index e34da020d..ee2e47111 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -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; };