wip - proof checking

fixes to smt_theory_checker. Generalize it to apply to arrays and fpa.
Missing: bv

src/sat/smt/euf_proof.cpp

@@ -22,19 +22,22 @@ Author:
 namespace euf {
 
     void solver::init_proof() {
-        if (!m_proof_initialized) {
+        if (m_proof_initialized)
-            get_drat().add_theory(get_id(), symbol("euf"));
+            return;
-            get_drat().add_theory(m.get_basic_family_id(), symbol("bool"));
+
-        }
+        if (s().get_config().m_drat && 
-        if (!m_proof_out && s().get_config().m_drat && 
             (get_config().m_lemmas2console ||
              s().get_config().m_smt_proof_check ||
              s().get_config().m_smt_proof.is_non_empty_string())) {
+
+            get_drat().add_theory(get_id(), symbol("euf"));
+            get_drat().add_theory(m.get_basic_family_id(), symbol("bool"));
             TRACE("euf", tout << "init-proof " << s().get_config().m_smt_proof << "\n");
-            m_proof_out = alloc(std::ofstream, s().get_config().m_smt_proof.str(), std::ios_base::out);
+            if (s().get_config().m_smt_proof.is_non_empty_string())
+                m_proof_out = alloc(std::ofstream, s().get_config().m_smt_proof.str(), std::ios_base::out);
             get_drat().set_clause_eh(*this);
+            m_proof_initialized = true;
         }
-        m_proof_initialized = true;
     }
 
     /**
@@ -133,7 +136,8 @@ namespace euf {
         func_decl_ref cc(m), cc_comm(m);
         sort* proof = m.mk_proof_sort();
         ptr_buffer<sort> sorts;
-        expr_ref_vector args(m);
+        expr_ref_vector& args = s.m_expr_args;
+        args.reset();
         if (m_cc_head < m_cc_tail) {
             sort* sorts[1] = { m.mk_bool_sort() };
             cc_comm = m.mk_func_decl(symbol("comm"), 1, sorts, proof);
@@ -325,16 +329,16 @@ namespace euf {
     void solver::on_check(unsigned n, literal const* lits, sat::status st) {
         if (!s().get_config().m_smt_proof_check)
             return;
-        expr_ref_vector clause(m);
+        m_clause.reset();
         for (unsigned i = 0; i < n; ++i) 
-            clause.push_back(literal2expr(lits[i]));
+            m_clause.push_back(literal2expr(lits[i]));
         auto hint = status2proof_hint(st);
         if (st.is_asserted() || st.is_redundant())
-            m_smt_proof_checker.infer(clause, hint);
+            m_smt_proof_checker.infer(m_clause, hint);
         else if (st.is_deleted())
-            m_smt_proof_checker.del(clause);
+            m_smt_proof_checker.del(m_clause);
         else if (st.is_input())
-            m_smt_proof_checker.assume(clause);
+            m_smt_proof_checker.assume(m_clause);
     }
         
     void solver::on_lemma(unsigned n, literal const* lits, sat::status st) {
@@ -391,7 +395,7 @@ namespace euf {
     void solver::display_inferred(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint) {
         expr_ref hint(proof_hint, m);
         if (!hint)
-            hint = m.mk_const(symbol("smt"), m.mk_proof_sort());
+            hint = m.mk_const(m_smt, m.mk_proof_sort()); 
         visit_expr(out, hint);
         display_hint(display_literals(out << "(infer", n, lits), hint) << ")\n";        
     }

src/sat/smt/euf_proof_checker.cpp

@@ -214,6 +214,7 @@ namespace euf {
 
         void register_plugins(theory_checker& pc) override {
             pc.register_plugin(symbol("euf"), this);
+            pc.register_plugin(symbol("smt"), this);
         }
     };
 
@@ -289,13 +290,11 @@ namespace euf {
         add_plugin(alloc(res_checker, m, *this));
         add_plugin(alloc(q::theory_checker, m));
         add_plugin(alloc(distinct::theory_checker, m));
-        add_plugin(alloc(smt_theory_checker_plugin, m, symbol("datatype"))); // no-op datatype proof checker
+        add_plugin(alloc(smt_theory_checker_plugin, m)); 
         add_plugin(alloc(tseitin::theory_checker, m));
     }
 
     theory_checker::~theory_checker() {
-        for (auto& [k, v] : m_checked_clauses)
-            dealloc(v);
     }
 
     void theory_checker::add_plugin(theory_checker_plugin* p) {
@@ -310,20 +309,14 @@ namespace euf {
     bool theory_checker::check(expr* e) {
         if (!e || !is_app(e))
             return false;
-        if (m_checked_clauses.contains(e))
-            return true;        
         app* a = to_app(e);
         theory_checker_plugin* p = nullptr;
         return m_map.find(a->get_decl()->get_name(), p) && p->check(a);
     }
 
     expr_ref_vector theory_checker::clause(expr* e) {
-        expr_ref_vector* rr;
-        if (m_checked_clauses.find(e, rr))
-            return *rr;
         SASSERT(is_app(e) && m_map.contains(to_app(e)->get_name()));
         expr_ref_vector r = m_map[to_app(e)->get_name()]->clause(to_app(e));
-        m_checked_clauses.insert(e, alloc(expr_ref_vector, r));
         return r;
     }
 
@@ -365,12 +358,16 @@ namespace euf {
 
     expr_ref_vector smt_theory_checker_plugin::clause(app* jst) {
         expr_ref_vector result(m);
-        SASSERT(jst->get_name() == m_rule);
         for (expr* arg : *jst) 
             result.push_back(mk_not(m, arg));
         return result;
     }
 
+    void smt_theory_checker_plugin::register_plugins(theory_checker& pc) {
+        pc.register_plugin(symbol("datatype"), this);
+        pc.register_plugin(symbol("array"), this);
+        pc.register_plugin(symbol("fpa"), this);
+    }
 
     smt_proof_checker::smt_proof_checker(ast_manager& m, params_ref const& p):
         m(m),
@@ -469,6 +466,7 @@ namespace euf {
         lbool is_sat = m_solver->check_sat();
         if (is_sat != l_false) {
             std::cout << "did not verify: " << is_sat << " " << clause << "\n";
+            std::cout << "vc:\n" << vc << "\n";
             if (proof_hint) 
                 std::cout << "hint: " << mk_bounded_pp(proof_hint, m, 4) << "\n";
             m_solver->display(std::cout);
@@ -486,6 +484,7 @@ namespace euf {
         for (expr* arg : clause)
             std::cout << "\n " << mk_bounded_pp(arg, m);
         std::cout << ")\n";
+
         if (is_rup(proof_hint)) 
             diagnose_rup_failure(clause);
             

src/sat/smt/euf_proof_checker.h

@@ -42,7 +42,6 @@ namespace euf {
         ast_manager& m;
         scoped_ptr_vector<theory_checker_plugin> m_plugins;                          // plugins of proof checkers
         map<symbol, theory_checker_plugin*, symbol_hash_proc, symbol_eq_proc> m_map; // symbol table of proof checkers
-        obj_map<expr, expr_ref_vector*> m_checked_clauses;                          // cache of previously checked proofs and their clauses.
         void add_plugin(theory_checker_plugin* p);
     public:
         theory_checker(ast_manager& m);
@@ -62,12 +61,11 @@ namespace euf {
      */
     class smt_theory_checker_plugin : public theory_checker_plugin {
         ast_manager& m;
-        symbol m_rule;
     public:
-        smt_theory_checker_plugin(ast_manager& m, symbol const& n): m(m), m_rule(n) {}
+        smt_theory_checker_plugin(ast_manager& m): m(m) {}
         bool check(app* jst) override { return false; }
         expr_ref_vector clause(app* jst) override;        
-        void register_plugins(theory_checker& pc) override { pc.register_plugin(m_rule, this); }
+        void register_plugins(theory_checker& pc) override;
     };
 
 

src/sat/smt/euf_solver.cpp

@@ -50,6 +50,8 @@ namespace euf {
         m_to_m(&m),
         m_to_si(&si),
         m_values(m),
+        m_clause(m),
+        m_expr_args(m),
         m_clause_visitor(m),
         m_smt_proof_checker(m, p)
     {

src/sat/smt/euf_solver.h

@@ -200,11 +200,14 @@ namespace euf {
 
         typedef std::pair<expr*, expr*> expr_pair;
         literal_vector    m_proof_literals;
-        svector<expr_pair> m_proof_eqs, m_proof_deqs, m_expr_pairs;
+        svector<expr_pair> m_proof_eqs, m_proof_deqs, m_expr_pairs;        
         unsigned m_lit_head = 0, m_lit_tail = 0, m_cc_head = 0, m_cc_tail = 0;
         unsigned m_eq_head = 0, m_eq_tail = 0, m_deq_head = 0, m_deq_tail = 0;
         symbol m_euf = symbol("euf");
         symbol m_smt = symbol("smt");            
+        expr_ref_vector m_clause;
+        expr_ref_vector m_expr_args;
+
         eq_proof_hint* mk_hint(symbol const& th, literal lit, literal_vector const& r);