na

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

src/math/polysat/conflict.cpp

@@ -243,13 +243,13 @@ namespace polysat {
         for (unsigned v : m_vars) {
             if (!is_pmarked(v))
                 continue;
-            s.inc_activity(v);
             auto eq = s.eq(s.var(v), s.get_value(v));
             cm().ensure_bvar(eq.get());
             if (eq.bvalue(s) == l_undef) 
                 s.assign_eval(s.get_level(v), eq.blit());            
             lemma.push(~eq);
         }        
+        s.decay_activity();
 
         return lemma;
     }

src/math/polysat/constraint.h

@@ -284,6 +284,7 @@ namespace polysat {
         eval_interval               interval;
         vector<signed_constraint>   side_cond;
         signed_constraint           src;
+        rational                    coeff;
 
         struct less {
             bool operator()(fi_record const& a, fi_record const& b) const {

src/math/polysat/forbidden_intervals.cpp

@@ -27,12 +27,10 @@ namespace polysat {
      * \returns True iff a forbidden interval exists and the output parameters were set.
      */
 
-    bool forbidden_intervals::get_interval(signed_constraint const& c, pvar v, rational & coeff, eval_interval& out_interval, vector<signed_constraint>& out_side_cond) {
+    bool forbidden_intervals::get_interval(signed_constraint const& c, pvar v, fi_record& fi) {
         if (!c->is_ule())
             return false;
         
-        coeff = 1;
-        
         struct backtrack {
             bool released = false;
             vector<signed_constraint>& side_cond;
@@ -44,24 +42,30 @@ namespace polysat {
             }
         };
 
-        backtrack _backtrack(out_side_cond);        
+        backtrack _backtrack(fi.side_cond);     
 
-        auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_ule().lhs(), out_side_cond);
+        fi.coeff = 1;
-        auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), out_side_cond);
+        fi.src = c;
+
+        auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_ule().lhs(), fi.side_cond);
+        auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), fi.side_cond);
         if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero()))
             return false;
-        if (a1 != a2 && !a1.is_zero() && !a2.is_zero())
-            return false;
         SASSERT(b1.is_val());
         SASSERT(b2.is_val());
 
+        // TBD: use fi.coeff = -1 to tell caller to treat it as a diseq_lin.
+        // record a1, a2, b1, b2 for fast access and add side conditions on b1, b2?
+        if (a1 != a2 && !a1.is_zero() && !a2.is_zero())
+            return false;
+   
         _backtrack.released = true;
 
-        if (match_linear1(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond))
+        if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi.coeff, fi.interval, fi.side_cond))
             return true;
-        if (match_linear2(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond))
+        if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi.coeff, fi.interval, fi.side_cond))
             return true;
-        if (match_linear3(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond))
+        if (match_linear3(c, a1, b1, e1, a2, b2, e2, fi.coeff, fi.interval, fi.side_cond))
             return true;
 
         _backtrack.released = false;

src/math/polysat/forbidden_intervals.h

@@ -47,6 +47,6 @@ namespace polysat {
 
     public:
         forbidden_intervals(solver& s) :s(s) {}
-        bool get_interval(signed_constraint const& c, pvar v, rational & coeff, eval_interval& out_interval, vector<signed_constraint>& side_cond);
+        bool get_interval(signed_constraint const& c, pvar v, fi_record& fi);
     };
 }

src/math/polysat/solver.cpp

@@ -458,6 +458,7 @@ namespace polysat {
                     m_search.pop_asssignment();
                     continue;
                 }
+                inc_activity(v);
                 justification& j = m_justification[v];
                 if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) {
                     revert_decision(v);

src/math/polysat/viable.cpp

@@ -35,30 +35,38 @@ namespace polysat {
     }
 
     viable::entry* viable::alloc_entry() {       
-        rational coeff(1);
         if (m_alloc.empty())
-            return alloc(entry, coeff);
+            return alloc(entry);
         auto* e = m_alloc.back();
         e->side_cond.reset();
-        e->coeff = coeff;
+        e->coeff = 1;
         m_alloc.pop_back();
         return e;
     }
 
     void viable::pop_viable() {
-        auto& [v, is_unit, e] = m_trail.back();
+        auto& [v, k, e] = m_trail.back();
-        auto& vec = is_unit ? m_units[v] : m_non_units[v];
+        switch (k) {
-        e->remove_from(vec, e);
+        case entry_kind::unit_e: 
+            e->remove_from(m_units[v], e); 
+            break;
+        case entry_kind::equal_e: 
+            e->remove_from(m_equal_lin[v], e); 
+            break;
+        default: 
+            e->remove_from(m_diseq_lin[v], e); 
+            break;
+        }
         m_alloc.push_back(e);       
         m_trail.pop_back();
     }
 
     void viable::push_viable() {
-        auto& [v, is_unit, e] = m_trail.back();
+        auto& [v, k, e] = m_trail.back();
         SASSERT(e->prev() != e || !m_units[v]);
         SASSERT(e->prev() != e || e->next() == e);
-        SASSERT(is_unit);
+        SASSERT(k == entry_kind::unit_e);
-        (void)is_unit;
+        (void)k;
         if (e->prev() != e) {
             e->prev()->insert_after(e);
             if (e->interval.lo_val() < e->next()->interval.lo_val())
@@ -72,25 +80,35 @@ namespace polysat {
     bool viable::intersect(pvar v, signed_constraint const& c) {
         auto& fi = s.m_forbidden_intervals;
         entry* ne = alloc_entry();
-        if (!fi.get_interval(c, v, ne->coeff, ne->interval, ne->side_cond) || ne->interval.is_currently_empty()) {
+        if (!fi.get_interval(c, v, *ne)) {
+            m_alloc.push_back(ne);
+            return false;
+        }
+        else if (ne->interval.is_currently_empty()) {
             m_alloc.push_back(ne);
             return false;
         }
         else if (ne->coeff == 1) {
-            ne->src = c;
             return intersect(v, ne);
         }
-        else {
+        else if (ne->coeff == -1) {
-            ne->src = c;
+            insert(ne, v, m_diseq_lin, entry_kind::diseq_e);
-            m_trail.push_back({ v, false, ne });
-            s.m_trail.push_back(trail_instr_t::viable_add_i);
-            ne->init(ne);
-            if (!m_non_units[v])
-                m_non_units[v] = ne;
-            else
-                ne->insert_after(m_non_units[v]);
             return true;
         }
+        else {
+            insert(ne, v, m_equal_lin, entry_kind::equal_e);
+            return true;
+        }
+    }
+
+    void viable::insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k) {
+        m_trail.push_back({ v, k, e });
+        s.m_trail.push_back(trail_instr_t::viable_add_i);
+        e->init(e);
+        if (!entries[v])
+            entries[v] = e;
+        else
+            e->insert_after(entries[v]);
     }
 
     bool viable::intersect(pvar v, entry* ne) {
@@ -106,14 +124,14 @@ namespace polysat {
         }
 
         auto create_entry = [&]() {
-            m_trail.push_back({ v, true, ne });
+            m_trail.push_back({ v, entry_kind::unit_e, ne });
             s.m_trail.push_back(trail_instr_t::viable_add_i);
             ne->init(ne);            
             return ne;
         };
 
         auto remove_entry = [&](entry* e) {
-            m_trail.push_back({ v, true, e });
+            m_trail.push_back({ v, entry_kind::unit_e, e });
             s.m_trail.push_back(trail_instr_t::viable_rem_i);
             e->remove_from(m_units[v], e);
         };
@@ -170,7 +188,7 @@ namespace polysat {
     *   and division with coeff are valid. Is there a more relaxed scheme?
     */
     bool viable::refine_viable(pvar v, rational const& val) {
-        auto* e = m_non_units[v];
+        auto* e = m_equal_lin[v];
         if (!e)
             return true;
         entry* first = e;
@@ -222,6 +240,7 @@ namespace polysat {
                 entry* ne = alloc_entry();
                 ne->src = e->src;
                 ne->side_cond = e->side_cond;
+                // TODO: have forbidden_interval.cpp add these side conditions for non-unit equalities and diseq_lin?
                 ne->side_cond.push_back(s.eq(e->interval.hi(), e->interval.hi_val()));
                 ne->side_cond.push_back(s.eq(e->interval.lo(), e->interval.lo_val()));
                 ne->coeff = 1;
@@ -474,7 +493,7 @@ namespace polysat {
 
     std::ostream& viable::display(std::ostream& out, pvar v) const {
         display(out, v, m_units[v]);
-        display(out, v, m_non_units[v]);
+        display(out, v, m_equal_lin[v]);
         return out;
     }
 

src/math/polysat/viable.h

@@ -32,14 +32,15 @@ namespace polysat {
         solver& s;
         
         struct entry : public dll_base<entry>, public fi_record { 
-            rational coeff;
+            entry() : fi_record({ eval_interval::full(), {}, {}, rational::one()}) {}
-            entry(rational const& m) : fi_record({ eval_interval::full(), {}, {} }), coeff(m) {}
         };
+        enum class entry_kind { unit_e, equal_e, diseq_e };
         
         ptr_vector<entry>                    m_alloc;
         ptr_vector<entry>                    m_units;        // set of viable values based on unit multipliers
-        ptr_vector<entry>                    m_non_units;    // entries that have non-unit multipliers
+        ptr_vector<entry>                    m_equal_lin;    // entries that have non-unit multipliers, but are equal
-        svector<std::tuple<pvar, bool, entry*>>     m_trail; // undo stack
+        ptr_vector<entry>                    m_diseq_lin;    // entries that have distinct non-zero multipliers
+        svector<std::tuple<pvar, entry_kind, entry*>>     m_trail; // undo stack
 
         bool well_formed(entry* e);
 
@@ -51,15 +52,17 @@ namespace polysat {
 
         std::ostream& display(std::ostream& out, pvar v, entry* e) const;
 
+        void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);
+
     public:
         viable(solver& s);
 
         ~viable();
 
         // declare and remove var
-        void push(unsigned) { m_units.push_back(nullptr); m_non_units.push_back(nullptr); }
+        void push(unsigned) { m_units.push_back(nullptr); m_equal_lin.push_back(nullptr); }
 
-        void pop() { m_units.pop_back(); m_non_units.pop_back(); }
+        void pop() { m_units.pop_back(); m_equal_lin.pop_back(); }
 
         void pop_viable();