fix bugs in scc_tr

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

scripts/vsts-mac.sh

@@ -1,19 +0,0 @@
-#!/bin/sh
-
-cd ..
-mkdir build
-CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil CXX=clang++ CC=clang python scripts/mk_make.py  --java --python
-cd build
-make
-make test-z3
-make cpp_example
-make c_example
-# make java_example
-# make python_example
-./cpp_example
-./test_capi
-
-git clone https://github.com/z3prover/z3test.git z3test
-ls
-python z3test/scripts/test_benchmarks.py ./z3 ./z3test/regressions/smt2
-

src/sat/sat_asymm_branch.cpp

@@ -245,14 +245,14 @@ namespace sat {
             m_pos.push_back(l);
             m_neg.push_back(~l);
         }
-#if 1
         compare_left cmp(big);
         std::sort(m_pos.begin(), m_pos.end(), cmp);
         std::sort(m_neg.begin(), m_neg.end(), cmp);
-#else
+
-        radix_sort(big, m_pos);
+        // alternative: worse
-        radix_sort(big, m_neg);
+        // radix_sort(big, m_pos);
-#endif
+        // radix_sort(big, m_neg);
+
         IF_VERBOSE(100, 
                    for (literal l : m_pos) verbose_stream() << big.get_left(l) << " "; 
                    verbose_stream() << "\n";

src/sat/sat_big.cpp

@@ -164,8 +164,19 @@ namespace sat {
         DEBUG_CODE(for (unsigned i = 0; i < num_lits; ++i) { VERIFY(m_left[i] < m_right[i]);});
     }
 
-    unsigned big::reduce_tr(solver& s) {
+    // svector<std::pair<literal, literal>> big::s_del_bin;
 
+    bool big::in_del(literal u, literal v) const {
+        if (u.index() > v.index()) std::swap(u, v);
+        return m_del_bin.contains(std::make_pair(u, v));
+    }
+
+    void big::add_del(literal u, literal v) {
+        if (u.index() > v.index()) std::swap(u, v);
+        m_del_bin.push_back(std::make_pair(u, v));
+    }
+
+    unsigned big::reduce_tr(solver& s) {
         unsigned num_lits = s.num_vars() * 2;
         unsigned idx = 0;
         unsigned elim = 0;
@@ -182,7 +193,8 @@ namespace sat {
                     literal v = w.get_literal();
                     if (u != get_parent(v) && safe_reach(u, v)) {
                         ++elim;
-                        m_del_bin.push_back(std::make_pair(~u, v));
+                        add_del(~u, v);
+                        // IF_VERBOSE(1, verbose_stream() << "remove " << u << " -> " << v << "\n");
                         if (find_binary_watch(wlist, ~v)) {
                             IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n");
                             s.assign(~u, justification());
@@ -197,6 +209,23 @@ namespace sat {
             }
             wlist.set_end(itprev);
         }        
+
+#if 0
+        s_del_bin.append(m_del_bin);
+        IF_VERBOSE(1, 
+                   display(verbose_stream() << "Learned: " << learned() << ":");
+                   verbose_stream() << "del-bin\n";
+                   for (auto p : m_del_bin) {
+                       verbose_stream() << p.first << " " << p.second << "\n";
+                       if (safe_reach(~p.first, p.second)) {
+                           display_path(verbose_stream(), ~p.first, p.second) << " " << "\n";
+                       }
+                       else {
+                           display_path(verbose_stream(), ~p.second, p.first) << " " << "\n";
+                       }                       
+                   }
+                   );
+#endif
         s.propagate(false);
         return elim;
     }
@@ -205,8 +234,7 @@ namespace sat {
         if (!reaches(u, v)) return false;
         while (u != v) {
             literal w = next(u, v);
-            if (m_del_bin.contains(std::make_pair(~u, w)) ||
+            if (in_del(~u, w)) {
-                m_del_bin.contains(std::make_pair(~w, u))) {
                 return false;
             }
             u = w;
@@ -216,11 +244,27 @@ namespace sat {
 
     literal big::next(literal u, literal v) const {
         SASSERT(reaches(u, v));
+        literal result = null_literal;
+        int left = m_right[u.index()];
+        // identify the path from the reachability graph
         for (literal w : m_dag[u.index()]) {
-            if (reaches(u, w) && (w == v || reaches(w, v))) return w;
+            if (reaches(u, w) && 
+                (w == v || reaches(w, v)) &&
+                m_left[w.index()] < left) {
+                left = m_left[w.index()];
+                result = w;
+            }
         }
-        UNREACHABLE();
+        SASSERT(result != null_literal);
-        return null_literal;
+        return result;
+    }
+
+    std::ostream& big::display_path(std::ostream& out, literal u, literal v) const {
+        while (u != v) {
+            out << u << " -> ";
+            u = next(u, v);
+        }
+        return out << v;
     }
 
     void big::display(std::ostream& out) const {
@@ -228,6 +272,12 @@ namespace sat {
         for (auto& next : m_dag) {
             if (!next.empty()) {
                 out << to_literal(idx) << " : " << m_left[idx] << ":" << m_right[idx] << " -> " << next << "\n";
+#if 0
+                for (literal n : next) {
+                    out << n << "[" << m_left[n.index()] << ":" << m_right[n.index()] << "] ";
+                }
+                out << "\n";
+#endif
             }
             ++idx;
         }

src/sat/sat_big.h

@@ -45,8 +45,15 @@ namespace sat {
         bool safe_reach(literal u, literal v);
         literal next(literal u, literal v) const;
 
+        std::ostream& display_path(std::ostream& out, literal u, literal v) const;
+
+        void add_del(literal u, literal v);
+        bool in_del(literal u, literal v) const;
+
     public:
 
+        // static svector<std::pair<literal, literal>> s_del_bin;
+
         big(random_gen& rand);
         /**
            \brief initialize a BIG from a solver.

src/sat/sat_cleaner.cpp

@@ -117,19 +117,13 @@ namespace sat {
             else {
                 unsigned new_sz = j;
                 CTRACE("sat_cleaner_bug", new_sz < 2, tout << "new_sz: " << new_sz << "\n";
-                       if (c.size() > 0) tout << "unit: " << c[0] << "\n";);
+                       if (c.size() > 0) tout << "unit: " << c[0] << "\n";
-                SASSERT(c.frozen() || new_sz >= 2);
+                       s.display_watches(tout););
                 if (new_sz == 0) {
-                    // It can only happen with frozen clauses.
-                    // active clauses would have signed the conflict.
-                    SASSERT(c.frozen());
                     s.set_conflict(justification());
                     s.del_clause(c);
                 }
                 else if (new_sz == 1) {
-                    // It can only happen with frozen clauses.
-                    // active clauses would have propagated the literal
-                    SASSERT(c.frozen());
                     s.assign(c[0], justification());
                     s.del_clause(c);
                 }
@@ -188,6 +182,7 @@ namespace sat {
         CASSERT("cleaner_bug", s.check_invariant());
         unsigned trail_sz = s.m_trail.size();
         s.propagate(false); // make sure that everything was propagated.
+        TRACE("sat_cleaner_bug", s.display(tout); s.display_watches(tout););
         if (s.m_inconsistent)
             return false;
         if (m_last_num_units == trail_sz)

src/sat/sat_params.pyg

@@ -33,8 +33,8 @@ def_module_params('sat',
                           ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
                           ('drat.check_unsat', BOOL, False, 'build up internal proof and check'),
                           ('drat.check_sat', BOOL, False, 'build up internal trace, check satisfying model'),
-                          ('cardinality.solver', BOOL, False, 'use cardinality solver'),
+                          ('cardinality.solver', BOOL, True, 'use cardinality solver'),
-                          ('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'),
+                          ('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use native solver)'),
                           ('xor.solver', BOOL, False, 'use xor solver'),
                           ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),

src/sat/sat_solver.cpp

@@ -1634,6 +1634,15 @@ namespace sat {
         }
         TRACE("sat_mc_bug", m_mc.display(tout););
 
+#if 0
+        IF_VERBOSE(0, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";);
+        for (auto p : big::s_del_bin) {
+            if (value(p.first) != l_true && value(p.second) != l_true) {
+                IF_VERBOSE(0, verbose_stream() << "binary violation: " << p.first << " " << p.second << "\n");
+            }
+        }
+#endif
+
         IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";);
         if (!check_clauses(m_model)) {
             throw solver_exception("check model failed");