wip - adding proof checkers, fixes to quantifier proof certificates

src/cmd_context/extra_cmds/proof_cmds.cpp

@@ -158,10 +158,15 @@ public:
         // then check the simplified VC: phi(t) => psi.
         // in case psi is the literal instantiation, then the clause is a propositional tautology.
         // The VC function is a no-op if the proof hint does not have an associated vc generator.
-        m_checker.vc(proof_hint, clause);
+        expr_ref_vector vc(clause);
+        if (m_checker.vc(proof_hint, clause, vc)) {
+            std::cout << "(verified-" << proof_hint->get_name() << ")\n";
+            add_clause(clause);
+            return;
+        }
         
         m_solver->push();
-        for (expr* lit : clause)
+        for (expr* lit : vc)
             m_solver->assert_expr(m.mk_not(lit));
         lbool is_sat = m_solver->check_sat();
         if (is_sat != l_false) {
@@ -175,7 +180,11 @@ public:
             exit(0);
         }
         m_solver->pop(1);
-        std::cout << "(verified-smt)\n";
+        std::cout << "(verified-smt"; 
+        if (proof_hint) std::cout << " " << mk_pp(proof_hint, m);
+        for (expr* arg : clause)
+            std::cout << " " << mk_pp(arg, m);
+        std::cout << ")\n";
         add_clause(clause);
     }
 

src/sat/smt/CMakeLists.txt

@@ -41,6 +41,7 @@ z3_add_component(sat_smt
     q_solver.cpp
     recfun_solver.cpp
     sat_th.cpp
+    tseitin_proof_checker.cpp
     user_solver.cpp
   COMPONENT_DEPENDENCIES
     sat

src/sat/smt/euf_internalize.cpp

@@ -160,8 +160,13 @@ namespace euf {
             s().set_external(v);
             s().set_eliminated(v, false);
             sat::literal lit2 = literal(v, false);
-            s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
-            s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
+            th_proof_hint* ph1 = nullptr, * ph2 = nullptr;
+            if (use_drat()) {
+                ph1 = mk_smt_hint(symbol("tseitin"), ~lit, lit2);
+                ph2 = mk_smt_hint(symbol("tseitin"), lit, ~lit2);
+            }
+            s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id(), ph1));
+            s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id(), ph2));
             add_aux(~lit, lit2);
             add_aux(lit, ~lit2);
             lit = lit2;
@@ -310,8 +315,8 @@ namespace euf {
                 sat::literal lit_el = mk_literal(eq_el);
                 add_root(~lit_c, lit_th);
                 add_root(lit_c, lit_el);
-                s().add_clause(~lit_c, lit_th, st);
-                s().add_clause(lit_c, lit_el, st);
+                s().add_clause(~lit_c, lit_th, mk_tseitin_status(~lit_c, lit_th));
+                s().add_clause(lit_c, lit_el, mk_tseitin_status(lit_c, lit_el));
             }
         }
         else if (m.is_distinct(e)) {
@@ -329,8 +334,8 @@ namespace euf {
             sat::literal some_eq = si.internalize(fml, m_is_redundant);
             add_root(~dist, ~some_eq);
             add_root(dist, some_eq);
-            s().add_clause(~dist, ~some_eq, st);
-            s().add_clause(dist, some_eq, st);
+            s().add_clause(~dist, ~some_eq, mk_tseitin_status(~dist, ~some_eq));
+            s().add_clause(dist, some_eq, mk_tseitin_status(dist, some_eq));
         }
         else if (m.is_eq(e, th, el) && !m.is_iff(e)) {
             sat::literal lit1 = expr2literal(e);
@@ -341,8 +346,8 @@ namespace euf {
                 sat::literal lit2 = expr2literal(e2);
                 add_root(~lit1, lit2);
                 add_root(lit1, ~lit2);
-                s().add_clause(~lit1, lit2, st);
-                s().add_clause(lit1, ~lit2, st);
+                s().add_clause(~lit1, lit2, mk_tseitin_status(~lit1, lit2));
+                s().add_clause(lit1, ~lit2, mk_tseitin_status(lit1, ~lit2));
             }
         }
     }

src/sat/smt/euf_proof.cpp

@@ -164,7 +164,16 @@ namespace euf {
         return mk_smt_hint(n, nl, lits, ne, m_expr_pairs.data());
     }
 
+    sat::status solver::mk_tseitin_status(sat::literal a, sat::literal b) {
+        sat::literal lits[2] = { a, b };
+        return mk_tseitin_status(2, lits);
+    }
 
+    sat::status solver::mk_tseitin_status(unsigned n, sat::literal const* lits) {
+        th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("tseitin"), n, lits) : nullptr;
+        return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph);        
+    }
+    
     expr* smt_proof_hint::get_hint(euf::solver& s) const {
         ast_manager& m = s.get_manager();
         sort* proof = m.mk_proof_sort();

src/sat/smt/euf_proof_checker.cpp

@@ -22,6 +22,7 @@ Author:
 #include "sat/smt/euf_proof_checker.h"
 #include "sat/smt/arith_proof_checker.h"
 #include "sat/smt/q_proof_checker.h"
+#include "sat/smt/tseitin_proof_checker.h"
 #include <iostream>
 
 namespace euf {
@@ -145,10 +146,7 @@ namespace euf {
                         else 
                             merge(x, y);
                     }
-                    else if (m.is_not(arg, arg))
-                        merge(arg, m.mk_false());
-                    else
-                        merge(arg, m.mk_true());
+                    merge(arg, sign ? m.mk_false() : m.mk_true());
                 }
                 else if (m.is_proof(arg)) {
                     if (!is_app(arg))
@@ -277,6 +275,7 @@ namespace euf {
         add_plugin(alloc(res_proof_checker, m, *this));
         add_plugin(alloc(q::proof_checker, m));
         add_plugin(alloc(smt_proof_checker_plugin, m, symbol("datatype"))); // no-op datatype proof checker
+        add_plugin(alloc(tseitin::proof_checker, m));
     }
 
     proof_checker::~proof_checker() {
@@ -302,10 +301,8 @@ namespace euf {
         proof_checker_plugin* p = nullptr;
         if (!m_map.find(a->get_decl()->get_name(), p))
             return false;
-        if (!p->check(a)) {
-            std::cout << "(missed-hint " << mk_pp(e, m) << ")\n";
-            return false;
-        }
+        if (!p->check(a)) 
+            return false;        
         return true;
     }
 
@@ -319,14 +316,14 @@ namespace euf {
         return r;
     }
 
-    void proof_checker::vc(expr* e, expr_ref_vector& clause) {
+    bool proof_checker::vc(expr* e, expr_ref_vector const& clause, expr_ref_vector& v) {
         SASSERT(is_app(e));
         app* a = to_app(e);
         proof_checker_plugin* p = nullptr;
         if (m_map.find(a->get_name(), p))
-            p->vc(a, clause);
-        else 
-            IF_VERBOSE(0, verbose_stream() << "there is no proof plugin for " << mk_pp(e, m) << "\n");
+            return p->vc(a, clause, v);
+        IF_VERBOSE(0, verbose_stream() << "there is no proof plugin for " << mk_pp(e, m) << "\n");
+        return false;
     }
    
     bool proof_checker::check(expr_ref_vector const& clause1, expr* e, expr_ref_vector & units) {

src/sat/smt/euf_proof_checker.h

@@ -30,7 +30,7 @@ namespace euf {
         virtual bool check(app* jst) = 0;
         virtual expr_ref_vector clause(app* jst) = 0;
         virtual void register_plugins(proof_checker& pc) = 0;
-        virtual void vc(app* jst, expr_ref_vector& clause) { }
+        virtual bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) { return false; }
     };
 
     class proof_checker {
@@ -45,7 +45,7 @@ namespace euf {
         void register_plugin(symbol const& rule, proof_checker_plugin*);
         bool check(expr* jst);
         expr_ref_vector clause(expr* jst);
-        void vc(expr* jst, expr_ref_vector& clause);
+        bool vc(expr* jst, expr_ref_vector const& clause, expr_ref_vector& v);
         bool check(expr_ref_vector const& clause, expr* e, expr_ref_vector& units);
     };
 

src/sat/smt/euf_solver.h

@@ -390,7 +390,7 @@ namespace euf {
             return mk_smt_hint(n, lits.size(), lits.data(), 0, (expr_pair const*) nullptr);            
         }
         smt_proof_hint* mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne, expr_pair const* eqs, unsigned nd = 0, expr_pair const* deqs = nullptr); 
-        smt_proof_hint* mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne, enode_pair const* eqs); 
+        smt_proof_hint* mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne = 0, enode_pair const* eqs = nullptr); 
         smt_proof_hint* mk_smt_hint(symbol const& n, literal lit, unsigned ne, expr_pair const* eqs) { return mk_smt_hint(n, 1, &lit, ne, eqs); }
         smt_proof_hint* mk_smt_hint(symbol const& n, literal lit) { return mk_smt_hint(n, 1, &lit, 0, (expr_pair const*)nullptr); }
         smt_proof_hint* mk_smt_hint(symbol const& n, literal l1, literal l2) { literal ls[2] = {l1,l2}; return mk_smt_hint(n, 2, ls, 0, (expr_pair const*)nullptr); }
@@ -399,6 +399,8 @@ namespace euf {
         smt_proof_hint* mk_smt_prop_hint(symbol const& n, literal lit, expr* a, expr* b) { expr_pair e(a, b); return mk_smt_hint(n, 1, &lit, 0, nullptr, 1, &e); }        
         smt_proof_hint* mk_smt_prop_hint(symbol const& n, literal lit, enode* a, enode* b) { return mk_smt_prop_hint(n, lit, a->get_expr(), b->get_expr()); }
         smt_proof_hint* mk_smt_hint(symbol const& n, enode* a, enode* b) { expr_pair e(a->get_expr(), b->get_expr()); return mk_smt_hint(n, 0, nullptr, 1, &e); }
+        sat::status mk_tseitin_status(sat::literal a, sat::literal b);
+        sat::status mk_tseitin_status(unsigned n, sat::literal const* lits);
 
         scoped_ptr<std::ostream> m_proof_out;
 

src/sat/smt/q_ematch.cpp

@@ -387,7 +387,7 @@ namespace q {
         m_qs.log_instantiation(lits, &j);
         euf::th_proof_hint* ph = nullptr;
         if (ctx.use_drat()) 
-            ph = q_proof_hint::mk(ctx, lits, j.m_clause.size(), j.m_binding);
+            ph = q_proof_hint::mk(ctx, lits, j.m_clause.num_decls(), j.m_binding);
         m_qs.add_clause(lits, ph);               
     }
 

src/sat/smt/q_mbi.cpp

@@ -232,6 +232,7 @@ namespace q {
     }
 
     expr_ref_vector mbqi::extract_binding(quantifier* q) {
+        SASSERT(!ctx.use_drat() || !m_defs.empty());
         if (!m_defs.empty()) {
             expr_safe_replace sub(m);
             for (unsigned i = m_defs.size(); i-- > 0; ) {
@@ -543,6 +544,14 @@ namespace q {
                 body = subst(q_flat->get_expr(), binding);
                 if (is_forall(q))
                     body = ::mk_not(m, body);
+                if (ctx.use_drat()) {
+                    m_defs.reset();
+                    for (unsigned i = 0; i < binding.size(); ++i) {
+                        expr_ref v(qb.vars.get(i), m);
+                        expr_ref t(binding.get(i), m);
+                        m_defs.push_back(mbp::def(v, t));
+                    }
+                }
                 add_instantiation(q, body);
                 ++num_bindings;
             }                

src/sat/smt/q_proof_checker.cpp

@@ -25,27 +25,33 @@ namespace q {
         expr_ref_vector result(m);
         for (expr* arg : *jst) 
             if (!is_bind(arg))
-                result.push_back(arg);
+                result.push_back(mk_not(m, arg));
         return result;
     }
 
     expr_ref_vector proof_checker::binding(app* jst) {
         expr_ref_vector result(m);
         for (expr* arg : *jst) 
-            if (is_bind(arg))
-                result.push_back(to_app(arg)->get_arg(0));
+            if (is_bind(arg)) {
+                result.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
+                break;
+            }
         return result;        
     }
     
-    void proof_checker::vc(app* jst, expr_ref_vector& clause) {
+    bool proof_checker::vc(app* jst, expr_ref_vector const& clause0, expr_ref_vector& v) {
         expr* q = nullptr;
         if (!is_inst(jst))
-            return;
-        SASSERT(clause.size() >= 2);
-        VERIFY(m.is_not(clause.get(0), q) && is_forall(q));
+            return false;
+        auto clause1 = clause(jst);
+        SASSERT(clause1.size() >= 2);
+        VERIFY(m.is_not(clause1.get(0), q) && is_forall(q));
         auto inst = binding(jst);
         expr_ref qi = instantiate(m, to_quantifier(q), inst.begin());
-        clause[0] = m.mk_not(qi);
+        clause1[0] = m.mk_not(qi);
+        v.reset();
+        v.append(clause1);
+        return qi == clause1.get(1);
     }
 
     bool proof_checker::is_inst(expr* jst) {

src/sat/smt/q_proof_checker.h

@@ -53,7 +53,7 @@ namespace q {
             pc.register_plugin(symbol("inst"), this);
         }
 
-        void vc(app* jst, expr_ref_vector& clause) override;
+        bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) override;
         
     };
 

src/sat/smt/q_solver.cpp

@@ -365,6 +365,7 @@ namespace q {
     }
 
     q_proof_hint* q_proof_hint::mk(euf::solver& s, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings) {
+        SASSERT(n > 0);
         auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, lits.size()));
         q_proof_hint* ph = new (mem) q_proof_hint(n, lits.size());
         for (unsigned i = 0; i < n; ++i)
@@ -375,6 +376,7 @@ namespace q {
     }
 
     q_proof_hint* q_proof_hint::mk(euf::solver& s, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings) {
+        SASSERT(n > 0);
         auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, 2));
         q_proof_hint* ph = new (mem) q_proof_hint(n, 2);
         for (unsigned i = 0; i < n; ++i)

src/sat/smt/sat_th.cpp

@@ -144,10 +144,9 @@ namespace euf {
         return is_new;
     }
     
-    bool th_euf_solver::add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps) {
-        SASSERT(ps);
+    bool th_euf_solver::add_clause(sat::literal a, sat::literal b, th_proof_hint const* ph) {
         sat::literal lits[2] = { a, b };
-        return add_clause(2, lits, ps);
+        return add_clause(2, lits, ph);
     }
 
     bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, th_proof_hint const* ps) {
@@ -161,7 +160,7 @@ namespace euf {
     }
 
     bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) {
-        //SASSERT(!ctx.use_drat() || ps); - very far from true, and isn't a requirement
+        SASSERT(!ctx.use_drat() || ps); // - very far from true, and isn't a requirement
         bool was_true = false;
         for (unsigned i = 0; i < n; ++i)       
             was_true |= is_true(lits[i]);

src/sat/smt/tseitin_proof_checker.cpp

@@ -0,0 +1,78 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    tseitin_proof_checker.cpp
+
+Abstract:
+
+    Plugin for checking quantifier instantiations
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-07
+
+
+--*/
+
+#include "sat/smt/tseitin_proof_checker.h"
+
+namespace tseitin {
+
+        
+    expr_ref_vector proof_checker::clause(app* jst) {
+        expr_ref_vector result(m);
+        result.append(jst->get_num_args(), jst->get_args());
+        return result;
+    }
+        
+    bool proof_checker::check(app* jst) {
+        expr* main_expr = nullptr;
+        unsigned max_depth = 0;
+        for (expr* arg : *jst) {
+            if (get_depth(arg) > max_depth) {
+                main_expr = arg;
+                max_depth = get_depth(arg);
+            }
+        }
+        if (!main_expr)
+            return false;
+
+        expr* a;
+        if (m.is_not(main_expr, a)) {
+            for (expr* arg : *jst)
+                if (equiv(a, arg))
+                    return true;
+            
+            if (m.is_and(a))
+                for (expr* arg1 : *to_app(a))
+                    for (expr* arg2 : *jst)
+                        if (equiv(arg1, arg2))
+                            return true;
+            
+            if (m.is_or(a))
+                return false;
+            if (m.is_implies(a))
+                return false;
+            if (m.is_eq(a))
+                return false;
+            if (m.is_ite(a))
+                return false;
+            if (m.is_distinct(a))
+                return false;
+        }
+        return false;
+    }
+
+    bool proof_checker::equiv(expr* a, expr* b) {
+        if (a == b)
+            return true;
+        expr* x, *y, *z, *u;
+        if (m.is_eq(a, x, y) && m.is_eq(b, z, u))
+            return x == u && y == z;
+        return false;
+    }
+
+
+}

src/sat/smt/tseitin_proof_checker.h

@@ -0,0 +1,50 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    tseitin_proof_checker.h
+
+Abstract:
+
+    Plugin for checking quantifier instantiations
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-07
+
+
+--*/
+#pragma once
+
+#include "util/obj_pair_set.h"
+#include "ast/ast_trail.h"
+#include "ast/ast_util.h"
+#include "sat/smt/euf_proof_checker.h"
+#include <iostream>
+
+namespace tseitin {
+
+    class proof_checker : public euf::proof_checker_plugin {
+        ast_manager& m;
+
+        bool equiv(expr* a, expr* b);
+        
+    public:
+        proof_checker(ast_manager& m): 
+            m(m) {
+        }
+
+        ~proof_checker() override {}
+        
+        expr_ref_vector clause(app* jst) override;
+        
+        bool check(app* jst) override;
+
+        void register_plugins(euf::proof_checker& pc) override {
+            pc.register_plugin(symbol("tseitin"), this);
+        }
+        
+    };
+
+}

src/sat/tactic/goal2sat.cpp

@@ -68,15 +68,15 @@ struct goal2sat::imp : public sat::sat_internalizer {
     sat::solver_core &          m_solver;
     atom2bool_var &             m_map;
     dep2asm_map &               m_dep2asm;
-    obj_map<expr, sat::bool_var>* m_expr2var_replay { nullptr };
+    obj_map<expr, sat::bool_var>* m_expr2var_replay = nullptr;
     bool                        m_ite_extra;
     unsigned long long          m_max_memory;
     expr_ref_vector             m_trail;
     func_decl_ref_vector        m_unhandled_funs;
     bool                        m_default_external;
-    bool                        m_euf { false };
-    bool                        m_is_redundant { false };
-    bool                        m_top_level { false };
+    bool                        m_euf = false;
+    bool                        m_is_redundant = false;
+    bool                        m_top_level = false;
     sat::literal_vector         aig_lits;
     
     imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
@@ -108,8 +108,24 @@ struct goal2sat::imp : public sat::sat_internalizer {
         throw tactic_exception(std::move(s0));
     }
 
-    sat::status mk_status() const {
-        return sat::status::th(m_is_redundant, m.get_basic_family_id());
+    symbol m_tseitin = symbol("tseitin");
+
+    euf::th_proof_hint* mk_tseitin(unsigned n, sat::literal const* lits) {
+        if (m_euf && ensure_euf()->use_drat())
+            return ensure_euf()->mk_smt_hint(m_tseitin, n, lits);
+        return nullptr;
+    }
+
+    euf::th_proof_hint* mk_tseitin(sat::literal a, sat::literal b) {
+        if (m_euf && ensure_euf()->use_drat()) {
+            sat::literal lits[2] = { a, b };
+            return ensure_euf()->mk_smt_hint(m_tseitin, 2, lits);
+        }
+        return nullptr;
+    }
+
+    sat::status mk_status(euf::th_proof_hint* ph = nullptr) const {
+        return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph);
     }
 
     bool relevancy_enabled() {
@@ -124,42 +140,42 @@ struct goal2sat::imp : public sat::sat_internalizer {
         mk_clause(1, &l);
     }
 
-    void mk_clause(sat::literal l1, sat::literal l2) {
+    void mk_clause(sat::literal l1, sat::literal l2, euf::th_proof_hint* ph = nullptr) {
         sat::literal lits[2] = { l1, l2 };
-        mk_clause(2, lits);
+        mk_clause(2, lits, ph);
     }
 
-    void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
+    void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3, euf::th_proof_hint* ph = nullptr) {
         sat::literal lits[3] = { l1, l2, l3 };
-        mk_clause(3, lits);
+        mk_clause(3, lits, ph);
     }
 
-    void mk_clause(unsigned n, sat::literal * lits) {
+    void mk_clause(unsigned n, sat::literal * lits, euf::th_proof_hint* ph = nullptr) {
         TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
         if (relevancy_enabled())
             ensure_euf()->add_aux(n, lits);
-        m_solver.add_clause(n, lits, mk_status());
+        m_solver.add_clause(n, lits, mk_status(ph));
     }
 
     void mk_root_clause(sat::literal l) {
         mk_root_clause(1, &l);
     }
 
-    void mk_root_clause(sat::literal l1, sat::literal l2) {
+    void mk_root_clause(sat::literal l1, sat::literal l2, euf::th_proof_hint* ph = nullptr) {
         sat::literal lits[2] = { l1, l2 };
-        mk_root_clause(2, lits);
+        mk_root_clause(2, lits, ph);
     }
 
-    void mk_root_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
+    void mk_root_clause(sat::literal l1, sat::literal l2, sat::literal l3, euf::th_proof_hint* ph = nullptr) {
         sat::literal lits[3] = { l1, l2, l3 };
-        mk_root_clause(3, lits);
+        mk_root_clause(3, lits, ph);
     }
 
-    void mk_root_clause(unsigned n, sat::literal * lits) {
+    void mk_root_clause(unsigned n, sat::literal * lits, euf::th_proof_hint* ph = nullptr) {
         TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
         if (relevancy_enabled())
             ensure_euf()->add_root(n, lits);
-        m_solver.add_clause(n, lits, m_is_redundant ? mk_status() : sat::status::input());
+        m_solver.add_clause(n, lits, m_is_redundant ? mk_status(ph) : sat::status::input());
     }
 
     sat::bool_var add_var(bool is_ext, expr* n) {