na

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

src/math/polysat/polysat.cpp

@@ -45,6 +45,18 @@ namespace polysat {
         return !b.is_false();
     }
 
+    void solver::add_non_viable(unsigned var, rational const& val) {
+        bdd value = m_bdd.mk_true();
+        for (unsigned k = size(var); k-- > 0; ) 
+            value &= val.get_bit(k) ? m_bdd.mk_var(k) : m_bdd.mk_nvar(k);
+        m_viable[var] &= !value;        
+    }
+
+    lbool solver::find_viable(unsigned var, rational & val) {
+        return l_false;
+    }
+
+
     struct solver::t_del_var : public trail {
         solver& s;
         t_del_var(solver& s): s(s) {}
@@ -55,6 +67,8 @@ namespace polysat {
     solver::solver(trail_stack& s): 
         m_trail(s),
         m_bdd(1000),
+        m_dep_manager(m_value_manager, m_alloc),
+        m_lemma_dep(nullptr, m_dep_manager),
         m_free_vars(m_activity) {
     }
 
@@ -102,7 +116,8 @@ namespace polysat {
     }
 
     void solver::add_eq(pdd const& p, unsigned dep) {
-        constraint* c = constraint::eq(m_level, p, m_dep_manager.mk_leaf(dep));
+        p_dependency_ref d(m_dep_manager.mk_leaf(dep), m_dep_manager);
+        constraint* c = constraint::eq(m_level, p, d);
         m_constraints.push_back(c);
         add_watch(*c);
     }
@@ -135,7 +150,7 @@ namespace polysat {
 
     void solver::assign(unsigned var, unsigned index, bool value, unsigned dep) {
         m_viable[var] &= value ? m_bdd.mk_var(index) : m_bdd.mk_nvar(index);
-        m_trail.push(vector_value_trail<u_dependency*, false>(m_vdeps, var));
+        m_trail.push(vector_value_trail<p_dependency*, false>(m_vdeps, var));
         m_vdeps[var] = m_dep_manager.mk_join(m_vdeps[var], m_dep_manager.mk_leaf(dep));
         if (m_viable[var].is_false()) {
             // TBD: set conflict
@@ -357,8 +372,7 @@ namespace polysat {
         m_conflict = nullptr;
         pdd p = c.p();
         m_lemma_level = c.level();        
-        m_lemma_deps.reset();
+        m_lemma_dep = c.dep();
-        m_lemma_deps.push_back(c.dep());
         unsigned new_lemma_level = 0;
         reset_marks();
         for (auto v : c.vars())
@@ -442,27 +456,32 @@ namespace polysat {
         auto v = m_search[i];
         SASSERT(m_justification[v].is_decision());
         SASSERT(m_lemma_level <= m_justification[v].level());
-        // 
+        constraint* c = constraint::eq(m_lemma_level, p, m_lemma_dep);
-        // TBD: convert m_lemma_deps into deps.
-        // the scope of the new constraint should be confined to 
-        // m_lemma_level so could be below the current user scope.
-        // What to do in this case is TBD.
-        // 
-        unsigned level = m_lemma_level;
-        u_dependency* deps = nullptr; 
-        constraint* c = constraint::eq(level, p, deps);
         m_cjust[v].push_back(c);        
         add_lemma(c);
+        add_non_viable(v, m_value[v]);
+
+        // TBD conditions for when backjumping applies to be clarified.
+        unsigned new_level = m_justification[v].level();
+        backjump(new_level);
         // 
-        // TBD: remove current value from viable
+        // find a new decision if there is one, 
-        // m_values[v]
+        // propagate if decision is singular,
-        // 
+        // otherwise if there are no viable decisions, backjump
-        // 1. undo levels until i
+        //  and set a new conflict.
-        // 2. find a new decision if there is one, 
-        //    propagate if decision is singular,
-        //    otherwise if there are no viable decisions, backjump
-        //    and set a new conflict.
         // 
+        rational value;
+        switch (find_viable(v, value)) {
+        case l_true:
+            // unit propagation
+            break;
+        case l_undef:
+            // branch
+            break;
+        case l_false:
+            // no viable.
+            break;
+        }
     }
     
     void solver::backjump(unsigned new_level) {
@@ -490,10 +509,6 @@ namespace polysat {
     
     /**
      * Return residue of superposing p and q with respect to v.
-     * 
-     * TBD: should also collect dependencies (deps)
-     * and maximal level of constraints so learned lemma
-     * is given the appropriate level.
      */
     pdd solver::resolve(unsigned v, pdd const& p, unsigned& resolve_level) {
         resolve_level = 0;
@@ -507,7 +522,7 @@ namespace polysat {
                     // add parity condition to presere falsification
                     degree = r.degree(v);
                     resolve_level = std::max(resolve_level, c->level());
-                    m_lemma_deps.push_back(c->dep());
+                    m_lemma_dep = m_dep_manager.mk_join(m_lemma_dep.get(), c->dep());
                 }
             }
         }
@@ -538,14 +553,12 @@ namespace polysat {
 
     void solver::push() {
         push_level();
-        m_dep_manager.push_scope();
         m_scopes.push_back(m_level);
     }
 
     void solver::pop(unsigned num_scopes) {
         unsigned base_level = m_scopes[m_scopes.size() - num_scopes];
         pop_levels(m_level - base_level - 1);
-        m_dep_manager.pop_scope(num_scopes);
     }
 
     bool solver::at_base_level() const {

src/math/polysat/polysat.h

@@ -30,6 +30,23 @@ namespace polysat {
     typedef dd::pdd pdd;
     typedef dd::bdd bdd;
 
+    struct dep_value_manager {
+        void inc_ref(unsigned) {}
+        void dec_ref(unsigned) {}
+    };
+
+    struct dep_config {
+        typedef dep_value_manager value_manager;
+        typedef unsigned value;
+        typedef small_object_allocator allocator;
+        static const bool ref_count = false;
+    };
+
+    typedef dependency_manager<dep_config> poly_dep_manager;
+    typedef poly_dep_manager::dependency p_dependency;
+
+    typedef obj_ref<p_dependency, poly_dep_manager> p_dependency_ref; 
+
     enum ckind_t { eq_t, ule_t, sle_t };
 
     class constraint {
@@ -37,20 +54,20 @@ namespace polysat {
         ckind_t m_kind;
         pdd    m_poly;
         pdd    m_other;
-        u_dependency* m_dep;
+        p_dependency_ref m_dep;
         unsigned_vector m_vars;
-        constraint(unsigned lvl, pdd const& p, pdd const& q, u_dependency* dep, ckind_t k): 
+        constraint(unsigned lvl, pdd const& p, pdd const& q, p_dependency_ref& dep, ckind_t k): 
             m_level(lvl), m_kind(k), m_poly(p), m_other(q), m_dep(dep) {
             m_vars.append(p.free_vars());
             if (q != p) 
                 for (auto v : q.free_vars())
                     m_vars.insert(v);            
-        }
+            }
     public:
-        static constraint* eq(unsigned lvl, pdd const& p, u_dependency* d) { 
+        static constraint* eq(unsigned lvl, pdd const& p, p_dependency_ref& d) { 
             return alloc(constraint, lvl, p, p, d, ckind_t::eq_t); 
         }
-        static constraint* ule(unsigned lvl, pdd const& p, pdd const& q, u_dependency* d) { 
+        static constraint* ule(unsigned lvl, pdd const& p, pdd const& q, p_dependency_ref& d) { 
             return alloc(constraint, lvl, p, q, d, ckind_t::ule_t); 
         }
         ckind_t kind() const { return m_kind; }
@@ -58,7 +75,7 @@ namespace polysat {
         pdd const &  lhs() const { return m_poly; }
         pdd const &  rhs() const { return m_other; }
         std::ostream& display(std::ostream& out) const;
-        u_dependency* dep() const { return m_dep; }
+        p_dependency* dep() const { return m_dep; }
         unsigned_vector& vars() { return m_vars; }
         unsigned level() const { return m_level; }
     };
@@ -97,7 +114,10 @@ namespace polysat {
         trail_stack&             m_trail;
         scoped_ptr_vector<dd::pdd_manager> m_pdd;
         dd::bdd_manager          m_bdd;
-        u_dependency_manager     m_dep_manager;
+        dep_value_manager        m_value_manager;
+        small_object_allocator   m_alloc;
+        poly_dep_manager         m_dep_manager;
+        p_dependency_ref         m_lemma_dep;
         var_queue                m_free_vars;
 
         // Per constraint state
@@ -106,7 +126,7 @@ namespace polysat {
 
         // Per variable information
         vector<bdd>              m_viable;   // set of viable values.
-        ptr_vector<u_dependency> m_vdeps;    // dependencies for viable values
+        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
@@ -132,6 +152,20 @@ namespace polysat {
          */
         bool is_viable(unsigned var, rational const& val);
 
+        /**
+         * register that val is non-viable for var.
+         */
+        void add_non_viable(unsigned var, rational const& val);
+
+        
+        /**
+         * Find a next viable value for varible.
+         * l_false - there are no viable values.
+         * l_true  - there is only one viable value left.
+         * l_undef - there are multiple viable values, return a guess
+         */
+        lbool find_viable(unsigned var, rational & val);
+
         /**
          * undo trail operations for backtracking.
          * Each struct is a subclass of trail and implements undo().
@@ -169,7 +203,6 @@ namespace polysat {
         void set_mark(unsigned v) { m_marks[v] = m_clock; }
 
         unsigned                 m_lemma_level { 0 };
-        ptr_vector<u_dependency> m_lemma_deps;
 
         pdd isolate(unsigned v);
         pdd resolve(unsigned v, pdd const& p, unsigned& resolve_level);

src/util/dependency.h

@@ -107,11 +107,8 @@ private:
     }
 
     void unmark_todo() {
-        typename ptr_vector<dependency>::iterator it  = m_todo.begin();
+        for (auto* d : m_todo) 
-        typename ptr_vector<dependency>::iterator end = m_todo.end();
+            d->unmark();
-        for (; it != end; ++it) {
-            (*it)->unmark();
-        }
         m_todo.reset();
     }
 
@@ -193,30 +190,47 @@ public:
         return false;
     }
 
-    void linearize(dependency * d, vector<value, false> & vs) {
+    void linearize(vector<value, false>& vs) {
-        if (d) {
+        unsigned qhead = 0;
-            m_todo.reset();
+        while (qhead < m_todo.size()) {
-            d->mark();
+            dependency * d = m_todo[qhead];
-            m_todo.push_back(d);
+            qhead++;
-            unsigned qhead = 0;
+            if (d->is_leaf()) {
-            while (qhead < m_todo.size()) {
+                vs.push_back(to_leaf(d)->m_value);
-                d = m_todo[qhead];
+            }
-                qhead++;
+            else {
-                if (d->is_leaf()) {
+                for (unsigned i = 0; i < 2; i++) {
-                    vs.push_back(to_leaf(d)->m_value);
+                    dependency * child = to_join(d)->m_children[i];
-                }
+                    if (!child->is_marked()) {
-                else {
+                        m_todo.push_back(child);
-                    for (unsigned i = 0; i < 2; i++) {
+                        child->mark();
-                        dependency * child = to_join(d)->m_children[i];
-                        if (!child->is_marked()) {
-                            m_todo.push_back(child);
-                            child->mark();
-                        }
                     }
                 }
             }
-            unmark_todo();
         }
+        unmark_todo();
+    }
+
+    void linearize(dependency * d, vector<value, false> & vs) {
+        if (!d) 
+            return;
+        m_todo.reset();
+        d->mark();
+        m_todo.push_back(d);
+        linearize(vs);
+    }
+
+    void linearize(ptr_vector<dependency>& deps, vector<value, false> & vs) {
+        if (deps.empty())
+            return;
+        m_todo.reset();
+        for (auto* d : deps) {
+            if (d && !d->is_marked()) {
+                d->mark();
+                m_todo.push_back(d);
+            }
+        }
+        linearize(vs);
     }
 };
 
@@ -304,6 +318,10 @@ public:
         return m_dep_manager.linearize(d, vs);
     }    
 
+    void linearize(ptr_vector<dependency>& d, vector<value, false> & vs) {
+        return m_dep_manager.linearize(d, vs);
+    }    
+    
     void reset() {
         m_allocator.reset();
     }