wip: enabling reinit approach

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

src/math/polysat/constraint_manager.cpp

@@ -74,6 +74,7 @@ namespace polysat {
         register_clause(cl);
         watch(*cl);
         cl->set_active();
+        s.push_reinit_stack(*cl);
     }
 
     // Release constraints at the given level and above.

src/math/polysat/op_constraint.cpp

@@ -131,10 +131,8 @@ namespace polysat {
         if (first)
             activate(s);
 
-        if (clause_ref lemma = produce_lemma(s, s.get_assignment())) {
+        if (clause_ref lemma = produce_lemma(s, s.get_assignment())) 
             s.add_clause(*lemma);
-            s.push_reinit_stack(*lemma);
-        }
 
         if (!s.is_conflict() && is_currently_false(s, is_positive))
             s.set_conflict(signed_constraint(this, is_positive));
@@ -552,8 +550,8 @@ namespace polysat {
 
         pdd prod = p() * r();
         rational prodv = (pv * rv).val();
-        if (prodv != rational::power_of_two(parity_pv))
+//        if (prodv != rational::power_of_two(parity_pv))
-            verbose_stream() << prodv << " " << rational::power_of_two(parity_pv) << " " << parity_pv << " " << pv << " " << rv << "\n";
+//            verbose_stream() << prodv << " " << rational::power_of_two(parity_pv) << " " << parity_pv << " " << pv << " " << rv << "\n";
         unsigned lower = 0, upper = m.power_of_2();
         // binary search for the parity (otw. we would have justifications like "parity_at_most(k) && parity_at_least(k)" for at most "k" widths
         while (lower + 1 < upper) {

src/math/polysat/saturation.cpp

@@ -1275,7 +1275,7 @@ namespace polysat {
                 m_lemma.reset();
                 m_lemma.insert(~c);
                 if (propagate(x, core, a_l_b, s.eq(i.lhs() - i.rhs()))) {
-                    verbose_stream() << "infer equality " << s.eq(i.lhs() - i.rhs()) << "\n";
+                    IF_VERBOSE(1, verbose_stream() << "infer equality " << s.eq(i.lhs() - i.rhs()) << "\n");
                     return true;
                 }
             }
@@ -1865,7 +1865,7 @@ namespace polysat {
         // IF_VERBOSE(0, verbose_stream() << "min-max: x := v" << x << " [" << x_min << "," << x_max << "] y := v" << y << " [" << y_min << ", " << y_max << "] y0 " << y0 << "\n");
         if (!update_bounds_for_xs(x_sp2, x_max,   y_min, y_max, y0, a1, b1, c1, d1, a2, b2, c2, d2, M, a_l_b))
             return false;
-        IF_VERBOSE(0, verbose_stream() << "min-max: x := v" << x << " [" << x_min << "," << x_max << "] y := v" << y << " [" << y_min << ", " << y_max << "] y0 " << y0 << "\n");
+        IF_VERBOSE(1, verbose_stream() << "min-max: x := v" << x << " [" << x_min << "," << x_max << "] y := v" << y << " [" << y_min << ", " << y_max << "] y0 " << y0 << "\n");
 
         SASSERT(y_min <= y0 && y0 <= y_max);
         VERIFY(y_min <= y0 && y0 <= y_max);
@@ -1917,7 +1917,7 @@ namespace polysat {
         if (k == N)
             return false;
         if (rational::power_of_two(k) > p_val) {
-            verbose_stream() << k << " " << p_val << " " << a_l_b << "\n";
+            // verbose_stream() << k << " " << p_val << " " << a_l_b << "\n";
             m_lemma.reset();
             for (auto const& c : at_least_k)
                 m_lemma.insert_eval(~c);

src/math/polysat/simplify_clause.cpp

@@ -560,6 +560,9 @@ namespace polysat {
                 return args->hash();
             }
         };
+
+        if (!s.inc())
+            return false;
         
         ptr_vector<pdd_info> info_list;
         map<optional<pdd>, pdd_info*, optional_pdd_hash, default_eq<optional<pdd>>> info_table;

src/math/polysat/solver.cpp

@@ -334,22 +334,12 @@ namespace polysat {
     }
 
 
-    // TODO
-    // pop_levels is called from pop and backjump
-    // backjump invoked a few places.
-    // the logic for propagating clauses after a pop or backjump
-    // is different. pop_levels inserts into repropagate
-    // pop_levels should end with a call to reinit_clauses where
-    // old_sz is the current trail head for clauses created within the scope.
-    //
-    // pop-levels can also update the scope of variables created below the pop level.
-    // the scope of variables would be set to the new level for clauses surviving a pop.
     
     void solver::reinit_clauses(unsigned old_sz) {
         unsigned sz = m_clauses_to_reinit.size();
         SASSERT(old_sz <= sz);
         unsigned j = old_sz;
-        for (unsigned i = old_sz; i < sz; i++) {
+        for (unsigned i = old_sz; i < sz; ++i) {
             clause& c = *m_clauses_to_reinit[i];
             SASSERT(c.on_reinit_stack());
             bool reinit = false;
@@ -364,17 +354,42 @@ namespace polysat {
             // Each Boolean has a "scope". The scope is initialized to the scope where
             // the Boolean is created.
             
-            if (reinit && !at_base_level()) 
+            if (reinit) 
                 // clause propagated literal, must keep it in the reinit stack.
                 m_clauses_to_reinit[j++] = &c;            
-            else if (has_variables_to_reinit(c) && !at_base_level())
+            else if (has_variables_to_reinit(c) && false)
                 m_clauses_to_reinit[j++] = &c;
             else 
                 c.set_on_reinit_stack(false);
+            for (auto lit : c)
+                m_literals_to_reinit.push_back(lit);
         }
         m_clauses_to_reinit.shrink(j);
+        for (auto lit : m_literals_to_reinit)
+            reinit_literal(lit);
+        m_literals_to_reinit.reset();
     }
 
+    void solver::reinit_literal(sat::literal lit) {
+        // check for missed lower evaluations
+        if (m_bvars.is_undef(lit)) {
+            switch (lit2cnstr(lit).eval(*this)) {
+            case l_true:
+                assign_eval(lit);
+                break;
+            case l_false:
+                assign_eval(~lit);
+                break;
+            default:
+                break;
+            }
+        }
+        // put the interval back into viable if we lost it
+        if (m_bvars.is_assigned(lit)) {
+            signed_constraint sc = m_bvars.is_true(lit) ? lit2cnstr(lit) : ~lit2cnstr(lit);
+            sc.narrow(*this, false);
+        }
+    }
 
     bool solver::can_repropagate() {
         return !m_repropagate_lits.empty() && !is_conflict();
@@ -405,24 +420,8 @@ namespace polysat {
             LOG("Repropagate lit " << lit);
             // check for missed lower boolean propagations
             repropagate(lit);
-            // check for missed lower evaluations
+
-            if (m_bvars.is_undef(lit)) {
+            reinit_literal(lit);
-                switch (lit2cnstr(lit).eval(*this)) {
-                case l_true:
-                    assign_eval(lit);
-                    break;
-                case l_false:
-                    assign_eval(~lit);
-                    break;
-                default:
-                    break;
-                }
-            }
-            // put the interval back into viable if we lost it
-            if (m_bvars.is_assigned(lit)) {
-                signed_constraint sc = m_bvars.is_true(lit) ? lit2cnstr(lit) : ~lit2cnstr(lit);
-                sc.narrow(*this, false);
-            }
         }
     }
 
@@ -790,7 +789,9 @@ namespace polysat {
                     // Unit clauses are not stored in watch lists and must be re-propagated separately.
                     m_repropagate_units.push_back(reason);
                 }
-                else if (!ENABLE_REINIT_STACK) 
+                else if (ENABLE_REINIT_STACK)
+                    m_literals_to_reinit.push_back(lit);
+                else 
                     m_repropagate_lits.push_back(lit);
                 m_bvars.unassign(lit);
                 m_search.pop();
@@ -1139,6 +1140,7 @@ namespace polysat {
             appraise_lemma(lemmas.back());
         }
         if (!best_lemma) {
+            display(verbose_stream());
             verbose_stream() << "conflict: " << m_conflict << "\n";
             verbose_stream() << "no lemma\n";
             for (clause* cl: lemmas) {
@@ -1146,6 +1148,7 @@ namespace polysat {
                 for (sat::literal lit : *cl)
                     verbose_stream() << "    " << lit_pp(*this, lit) << "\n";
             }
+            
         }
         SASSERT(best_score < lemma_score::max());
         VERIFY(best_lemma);

src/math/polysat/solver.h

@@ -352,10 +352,12 @@ namespace polysat {
 
         // clause reinitialization
         ptr_vector<clause>       m_clauses_to_reinit;
+        sat::literal_vector      m_literals_to_reinit;
         unsigned_vector          m_reinit_heads;
         unsigned                 m_reinit_head = 0;
         void reinit_clauses(unsigned old_sz);
         bool has_variables_to_reinit(clause const& c) const;
+        void reinit_literal(sat::literal lit);
 
         bool inc() { return m_lim.inc(); }