local

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

src/sat/sat_bdd.cpp

@@ -43,6 +43,8 @@ namespace sat {
         m_max_num_bdd_nodes = 1 << 24; // up to 16M nodes
         m_mark_level = 0;
         alloc_free_nodes(1024 + num_vars);
+        m_disable_gc = false;
+        m_is_new_node = false;
         
         // add variables
         for (unsigned i = 0; i < num_vars; ++i) {
@@ -203,6 +205,7 @@ namespace sat {
     }
 
     bdd_manager::BDD bdd_manager::make_node(unsigned level, BDD l, BDD r) {
+        m_is_new_node = false;
         if (l == r) {
             return l;
         }
@@ -214,7 +217,7 @@ namespace sat {
         }
         e->get_data().m_refcount = 0;
         bool do_gc = m_free_nodes.empty();
-        if (do_gc) {
+        if (do_gc && !m_disable_gc) {
             gc();
             e = m_node_table.insert_if_not_there2(n);
             e->get_data().m_refcount = 0;
@@ -223,15 +226,14 @@ namespace sat {
             if (m_nodes.size() > m_max_num_bdd_nodes) {
                 throw mem_out();
             }
-            e->get_data().m_index = m_nodes.size();
-            m_nodes.push_back(e->get_data());
             alloc_free_nodes(m_nodes.size()/2);
         }
-        else {
+
+        SASSERT(!m_free_nodes.empty());
         e->get_data().m_index = m_free_nodes.back();
         m_nodes[e->get_data().m_index] = e->get_data();
         m_free_nodes.pop_back();        
-        }
+        m_is_new_node = true;
         return e->get_data().m_index;
     }
 
@@ -241,10 +243,45 @@ namespace sat {
 
     void bdd_manager::sift_up(unsigned lvl) {
         // exchange level and level + 1.
-#if 0
+        m_S.reset();
-        m_relevel.reset(); // nodes to be re-leveled.
+        m_T.reset();
+        m_disable_gc = true;
 
         for (unsigned n : m_level2nodes[lvl + 1]) {
+            BDD l = lo(n);
+            BDD h = hi(n);
+            if (l == 0 && h == 0) continue;
+            if ((is_const(l) || level(l) != lvl) &&
+                (is_const(h) || level(h) != lvl)) {
+                m_S.push_back(n);
+            }
+            else {
+                m_T.push_back(n);
+            }
+            m_node_table.remove(m_nodes[n]);
+        }
+
+        for (unsigned n : m_level2nodes[lvl]) {
+            bdd_node& node = m_nodes[n];
+            m_node_table.remove(node);
+            if (m_max_parent[n] == lvl + 1 && node.m_refcount == 0) {
+                node.set_internal();
+                m_free_nodes.push_back(n);
+            }
+            else {
+                node.m_level = lvl + 1;
+                m_node_table.insert(node);
+            }
+        }
+
+        for (unsigned n : m_S) {
+            m_nodes[n].m_level = lvl;
+            m_node_table.insert(m_nodes[n]);
+        }
+
+        std::swap(m_level2nodes[lvl], m_level2nodes[lvl + 1]);
+
+        for (unsigned n : m_T) {
             BDD l = lo(n);
             BDD h = hi(n);
             if (l == 0 && h == 0) continue;
@@ -264,28 +301,42 @@ namespace sat {
                 c = d = h;
             }
 
-            push(make_node(lvl, a, c));
+            unsigned ac = make_node(lvl, a, c);
-            push(make_node(lvl, b, d));
+            if (is_new_node()) {
-            m_node_table.remove(m_nodes[n]);
+                m_level2nodes[lvl].push_back(ac);
-            m_nodes[n].m_lo = read(2);
+                m_max_parent.setx(ac, lvl + 1, 0);
-            m_nodes[n].m_hi = read(1);
+            }
-            m_relevel.push_back(l);
+            unsigned bd = make_node(lvl, b, d);
-            m_relevel.push_back(r);
+            if (is_new_node()) {
-            // TBD: read(2); read(1); should be inserted into m_level2nodes[lvl];
+                m_level2nodes[lvl].push_back(bd);
-            pop(2);
+                m_max_parent.setx(bd, lvl + 1, 0);
+            }
+            m_nodes[n].m_lo = ac;
+            m_nodes[n].m_hi = bd;
             m_node_table.insert(m_nodes[n]);
         }
         unsigned v = m_level2var[lvl];
         unsigned w = m_level2var[lvl+1];
         std::swap(m_level2var[lvl], m_level2var[lvl+1]);
         std::swap(m_var2level[v], m_var2level[w]);
-        for (unsigned n : m_relevel) {
+        m_disable_gc = false;
-            if (level(n) == lvl) {
-                // whoever points to n uses it as if it is level lvl + 1.
-                m_level2nodes[m_node2levelpos[n]];
     }
+
+    void bdd_manager::init_reorder() {
+        m_level2nodes.reset();
+        unsigned sz = m_nodes.size();
+        m_max_parent.fill(sz, 0);
+        for (unsigned i = 0; i < m_level2var.size(); ++i) {
+            m_level2nodes.push_back(unsigned_vector());
+        }
+        for (unsigned i = 0; i < sz; ++i) {
+            bdd_node const& n = m_nodes[i];
+            if (n.is_internal()) continue;
+            SASSERT(i == m_nodes[i].m_index);
+            m_level2nodes[n.m_level].push_back(i);
+            m_max_parent[n.m_lo] = std::max(m_max_parent[n.m_lo], n.m_level);
+            m_max_parent[n.m_hi] = std::max(m_max_parent[n.m_hi], n.m_level);
         }
-#endif
     }
 
     bdd bdd_manager::mk_var(unsigned i) {
@@ -498,7 +549,7 @@ namespace sat {
         }
         for (unsigned i = m_nodes.size(); i-- > 2; ) {
             if (!reachable[i]) {
-                m_nodes[i].m_lo = m_nodes[i].m_hi = 0;
+                m_nodes[i].set_internal();
                 m_free_nodes.push_back(i);                
             }
         }
@@ -559,7 +610,7 @@ namespace sat {
     std::ostream& bdd_manager::display(std::ostream& out) {
         for (unsigned i = 0; i < m_nodes.size(); ++i) {
             bdd_node const& n = m_nodes[i];
-            if (n.m_lo == 0 && n.m_hi == 0) continue;
+            if (n.is_internal()) continue;
             out << i << " : " << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << "\n";
         }
         return out;

src/sat/sat_bdd.h

@@ -57,6 +57,8 @@ namespace sat {
             BDD      m_hi;
             unsigned m_index;
             unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); }
+            bool is_internal() const { return m_lo == 0 && m_hi == 0; }
+            void set_internal() { m_lo = m_hi = 0; }
         };
 
         struct hash_node {
@@ -112,9 +114,15 @@ namespace sat {
         mutable unsigned           m_mark_level;
         mutable svector<double>    m_count;
         mutable svector<BDD>       m_todo;
+        bool                       m_disable_gc;
+        bool                       m_is_new_node;
         unsigned                   m_max_num_bdd_nodes;
+        unsigned_vector            m_S, m_T;  // used for reordering
+        vector<unsigned_vector>    m_level2nodes;
+        unsigned_vector            m_max_parent;
 
         BDD make_node(unsigned level, BDD l, BDD r);
+        bool is_new_node() const { return m_is_new_node; }
 
         BDD apply_const(BDD a, BDD b, bdd_op op);
         BDD apply(BDD arg1, BDD arg2, bdd_op op);
@@ -142,6 +150,7 @@ namespace sat {
         bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; }
 
         void try_reorder();
+        void init_reorder();
         void sift_up(unsigned level);
 
         static const BDD false_bdd = 0;

src/util/vector.h

@@ -410,7 +410,7 @@ public:
 
     void fill(unsigned sz, T const & elem) {
         resize(sz);
-        fill(sz, elem);
+        fill(elem);
     }
 
     bool contains(T const & elem) const {