From 5708de43016ea42ed299aa545d96fda59cfcc402 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 12 Nov 2021 11:20:35 -0800
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/viable2.cpp | 79 ++++++++++++++++++++++++++----------
 src/math/polysat/viable2.h   |  2 +
 src/util/dlist.h             | 10 ++++-
 3 files changed, 68 insertions(+), 23 deletions(-)

diff --git a/src/math/polysat/viable2.cpp b/src/math/polysat/viable2.cpp
index a9e05773e..a3754019d 100644
--- a/src/math/polysat/viable2.cpp
+++ b/src/math/polysat/viable2.cpp
@@ -33,34 +33,45 @@ namespace polysat {
     }
 
     void viable2::intersect(pvar v, signed_constraint const& c) {
+        entry* e = m_viable[v];
+        if (e && e->interval.is_full())
+            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))
             return;
 
-        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);
+        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);
+            return ne;
+        };
 
-        entry* e = m_viable[v];
         if (!e) 
-            m_viable[v] = ne;            
+            m_viable[v] = create_entry();
         else {
             entry* first = e;
             do {
-                // TODO: keep track of subsumption
+                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()) {
-                    e->insert(ne);
+                    e->insert_before(create_entry());
+                    if (e == first)
+                        m_viable[v] = e->prev();
                     return;
                 }
                 e = e->next();
             }             
             while (e != first);
+            // otherwise, append to end of list
+            first->insert_before(create_entry());
         }
-        // otherwise, append to end of list
-        e->prev()->insert(ne);
+        SASSERT(is_sorted(m_viable[v]));
     }
 
     bool viable2::has_viable(pvar v) { 
@@ -70,15 +81,17 @@ namespace polysat {
         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;
-            }
+            if (e->interval.is_full())
+                return false;
+            if (!e->interval.currently_contains(lo))
+                return true;
+            lo = e->interval.hi_val();            
             e = e->next();
         }         
         while (e != first);
-        return true; 
+        // ???
+        return !first->prev()->interval.currently_contains(lo) &&
+            first->interval.hi_val() <= lo;
     }
 
     bool viable2::is_viable(pvar v, rational const& val) { 
@@ -113,7 +126,7 @@ namespace polysat {
         if (!e) 
             return dd::find_t::multiple;
         
-        
+        // TODO
         entry* first = e;
         do {
             if (e->interval.is_full())
@@ -129,10 +142,14 @@ namespace polysat {
 
     void viable2::log(pvar v) {
         auto* e = m_viable[v];
-#if 0
-        for (auto const& [i, conds, c] : *s) 
-            LOG("v" << v << ": " << i);     
-#endif
+        if (!e)
+            return;
+        entry* first = e;
+        do {
+            LOG("v" << v << ": " << e->interval << " " << e->side_cond << " " << e->src);
+            e = e->next();
+        }         
+        while (e != first);
     }
 
     void viable2::log() {
@@ -140,6 +157,24 @@ namespace polysat {
             log(v);
     }
 
+    bool viable2::is_sorted(entry* e) {
+        entry* first = e;
+        while (true) {
+            if (e->interval.is_full())
+                return true;
+            auto* n = e->next();
+            if (n == first)
+                break;
+            if (e->interval.lo_val() > n->interval.lo_val())
+                return false;
+            if (e->interval.lo_val() == n->interval.lo_val() &&
+                e->interval.current_len() > n->interval.current_len())
+                return false;
+            e = n;
+        }
+        return true;
+    }
+
 
 }
 
diff --git a/src/math/polysat/viable2.h b/src/math/polysat/viable2.h
index d09570227..60dfcd8e8 100644
--- a/src/math/polysat/viable2.h
+++ b/src/math/polysat/viable2.h
@@ -42,6 +42,8 @@ namespace polysat {
         ptr_vector<entry>                    m_viable;   // set of viable values.
         svector<std::pair<pvar, entry*>>     m_trail;    // undo stack
 
+        bool is_sorted(entry* e);
+
     public:
         viable2(solver& s);
 
diff --git a/src/util/dlist.h b/src/util/dlist.h
index 8e2f6a32a..7efe5bb53 100644
--- a/src/util/dlist.h
+++ b/src/util/dlist.h
@@ -41,13 +41,21 @@ public:
         return head;
     }
 
-    void insert(T* elem) {
+    void insert_after(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;
     }
+
+    void insert_before(T* elem) {
+        T* prev = this->m_prev;
+        elem->m_next = prev->m_next;
+        elem->m_prev = prev;
+        prev->m_next = elem;
+        this->m_prev = elem;
+    }
     
     static void remove_from(T*& list, T* elem) {
         if (list->m_next == list) {