na

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

src/math/dd/dd_pdd.cpp

@@ -126,7 +126,7 @@ namespace dd {
      * Example: 2^4*x + 2 is non-zero for every x.
      */
 
-    bool pdd_manager::is_non_zero(PDD p) {
+    bool pdd_manager::is_never_zero(PDD p) {
         if (is_val(p))
             return !is_zero(p);
         if (m_semantics != mod2N_e)

src/math/dd/dd_pdd.h

@@ -206,7 +206,7 @@ namespace dd {
         inline bool is_one(PDD p) const { return p == one_pdd; } 
         inline bool is_val(PDD p) const { return m_nodes[p].is_val(); }
         inline bool is_internal(PDD p) const { return m_nodes[p].is_internal(); }
-        bool is_non_zero(PDD p);
+        bool is_never_zero(PDD p);
         inline unsigned level(PDD p) const { return m_nodes[p].m_level; }
         inline unsigned var(PDD p) const { return m_level2var[level(p)]; }
         inline PDD lo(PDD p) const { return m_nodes[p].m_lo; }
@@ -343,7 +343,7 @@ namespace dd {
         bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } 
         bool is_binary() const { return m.is_binary(root); }
         bool is_monomial() const { return m.is_monomial(root); }
-        bool is_non_zero() const { return m.is_non_zero(root); }
+        bool is_never_zero() const { return m.is_never_zero(root); }
         bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
 
         pdd operator-() const { return m.minus(*this); }

src/math/polysat/polysat.cpp

@@ -73,20 +73,18 @@ namespace polysat {
         return l_undef;
     }
 
-
     struct solver::t_del_var : public trail {
         solver& s;
         t_del_var(solver& s): s(s) {}
         void undo() override { s.del_var(); }
     };
     
-    
     solver::solver(trail_stack& s, reslimit& lim): 
         m_trail(s),
         m_lim(lim),
         m_bdd(1000),
-        m_dep_manager(m_value_manager, m_alloc),
+        m_dm(m_value_manager, m_alloc),
-        m_conflict_dep(nullptr, m_dep_manager),
+        m_conflict_dep(nullptr, m_dm),
         m_free_vars(m_activity) {
     }
 
@@ -108,7 +106,7 @@ namespace polysat {
         m_value.push_back(rational::zero());
         m_justification.push_back(justification::unassigned());
         m_viable.push_back(m_bdd.mk_true());
-        m_vdeps.push_back(m_dep_manager.mk_empty());
+        m_vdeps.push_back(m_dm.mk_empty());
         m_cjust.push_back(constraints());
         m_watch.push_back(ptr_vector<constraint>());
         m_activity.push_back(0);
@@ -134,7 +132,7 @@ namespace polysat {
     }
 
     void solver::add_eq(pdd const& p, unsigned dep) {
-        p_dependency_ref d(mk_dep(dep), m_dep_manager);
+        p_dependency_ref d(mk_dep(dep), m_dm);
         constraint* c = constraint::eq(m_level, p, d);
         m_constraints.push_back(c);
         add_watch(*c);
@@ -178,7 +176,7 @@ namespace polysat {
         if (!dep)
             return;
         m_trail.push(vector_value_trail<p_dependency*, false>(m_vdeps, var));
-        m_vdeps[var] = m_dep_manager.mk_join(m_vdeps[var], dep);
+        m_vdeps[var] = m_dm.mk_join(m_vdeps[var], dep);
     }
 
     bool solver::can_propagate() {
@@ -232,15 +230,11 @@ namespace polysat {
             }
         }        
 
-        vector<std::pair<unsigned, rational>> sub;
-        for (auto w : vars) 
-            if (is_assigned(w))
-                sub.push_back(std::make_pair(w, m_value[w]));
 
-        auto p = c.p().subst_val(sub);
+        auto p = c.p().subst_val(m_sub);
         if (p.is_zero()) 
             return false;
-        if (p.is_non_zero()) {
+        if (p.is_never_zero()) {
             // we could tag constraint to allow early substitution before 
             // swapping watch variable in case we can detect conflict earlier.
             set_conflict(c);
@@ -266,7 +260,7 @@ namespace polysat {
             VERIFY(a.mult_inverse(sz, inv_a)); 
             rational val = mod(inv_a * -b, rational::power_of_two(sz));
             m_cjust[other_var].push_back(&c);
-            propagate(other_var, val, justification::propagation(m_level));
+            propagate(other_var, val, c);
             return false;
         }
 
@@ -277,12 +271,11 @@ namespace polysat {
         return false;
     }
 
-    void solver::propagate(unsigned var, rational const& val, justification const& j) {
+    void solver::propagate(unsigned var, rational const& val, constraint& c) {
-        SASSERT(j.is_propagation());
         if (is_viable(var, val)) 
-            assign_core(var, val, j);        
+            assign_core(var, val, justification::propagation(m_level));        
         else 
-            set_conflict(*m_cjust[var].back());
+            set_conflict(c);
     }
 
     void solver::push_level() {
@@ -312,9 +305,8 @@ namespace polysat {
      */
     void solver::pop_assignment() {
         while (!m_search.empty() && m_justification[m_search.back()].level() > m_level) {
-            auto v = m_search.back();
             undo_var(m_search.back());
-            m_search.pop_back();
+            pop_search();
         }
     }
     
@@ -322,7 +314,18 @@ namespace polysat {
         m_justification[v] = justification::unassigned();
         m_free_vars.unassign_var_eh(v);
         m_cjust[v].reset();
-        m_viable[v] = m_bdd.mk_true();
+        m_viable[v] = m_bdd.mk_true(); // TBD does not work with external bit-assignments
+    }
+
+    void solver::pop_search() {
+        m_search.pop_back();
+        m_sub.pop_back();
+    }
+
+    void solver::push_search(unsigned var, rational const& val) {
+        m_search.push_back(var);
+        m_value[var] = val;
+        m_sub.push_back(std::make_pair(var, val));
     }
 
     void solver::add_watch(constraint& c) {
@@ -361,7 +364,7 @@ namespace polysat {
         unsigned var = m_free_vars.next_var();
         switch (find_viable(var, val)) {
         case l_false:
-            set_conflict(m_cjust[var]);
+            set_conflict(var);
             break;
         case l_true:
             assign_core(var, val, justification::propagation(m_level));
@@ -375,15 +378,30 @@ namespace polysat {
 
     void solver::assign_core(unsigned var, rational const& val, justification const& j) {
         SASSERT(is_viable(var, val));
-        m_search.push_back(var);
+        push_search(var, val);
-        m_value[var] = val;
         m_justification[var] = j; 
     }
 
+    void solver::set_conflict(constraint& c) { 
+        SASSERT(m_conflict_cs.empty());
+        m_conflict_cs.push_back(&c); 
+        m_conflict_dep = nullptr;
+    }
+
+    void solver::set_conflict(unsigned v) {
+        SASSERT(m_conflict_cs.empty());
+        m_conflict_cs.append(m_cjust[v]);
+        m_conflict_dep = m_vdeps[v];
+        if (m_cjust[v].empty())
+            m_conflict_cs.push_back(nullptr);
+    }
+
+        
     /**
      * Conflict resolution.
-     * - m_conflict are constraints that are infeasible in the current assignment.
+     * - m_conflict_cs are constraints that are infeasible in the current assignment.
-     * 1. walk m_search from top down until last variable in m_conflict.
+     * - m_conflict_dep are dependencies for infeasibility
+     * 1. walk m_search from top down until last variable in m_conflict_cs.
      * 2. resolve constraints in m_cjust to isolate lowest degree polynomials
      *    using variable.
      *    Use Olm-Seidl division by powers of 2 to preserve invertibility.
@@ -399,12 +417,10 @@ namespace polysat {
      * 
      */
     void solver::resolve_conflict() {
+
         vector<pdd> ps = init_conflict();
         unsigned v = UINT_MAX;
         unsigned i = m_search.size();
-        vector<std::pair<unsigned, rational>> sub;
-        for (auto w : m_search) 
-            sub.push_back(std::make_pair(w, m_value[w]));
 
         for (; i-- > 0; ) {
             v = m_search[i];
@@ -422,12 +438,12 @@ namespace polysat {
                 return;
             }
             pdd r = resolve(v, ps);
-            pdd rval = r.subst_val(sub);
+            pdd rval = r.subst_val(m_sub);
-            if (r.is_val() && rval.is_non_zero()) {
+            if (r.is_val() && rval.is_never_zero()) {
                 report_unsat();
                 return;
             }
-            if (!rval.is_non_zero()) {
+            if (!rval.is_never_zero()) {
                 backtrack(i);
                 return;
             }
@@ -442,28 +458,23 @@ namespace polysat {
     }
 
     vector<pdd> solver::init_conflict() {
-        SASSERT(!m_conflict.empty());
+        SASSERT(!m_conflict_cs.empty());
+        m_conflict_level = 0;
         vector<pdd> ps;
         reset_marks();
-        m_conflict_level = 0;
+        for (auto* c : m_conflict_cs) {
-        m_conflict_dep = nullptr;
+            if (!c)
-        for (auto* c : m_conflict) {
+                continue;
             for (auto v : c->vars())
                 set_mark(v);
             ps.push_back(c->p());
             m_conflict_level = std::max(m_conflict_level, c->level());        
-            m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep, c->dep());
+            m_conflict_dep = m_dm.mk_join(m_conflict_dep, c->dep());
         }
-        m_conflict.reset();
+        m_conflict_cs.reset();
         return ps;
     }
 
-    /**
-     * TBD: m_conflict_dep is a justification that m_value[v] is not viable.
-     * it is currently not yet being accounted for.
-     * A more general data-structure could be to maintain a p_dependency
-     * with each variable state. The dependencies are augmented on backtracking.
-     */
     void solver::backtrack(unsigned i) {
         do {
             auto v = m_search[i];
@@ -481,16 +492,17 @@ namespace polysat {
 
     void solver::report_unsat() {
         backjump(base_level());
-        m_conflict.push_back(nullptr);
+        SASSERT(m_conflict_cs.empty());
+        m_conflict_cs.push_back(nullptr);
     }
 
     void solver::unsat_core(unsigned_vector& deps) {
         deps.reset();
-        for (auto* c : m_conflict) {
+        for (auto* c : m_conflict_cs) {
             if (c)
-                m_conflict_dep = m_dep_manager.mk_join(c->dep(), m_conflict_dep);
+                m_conflict_dep = m_dm.mk_join(c->dep(), m_conflict_dep);
         }
-        m_dep_manager.linearize(m_conflict_dep, deps);
+        m_dm.linearize(m_conflict_dep, deps);
     }
 
 
@@ -520,16 +532,15 @@ namespace polysat {
             backjump(new_level + 1);        
         while (m_search.back() != v) {
             undo_var(m_search.back());
-            m_search.pop_back();
+            pop_search();
         }
         SASSERT(!m_search.empty());
         SASSERT(m_search.back() == v);
-        m_search.pop_back();
+        pop_search();
         add_non_viable(v, m_value[v]);
         add_viable_dep(v, m_conflict_dep);
         m_qhead = m_search.size();
         rational value;
-        m_conflict_dep = nullptr;
         switch (find_viable(v, value)) {
         case l_true: 
             assign_core(v, value, justification::propagation(new_level));
@@ -538,7 +549,7 @@ namespace polysat {
             assign_core(v, value, justification::decision(new_level));
             break;
         case l_false:
-            set_conflict(m_cjust[v]);
+            set_conflict(v);
             break;
         }
     }
@@ -569,6 +580,7 @@ namespace polysat {
         auto const& cs = m_cjust[v];
         pdd r = isolate(v, ps);
         auto degree = r.degree(v);
+        m_conflict_dep = m_dm.mk_join(m_conflict_dep, m_vdeps[v]);
         while (degree > 0) {
             for (auto * c : cs) {
                 if (degree >= c->p().degree(v)) {
@@ -576,7 +588,7 @@ namespace polysat {
                     // add parity condition to presere falsification
                     degree = r.degree(v);
                     m_conflict_level = std::max(m_conflict_level, c->level());
-                    m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep.get(), c->dep());
+                    m_conflict_dep = m_dm.mk_join(m_conflict_dep.get(), c->dep());
                 }
             }
         }
@@ -624,6 +636,10 @@ namespace polysat {
     }
         
     std::ostream& solver::display(std::ostream& out) const {
+        for (auto v : m_search) {
+            out << "v" << v << " := " << m_value[v] << "\n";
+            out << m_viable[v] << "\n";
+        }
         for (auto* c : m_constraints)
             out << *c << "\n";
         for (auto* c : m_redundant)

src/math/polysat/polysat.h

@@ -32,6 +32,7 @@ namespace polysat {
     typedef dd::bdd bdd;
 
     const unsigned null_dependency = UINT_MAX;
+    const unsigned null_var = UINT_MAX;
 
     struct dep_value_manager {
         void inc_ref(unsigned) {}
@@ -120,9 +121,10 @@ namespace polysat {
         dd::bdd_manager          m_bdd;
         dep_value_manager        m_value_manager;
         small_object_allocator   m_alloc;
-        poly_dep_manager         m_dep_manager;
+        poly_dep_manager         m_dm;
-        p_dependency_ref         m_conflict_dep;
         var_queue                m_free_vars;
+        p_dependency_ref         m_conflict_dep;
+        ptr_vector<constraint>   m_conflict_cs;
 
         // Per constraint state
         scoped_ptr_vector<constraint>   m_constraints;
@@ -133,7 +135,7 @@ namespace polysat {
         ptr_vector<p_dependency> m_vdeps;    // dependencies for viable values
         vector<rational>         m_value;    // assigned value
         vector<justification>    m_justification; // justification for variable assignment
-        vector<constraints>      m_cjust;    // constraints used for justification
+        vector<constraints>      m_cjust;    // constraints justifying variable range.
         vector<constraints>      m_watch;    // watch list datastructure into constraints.
         unsigned_vector          m_activity; 
         vector<pdd>              m_vars;
@@ -141,6 +143,8 @@ namespace polysat {
 
         // search state that lists assigned variables
         unsigned_vector          m_search;
+        vector<std::pair<unsigned, rational>> m_sub;
+
         unsigned                 m_qhead { 0 };
         unsigned                 m_level { 0 };
 
@@ -190,6 +194,9 @@ namespace polysat {
         void pop_assignment();
         void pop_constraints(scoped_ptr_vector<constraint>& cs);
 
+        void push_search(unsigned v, rational const& val);
+        void pop_search();
+
         void assign_core(unsigned var, rational const& val, justification const& j);
 
         bool is_assigned(unsigned var) const { return !m_justification[var].is_unassigned(); }
@@ -197,13 +204,13 @@ namespace polysat {
         void propagate(unsigned v);
         bool propagate(unsigned v, constraint& c);
         bool propagate_eq(unsigned v, constraint& c);
-        void propagate(unsigned var, rational const& val, justification const& j);
+        void propagate(unsigned var, rational const& val, constraint& c);
         void erase_watch(unsigned v, constraint& c);
         void erase_watch(constraint& c);
         void add_watch(constraint& c);
 
-        void set_conflict(constraint& c) { m_conflict.push_back(&c); }
+        void set_conflict(constraint& c);
-        void set_conflict(ptr_vector<constraint>& cs) { m_conflict.append(cs); }
+        void set_conflict(unsigned v);
 
         unsigned_vector m_marks;
         unsigned        m_clock { 0 };
@@ -219,7 +226,7 @@ namespace polysat {
         bool can_decide() const { return !m_free_vars.empty(); }
         void decide();
 
-        p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dep_manager.mk_leaf(dep); }
+        p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); }
 
         bool is_conflict() const { return !m_conflict.empty(); }
         bool at_base_level() const;

src/test/pdd.cpp

@@ -314,12 +314,12 @@ public :
         std::cout << "sub 2 " << p.subst_val(sub2) << "\n";
         std::cout << "sub 3 " << p.subst_val(sub3) << "\n";
 
-        std::cout << "expect 1 " << (2*a + 1).is_non_zero() << "\n";
+        std::cout << "expect 1 " << (2*a + 1).is_never_zero() << "\n";
-        std::cout << "expect 1 " << (2*a*b + 2*b + 1).is_non_zero() << "\n";
+        std::cout << "expect 1 " << (2*a*b + 2*b + 1).is_never_zero() << "\n";
-        std::cout << "expect 0 " << (2*a + 2).is_non_zero() << "\n";
+        std::cout << "expect 0 " << (2*a + 2).is_never_zero() << "\n";
-        SASSERT((2*a + 1).is_non_zero());
+        SASSERT((2*a + 1).is_never_zero());
-        SASSERT((2*a + 2*b + 1).is_non_zero());
+        SASSERT((2*a + 2*b + 1).is_never_zero());
-        SASSERT(!(2*a*b + 3*b + 2).is_non_zero());
+        SASSERT(!(2*a*b + 3*b + 2).is_never_zero());
     }
 
 };