viable 2 with dlist

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

src/math/polysat/constraint.h

@@ -268,4 +268,16 @@ namespace polysat {
     inline std::ostream& operator<<(std::ostream& out, signed_constraint const& c) {
         return c.display(out);
     }
+
+    struct fi_record {
+        eval_interval               interval;
+        vector<signed_constraint>   side_cond;
+        signed_constraint           src;
+
+        struct less {
+            bool operator()(fi_record const& a, fi_record const& b) const {
+                return a.interval.lo_val() < b.interval.lo_val();
+            }
+        };
+    };
 }

src/math/polysat/forbidden_intervals.cpp

@@ -22,12 +22,6 @@ Author:
 
 namespace polysat {
 
-    struct fi_record {
-        eval_interval interval;
-        vector<signed_constraint> side_cond;  
-        signed_constraint src;
-    };
-
     /**
      * Find a sequence of intervals that covers all of Z_modulus.
      *

src/math/polysat/solver.h

@@ -109,11 +109,6 @@ namespace polysat {
 
         unsigned_vector          m_base_levels;  // External clients can push/pop scope. 
 
-
-        void push_viable(pvar v) {
-            m_viable.push_viable(v);
-        }
-
         void push_qhead() { 
             m_trail.push_back(trail_instr_t::qhead_i);
             m_qhead_trail.push_back(m_qhead);

src/math/polysat/viable.h

@@ -49,6 +49,8 @@ namespace polysat {
         dd::fdd const& var2bits(pvar v);
 
 
+        void push_viable(pvar v);
+
     public:
         viable(solver& s);
 
@@ -58,12 +60,10 @@ namespace polysat {
             m_viable.push_back(m_bdd.mk_true()); 
         }
 
-        void pop() { 
+        void pop() {
-            m_viable.pop_back(); 
+            m_viable.pop_back();
         }
 
-        void push_viable(pvar v);
-
         void pop_viable();
 
         /**

src/math/polysat/viable2.cpp

@@ -14,6 +14,7 @@ Author:
 --*/
 
 
+#include "util/debug.h"
 #include "math/polysat/viable2.h"
 #include "math/polysat/solver.h"
 
@@ -24,44 +25,114 @@ namespace polysat {
 
     viable2::~viable2() {}
 
-    void viable2::push_viable(pvar v) {
-        m_trail.push_back(std::make_pair(v, m_viable[v]));
-    }
-
     void viable2::pop_viable() {
-        auto const& [v, s] = m_trail.back();
+        auto& [v, e] = m_trail.back();
-        m_viable[v] = s;
+        e->remove_from(m_viable[v], e);
+        dealloc(e);
         m_trail.pop_back();
     }
 
     void viable2::intersect(pvar v, signed_constraint const& c) {
         auto& fi = s.m_forbidden_intervals;
-        vector<signed_constraint> side_cond;
+        fi_record r = { eval_interval::full(), {}, c };
-        eval_interval interval = eval_interval::full();
+        if (!fi.get_interval(c, v, r.interval, r.side_cond))
-        if (!fi.get_interval(c, v, interval, side_cond))
             return;
-        auto& s = m_viable[v];
-        for (unsigned i = 0; i < s.size(); ++i) {
 
+        entry* ne = alloc(entry);
+        *static_cast<fi_record*>(ne) = r;
+        ne->init(ne);
+        m_trail.push_back({ v, ne });
+        s.m_trail.push_back(trail_instr_t::viable_i);
+
+        entry* e = m_viable[v];
+        if (!e) 
+            m_viable[v] = ne;            
+        else {
+            entry* first = e;
+            do {
+                // TODO: keep track of subsumption
+                if (e->interval.lo_val() >= r.interval.lo_val()) {
+                    e->insert(ne);
+                    return;
+                }
+                e = e->next();
+            }             
+            while (e != first);
         }
+        // otherwise, append to end of list
+        e->prev()->insert(ne);
     }
 
-    bool viable2::has_viable(pvar v) { return true; }
+    bool viable2::has_viable(pvar v) { 
+        auto* e = m_viable[v];
+        if (!e)
+            return true;
+        entry* first = e;
+        rational lo(0);
+        do {
+            if (e->interval.lo_val() <= lo && lo < e->interval.hi_val()) {
+                lo = e->interval.hi_val();
+                e = e->next();
+                continue;
+            }
+            e = e->next();
+        }         
+        while (e != first);
+        return true; 
+    }
 
-    bool viable2::is_viable(pvar v, rational const& val) { return true; }
+    bool viable2::is_viable(pvar v, rational const& val) { 
+        auto* e = m_viable[v];
+        if (!e)
+            return true;
+        entry* first = e;
+        do {
+            if (e->interval.currently_contains(val))
+                return false;
+            e = e->next();
+        }         
+        while (e != first);
+        return true; 
+    }
 
-    void viable2::add_non_viable(pvar v, rational const& val) { }
+    void viable2::add_non_viable(pvar v, rational const& val) { 
+        NOT_IMPLEMENTED_YET();
+    }
 
-    rational viable2::min_viable(pvar v) { return rational::zero(); }
+    rational viable2::min_viable(pvar v) { 
+        return rational::zero(); 
+    }
 
-    rational viable2::max_viable(pvar v) { return rational::zero(); }
+    rational viable2::max_viable(pvar v) { 
+        return rational::zero(); 
+    }
 
-    dd::find_t viable2::find_viable(pvar v, rational& val) { return dd::find_t::multiple; }
+    dd::find_t viable2::find_viable(pvar v, rational& val) { 
+        auto* e = m_viable[v];
+        val = 0;
+        if (!e) 
+            return dd::find_t::multiple;
+        
+        
+        entry* first = e;
+        do {
+            if (e->interval.is_full())
+                return dd::find_t::empty;
+            if (e->interval.currently_contains(val)) {
+                val = e->interval.hi_val();
+            }
+        }         
+        while (e != first);
+
+        return dd::find_t::multiple;
+    }
 
     void viable2::log(pvar v) {
-        auto const& s = m_viable[v];
+        auto* e = m_viable[v];
-        for (auto const& [i, c] : s) 
+#if 0
-            LOG("v" << v << ": " << i);        
+        for (auto const& [i, conds, c] : *s) 
+            LOG("v" << v << ": " << i);     
+#endif
     }
 
     void viable2::log() {

src/math/polysat/viable2.h

@@ -18,24 +18,29 @@ Author:
 
 
 #include <limits>
-
+#include "util/dlist.h"
+#include "util/small_object_allocator.h"
 #include "math/polysat/types.h"
 #include "math/polysat/constraint.h"
 
 
+
+
 namespace polysat {
 
     class solver;
 
     class viable2 {
         solver& s;
-
-        typedef std::tuple<eval_interval, vector<signed_constraint>> entry;
-        typedef vector<entry> state;
         
-        vector<state>                          m_viable;   // set of viable values.
+        struct entry : public dll_base<entry>, public fi_record { 
-        vector<std::pair<pvar, state>>         m_trail;
+        public: 
-
+            entry() : fi_record({ eval_interval::full(), {}, {} }) {}
+        };
+        
+        small_object_allocator               m_alloc;
+        ptr_vector<entry>                    m_viable;   // set of viable values.
+        svector<std::pair<pvar, entry*>>     m_trail;    // undo stack
 
     public:
         viable2(solver& s);
@@ -43,15 +48,13 @@ namespace polysat {
         ~viable2();
 
         void push(unsigned) {
-            m_viable.push_back({});
+            m_viable.push_back(nullptr);
         }
 
         void pop() { 
             m_viable.pop_back(); 
         }
 
-        void push_viable(pvar v);
-
         void pop_viable();
 
         /**

src/util/dlist.h

@@ -40,6 +40,14 @@ public:
         remove_from(list, head);
         return head;
     }
+
+    void insert(T* elem) {
+        T* next = this->m_next;
+        elem->m_prev = next->m_prev;
+        elem->m_next = next;
+        this->m_next = elem;
+        next->m_prev = elem;
+    }
     
     static void remove_from(T*& list, T* elem) {
         if (list->m_next == list) {