prepare viable

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

src/math/polysat/viable.cpp

@@ -11,13 +11,13 @@ namespace polysat {
 
     void viable::push_viable(pvar v) {
         s.m_trail.push_back(trail_instr_t::viable_i);
-        m_viable_trail.push_back(std::make_pair(v, m_viable[v]));
+        m_viable_trail.push_back(std::make_pair(v, m_viable_bdd[v]));
     }
 
     void viable::pop_viable() {
         auto p = m_viable_trail.back();
         LOG_V("Undo viable_i");
-        m_viable[p.first] = p.second;
+        m_viable_bdd[p.first] = p.second;
         m_viable_trail.pop_back();
     }
 
@@ -62,11 +62,11 @@ namespace polysat {
     }
 
     bool viable::has_viable(pvar v) {
-        return !m_viable[v].is_false();
+        return !m_viable_bdd[v].is_false();
     }
 
     bool viable::is_viable(pvar v, rational const& val) {
-        return var2bits(v).contains(m_viable[v], val);
+        return var2bits(v).contains(m_viable_bdd[v], val);
     }
 
     void viable::add_non_viable(pvar v, rational const& val) {
@@ -78,13 +78,13 @@ namespace polysat {
 
     void viable::intersect_viable(pvar v, bdd vals) {
         push_viable(v);
-        m_viable[v] &= vals;
-        if (m_viable[v].is_false())
+        m_viable_bdd[v] &= vals;
+        if (m_viable_bdd[v].is_false())
             s.set_conflict(v);
     }
 
     dd::find_t viable::find_viable(pvar v, rational & val) {
-        return var2bits(v).find_hint(m_viable[v], s.m_value[v], val);
+        return var2bits(v).find_hint(m_viable_bdd[v], s.m_value[v], val);
     }
 
     dd::fdd const& viable::sz2bits(unsigned sz) {
@@ -100,23 +100,20 @@ namespace polysat {
 #if POLYSAT_LOGGING_ENABLED
     void viable::log() {
         // only for small problems
-        if (m_viable.size() < 10) {
-            for (pvar v = 0; v < m_viable.size(); ++v) {
-                log(v);
-            }
-        }
+        for (pvar v = 0; v < std::min(10u, m_viable.size()); ++v) 
+            log(v);            
     }
 
     void viable::log(pvar v) {
         if (s.size(v) <= 5) {
             vector<rational> xs;
-            for (rational x = rational::zero(); x < rational::power_of_two(s.size(v)); x += 1) {
-                if (is_viable(v, x)) {
+            for (rational x = rational::zero(); x < rational::power_of_two(s.size(v)); x += 1) 
+                if (is_viable(v, x)) 
                     xs.push_back(x);
-                }
-            }
+                            
             LOG("Viable for pvar " << v << ": " << xs);
-        } else {
+        } 
+        else {
             LOG("Viable for pvar " << v << ": <range too big>");
         }
     }

src/math/polysat/viable.h

@@ -15,6 +15,7 @@ Author:
 #pragma once
 
 #include <limits>
+#include "util/tbv.h"
 #include "math/dd/dd_bdd.h"
 #include "math/interval/mod_interval.h"
 #include "math/polysat/types.h"
@@ -23,9 +24,23 @@ namespace polysat {
 
     class solver;
 
-    class viable_values : public mod_interval<rational> {
-
-
+    //
+    // replace BDDs by viable sets that emulate affine relations.
+    // viable_set has an interval of feasible values.
+    // it also can use ternary bit-vectors.
+    //
+    class viable_set : public mod_interval<rational> {
+        unsigned m_num_bits;
+        tbv* m_tbv = nullptr;
+    public:
+        viable_set(unsigned num_bits): m_num_bits(num_bits) {}
+        bool is_singleton(rational& val) const; // all bits in tbv are fixed and !is_empty() for mod_interval
+        void set_lo(rational const& lo);
+        void set_hi(rational const& hi);
+        void set_eq(rational const& val);
+        void seq_ne(rational const& val);
+        void set_ule(rational const& a, rational const& b, rational const& c, rational const& d);
+        void set_ugt(rational const& a, rational const& b, rational const& c, rational const& d);
     };
 
     class viable {
@@ -33,9 +48,12 @@ namespace polysat {
         solver& s;
         dd::bdd_manager              m_bdd;
         scoped_ptr_vector<dd::fdd>   m_bits;
-        vector<bdd>                  m_viable;   // set of viable values.
+        vector<bdd>                  m_viable_bdd;   // set of viable values.
         vector<std::pair<pvar, bdd>> m_viable_trail;
 
+
+        vector<viable_set>        m_viable; // future representation of viable values
+
         /**
          * Register all values that are not contained in vals as non-viable.
          */
@@ -48,8 +66,8 @@ namespace polysat {
     public:
         viable(solver& s);
 
-        void push() { m_viable.push_back(m_bdd.mk_true()); }
-        void pop() { m_viable.pop_back(); }
+        void push() { m_viable_bdd.push_back(m_bdd.mk_true()); }
+        void pop() { m_viable_bdd.pop_back(); }
 
         void push_viable(pvar v);
 
@@ -69,7 +87,7 @@ namespace polysat {
          */
         bool has_viable(pvar v);
 
-        bool is_false(pvar v) { return m_viable[v].is_false(); }
+        bool is_false(pvar v) { return m_viable_bdd[v].is_false(); }
 
         /**
          * check if value is viable according to m_viable.