fix pbge and reduce_tr

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

src/ast/rewriter/pb_rewriter.cpp

@@ -296,8 +296,7 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
                     slack -= c;
                     k -= c;
                 }
-                else if (c >= k) {
+                else if (c >= k && k.is_pos()) {
-                    slack -= c;
                     disj.push_back(m_args[i]);
                 }
                 else {
@@ -309,7 +308,7 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
             m_args.shrink(j);
             m_coeffs.shrink(j);
             sz = j;
-            if (k.is_pos() && sz > 0 && slack >= k) {
+            if (sz > 0) {
                 disj.push_back(m_util.mk_ge(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k));
             }
             if (!disj.empty()) {

src/sat/sat_big.cpp

@@ -165,9 +165,11 @@ namespace sat {
     }
 
     unsigned big::reduce_tr(solver& s) {
+
         unsigned num_lits = s.num_vars() * 2;
         unsigned idx = 0;
         unsigned elim = 0;
+        m_del_bin.reset();
         for (watch_list & wlist : s.m_watches) {
             if (s.inconsistent()) break;
             literal u = to_literal(idx++);
@@ -178,8 +180,9 @@ namespace sat {
                 watched& w = *it;
                 if (learned() ? w.is_binary_learned_clause() : w.is_binary_clause()) {
                     literal v = w.get_literal();
-                    if (reaches(u, v) && u != get_parent(v)) {
+                    if (u != get_parent(v) && safe_reach(u, v)) {
                         ++elim;
+                        m_del_bin.push_back(std::make_pair(~u, v));
                         if (find_binary_watch(wlist, ~v)) {
                             IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n");
                             s.assign(~u, justification());
@@ -193,11 +196,33 @@ namespace sat {
                 itprev++;
             }
             wlist.set_end(itprev);
-        }
+        }        
         s.propagate(false);
         return elim;
     }
 
+    bool big::safe_reach(literal u, literal v) {
+        if (!reaches(u, v)) return false;
+        while (u != v) {
+            literal w = next(u, v);
+            if (m_del_bin.contains(std::make_pair(~u, w)) ||
+                m_del_bin.contains(std::make_pair(~w, u))) {
+                return false;
+            }
+            u = w;
+        }
+        return true;
+    }
+
+    literal big::next(literal u, literal v) const {
+        SASSERT(reaches(u, v));
+        for (literal w : m_dag[u.index()]) {
+            if (reaches(u, w) && (w == v || reaches(w, v))) return w;
+        }
+        UNREACHABLE();
+        return null_literal;
+    }
+
     void big::display(std::ostream& out) const {
         unsigned idx = 0;
         for (auto& next : m_dag) {

src/sat/sat_big.h

@@ -36,9 +36,15 @@ namespace sat {
         bool                   m_learned;
         bool                   m_binary;   // is the BIG produced from binary clauses or hyper-binary resolution?
 
+        svector<std::pair<literal, literal>> m_del_bin;
+        
+
         void init_dfs_num();
         struct pframe;
 
+        bool safe_reach(literal u, literal v);
+        literal next(literal u, literal v) const;
+
     public:
 
         big(random_gen& rand);

src/sat/sat_elim_eqs.cpp

@@ -33,17 +33,18 @@ namespace sat {
             return roots[l.var()];
     }
 
-    void elim_eqs::cleanup_bin_watches(literal_vector const & roots) {
+    void elim_eqs::cleanup_bin_watches(literal_vector const & roots) {        
         unsigned l_idx = 0;
+        m_new_bin.reset();
         for (watch_list & wlist : m_solver.m_watches) {
             literal l1 = ~to_literal(l_idx++);
             literal r1 = norm(roots, l1);
-            watch_list::iterator it2    = wlist.begin();
+            watch_list::iterator it     = wlist.begin();
-            watch_list::iterator itprev = it2;
+            watch_list::iterator itprev = it;
-            watch_list::iterator end2   = wlist.end();
+            watch_list::iterator end    = wlist.end();
-            for (; it2 != end2; ++it2) {
+            for (; it != end; ++it) {
-                if (it2->is_binary_clause()) {
+                if (it->is_binary_clause()) {
-                    literal l2 = it2->get_literal();
+                    literal l2 = it->get_literal();
                     literal r2 = norm(roots, l2);
                     if (r1 == r2) {
                         m_solver.assign(r1, justification());
@@ -56,18 +57,33 @@ namespace sat {
                         // consume tautology
                         continue;
                     }
+#if 0
                     if (l1 != r1) {
                         // add half r1 => r2, the other half ~r2 => ~r1 is added when traversing l2 
-                        m_solver.m_watches[(~r1).index()].push_back(watched(r2, it2->is_learned()));
+                        m_solver.m_watches[(~r1).index()].push_back(watched(r2, it->is_learned()));
                         continue;
                     }
-                    it2->set_literal(r2); // keep it
+                    it->set_literal(r2); // keep it.
+#else
+                    if (l1 != r1 || l2 != r2) {
+                        if (r1.index() < r2.index()) {
+                            m_new_bin.push_back(bin(r1, r2, it->is_learned()));
+                        }
+                        continue;
+                    }
+                    // keep it
+#endif
                 }
-                *itprev = *it2;
+                *itprev = *it;
                 itprev++;
             }
             wlist.set_end(itprev);
         }
+
+        for (auto const& b : m_new_bin) {
+            m_solver.mk_bin_clause(b.l1, b.l2, b.learned);
+        }
+        m_new_bin.reset();
     }
 
     void elim_eqs::cleanup_clauses(literal_vector const & roots, clause_vector & cs) {

src/sat/sat_elim_eqs.h

@@ -25,6 +25,12 @@ namespace sat {
     class solver;
     
     class elim_eqs {
+        struct bin {
+            literal l1, l2;
+            bool learned;
+            bin(literal l1, literal l2, bool learned): l1(l1), l2(l2), learned(learned) {}
+        };
+        svector<bin> m_new_bin;
         solver & m_solver;
         void save_elim(literal_vector const & roots, bool_var_vector const & to_elim);
         void cleanup_clauses(literal_vector const & roots, clause_vector & cs);

src/sat/sat_scc.cpp

@@ -222,7 +222,7 @@ namespace sat {
             }
         }
         TRACE("scc", for (unsigned i = 0; i < roots.size(); i++) { tout << i << " -> " << roots[i] << "\n"; }
-              tout << "to_elim: "; for (unsigned i = 0; i < to_elim.size(); i++) tout << to_elim[i] << " "; tout << "\n";);
+              tout << "to_elim: "; for (literal l : to_elim) tout << l << " "; tout << "\n";);
         m_num_elim += to_elim.size();
         elim_eqs eliminator(m_solver);
         eliminator(roots, to_elim);

src/sat/sat_solver.cpp

@@ -1632,7 +1632,6 @@ namespace sat {
 
         IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";);
         if (!check_clauses(m_model)) {
-            UNREACHABLE();
             throw solver_exception("check model failed");
         }
         
@@ -1644,7 +1643,6 @@ namespace sat {
         
         if (!check_clauses(m_model)) {
             IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";);
-            UNREACHABLE();
             throw solver_exception("check model failed");
         }
 
@@ -1652,8 +1650,12 @@ namespace sat {
 
         if (m_clone) {
             IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model (on original set of clauses)\"\n";);
-            if (!m_clone->check_model(m_model))
+            if (!m_clone->check_model(m_model)) {
+                //IF_VERBOSE(0, display(verbose_stream()));
+                //IF_VERBOSE(0, display_watches(verbose_stream()));
+                //IF_VERBOSE(0, m_mc.display(verbose_stream()));
                 throw solver_exception("check model failed (for cloned solver)");
+            }
         }
     }
 
@@ -1683,8 +1685,11 @@ namespace sat {
                     if (!w.is_binary_non_learned_clause())
                         continue;
                     literal l2 = w.get_literal();
+                    if (l.index() > l2.index()) 
+                        continue;
                     if (value_at(l2, m) != l_true) {
-                        IF_VERBOSE(0, verbose_stream() << "failed binary: " << l << " " << l2 << "\n";);
+                        IF_VERBOSE(0, verbose_stream() << "failed binary: " << l << " := " << value_at(l, m) << " " << l2 <<  " := " << value_at(l2, m) << "\n");
+                        IF_VERBOSE(0, verbose_stream() << "elim l1: " << was_eliminated(l.var()) << " elim l2: " << was_eliminated(l2) << "\n");
                         TRACE("sat", m_mc.display(tout << "failed binary: " << l << " " << l2 << "\n"););
                         ok = false;
                     }
@@ -3399,14 +3404,16 @@ namespace sat {
         out.flush();
     }
 
+    void solver::display_watches(std::ostream & out, literal lit) const {
+        sat::display_watch_list(out << lit << ": ", m_cls_allocator, get_wlist(lit)) << "\n";
+    }
 
     void solver::display_watches(std::ostream & out) const {
         unsigned l_idx = 0;
         for (watch_list const& wlist : m_watches) {
             literal l = to_literal(l_idx++);
-            out << l << ": ";
+            if (!wlist.empty()) 
-            sat::display_watch_list(out, m_cls_allocator, wlist);
+                sat::display_watch_list(out << l << ": ", m_cls_allocator, wlist) << "\n";
-            out << "\n";
         }
     }
 

src/sat/sat_solver.h

@@ -625,6 +625,7 @@ namespace sat {
         bool check_invariant() const;
         void display(std::ostream & out) const;
         void display_watches(std::ostream & out) const;
+        void display_watches(std::ostream & out, literal lit) const;
         void display_dimacs(std::ostream & out) const;
         void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const;
         void display_assignment(std::ostream & out) const;