tuning and fixing drat checker

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

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -49,7 +49,7 @@ struct pb2bv_rewriter::imp {
         expr_ref_vector m_args;
         rational     m_k;
         vector<rational> m_coeffs;
-        bool m_enable_card;
+        bool m_keep_cardinality_constraints;
 
         template<lbool is_le>
         expr_ref mk_le_ge(expr_ref_vector& fmls, expr* a, expr* b, expr* bound) {
@@ -240,7 +240,7 @@ struct pb2bv_rewriter::imp {
             bv(m),
             m_trail(m),
             m_args(m),
-            m_enable_card(false)
+            m_keep_cardinality_constraints(true)
         {}
 
         bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
@@ -354,27 +354,27 @@ struct pb2bv_rewriter::imp {
         bool mk_pb(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
             SASSERT(f->get_family_id() == pb.get_family_id());
             if (is_or(f)) {
-                if (m_enable_card) return false;
+                if (m_keep_cardinality_constraints) return false;
                 result = m.mk_or(sz, args);
             }
             else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) {
-                if (m_enable_card) return false;
+                if (m_keep_cardinality_constraints) return false;
                 result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args);
             }
             else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) {
-                if (m_enable_card) return false;
+                if (m_keep_cardinality_constraints) return false;
                 result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
             }
             else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
-                if (m_enable_card) return false;
+                if (m_keep_cardinality_constraints) return false;
                 result = m_sort.eq(full, pb.get_k(f).get_unsigned(), sz, args);
             }
             else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
-                if (m_enable_card) return false;
+                if (m_keep_cardinality_constraints) return false;
                 result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args);
             }
             else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
-                if (m_enable_card) return false;
+                if (m_keep_cardinality_constraints) return false;
                 result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
             }
             else {
@@ -406,9 +406,8 @@ struct pb2bv_rewriter::imp {
             m_imp.m_lemmas.push_back(mk_or(m, n, lits));
         }        
 
-        void enable_card(bool f) {
+        void keep_cardinality_constraints(bool f) {
-            m_enable_card = f;
+            m_keep_cardinality_constraints = f;
-            m_enable_card = true;
         }
     };
 
@@ -421,7 +420,7 @@ struct pb2bv_rewriter::imp {
             return m_r.mk_app_core(f, num, args, result);
         }
         card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}
-        void enable_card(bool f) { m_r.enable_card(f); }
+        void keep_cardinality_constraints(bool f) { m_r.keep_cardinality_constraints(f); }
     };
     
     class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
@@ -430,7 +429,7 @@ struct pb2bv_rewriter::imp {
         card_pb_rewriter(imp& i, ast_manager & m):
             rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
             m_cfg(i, m) {}
-        void enable_card(bool f) { m_cfg.enable_card(f); }
+        void keep_cardinality_constraints(bool f) { m_cfg.keep_cardinality_constraints(f); }
     };
 
     card_pb_rewriter m_rw;
@@ -440,13 +439,17 @@ struct pb2bv_rewriter::imp {
         m_fresh(m),
         m_num_translated(0), 
         m_rw(*this, m) {
-        m_rw.enable_card(p.get_bool("cardinality_solver", false));
+        m_rw.keep_cardinality_constraints(p.get_bool("keep_cardinality_constraints", true));
     }
 
     void updt_params(params_ref const & p) {
         m_params.append(p);
-        m_rw.enable_card(m_params.get_bool("cardinality_solver", false));        
+        m_rw.keep_cardinality_constraints(m_params.get_bool("keep_cardinality_constraints", true));
     }
+    void collect_param_descrs(param_descrs& r) const {
+        r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver");
+    }
+
     unsigned get_num_steps() const { return m_rw.get_num_steps(); }
     void cleanup() { m_rw.cleanup(); }
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof) {
@@ -483,6 +486,8 @@ struct pb2bv_rewriter::imp {
 pb2bv_rewriter::pb2bv_rewriter(ast_manager & m, params_ref const& p) {  m_imp = alloc(imp, m, p); }
 pb2bv_rewriter::~pb2bv_rewriter() { dealloc(m_imp); }
 void pb2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
+void pb2bv_rewriter::collect_param_descrs(param_descrs& r) const { m_imp->collect_param_descrs(r); }
+
 ast_manager & pb2bv_rewriter::m() const { return m_imp->m; }
 unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
 void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p);  }

src/ast/rewriter/pb2bv_rewriter.h

@@ -31,6 +31,7 @@ public:
     ~pb2bv_rewriter();
 
     void updt_params(params_ref const & p);
+    void collect_param_descrs(param_descrs& r) const;
     ast_manager & m() const;
     unsigned get_num_steps() const;
     void cleanup();

src/sat/sat_drat.cpp

@@ -38,10 +38,7 @@ namespace sat {
         dealloc(m_out);
         for (unsigned i = 0; i < m_proof.size(); ++i) {
             clause* c = m_proof[i];
-            if (m_status[i] == status::deleted || m_status[i] == status::external) {
+            if (c && (c->size() == 2 || m_status[i] == status::deleted || m_status[i] == status::external)) {
-                s.m_cls_allocator.del_clause(c);
-            }
-            else if (c && c->size() == 2) {
                 s.m_cls_allocator.del_clause(c);
             }
         }
@@ -116,8 +113,10 @@ namespace sat {
             clause* c = s.m_cls_allocator.mk_clause(2, lits, st == status::learned);
             m_proof.push_back(c);
             m_status.push_back(st);
-            m_watches[(~l1).index()].push_back(c);
+            unsigned idx = m_watched_clauses.size();
-            m_watches[(~l2).index()].push_back(c);
+            m_watched_clauses.push_back(watched_clause(c, l1, l2));
+            m_watches[(~l1).index()].push_back(idx);
+            m_watches[(~l2).index()].push_back(idx);
 
             if (value(l1) == l_false && value(l2) == l_false) {
                 m_inconsistent = true;
@@ -146,34 +145,43 @@ namespace sat {
             del_watch(c, c[1]);
             return;
         }
-        literal l1 = null_literal, l2 = null_literal;
+        unsigned num_watch = 0;
+        literal l1, l2;
         for (unsigned i = 0; i < n; ++i) {
             if (value(c[i]) != l_false) {
-                if (l1 == null_literal) {
+                if (num_watch == 0) {
-                    l1 = c[i];                    
+                    l1 = c[i];
+                    ++num_watch;
                 }
                 else {
                     l2 = c[i];
+                    ++num_watch;
                     break;
                 }
             }
         }
-        if (l2 == null_literal && l1 != null_literal) {
+        switch (num_watch) {
-            assign_propagate(l1);
+        case 0: 
+            m_inconsistent = true; 
+            break;
+        case 1: 
+            assign_propagate(l1); 
+            break;
+        default: {
+            SASSERT(num_watch == 2);
+            unsigned idx = m_watched_clauses.size();
+            m_watched_clauses.push_back(watched_clause(&c, l1, l2));
+            m_watches[(~l1).index()].push_back(idx);
+            m_watches[(~l2).index()].push_back(idx);
+            break;
         }
-        else if (l1 == null_literal) {
-            m_inconsistent = true;
-        }
-        else {
-            m_watches[(~l1).index()].push_back(&c);
-            m_watches[(~l2).index()].push_back(&c);
         }
     }
 
     void drat::del_watch(clause& c, literal l) {
         watch& w = m_watches[(~l).index()];      
         for (unsigned i = 0; i < w.size(); ++i) {
-            if (w[i] == &c) {
+            if (m_watched_clauses[w[i]].m_clause == &c) {
                 w[i] = w.back();
                 w.pop_back();
                 break;
@@ -196,6 +204,9 @@ namespace sat {
         for (unsigned i = 0; !m_inconsistent && i < n; ++i) {            
             assign_propagate(~c[i]);
         }
+        if (!m_inconsistent) {
+            TRACE("sat", display(tout););
+        }
         for (unsigned i = num_units; i < m_units.size(); ++i) {
             m_assignment[m_units[i].var()] = l_undef;
         }
@@ -233,36 +244,53 @@ namespace sat {
         else {
             std::cout << "Verification failed\n";
             display(std::cout);
+            TRACE("sat", display(tout); s.display(tout););
+            UNREACHABLE();
             exit(0);
         }
     }
 
     void drat::display(std::ostream& out) const {
         out << "units: " << m_units << "\n";
-#if 0
+#if 1
         for (unsigned i = 0; i < m_assignment.size(); ++i) {
-            lbool v = value(literal(i, false));
+            lbool v = value(literal(i, false));            
-            if (v != l_undef) std::cout << i << ": " << v << "\n";
+            if (v != l_undef) out << i << ": " << v << "\n";
         }
 #endif
         for (unsigned i = 0; i < m_proof.size(); ++i) {
             clause* c = m_proof[i];
             if (m_status[i] != status::deleted && c) {
+                unsigned num_true = 0;
+                unsigned num_undef = 0;
+                for (unsigned j = 0; j < c->size(); ++j) {
+                    switch (value((*c)[j])) {
+                    case l_true: num_true++; break;
+                    case l_undef: num_undef++; break;
+                    default: break;
+                    }
+                }
+                if (num_true == 0 && num_undef == 0) {
+                    out << "False ";
+                }
+                if (num_true == 0 && num_undef == 1) {
+                    out << "Unit ";
+                }
                 out << i << ": " << *c << "\n";
             }
         }
-#if 0
+#if 1
         for (unsigned i = 0; i < m_assignment.size(); ++i) {
             watch const& w1 = m_watches[2*i];
             watch const& w2 = m_watches[2*i + 1];
             if (!w1.empty()) {
                 out << i << " |-> ";
-                for (unsigned i = 0; i < w1.size(); ++i) out << w1[i] << " ";
+                for (unsigned i = 0; i < w1.size(); ++i) out << *(m_watched_clauses[w1[i]].m_clause) << " ";
                 out << "\n";
             }
             if (!w2.empty()) {
                 out << "-" << i << " |-> ";
-                for (unsigned i = 0; i < w2.size(); ++i) out << w2[i] << " ";
+                for (unsigned i = 0; i < w2.size(); ++i) out << *(m_watched_clauses[w2[i]].m_clause) << " ";
                 out << "\n";
             }
         }
@@ -302,41 +330,45 @@ namespace sat {
         watch::iterator it2 = it;
         watch::iterator end = clauses.end();
         for (; it != end; ++it) {
-            clause& c = *(*it);
+            unsigned idx = *it;
-            if (c[0] == ~l) {
+            watched_clause& wc = m_watched_clauses[idx];
-                std::swap(c[0], c[1]);
+            clause& c = *wc.m_clause;
+
+            TRACE("sat", tout << "Propagate " << l << " " << c << " watch: " << wc.m_l1 << " " << wc.m_l2 << "\n";);
+            if (wc.m_l1 == ~l) {
+                std::swap(wc.m_l1, wc.m_l2);
             }
-            if (c[1] != ~l) {
+            if (wc.m_l2 != ~l) {
+                std::cout << wc.m_l1 << " " << wc.m_l2 << " ~l: " << ~l << "\n";
+                std::cout << *wc.m_clause << "\n";
+            }
+            SASSERT(wc.m_l2 == ~l);
+            if (value(wc.m_l1) == l_true) {
                 *it2 = *it;
                 it2++;
-                continue;
-            }
-            SASSERT(c[1] == ~l);
-            if (value(c[0]) == l_true) {
-                it2++;
             }
             else {
-                literal * l_it = c.begin() + 2;
-                literal * l_end = c.end();
                 bool done = false;
-                for (; l_it != l_end && !done; ++l_it) {
+                for (unsigned i = 0; !done && i < c.size(); ++i) {
-                    if (value(*l_it) != l_false) {
+                    literal lit = c[i];
-                        c[1] = *l_it;
+                    if (lit != wc.m_l1 && lit != wc.m_l2 && value(lit) != l_false) {
-                        *l_it = ~l;
+                        wc.m_l2 = lit;
-                        m_watches[(~c[1]).index()].push_back(&c);
+                        m_watches[(~lit).index()].push_back(idx);
                         done = true;
-                    }
+                    } 
                 }
-                if (done) 
+                if (done) {
+                    it2++;
                     continue;                
-                else if (value(c[0]) == l_false) {
+                }
+                else if (value(wc.m_l1) == l_false) {
                     m_inconsistent = true;
                     goto end_process_watch;
                 }
                 else {
                     *it2 = *it;
                     it2++;
-                    assign(c[0]);
+                    assign(wc.m_l1);
                 }
             }
         }

src/sat/sat_drat.h

@@ -36,7 +36,14 @@ namespace sat {
         };
     private:
         enum status { asserted, learned, deleted, external };
-        typedef ptr_vector<clause> watch;
+        struct watched_clause {
+            clause* m_clause;
+            literal m_l1, m_l2;
+            watched_clause(clause* c, literal l1, literal l2):
+                m_clause(c), m_l1(l1), m_l2(l2) {}
+        };
+        svector<watched_clause>   m_watched_clauses;
+        typedef svector<unsigned> watch;
         solver& s;
         std::ostream*           m_out;
         ptr_vector<clause>      m_proof;

src/sat/sat_params.pyg

@@ -23,7 +23,6 @@ def_module_params('sat',
                           ('core.minimize', BOOL, False, 'minimize computed core'),
                           ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
                           ('parallel_threads', UINT, 1, 'number of parallel threads to use'),
-                          ('cardinality_solver', BOOL, False, 'enable cardinality based solver'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
                           ('drat', BOOL, False, 'produce DRAT proofs'),
                           ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),

src/sat/sat_solver.cpp

@@ -718,8 +718,8 @@ namespace sat {
                         assign_core(c[0], justification(cls_off));
 #ifdef UPDATE_GLUE
                         if (update && c.is_learned() && c.glue() > 2) {
-                            unsigned glue = num_diff_levels(c.size(), c.begin());
+                            unsigned glue;
-                            if (glue+1 < c.glue()) {
+                            if (num_diff_levels_below(c.size(), c.begin(), c.glue()-1, glue)) {
                                 c.set_glue(glue);
                             }
                         }
@@ -2142,6 +2142,26 @@ namespace sat {
         return r;
     }
 
+    bool solver::num_diff_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue) {
+        m_diff_levels.reserve(scope_lvl() + 1, false);
+        glue = 0;
+        unsigned i = 0;
+        for (; i < num && glue < max_glue; i++) {
+            SASSERT(value(lits[i]) != l_undef);
+            unsigned lit_lvl = lvl(lits[i]);
+            if (m_diff_levels[lit_lvl] == false) {
+                m_diff_levels[lit_lvl] = true;
+                glue++;
+            }
+        }
+        num = i;
+        // reset m_diff_levels.
+        for (i = 0; i < num; i++)
+            m_diff_levels[lvl(lits[i])] = false;
+        return glue < max_glue;        
+    }
+
+
     /**
        \brief Process an antecedent for lemma minimization.
     */
@@ -2278,11 +2298,14 @@ namespace sat {
         unsigned sz   = m_lemma.size();
         unsigned i    = 1; // the first literal is the FUIP
         unsigned j    = 1;
+        //bool drop = false;
+        //unsigned bound = sz/5+10;
         for (; i < sz; i++) {
             literal l = m_lemma[i];
             if (implied_by_marked(l)) {
                 TRACE("sat", tout << "drop: " << l << "\n";);
                 m_unmark.push_back(l.var());
+                //drop = true;
             }
             else {
                 if (j != i) {
@@ -2290,6 +2313,13 @@ namespace sat {
                 }
                 j++;
             }
+#if 0
+            if (!drop && i >= bound) {
+                // std::cout << "drop\n";
+                j = sz;
+                break;
+            }
+#endif
         }
 
         reset_unmark(0);

src/sat/sat_solver.h

@@ -394,6 +394,7 @@ namespace sat {
         void updt_phase_counters();
         svector<char> m_diff_levels;
         unsigned num_diff_levels(unsigned num, literal const * lits);
+        bool     num_diff_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue);
 
         // lemma minimization
         typedef approx_set_tpl<unsigned, u2u, unsigned> level_approx_set;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -84,7 +84,6 @@ public:
         m_unknown("no reason given") {
         m_params.set_bool("elim_vars", false);
         sat_params p1(m_params);
-        m_params.set_bool("cardinality_solver", p1.cardinality_solver());
         m_solver.updt_params(m_params);
         init_preprocess();
     }
@@ -219,7 +218,6 @@ public:
     virtual void updt_params(params_ref const & p) {
         m_params.append(p);
         sat_params p1(p);
-        m_params.set_bool("cardinality_solver", p1.cardinality_solver());
         m_params.set_bool("elim_vars", false);
         std::cout << m_params << "\n";
         m_solver.updt_params(m_params);

src/tactic/portfolio/pb2bv_solver.cpp

@@ -70,8 +70,8 @@ public:
         return m_solver->check_sat(num_assumptions, assumptions);
     }
 
-    virtual void updt_params(params_ref const & p) { m_solver->updt_params(p);  }
+    virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); m_rewriter.updt_params(p); }
-    virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }    
+    virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); m_rewriter.collect_param_descrs(r); }    
     virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
     virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback);  }
     virtual void collect_statistics(statistics & st) const {