fixes to mbqi in the new core based on #6575

src/ast/ast.cpp

@@ -3296,7 +3296,7 @@ proof * ast_manager::mk_redundant_del(expr* e) {
     return mk_clause_trail_elem(nullptr, e, PR_REDUNDANT_DEL);
 }
 
-proof * ast_manager::mk_clause_trail(unsigned n, proof* const* ps) {    
+proof * ast_manager::mk_clause_trail(unsigned n, expr* const* ps) {    
     ptr_buffer<expr> args;
     args.append(n, (expr**) ps);
     return mk_app(basic_family_id, PR_CLAUSE_TRAIL, 0, nullptr, args.size(), args.data());

src/ast/ast.h

@@ -2335,7 +2335,7 @@ public:
     proof * mk_th_assumption_add(proof* pr, expr* e);
     proof * mk_th_lemma_add(proof* pr, expr* e);
     proof * mk_redundant_del(expr* e);
-    proof * mk_clause_trail(unsigned n, proof* const* ps);
+    proof * mk_clause_trail(unsigned n, expr* const* ps);
 
     proof * mk_def_axiom(expr * ax);
     proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs);

src/ast/ast_pp_util.cpp

@@ -43,11 +43,11 @@ void ast_pp_util::display_decls(std::ostream& out) {
     for (unsigned i = m_sorts; i < n; ++i) 
         pp.display_sort_decl(out, coll.get_sorts()[i], seen);
     m_sorts = n;
-    
+
     n = coll.get_num_decls();
     for (unsigned i = m_decls; i < n; ++i) {
         func_decl* f = coll.get_func_decls()[i];
-        if (f->get_family_id() == null_family_id && !m_removed.contains(f)) 
+        if (coll.should_declare(f) && !m_removed.contains(f)) 
             ast_smt2_pp(out, f, m_env) << "\n";
     }
     m_decls = n;
@@ -80,7 +80,7 @@ void ast_pp_util::display_skolem_decls(std::ostream& out) {
     unsigned n = coll.get_num_decls();
     for (unsigned i = m_decls; i < n; ++i) {
         func_decl* f = coll.get_func_decls()[i];
-        if (f->get_family_id() == null_family_id && !m_removed.contains(f) && f->is_skolem()) 
+        if (coll.should_declare(f) && !m_removed.contains(f) && f->is_skolem()) 
             ast_smt2_pp(out, f, m_env) << "\n";
     }
     m_decls = n;    

src/ast/decl_collector.cpp

@@ -24,7 +24,7 @@ Revision History:
 void decl_collector::visit_sort(sort * n) {
     SASSERT(!m_visited.is_marked(n));
     family_id fid = n->get_family_id();
-    if (m().is_uninterp(n))
+    if (m.is_uninterp(n))
         m_sorts.push_back(n);
     else if (fid == m_dt_fid) {
         m_sorts.push_back(n);
@@ -43,7 +43,7 @@ void decl_collector::visit_sort(sort * n) {
 }
 
 bool decl_collector::is_bool(sort * s) {
-    return m().is_bool(s);
+    return m.is_bool(s);
 }
 
 void decl_collector::visit_func(func_decl * n) {
@@ -51,10 +51,10 @@ void decl_collector::visit_func(func_decl * n) {
 
     if (!m_visited.is_marked(n)) {
         family_id fid = n->get_family_id();
-        if (fid == null_family_id) 
+        if (should_declare(n))
             m_decls.push_back(n);
         else if (fid == m_rec_fid) {
-            recfun::util u(m());
+            recfun::util u(m);
             if (u.has_def(n)) {
                 m_rec_decls.push_back(n);
                 m_todo.push_back(u.get_def(n).get_rhs());
@@ -69,12 +69,17 @@ void decl_collector::visit_func(func_decl * n) {
     }
 }
 
+bool decl_collector::should_declare(func_decl* f) const {
+    return f->get_family_id() == null_family_id || m.is_model_value(f);
+}
+
+
 decl_collector::decl_collector(ast_manager & m):
-    m_manager(m),
+    m(m),
     m_trail(m),
     m_dt_util(m),
     m_ar_util(m) {
-    m_basic_fid = m_manager.get_basic_family_id();
+    m_basic_fid = m.get_basic_family_id();
     m_dt_fid = m_dt_util.get_family_id();
     recfun::util rec_util(m);
     m_rec_fid = rec_util.get_family_id();
@@ -83,7 +88,7 @@ decl_collector::decl_collector(ast_manager & m):
 void decl_collector::visit(ast* n) {
     if (m_visited.is_marked(n)) 
         return;
-    datatype_util util(m());
+    datatype_util util(m);
     m_todo.push_back(n);
     while (!m_todo.empty()) {
         n = m_todo.back();

src/ast/decl_collector.h

@@ -26,7 +26,7 @@ Revision History:
 #include "ast/array_decl_plugin.h"
 
 class decl_collector {
-    ast_manager &         m_manager;
+    ast_manager &         m;
     lim_svector<sort*>      m_sorts;
     lim_svector<func_decl*> m_decls;
     lim_svector<func_decl*> m_rec_decls;
@@ -48,10 +48,10 @@ class decl_collector {
     void collect_deps(top_sort<sort>& st);
     void collect_deps(sort* s, sort_set& set);
 
-
 public:
     decl_collector(ast_manager & m);
-    ast_manager & m() { return m_manager; }
+
+    bool should_declare(func_decl* f) const;
 
     void reset() { m_sorts.reset(); m_decls.reset(); m_visited.reset(); m_trail.reset(); }
     void visit_func(func_decl* n);

src/sat/smt/q_mbi.cpp

@@ -357,8 +357,7 @@ namespace q {
                     return expr_ref(m);                    
             }
             else if (!(*p)(*m_model, vars, fmls)) {
-                TRACE("q", tout << "theory projection failed\n");
-                return expr_ref(m);
+                TRACE("q", tout << "theory projection failed - use value\n");
             }
         }
         for (app* v : vars) {

src/smt/smt_clause_proof.cpp

@@ -233,7 +233,7 @@ namespace smt {
         TRACE("context", tout << "get-proof " << ctx.get_fparams().m_clause_proof << "\n";);
         if (!ctx.get_fparams().m_clause_proof) 
             return proof_ref(m);
-        proof_ref_vector ps(m);
+        expr_ref_vector ps(m);
         for (auto& info : m_trail) {
             expr_ref fact = mk_or(info.m_clause);
             proof* pr = info.m_proof;

src/solver/check_sat_result.cpp

@@ -41,8 +41,10 @@ void check_sat_result::set_reason_unknown(event_handler& eh) {
 
 proof* check_sat_result::get_proof() {
     if (!m_log.empty() && !m_proof) {
-        app* last = m_log.back();
-        m_log.push_back(to_app(m.get_fact(last)));
+        SASSERT(is_app(m_log.back()));
+        app* last = to_app(m_log.back());
+        expr* fact = m.get_fact(last);
+        m_log.push_back(fact);
         m_proof = m.mk_clause_trail(m_log.size(), m_log.data());            
     }
     if (m_proof)

src/solver/check_sat_result.h

@@ -40,7 +40,7 @@ Notes:
 class check_sat_result {
 protected:
     ast_manager& m;
-    proof_ref_vector m_log;
+    expr_ref_vector m_log;
     proof_ref        m_proof;
     unsigned    m_ref_count = 0;
     lbool       m_status = l_undef;