roll in new-viable

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

src/math/polysat/solver.h

@@ -36,7 +36,7 @@ Author:
 #include "math/polysat/log.h"
 
 
-#define NEW_VIABLE 0
+#define NEW_VIABLE 1
 
 namespace polysat {
 
@@ -75,12 +75,13 @@ namespace polysat {
 
         reslimit&                m_lim;
         params_ref               m_params;
+
+        scoped_ptr_vector<dd::pdd_manager> m_pdd;
 #if NEW_VIABLE
         viable2                  m_viable;
 #else
         viable                   m_viable;   // viable sets per variable
 #endif
-        scoped_ptr_vector<dd::pdd_manager> m_pdd;
         linear_solver            m_linear_solver;
         conflict                 m_conflict;        
         forbidden_intervals      m_forbidden_intervals;
@@ -224,7 +225,6 @@ namespace polysat {
         void restart();
 
         signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }
-        void assert_constraint(signed_constraint c, unsigned dep);
         static void insert_constraint(signed_constraints& cs, signed_constraint c);
 
         bool inc() { return m_lim.inc(); }
@@ -348,8 +348,6 @@ namespace polysat {
 
         void updt_params(params_ref const& p);
 
-        void get_param_descrs(param_descrs& pd);
-
     };
 
     class assignments_pp {

src/math/polysat/viable2.cpp

@@ -47,8 +47,11 @@ namespace polysat {
         auto& [v, e] = m_trail.back();
         SASSERT(e->prev() != e || !m_viable[v]);
         SASSERT(e->prev() != e || e->next() == e);
-        if (e->prev() != e) 
+        if (e->prev() != e) {
             e->prev()->insert_after(e);
+            if (e->interval.lo_val() < e->next()->interval.lo_val())
+                m_viable[v] = e;
+        }
         else 
             m_viable[v] = e;        
         m_trail.pop_back();
@@ -143,10 +146,10 @@ namespace polysat {
             entry* n = e->next();
             if (n == e)
                 return true;
-            if (n == first)
-                return e->interval.hi_val() != max_value;
             if (e->interval.hi_val() < n->interval.lo_val())
                 return true;
+            if (n == first)
+                return e->interval.lo_val() <= e->interval.hi_val();
             e = n;
         }         
         while (e != first);
@@ -268,6 +271,7 @@ namespace polysat {
             }
             for (auto sc : e->side_cond)
                 core.insert(sc);
+            e->src->set_var_dependent(); // ?
             core.insert(e->src);
             e = n;
         }             
@@ -285,6 +289,8 @@ namespace polysat {
     }
 
     void viable2::log(pvar v) {
+        if (!well_formed(m_viable[v]))
+            LOG("v" << v << " not well formed");
         auto* e = m_viable[v];
         if (!e)
             return;
@@ -326,6 +332,8 @@ namespace polysat {
     * it suffices to check containment in one direction).
     */
     bool viable2::well_formed(entry* e) {
+        if (!e)
+            return true;
         entry* first = e;
         while (true) {
             if (e->interval.is_full())

src/math/polysat/viable2.h

@@ -53,13 +53,10 @@ namespace polysat {
 
         ~viable2();
 
-        void push(unsigned) {
+        // declare and remove var
-            m_viable.push_back(nullptr);
+        void push(unsigned) { m_viable.push_back(nullptr); }
-        }
 
-        void pop() { 
+        void pop() { m_viable.pop_back(); }
-            m_viable.pop_back(); 
-        }
 
         void pop_viable();
 

src/test/polysat.cpp

@@ -1081,7 +1081,6 @@ void tst_polysat() {
     // working
     // NOT: polysat::test_fixed_point_arith_mul_div_inverse();
             
-    
     // polysat::test_monot_bounds(8);
 
     polysat::test_add_conflicts();