move to stash model

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

src/math/polysat/polysat.cpp

@@ -84,6 +84,7 @@ namespace polysat {
         m_lim(lim),
         m_bdd(1000),
         m_dm(m_value_manager, m_alloc),
+        m_vdeps(m_dm),
         m_conflict_dep(nullptr, m_dm),
         m_free_vars(m_activity) {
     }
@@ -175,8 +176,7 @@ namespace polysat {
     void solver::add_viable_dep(unsigned var, p_dependency* dep) {
         if (!dep)
             return;
-        m_trail.push(vector_value_trail<p_dependency*, false>(m_vdeps, var));
-        m_vdeps[var] = m_dm.mk_join(m_vdeps[var], dep);
+        m_vdeps[var] = m_dm.mk_join(m_vdeps.get(var), dep);
     }
 
     bool solver::can_propagate() {
@@ -314,6 +314,7 @@ namespace polysat {
         m_justification[v] = justification::unassigned();
         m_free_vars.unassign_var_eh(v);
         m_cjust[v].reset();
+        m_vdeps[v] = nullptr;
         m_viable[v] = m_bdd.mk_true(); // TBD does not work with external bit-assignments
     }
 
@@ -345,7 +346,7 @@ namespace polysat {
     }
 
     void solver::erase_watch(unsigned v, constraint& c) {
-        if (v == UINT_MAX)
+        if (v == null_var)
             return;
         auto& wlist = m_watch[v];
         unsigned sz = wlist.size();
@@ -391,7 +392,7 @@ namespace polysat {
     void solver::set_conflict(unsigned v) {
         SASSERT(m_conflict_cs.empty());
         m_conflict_cs.append(m_cjust[v]);
-        m_conflict_dep = m_vdeps[v];
+        m_conflict_dep = m_vdeps.get(v);
         if (m_cjust[v].empty())
             m_conflict_cs.push_back(nullptr);
     }
@@ -419,11 +420,9 @@ namespace polysat {
     void solver::resolve_conflict() {
 
         vector<pdd> ps = init_conflict();
-        unsigned v = UINT_MAX;
-        unsigned i = m_search.size();
 
-        for (; i-- > 0; ) {
-            v = m_search[i];
+        for (unsigned i = m_search.size(); i-- > 0; ) {
+            unsigned v = m_search[i];
             if (!is_marked(v))
                 continue;
             justification& j = m_justification[v];
@@ -526,33 +525,34 @@ namespace polysat {
     void solver::revert_decision(unsigned i) {
         auto v = m_search[i];
         SASSERT(m_justification[v].is_decision());
-
-        unsigned new_level = m_justification[v].level();
-        if (new_level < m_level)
-            backjump(new_level + 1);        
-        while (m_search.back() != v) {
-            undo_var(m_search.back());
-            pop_search();
-        }
-        SASSERT(!m_search.empty());
-        SASSERT(m_search.back() == v);
-        pop_search();
+        stash_deps(v);
+        backjump(m_justification[v].level()-1);
+        unstash_deps(v);
         add_non_viable(v, m_value[v]);
         add_viable_dep(v, m_conflict_dep);
-        m_qhead = m_search.size();
         rational value;
         switch (find_viable(v, value)) {
         case l_true: 
-            assign_core(v, value, justification::propagation(new_level));
+            assign_core(v, value, justification::propagation(m_level));
             break;
         case l_undef:
-            assign_core(v, value, justification::decision(new_level));
+            push_level();
+            assign_core(v, value, justification::decision(m_level));
             break;
         case l_false:
             set_conflict(v);
             break;
         }
     }
+
+    void solver::stash_deps(unsigned v) {
+        // save vdeps[v] and cjust[v] aside
+        // they are removed by backtracking
+    }
+
+    void solver::unstash_deps(unsigned v) {
+        // retrieve saved vdeps[v] and cjust[v] 
+    }
     
     void solver::backjump(unsigned new_level) {
         unsigned num_levels = m_level - new_level;
@@ -580,7 +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]);
+        m_conflict_dep = m_dm.mk_join(m_conflict_dep, m_vdeps.get(v));
         while (degree > 0) {
             for (auto * c : cs) {
                 if (degree >= c->p().degree(v)) {

src/math/polysat/polysat.h

@@ -22,6 +22,7 @@ Author:
 #include "util/rlimit.h"
 #include "util/scoped_ptr_vector.h"
 #include "util/var_queue.h"
+#include "util/ref_vector.h"
 #include "math/dd/dd_pdd.h"
 #include "math/dd/dd_bdd.h"
 
@@ -50,6 +51,7 @@ namespace polysat {
     typedef poly_dep_manager::dependency p_dependency;
 
     typedef obj_ref<p_dependency, poly_dep_manager> p_dependency_ref; 
+    typedef ref_vector<p_dependency, poly_dep_manager> p_dependency_refv;
 
     enum ckind_t { eq_t, ule_t, sle_t };
 
@@ -132,7 +134,7 @@ namespace polysat {
 
         // Per variable information
         vector<bdd>              m_viable;   // set of viable values.
-        ptr_vector<p_dependency> m_vdeps;    // dependencies for viable values
+        p_dependency_refv        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 justifying variable range.
@@ -226,6 +228,9 @@ namespace polysat {
         bool can_decide() const { return !m_free_vars.empty(); }
         void decide();
 
+        void stash_deps(unsigned v);
+        void unstash_deps(unsigned v);
+
         p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); }
 
         bool is_conflict() const { return !m_conflict.empty(); }