remove unsound use of sat_big reduction

chores.txt

@@ -0,0 +1,52 @@
+    
+1. expand unit test for pdd to test the exposed functionality
+2. develop nla bridge to pdd_grobner, similar to how grobner wraps 
+   around grobner_core in nla_grobner
+3. self-contained unit test for pdd_grobner 
+4. examine perf / memory for latest rebase.
+   Possibly nla2bv is used more, but could take resources in the sat solver.
+   We can put some limits on sat solver by configuring sat.max_conflicts.
+
+Details:
+
+1.1 test tree_size, dag_size, degree
+1.2 test out of memory scenarios (already tested for 
+    dd_bdd and code is similar)
+1.3 tests for reduce (expose bugs with small examples)
+1.4 tests for spoly
+
+2.1 add an eval module for pdd. Sample signature:
+    class pdd_eval {
+        pdd_manager& m;
+        std::function<rational (unsigned)> m_var2val;
+    public:
+        pdd_eval(pdd_manager& m): m(m) {}
+        void operator=(std::function<rational (unsigned)>& v2v) { m_var2val = v2i; }
+        rational operator()(pdd const& p);        
+    };
+2.2 disentangle nla_intervals into dep_intervals + nla_intervals 
+    (which uses dep_intervals and provides services for nex/lar_solver).
+2.3 add interval module for pdd. Sample signature:
+
+    typedef dep_intervals::interval interval;
+
+    class pdd_interval {
+        pdd_manager&  m;
+        dep_intervals m_intervals;
+        std::function<interval (unsigned)> m_var2interval;
+    public:
+        pdd_interval(pdd_manager& m, reslimit& lim): m(m) m_intervals(lim) {}
+        void operator=(std::function<interval (unsigned)>& v2i) { m_var2interval = v2i; }
+        interval operator()(pdd const& p);
+        bool separated_from_zero(pdd const& p, u_dependency*& dep) { return m_intervals.separated_from_zero((*this)(p), dep); }
+    };
+
+2.4 port other code from nla::grobner class to wrap around grobner
+2.5 review pdd_grobner for feature compatibility with grobner_core
+    There are two modes for pdd_grobner: basic and tuned. basic is similar to nla_grobner.
+    tuned is going to be full of implementation and some conceptual bugs. It is somewhat mild extension over base
+    so debugging it should be doable.
+
+
+3.1 unit tests for pdd_grobner. Maybe I take a stab at this as a starting point.
+

src/sat/sat_big.cpp

@@ -191,7 +191,7 @@ namespace sat {
                 watched& w = *it;
                 if (learned() ? w.is_binary_learned_clause() : w.is_binary_clause()) {
                     literal v = w.get_literal();
-                    if (u != get_parent(v) && safe_reach(u, v)) {
+                    if (u != get_parent(v) && ~u != get_parent(v) && safe_reach(u, v)) {
                         ++elim;
                         add_del(~u, v);
                         if (s.get_config().m_drat) s.m_drat.del(~u, v);
@@ -267,7 +267,7 @@ namespace sat {
         for (auto& next : m_dag) {
             if (!next.empty()) {
                 out << to_literal(idx) << " : " << m_left[idx] << ":" << m_right[idx] << " -> " << next << "\n";
-#if 0
+#if 1
                 for (literal n : next) {
                     out << n << "[" << m_left[n.index()] << ":" << m_right[n.index()] << "] ";
                 }

src/sat/sat_drat.cpp

@@ -738,7 +738,6 @@ namespace sat {
     void drat::del(literal l1, literal l2) {
         ++m_num_del;
         literal ls[2] = {l1, l2};
-        SASSERT(!(l1 == literal(13923, false) && l2 == literal(14020, true)));
         if (m_out) dump(2, ls, status::deleted);
         if (m_bout) bdump(2, ls, status::deleted);
         if (m_check) append(l1, l2, status::deleted);

src/sat/sat_simplifier.cpp

@@ -134,7 +134,7 @@ namespace sat {
             }
             m_sub_todo.erase(c);
             c.set_removed(true);
-            TRACE("resolution_bug", tout << "del_clause: " << c << "\n";);
+            TRACE("sat_simplifier", tout << "del_clause: " << c << "\n";);
             m_need_cleanup = true;
             m_use_list.erase(c);
         }
@@ -429,7 +429,7 @@ namespace sat {
         clause_use_list const & cs = m_use_list.get(target);
         for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
             clause & c2 = it.curr();
-            CTRACE("resolution_bug", c2.was_removed(), tout << "clause has been removed:\n" << c2 << "\n";);
+            CTRACE("sat_simplifier", c2.was_removed(), tout << "clause has been removed:\n" << c2 << "\n";);
             SASSERT(!c2.was_removed());
             if (&c2 != &c1 &&
                 c1.size() <= c2.size() &&
@@ -1736,7 +1736,7 @@ namespace sat {
         unsigned num_bin_pos = num_nonlearned_bin(pos_l);
         unsigned num_bin_neg = num_nonlearned_bin(neg_l);
         unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos;
-        CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos
+        CTRACE("sat_simplifier", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos
                << " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";);
         return cost;
     }
@@ -1761,7 +1761,7 @@ namespace sat {
         }
         m_elim_todo.reset();
         std::stable_sort(tmp.begin(), tmp.end(), bool_var_and_cost_lt());
-        TRACE("elim_vars",
+        TRACE("sat_simplifier",
               for (auto& p : tmp) tout << "(" << p.first << ", " << p.second << ") ";
               tout << "\n";);
         for (auto& p : tmp) 
@@ -1888,14 +1888,14 @@ namespace sat {
                 c.set_removed(true);
                 m_use_list.erase(c, l);
                 m_sub_todo.erase(c);
-                TRACE("resolution_bug", tout << "del_clause (elim_var): " << c << "\n";);
+                TRACE("sat_simplifier", tout << "del_clause (elim_var): " << c << "\n";);
                 m_need_cleanup = true;
             }
         }
     }
 
     bool simplifier::try_eliminate(bool_var v) {
-        TRACE("resolution_bug", tout << "processing: " << v << "\n";);
+        TRACE("sat_simplifier", tout << "processing: " << v << "\n";);
         if (value(v) != l_undef)
             return false;
 
@@ -1908,7 +1908,7 @@ namespace sat {
         unsigned num_pos = pos_occs.num_irredundant() + num_bin_pos;
         unsigned num_neg = neg_occs.num_irredundant() + num_bin_neg;
 
-        TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
+        TRACE("sat_simplifier", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
 
         if (num_pos >= m_res_occ_cutoff && num_neg >= m_res_occ_cutoff)
             return false;
@@ -1925,7 +1925,7 @@ namespace sat {
                 before_lits += it.curr().size();
         }
 
-        TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << " before_lits: " << before_lits << "\n";);
+        TRACE("sat_simplifier", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << " before_lits: " << before_lits << "\n";);
 
         if (num_pos >= m_res_occ_cutoff3 && num_neg >= m_res_occ_cutoff3 && before_lits > m_res_lit_cutoff3 && s.m_clauses.size() > m_res_cls_cutoff2)
             return false;
@@ -1941,24 +1941,24 @@ namespace sat {
         collect_clauses(pos_l, m_pos_cls);
         collect_clauses(neg_l, m_neg_cls);
 
-        TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
+        TRACE("sat_simplifier", tout << "collecting number of after_clauses\n";);
         unsigned before_clauses = num_pos + num_neg;
         unsigned after_clauses  = 0;
         for (clause_wrapper& c1 : m_pos_cls) {
             for (clause_wrapper& c2 : m_neg_cls) {
                 m_new_cls.reset();
                 if (resolve(c1, c2, pos_l, m_new_cls)) {
-                    TRACE("resolution_detail", tout << c1 << "\n" << c2 << "\n-->\n";
+                    TRACE("sat_simplifier", tout << c1 << "\n" << c2 << "\n-->\n";
                           for (literal l : m_new_cls) tout << l << " "; tout << "\n";);
                     after_clauses++;
                     if (after_clauses > before_clauses) {
-                        TRACE("resolution", tout << "too many after clauses: " << after_clauses << "\n";);
+                        TRACE("sat_simplifier", tout << "too many after clauses: " << after_clauses << "\n";);
                         return false;
                     }
                 }
             }
         }
-        TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
+        TRACE("sat_simplifier", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
         m_elim_counter -= num_pos * num_neg + before_lits;
 
         m_elim_counter -= num_pos * num_neg + before_lits;
@@ -1977,7 +1977,7 @@ namespace sat {
                 m_new_cls.reset();
                 if (!resolve(c1, c2, pos_l, m_new_cls))
                     continue;                
-                TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
+                TRACE("sat_simplifier", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
                 if (cleanup_clause(m_new_cls)) {
                     continue; // clause is already satisfied.
                 }