na

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

src/math/dd/dd_fdd.cpp

@@ -301,5 +301,36 @@ namespace dd {
         return true;
     }
 
+    bool_vector fdd::rational2bits(rational const& r) const {
+        bool_vector result;
+        for (unsigned i = 0; i < num_bits(); ++i)
+            result.push_back(r.get_bit(i));
+        return result;
+    }
+
+    rational fdd::bits2rational(bool_vector const& v) const {
+        rational result(0);
+        for (unsigned i = 0; i < num_bits(); ++i)
+            if (v[i])
+                result += rational::power_of_two(i);
+        return result;
+    }
+
+    bool fdd::sup(bdd const& b, rational& _lo) const {
+        bool_vector lo = rational2bits(_lo);
+        if (!sup(b, lo))
+            return false;
+        _lo = bits2rational(lo);
+        return true;
+    }
+    
+    bool fdd::inf(bdd const& b, rational& _hi) const {
+        bool_vector hi = rational2bits(_hi);
+        if (!inf(b, hi))
+            return false;
+        _hi = bits2rational(hi);
+        return true;
+    }
+
 
 }

src/math/dd/dd_fdd.h

@@ -47,6 +47,10 @@ namespace dd {
 
         bool contains(bdd const& b, bool_vector const& value) const;
 
+        rational bits2rational(bool_vector const& v) const;
+
+        bool_vector rational2bits(rational const& r) const;
+
     public:
         /** Initialize FDD using BDD variables from 0 to num_bits-1. */
         fdd(bdd_manager& manager, unsigned num_bits, unsigned start = 0, unsigned step = 1) : fdd(manager, seq(num_bits, start, step)) { }
@@ -90,6 +94,10 @@ namespace dd {
       
 	bool inf(bdd const& b, bool_vector& hi) const; 
 
+        bool sup(bdd const& b, rational& lo) const;
+
+        bool inf(bdd const& b, rational& hi) const;
+      
     };
 
 }

src/math/interval/mod_interval.h

@@ -18,6 +18,8 @@ Author:
 
 #pragma once
 
+#include "util/rational.h"
+
 
 template<typename Numeral>
 struct pp {
@@ -32,6 +34,10 @@ inline std::ostream& operator<<(std::ostream& out, pp<Numeral> const& p) {
     return out << p.n;
 }
 
+inline std::ostream& operator<<(std::ostream& out, pp<rational> const& p) {
+    return out << p.n;
+}
+
 template<typename Numeral>
 class mod_interval {
     bool emp { false };

src/math/polysat/constraint.h

@@ -211,8 +211,8 @@ namespace polysat {
 
         explicit operator bool() const { return !!m_constraint; }
         bool operator!() const { return !m_constraint; }
-        polysat::constraint* operator->() const { return m_constraint.get(); }
+        constraint* operator->() const { return m_constraint.get(); }
-        polysat::constraint const& operator*() const { return *m_constraint; }
+        constraint const& operator*() const { return *m_constraint; }
 
         constraint_literal& operator=(nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; }
     private:

src/math/polysat/eq_constraint.cpp

@@ -19,7 +19,7 @@ Author:
 namespace polysat {
 
     std::ostream& eq_constraint::display(std::ostream& out) const {
-        out << p() << " == 0 ";
+        out << p() << (is_positive() ? " == 0 " : " != 0");
         return display_extra(out);
     }
 

src/math/polysat/explain.cpp

@@ -81,16 +81,58 @@ namespace polysat {
         return lemma;
     }
 
+    /**
+     *  Polynomial superposition.
+     *  So far between two equalities.
+     *  TODO: Also handle =, != superposition here?
+     *  TODO: handle case when m_conflict.units().size() > 2
+     *  TODO: handle super-position into a clause?
+     */
     clause_ref conflict_explainer::by_polynomial_superposition() {
-        if (m_conflict.units().size() != 2 || m_conflict.clauses().size() > 0)
+        LOG_H3("units-size: " << m_conflict.units().size() << " conflict-clauses " << m_conflict.clauses().size());
+        constraint* c1 = nullptr, *c2 = nullptr;
+        if (m_conflict.units().size() == 2 && m_conflict.clauses().size() == 0) {
+            c1 = m_conflict.units()[0];
+            c2 = m_conflict.units()[1];
+        }
+        else {
+            // other combinations?
+
+#if 0
+            // A clause can also be a unit.
+            // Even if a clause is not a unit, we could still resolve a propagation 
+            // into some literal in the current conflict clause.
+            // Selecting resolvents should not be specific to superposition.
+            // 
+
+            for (auto clause : m_conflict.clauses()) {
+                if (clause->size() == 1) {                    
+                    sat::literal lit = (*clause)[0];
+                    if (lit.sign())
+                        continue;
+                    constraint* c = m_solver.m_constraints.lookup(lit.var());                    
+                    LOG("unit clause: " << *c);
+                    if (c->is_eq() && c->is_positive()) {
+                        c1 = c;
+                        break;
+                    }
+                }
+            }
+            if (!c1)
                 return nullptr;
-        constraint* c1 = m_conflict.units()[0];
+
-        constraint* c2 = m_conflict.units()[1];
+            for (constraint* c : m_conflict.units()) {
-        if (c1 == c2)
+                if (c->is_eq() && c->is_positive()) {
+                    c2 = c;
+                    break;
+                }
+            }
+            std::cout << c1 << " " << c2 << "\n";
+#endif
+        }
+        if (!c1 || !c2 || c1 == c2)
             return nullptr;
-        if (!c1->is_eq() || !c2->is_eq())
+        if (c1->is_eq() && c2->is_eq() && c1->is_positive() && c2->is_positive()) {
-            return nullptr;
-        if (c1->is_positive() && c2->is_positive()) {
             pdd a = c1->to_eq().p();
             pdd b = c2->to_eq().p();
             pdd r = a;

src/math/polysat/solver.h

@@ -97,8 +97,8 @@ namespace polysat {
         search_state             m_search;
         assignment_t const& assignment() const { return m_search.assignment(); }
 
-        unsigned                 m_qhead { 0 }; // next item to propagate (index into m_search)
+        unsigned                 m_qhead = 0; // next item to propagate (index into m_search)
-        unsigned                 m_level { 0 };
+        unsigned                 m_level = 0;
 
         svector<trail_instr_t>   m_trail;
         unsigned_vector          m_qhead_trail;
@@ -157,8 +157,7 @@ namespace polysat {
         void decide_bool(sat::literal lit, clause& lemma);
         void propagate_bool(sat::literal lit, clause* reason);
 
-        void assign_core(pvar v, rational const& val, justification
+        void assign_core(pvar v, rational const& val, justification const& j);
-            const& j);
         bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }
 
 

src/math/polysat/viable.cpp

@@ -73,11 +73,11 @@ namespace polysat {
             else if (hi == 0 && is_max(a))
                 hi = a;
             else 
-                std::cout << "diseq " << lo << " " << a << " " << hi << "\n";
+                std::cout << "unhandled diseq " << lo << " " << a << " " << hi << "\n";
         }
     }
 
-    void viable_set::intersect_eq(rational const& a, rational const& b, bool is_positive) {
+    bool viable_set::intersect_eq(rational const& a, rational const& b, bool is_positive) {
         if (a.is_odd()) {
             if (b == 0)
                 intersect_eq(b, is_positive);
@@ -86,10 +86,20 @@ namespace polysat {
                 VERIFY(a.mult_inverse(m_num_bits, a_inv));
                 intersect_eq(mod(a_inv * -b, p2()), is_positive);
             }
+            return true;
         }
-	    else
+        else {
-	        std::cout << "intersect " << a << "*x " << " == " << b << " " << is_positive << "\n";
+            return false;
         }
+    }
+
+    void viable_set::intersect_eq(rational const& a, rational const& b, bool is_positive, unsigned& budget) {
+        std::function<bool(rational const&)> eval = [&](rational const& x) {
+            return is_positive == (mod(a * x + b, p2()) == 0);
+        };       
+        narrow(eval, budget);
+    }
+
 
     bool viable_set::intersect_ule(rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive) {
         // x <= 0
@@ -114,21 +124,13 @@ namespace polysat {
             else
                 set_hi(b - 1);
         }
-        else if (c == 0 && d == 0) {
-            // ax + b <= 0
-            // or ax + b > 0
-            intersect_eq(a, b, is_positive);
-        }
         else
             return false;
 
         return true;
     }
 
-    void viable_set::intersect_ule(rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive, unsigned& budget) {
+    void viable_set::narrow(std::function<bool(rational const&)>& eval, unsigned& budget) {
-        auto eval = [&](rational const& x) {
-            return is_positive == mod(a * x + b, p2()) <= mod(c * x + d, p2());
-        };        
         while (budget > 0 && !eval(lo) && !is_max(lo) && !is_empty()) {
             --budget;
             lo += 1;
@@ -141,6 +143,13 @@ namespace polysat {
         }
     }
 
+    void viable_set::intersect_ule(rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive, unsigned& budget) {
+        std::function<bool(rational const&)> eval = [&](rational const& x) {
+            return is_positive == mod(a * x + b, p2()) <= mod(c * x + d, p2());
+        };       
+        narrow(eval, budget);
+    }
+
     void viable_set::set_hi(rational const& d) {
         if (is_max(d))
             return;
@@ -150,8 +159,10 @@ namespace polysat {
             set_empty();
         else if (hi != 0 || d + 1 < hi)
             hi = d + 1;  
+        else if (d + 1 == hi)
+            return;
         else 
-            std::cout << "set hi " << lo << " " << d << " " << hi << "\n";
+            std::cout << "set hi " << d << " " << *this << "\n";
     }
 
     void viable_set::set_lo(rational const& b) {
@@ -161,8 +172,10 @@ namespace polysat {
             lo = b, hi = 0;
         else if (lo < b)
             lo = b;                    
+        else if (lo == b)
+            return;
         else 
-            std::cout << "set lo " << lo << " " << b << " " << hi << "\n";
+            std::cout << "set lo " << b << " " << *this << "\n";
     }
 #endif
 
@@ -187,7 +200,15 @@ namespace polysat {
     void viable::intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive) {
 #if NEW_VIABLE
         push_viable(v);
-        m_viable[v].intersect_eq(a, b, is_positive);
+        if (!m_viable[v].intersect_eq(a, b, is_positive)) {
+            IF_VERBOSE(10, verbose_stream() << "could not intersect v" << v << " " << m_viable[v] << "\n");
+            unsigned budget = 10;
+            m_viable[v].intersect_eq(a, b, is_positive, budget);
+            if (budget == 0) {
+                std::cout << "budget used\n";
+                // then narrow the range using BDDs
+            }
+        }
         if (m_viable[v].is_empty())
             s.set_conflict(v);
 #else
@@ -218,6 +239,9 @@ namespace polysat {
 
     void viable::intersect_ule(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive) {
 #if NEW_VIABLE
+        // 
+        // TODO This code needs to be partitioned into self-contained pieces.
+        //
         push_viable(v);
         if (!m_viable[v].intersect_ule(a, b, c, d, is_positive)) {
             unsigned budget = 10;
@@ -235,15 +259,30 @@ namespace polysat {
                     other = alloc(ineq_entry, sz, a, b, c, d, le);
                     m_ineq_cache.insert(other);
                 }
-                le = is_positive ? other->repr : !other->repr;
+                bdd gt = is_positive ? !other->repr : other->repr;
                 other->m_activity++;
+
+                // 
+                // instead of using activity for GC, use the Move-To-Front approach 
+                // see sat/smt/bv_ackerman.h or sat/smt/euf_ackerman.h
+                // where hash table entries use a dll_base.
+                // 
+
                 // le(lo) is false: find min x >= lo, such that le(x) is false, le(x+1) is true
                 // le(hi) is false: find max x =< hi, such that le(x) is false, le(x-1) is true
                 
-                // bdd x_is_lo = m.mk_num(sz, m_viable[v].lo) == var2bits(v).var();
+                rational bound = m_viable[v].lo;
-                // bdd lo_is_sat = x_is_lo && lo;
+                if (var2bits(v).sup(gt, bound)) {
-                // if (lo_is_sat.is_false())
+                    m_viable[v].set_lo(bound);
-                //     find_min_above(lo, le);
+                    m_viable[v].set_ne(bound);
+                }
+                bound = m_viable[v].hi;
+                if (bound != 0) {
+                    bound = bound - 1;
+                    if (var2bits(v).inf(gt, bound)) {
+                        std::cout << "TODO: new upper bound " << bound << "\n";
+                    }
+                }
 
             }
 
@@ -285,8 +324,8 @@ namespace polysat {
     void viable::add_non_viable(pvar v, rational const& val) {
 #if NEW_VIABLE
         push_viable(v);
+        IF_VERBOSE(10, verbose_stream() << " v" << v << " != " << val << "\n");
         m_viable[v].set_ne(val);
-        std::cout << " v" << v << " != " << val << "\n";
         if (m_viable[v].is_empty())
             s.set_conflict(v);
 #else

src/math/polysat/viable.h

@@ -11,6 +11,11 @@ Author:
     Nikolaj Bjorner (nbjorner) 2021-03-19
     Jakob Rath 2021-04-6
 
+Notes:
+
+    NEW_VIABLE uses cheaper book-keeping, but is partial.
+    The implementation of NEW_VIABLE is atm incomplete and ad-hoc.
+    
 --*/
 #pragma once
 
@@ -18,10 +23,7 @@ Author:
 
 #include <limits>
 
-#if !NEW_VIABLE
 #include "math/dd/dd_bdd.h"
-#endif
-
 #include "math/polysat/types.h"
 #include "math/interval/mod_interval.h"
 
@@ -43,15 +45,17 @@ namespace polysat {
         unsigned m_num_bits;
         rational p2() const { return rational::power_of_two(m_num_bits); }
         bool is_max(rational const& a) const;
-        void set_lo(rational const& lo);
-        void set_hi(rational const& hi);
         void intersect_eq(rational const& a, bool is_positive);
+        void narrow(std::function<bool(rational const&)>& eval, unsigned& budget);
     public:
         viable_set(unsigned num_bits): m_num_bits(num_bits) {}
         bool is_singleton() const; 
         dd::find_t find_hint(rational const& c, rational& val) const;
         void set_ne(rational const& a) { intersect_eq(a, false); }
-        void intersect_eq(rational const& a, rational const& b, bool is_positive);
+        void set_lo(rational const& lo);
+        void set_hi(rational const& hi);
+        bool intersect_eq(rational const& a, rational const& b, bool is_positive);
+        void intersect_eq(rational const& a, rational const& b, bool is_positive, unsigned& budget);
         bool intersect_ule(rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive);
         void intersect_ule(rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive, unsigned& budget);
     };