track instantiations from MBQI in proof logging for new solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

src/sat/smt/q_mbi.h

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

src/sat/smt/q_solver.cpp

@@ -365,20 +365,29 @@ 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;
         for (unsigned i = 0; i < n; ++i)
             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();

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