na

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

src/math/polysat/interval.h

@@ -94,6 +94,17 @@ namespace polysat {
             else
                 return val < hi_val() || val >= lo_val();
         }
+        bool contains(eval_interval const& other) const {
+            if (is_full())
+                return true;
+            if (lo_val() <= other.lo_val() && other.hi_val() <= hi_val())
+                return true;
+            if (hi_val() < lo_val() && lo_val() <= other.lo_val() && other.lo_val() <= other.hi_val())
+                return true;
+            if (hi_val() < lo_val() && other.lo_val() < hi_val() && other.hi_val() <= hi_val())
+                return true;
+            return false;
+        }
     };
 
     inline std::ostream& operator<<(std::ostream& os, eval_interval const& i) {

src/math/polysat/solver.cpp

@@ -268,10 +268,14 @@ namespace polysat {
                 --num_levels;
                 break;
             }
-            case trail_instr_t::viable_i: {
+            case trail_instr_t::viable_add_i: {
                 m_viable.pop_viable();
                 break;
             }
+            case trail_instr_t::viable_rem_i: {
+                m_viable.push_viable();
+                break;
+            }
             case trail_instr_t::assign_i: {
                 auto v = m_search.back().var();
                 LOG_V("Undo assign_i: v" << v);
@@ -311,7 +315,7 @@ namespace polysat {
         m_constraints.release_level(m_level + 1);
         SASSERT(m_level == target_level);
         for (unsigned j = replay.size(); j-- > 0; ) {
-            auto lit = replay[j];
+            sat::literal lit = replay[j];
             m_trail.push_back(trail_instr_t::assign_bool_i);
             m_search.push_boolean(lit);
         }
@@ -777,7 +781,7 @@ namespace polysat {
         for (auto item : m_search) {
             if (item.is_assignment()) {
                 pvar v = item.var();
-                auto j = m_justification[v];
+                auto const& j = m_justification[v];
                 out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level();               
                 if (j.is_propagation())
                     out << " " << m_cjust[v];
@@ -795,8 +799,8 @@ namespace polysat {
         for (auto c : m_constraints)
             out << "\t" << c->bvar2string() << ": " << *c << "\n";
         out << "Clauses:\n";
-        for (auto cls : m_constraints.clauses()) {
-            for (auto cl : cls) {
+        for (auto const& cls : m_constraints.clauses()) {
+            for (auto const& cl : cls) {
                 out << "\t" << *cl << "\n";
                 for (auto lit : *cl) 
                     out << "\t\t" << lit << ": " << lit2cnstr(lit) << "\n";                
@@ -806,7 +810,7 @@ namespace polysat {
     }
 
     std::ostream& assignments_pp::display(std::ostream& out) const {
-        for (auto [var, val] : s.assignment())
+        for (auto const& [var, val] : s.assignment())
             out << assignment_pp(s, var, val) << " ";
         return out;
     }

src/math/polysat/trail.h

@@ -20,7 +20,8 @@ namespace polysat {
         qhead_i,
         add_var_i,
         inc_level_i,
-        viable_i,
+        viable_add_i,
+        viable_rem_i,
         assign_i,
         just_i,
         assign_bool_i

src/math/polysat/viable.cpp

@@ -29,13 +29,13 @@ namespace polysat {
     }
 
     void viable::push_viable(pvar v) {
-        s.m_trail.push_back(trail_instr_t::viable_i);
+        s.m_trail.push_back(trail_instr_t::viable_add_i);
         m_viable_trail.push_back(std::make_pair(v, m_viable[v]));
 
     }
 
     void viable::pop_viable() {
-        auto p = m_viable_trail.back();
+        auto const & p = m_viable_trail.back();
         m_viable.set(p.first, p.second);
         m_viable_trail.pop_back();
     }

src/math/polysat/viable.h

@@ -66,6 +66,7 @@ namespace polysat {
 
         void pop_viable();
 
+        void push_viable() {}
         /**
          * update state of viable for pvar v
          * based on affine constraints

src/math/polysat/viable2.cpp

@@ -23,12 +23,35 @@ namespace polysat {
 
     viable2::viable2(solver& s) : s(s) {}
 
-    viable2::~viable2() {}
+    viable2::~viable2() {
+        for (entry* e : m_alloc)
+            dealloc(e);
+    }
+
+    viable2::entry* viable2::alloc_entry() {
+        if (m_alloc.empty())
+            return alloc(entry);
+        auto* e = m_alloc.back();
+        m_alloc.pop_back();
+        return e;
+    }
 
     void viable2::pop_viable() {
         auto& [v, e] = m_trail.back();
         e->remove_from(m_viable[v], e);
-        dealloc(e);
+        m_alloc.push_back(e);       
+        m_trail.pop_back();
+    }
+
+    void viable2::push_viable() {
+        auto& [v, e] = m_trail.back();
+        if (e->prev() != e) 
+            e->prev()->insert_after(e);        
+        else {
+            SASSERT(!m_viable[v]);
+            SASSERT(e->next() == e);
+            m_viable[v] = e;
+        }
         m_trail.pop_back();
     }
 
@@ -38,31 +61,50 @@ namespace polysat {
             return;
 
         auto& fi = s.m_forbidden_intervals;
-        fi_record r = { eval_interval::full(), {}, c };
-        if (!fi.get_interval(c, v, r.interval, r.side_cond))
+        entry* ne = alloc_entry();
+        if (!fi.get_interval(c, v, ne->interval, ne->side_cond)) {
+            m_alloc.push_back(ne);
             return;
+        }
+        ne->init(ne);
 
         auto create_entry = [&]() {
-            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);
+            s.m_trail.push_back(trail_instr_t::viable_add_i);
             return ne;
         };
 
+        auto remove_entry = [&](entry* e) {
+            m_trail.push_back({ v, e });
+            s.m_trail.push_back(trail_instr_t::viable_rem_i);
+            e->remove_from(m_viable[v], e);
+        };
+
         if (!e) 
             m_viable[v] = create_entry();
         else {
             entry* first = e;
             do {
-                if (e->interval.lo_val() == r.interval.lo_val() &&
-                    e->interval.current_len() >= r.interval.current_len()) 
-                    return;                
-                if (e->interval.lo_val() >= r.interval.lo_val()) {
+                if (e->interval.contains(ne->interval)) {
+                    m_alloc.push_back(ne);
+                    return;
+                }
+                if (ne->interval.contains(e->interval)) {
+                    entry* n = e->next();
+                    remove_entry(e);
+                    if (e == n) {
+                        m_viable[v] = create_entry();
+                        break;
+                    }
+                    e = n;
+                    continue;
+                }             
+                SASSERT(e->interval.lo_val() != ne->interval.lo_val());
+                if (e->interval.lo_val() >= ne->interval.lo_val()) {
                     e->insert_before(create_entry());
                     if (e == first)
                         m_viable[v] = e->prev();
+                    SASSERT(well_formed(m_viable[v]));
                     return;
                 }
                 e = e->next();
@@ -71,7 +113,7 @@ namespace polysat {
             // otherwise, append to end of list
             first->insert_before(create_entry());
         }
-        SASSERT(is_sorted(m_viable[v]));
+        SASSERT(well_formed(m_viable[v]));
     }
 
     bool viable2::has_viable(pvar v) { 
@@ -79,19 +121,21 @@ namespace polysat {
         if (!e)
             return true;
         entry* first = e;
-        rational lo(0);
         do {
             if (e->interval.is_full())
                 return false;
-            if (!e->interval.currently_contains(lo))
+            entry* n = e->next();
+            if (n == e)
                 return true;
-            lo = e->interval.hi_val();            
-            e = e->next();
+            if (n == first)
+                return e->interval.hi_val() != e->interval.hi().manager().max_value();
+
+            if (e->interval.hi_val() < n->interval.lo_val())
+                return true;
+            e = n;
         }         
         while (e != first);
-        // ???
-        return !first->prev()->interval.currently_contains(lo) &&
-            first->interval.hi_val() <= lo;
+        return false;
     }
 
     bool viable2::is_viable(pvar v, rational const& val) { 
@@ -102,6 +146,8 @@ namespace polysat {
         do {
             if (e->interval.currently_contains(val))
                 return false;
+            if (e->interval.lo_val() < val)
+                return !first->prev()->interval.currently_contains(val);
             e = e->next();
         }         
         while (e != first);
@@ -113,7 +159,21 @@ namespace polysat {
     }
 
     rational viable2::min_viable(pvar v) { 
-        return rational::zero(); 
+        rational lo(0);
+        auto* e = m_viable[v];
+        if (!e)
+            return lo;
+        entry* first = e;
+        if (first->prev()->interval.currently_contains(lo))
+            lo = first->prev()->interval.hi_val();
+        do {
+            if (!e->interval.currently_contains(lo))
+                return lo;
+            lo = e->interval.hi_val();
+            e = e->next();
+        }         
+        while (e != first);
+        return lo;
     }
 
     rational viable2::max_viable(pvar v) { 
@@ -125,7 +185,28 @@ namespace polysat {
         val = 0;
         if (!e) 
             return dd::find_t::multiple;
+
+
+        entry* first = e;
+        do {
+            if (e->interval.is_full())
+                return dd::find_t::empty;
+            entry* n = e->next();
+            if (n == e && e->interval.lo_val() != 0) {
+                val = 0;
+                if (e->interval.lo_val() > 1 || e->interval.hi_val() < e->interval.hi().manager().max_value())
+                    return dd::find_t::multiple;
+                return dd::find_t::singleton;
+            }
+            if (n == first) {
+                if (e->interval.hi_val() == e->interval.hi().manager().max_value())
+                    ;
+            }
+            e = n;
+        }         
+        while (e != first);
         
+#if 0
         // TODO
         entry* first = e;
         do {
@@ -136,6 +217,7 @@ namespace polysat {
             }
         }         
         while (e != first);
+#endif
 
         return dd::find_t::multiple;
     }
@@ -157,18 +239,22 @@ namespace polysat {
             log(v);
     }
 
-    bool viable2::is_sorted(entry* e) {
+    /*
+    * Lower bounds are strictly ascending.
+    * intervals don't contain each-other (since lower bounds are ascending, 
+    * it suffices to check containment in one direction).
+    */
+    bool viable2::well_formed(entry* e) {
         entry* first = e;
         while (true) {
             if (e->interval.is_full())
-                return true;
+                return e->next() == e;
             auto* n = e->next();
-            if (n == first)
-                break;
-            if (e->interval.lo_val() > n->interval.lo_val())
+            if (n != e && e->interval.contains(n->interval))
                 return false;
-            if (e->interval.lo_val() == n->interval.lo_val() &&
-                e->interval.current_len() > n->interval.current_len())
+            if (n == first)
+                break;            
+            if (e->interval.lo_val() >= n->interval.lo_val())
                 return false;
             e = n;
         }

src/math/polysat/viable2.h

@@ -38,11 +38,13 @@ namespace polysat {
             entry() : fi_record({ eval_interval::full(), {}, {} }) {}
         };
         
-        small_object_allocator               m_alloc;
+        ptr_vector<entry>                    m_alloc;
         ptr_vector<entry>                    m_viable;   // set of viable values.
         svector<std::pair<pvar, entry*>>     m_trail;    // undo stack
 
-        bool is_sorted(entry* e);
+        bool well_formed(entry* e);
+
+        entry* alloc_entry();
 
     public:
         viable2(solver& s);
@@ -59,6 +61,8 @@ namespace polysat {
 
         void pop_viable();
 
+        void push_viable();
+
         /**
          * update state of viable for pvar v
          * based on affine constraints