wip - proofs

src/sat/sat_extension.h

@@ -72,7 +72,7 @@ namespace sat {
         extension(symbol const& name, int id): m_id(id), m_name(name) { }
         virtual ~extension() = default;
         int get_id() const { return m_id; }
-        void set_solver(solver* s) { m_solver = s; }        
+        virtual void set_solver(solver* s) { m_solver = s; }        
         solver& s() { return *m_solver; }
         solver const& s() const { return *m_solver; }
         symbol const& name() const { return m_name;  }

src/sat/smt/euf_proof.cpp

@@ -28,7 +28,7 @@ namespace euf {
         }
         if (!m_proof_out && s().get_config().m_drat && 
             (get_config().m_lemmas2console || s().get_config().m_smt_proof.is_non_empty_string())) {
-            TRACE("euf", tout << "init-proof\n");
+            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 (get_config().m_lemmas2console) 
                 get_drat().set_clause_eh(*this);
@@ -284,10 +284,13 @@ namespace euf {
     }
 
     bool solver::visit_clause(std::ostream& out, unsigned n, literal const* lits) {
+        expr_ref k(m);
         for (unsigned i = 0; i < n; ++i) {
             expr* e = bool_var2expr(lits[i].var());
-            if (!e)
+            if (!e) {
-                return false;
+                k = m.mk_const(symbol(lits[i].var()), m.mk_bool_sort());
+                e = k;
+            }
             visit_expr(out, e);
         }
         return true;
@@ -335,8 +338,13 @@ namespace euf {
     }
 
     std::ostream& solver::display_literals(std::ostream& out, unsigned n, literal const* lits) {
+        expr_ref k(m);
         for (unsigned i = 0; i < n; ++i) {
             expr* e = bool_var2expr(lits[i].var());
+            if (!e) {
+                k = m.mk_const(symbol(lits[i].var()), m.mk_bool_sort());
+                e = k;
+            }
             if (lits[i].sign())
                 display_expr(out << " (not ", e) << ")";
             else

src/sat/smt/euf_proof_checker.cpp

@@ -322,7 +322,7 @@ namespace euf {
         proof_checker_plugin* p = nullptr;
         if (m_map.find(a->get_name(), p))
             return p->vc(a, clause, v);
-        IF_VERBOSE(0, verbose_stream() << "there is no proof plugin for " << mk_pp(e, m) << "\n");
+        IF_VERBOSE(10, verbose_stream() << "there is no proof plugin for " << mk_pp(e, m) << "\n");
         return false;
     }
    

src/sat/smt/euf_solver.cpp

@@ -72,6 +72,7 @@ namespace euf {
 
     void solver::updt_params(params_ref const& p) {
         m_config.updt_params(p);
+            use_drat();
     }
 
     /**

src/sat/smt/euf_solver.h

@@ -309,6 +309,7 @@ namespace euf {
         trail_stack& get_trail_stack() { return m_trail; }
 
         void updt_params(params_ref const& p);
+        void set_solver(sat::solver* s) override { m_solver = s; use_drat(); }
         void set_lookahead(sat::lookahead* s) override { m_lookahead = s; }
         void init_search() override;
         double get_reward(literal l, ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;
@@ -371,7 +372,7 @@ namespace euf {
 
 
         // proof
-        bool use_drat() { return s().get_config().m_drat && (init_proof(), true); }
+        bool use_drat() { return m_solver && s().get_config().m_drat && (init_proof(), true); }
         sat::drat& get_drat() { return s().get_drat(); }
 
         void set_tmp_bool_var(sat::bool_var b, expr* e);
@@ -420,6 +421,7 @@ namespace euf {
         expr_ref mk_eq(euf::enode* n1, euf::enode* n2) { return mk_eq(n1->get_expr(), n2->get_expr()); }
         euf::enode* e_internalize(expr* e);
         euf::enode* mk_enode(expr* e, unsigned n, enode* const* args);
+        void set_bool_var2expr(sat::bool_var v, expr* e) { m_bool_var2expr.setx(v, e, nullptr); }
         expr* bool_var2expr(sat::bool_var v) const { return m_bool_var2expr.get(v, nullptr); }
         expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return (e && lit.sign()) ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
         unsigned generation() const { return m_generation; }

src/sat/smt/q_mbi.cpp

@@ -113,6 +113,8 @@ namespace q {
     expr_ref mbqi::replace_model_value(expr* e) {
         auto const& v2r = ctx.values2root();
         euf::enode* r = nullptr;
+        if (m.is_bool(e))
+            return expr_ref(e, m);
         if (v2r.find(e, r))
             return choose_term(r);        
         if (is_app(e) && to_app(e)->get_num_args() > 0) {
@@ -135,7 +137,7 @@ namespace q {
                 r = n;
             }
             else if (n->generation() == gen) {
-                if ((m_qs.random() % ++count) == 0)
+                if ((m_qs.random() % ++count) == 0 && has_quantifiers(n->get_expr()))
                     r = n;
             }
             if (count > m_max_choose_candidates)
@@ -233,7 +235,8 @@ namespace q {
 
     expr_ref_vector mbqi::extract_binding(quantifier* q) {
         SASSERT(!ctx.use_drat() || !m_defs.empty());
-        if (!m_defs.empty()) {
+        if (m_defs.empty())
+            return expr_ref_vector(m);
         expr_safe_replace sub(m);
         for (unsigned i = m_defs.size(); i-- > 0; ) {
             sub(m_defs[i].term);
@@ -248,8 +251,6 @@ namespace q {
         }
         return inst;
     }
-        return expr_ref_vector(m);
-    }
 
 
     void mbqi::add_universe_restriction(q_body& qb) {
@@ -345,7 +346,6 @@ namespace q {
             if (ctx.use_drat()) {
                 if (!p->project(*m_model, vars, fmls, m_defs)) 
                     return expr_ref(m);                    
-                    
             }
             else if (!(*p)(*m_model, vars, fmls)) {
                 TRACE("q", tout << "theory projection failed\n");
@@ -363,7 +363,8 @@ namespace q {
             eqs.push_back(m.mk_eq(v, val));
         }
         rep(fmls);
-        TRACE("q", tout << "generated formulas\n" << fmls << "\ngenerated eqs:\n" << eqs << "\n";);
+        TRACE("q", tout << "generated formulas\n" << fmls << "\ngenerated eqs:\n" << eqs << "\n";
+                    for (auto const& [v,t] : m_defs) tout << v << " := " << t << "\n");
         return mk_and(fmls);
     }
 

src/sat/smt/tseitin_proof_checker.cpp

@@ -31,28 +31,75 @@ namespace tseitin {
         expr* main_expr = nullptr;
         unsigned max_depth = 0;
         for (expr* arg : *jst) {
-            if (get_depth(arg) > max_depth) {
+            unsigned arg_depth = get_depth(arg);
+            if (arg_depth > max_depth) {
                 main_expr = arg;
-                max_depth = get_depth(arg);
+                max_depth = arg_depth;
             }
+            if (arg_depth == max_depth && m.is_not(main_expr)) 
+                main_expr = arg;            
         }
+
         if (!main_expr)
             return false;
 
         expr* a;
+
+        // (or (and a b) (not a) (not b))
+        if (m.is_and(main_expr)) {            
+            scoped_mark sm(*this);
+            for (expr* arg : *jst)
+                if (m.is_not(arg, arg))
+                    mark(arg);
+            for (expr* arg : *to_app(main_expr)) {
+                if (!is_marked(arg))
+                    return false;
+            }
+            return true;
+        }
+
+        // (or (or a b) (not a))
+        if (m.is_or(main_expr)) {            
+            scoped_mark sm(*this);
+            for (expr* arg : *jst)
+                if (m.is_not(arg, arg))
+                    mark(arg);
+            for (expr* arg : *to_app(main_expr)) {
+                if (is_marked(arg))
+                    return true;
+            }
+            return false;
+        }
+        
         if (m.is_not(main_expr, a)) {
+            
+            // (or (not a) a')
             for (expr* arg : *jst)
                 if (equiv(a, arg))
                     return true;
             
-            if (m.is_and(a))
+            // (or (not (and a b)) a)
-                for (expr* arg1 : *to_app(a))
+            if (m.is_and(a)) {
-                    for (expr* arg2 : *jst)
+                scoped_mark sm(*this);
-                        if (equiv(arg1, arg2))
+                for (expr* arg : *jst)
+                    mark(arg);
+                for (expr* arg : *to_app(a))
+                    if (is_marked(arg))
                         return true;              
+            }
             
-            if (m.is_or(a))
+            // (or (not (or a b) a b))
+            if (m.is_or(a)) {
+                scoped_mark sm(*this);
+                for (expr* arg : *jst)
+                    mark(arg);
+                for (expr* arg : *to_app(a))
+                    if (!is_marked(arg))
                         return false;
+                return true;
+            }
+
+#if 0
             if (m.is_implies(a))
                 return false;
             if (m.is_eq(a))
@@ -61,6 +108,7 @@ namespace tseitin {
                 return false;
             if (m.is_distinct(a))
                 return false;
+#endif
         }
         return false;
     }

src/sat/smt/tseitin_proof_checker.h

@@ -28,8 +28,16 @@ namespace tseitin {
     class proof_checker : public euf::proof_checker_plugin {
         ast_manager& m;
 
+        expr_fast_mark1 m_mark;
         bool equiv(expr* a, expr* b);
         
+        void mark(expr* a) { m_mark.mark(a); }
+        bool is_marked(expr* a) { return m_mark.is_marked(a); }
+        struct scoped_mark {
+            proof_checker& pc;
+            scoped_mark(proof_checker& pc): pc(pc) {}
+            ~scoped_mark() { pc.m_mark.reset(); }
+        };
     public:
         proof_checker(ast_manager& m): 
             m(m) {

src/sat/tactic/goal2sat.cpp

@@ -183,6 +183,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (m_expr2var_replay && m_expr2var_replay->find(n, v))
             return v;
         v = m_solver.add_var(is_ext);
+        if (!is_ext && m_euf && ensure_euf()->use_drat())
+            ensure_euf()->set_bool_var2expr(v, n);
         return v;
     }
 
@@ -417,7 +419,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             cache(t, l);
             sat::literal * lits = m_result_stack.end() - num;       
             for (unsigned i = 0; i < num; i++) 
-                mk_clause(~lits[i], l);
+                mk_clause(~lits[i], l, mk_tseitin(~lits[i], l));
                        
             m_result_stack.push_back(~l);
             lits = m_result_stack.end() - num - 1;
@@ -427,7 +429,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             }
             // remark: mk_clause may perform destructive updated to lits.
             // I have to execute it after the binary mk_clause above.
-            mk_clause(num+1, lits);
+            mk_clause(num+1, lits, mk_tseitin(num+1, lits));
             if (aig()) 
                 aig()->add_or(l, num, aig_lits.data());
                         
@@ -470,7 +472,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
             // l => /\ lits
             for (unsigned i = 0; i < num; i++) {
-                mk_clause(~l, lits[i]);
+                mk_clause(~l, lits[i], mk_tseitin(~l, lits[i]));
             }
             // /\ lits => l
             for (unsigned i = 0; i < num; ++i) {
@@ -482,7 +484,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 aig_lits.reset();
                 aig_lits.append(num, lits);
             }
-            mk_clause(num+1, lits);
+            mk_clause(num+1, lits, mk_tseitin(num+1, lits));
             if (aig()) {
                 aig()->add_and(l, num, aig_lits.data());
             }        
@@ -934,6 +936,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
         expr_ref f(m), d_new(m);
         ptr_vector<expr> deps;
         expr_ref_vector  fmls(m);
+        if (m_euf)
+            ensure_euf();
         for (unsigned idx = 0; idx < size; idx++) {
             f = g.form(idx);
             // Add assumptions.