fixes to reset

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

src/math/dd/dd_pdd.cpp

@@ -30,7 +30,27 @@ namespace dd {
         m_disable_gc = false;
         m_is_new_node = false;
         m_semantics = s;
+        unsigned_vector l2v;
+        for (unsigned i = 0; i < num_vars; ++i) l2v.push_back(i);
+        init_nodes(l2v);
+    }
 
+    pdd_manager::~pdd_manager() {
+        if (m_spare_entry) {
+            m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry);
+            m_spare_entry = nullptr;
+        }
+        reset_op_cache();
+    }
+
+    void pdd_manager::reset(unsigned_vector const& level2var) {
+        reset_op_cache();
+        m_node_table.reset();
+        m_nodes.reset();
+        init_nodes(level2var);
+    }
+
+    void pdd_manager::init_nodes(unsigned_vector const& l2v) {
         // add dummy nodes for operations, and 0, 1 pdds.
         for (unsigned i = 0; i < pdd_no_op; ++i) {
             m_nodes.push_back(node());
@@ -41,23 +61,30 @@ namespace dd {
         init_value(rational::one(), 1);
         SASSERT(is_val(0));
         SASSERT(is_val(1));
-
+        alloc_free_nodes(1024 + l2v.size());   
-        alloc_free_nodes(1024 + num_vars);
+        init_vars(l2v);
-        
-        // add variables
-        for (unsigned i = 0; i < num_vars; ++i) {
-            reserve_var(i);
-        }            
     }
 
-    pdd_manager::~pdd_manager() {
+    void pdd_manager::init_vars(unsigned_vector const& level2var) {
-        if (m_spare_entry) {
+        unsigned n = level2var.size();
-            m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry);
+        m_level2var.resize(n);
+        m_var2level.resize(n);
+        m_var2pdd.resize(n);
+        for (unsigned l = 0; l < n; ++l) {
+            unsigned v = level2var[l];
+            m_var2pdd[v] = make_node(l, zero_pdd, one_pdd);
+            m_nodes[m_var2pdd[v]].m_refcount = max_rc;
+            m_var2level[v] = l;
+            m_level2var[l] = v;
         }
+    }
+
+    void pdd_manager::reset_op_cache() {
         for (auto* e : m_op_cache) {
             SASSERT(e != m_spare_entry);
             m_alloc.deallocate(sizeof(*e), e);
         }
+        m_op_cache.reset();
     }
 
     pdd pdd_manager::add(pdd const& a, pdd const& b) { return pdd(apply(a.root, b.root, pdd_add_op), this); }
@@ -645,10 +672,7 @@ namespace dd {
 
     void pdd_manager::try_gc() {
         gc();        
-        for (auto* e : m_op_cache) {
+        reset_op_cache();
-            m_alloc.deallocate(sizeof(*e), e);
-        }
-        m_op_cache.reset();
         SASSERT(m_op_cache.empty());
         SASSERT(well_formed());
     }
@@ -667,14 +691,6 @@ namespace dd {
         reserve_var(i);
         return pdd(m_var2pdd[i], this);        
     }
-
-    void pdd_manager::set_level2var(unsigned_vector const& level2var) {
-        SASSERT(level2var.size() == m_level2var.size());
-        for (unsigned i = 0; i < level2var.size(); ++i) {
-            m_var2level[level2var[i]] = i;
-            m_level2var[i] = level2var[i];
-        }
-    }
     
     unsigned pdd_manager::dag_size(pdd const& b) {
         init_mark();

src/math/dd/dd_pdd.h

@@ -160,6 +160,10 @@ namespace dd {
         unsigned_vector            m_free_values;
         rational                   m_freeze_value;
 
+        void reset_op_cache();
+        void init_nodes(unsigned_vector const& l2v);
+        void init_vars(unsigned_vector const& l2v);
+
         PDD make_node(unsigned level, PDD l, PDD r);
         PDD insert_node(node const& n);
         bool is_new_node() const { return m_is_new_node; }
@@ -237,8 +241,8 @@ namespace dd {
         pdd_manager(unsigned nodes, semantics s = free_e);
         ~pdd_manager();
 
+        void reset(unsigned_vector const& level2var);
         void set_max_num_nodes(unsigned n) { m_max_num_nodes = n; }
-        void set_level2var(unsigned_vector const& level2var);  
         unsigned_vector const& get_level2var() const { return m_level2var; }
 
         pdd mk_var(unsigned i);

src/math/grobner/pdd_grobner.cpp

@@ -240,17 +240,25 @@ namespace dd {
         equation_vector trivial;
         unsigned j = 0;
         for (equation* src : linear) {
-            equation_vector const& uses = use_list[src->poly().var()];
+            unsigned v = src->poly().var();
+            equation_vector const& uses = use_list[v];
+            TRACE("grobner", 
+                  display(tout << "uses of: ", *src) << "\n";
+                  for (equation* e : uses) {
+                      display(tout, *e) << "\n";
+                  });
             bool changed_leading_term;
             bool all_reduced = true;
             for (equation* dst : uses) {
                 if (src == dst || is_trivial(*dst)) {
                     continue;                    
                 }
-                if (!src->poly().is_binary() && !dst->poly().is_linear()) {
+                pdd q = dst->poly();
+                if (!src->poly().is_binary() && !q.is_linear()) {
                     all_reduced = false;
                     continue;
                 }
+                remove_from_use(dst, use_list, v);
                 simplify_using(*dst, *src, changed_leading_term);
                 if (is_trivial(*dst)) {
                     trivial.push_back(dst);
@@ -264,6 +272,9 @@ namespace dd {
                     pop_equation(dst);
                     push_equation(to_simplify, dst);
                 }
+                // v has been eliminated.
+                SASSERT(!m.free_vars(dst->poly()).contains(v));
+                add_to_use(dst, use_list);                
             }          
             if (all_reduced) {
                 linear[j++] = src;              
@@ -466,6 +477,16 @@ namespace dd {
         }
     }
 
+    void grobner::remove_from_use(equation* e, use_list_t& use_list, unsigned except_v) {
+        unsigned_vector const& fv = m.free_vars(e->poly());
+        for (unsigned v : fv) {
+            if (v != except_v) {
+                use_list.reserve(v + 1);
+                use_list[v].erase(e);
+            }
+        }
+    }
+
     grobner::use_list_t grobner::get_use_list() {
         use_list_t use_list;
         for (equation * e : m_to_simplify) {
@@ -823,6 +844,15 @@ namespace dd {
             }
         }
 
+        if (!head_vars.empty()) {
+            for (auto * e : m_to_simplify) {
+                for (auto v : m.free_vars(e->poly())) VERIFY(!head_vars.contains(v));
+            }
+            for (auto * e : m_processed) {
+                for (auto v : m.free_vars(e->poly())) VERIFY(!head_vars.contains(v));
+            }
+        }
+
         // equations in to_simplify have correct indices
         // they are labeled as non-processed
         // their top-most variable is watched

src/math/grobner/pdd_grobner.h

@@ -168,6 +168,7 @@ private:
     use_list_t get_use_list();
     void add_to_use(equation* e, use_list_t& use_list);
     void remove_from_use(equation* e, use_list_t& use_list);
+    void remove_from_use(equation* e, use_list_t& use_list, unsigned except_v);
 
     bool simplify_cc_step();
     bool simplify_elim_pure_step();

src/test/bdd.cpp

@@ -58,7 +58,7 @@ namespace dd {
         SASSERT(c2 == ((v0 && v1) || v1 || !v0));
     }
 
-    void test4() {
+    static void test4() {
         bdd_manager m(3);
         bdd v0 = m.mk_var(0);
         bdd v1 = m.mk_var(1);

src/test/pdd.cpp

@@ -83,10 +83,31 @@ namespace dd {
         std::cout << e << "\n";
     }
 
+    static void test_reset() {
+        std::cout << "\ntest reset\n";
+        pdd_manager m(4);
+        pdd a = m.mk_var(0);
+        pdd b = m.mk_var(1);
+        pdd c = m.mk_var(2);
+        pdd d = m.mk_var(3);
+        std::cout << (a + b)*(c + d) << "\n";
+
+        unsigned_vector l2v;
+        for (unsigned i = 0; i < 4; ++i) 
+            l2v.push_back(3 - i);
+        m.reset(l2v);
+        a = m.mk_var(0);
+        b = m.mk_var(1);
+        c = m.mk_var(2);
+        d = m.mk_var(3);
+        std::cout << (a + b)*(c + d) << "\n";
+    }
+
 }
 
 void tst_pdd() {
     dd::test1();
     dd::test2();
     dd::test3();
+    dd::test_reset();
 }