Move (unrecursified) bv::utils::numNodes to lazy_bitblaster.cpp. (#1594)

This unrecursifies and moves bv::utils::numNodes to an unnamed namespace in lazy_bitblaster.cpp
(only place where it is used). Tested against the recursive implementation (with a temporary
Assertion) on regression tests.

diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index cc4f52d8d17790960045aa7905a24b576e1a62ef..6cd4a3314f038a2d61b70fc4e6fa75fe58c5d38e 100644 (file)
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -33,6 +33,30 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
+namespace {
+
+/* Determine the number of uncached nodes that a given node consists of.  */
+uint64_t numNodes(TNode node, utils::NodeSet& seen)
+{
+  std::vector<TNode> stack;
+  uint64_t res = 0;
+
+  stack.push_back(node);
+  while (!stack.empty())
+  {
+    Node n = stack.back();
+    stack.pop_back();
+
+    if (seen.find(n) != seen.end()) continue;
+
+    res += 1;
+    seen.insert(n);
+    stack.insert(stack.end(), n.begin(), n.end());
+  }
+  return res;
+}
+}
+
 
 TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
                                  const std::string name, bool emptyNotify)
@@ -188,13 +212,13 @@ void TLazyBitblaster::makeVariable(TNode var, Bits& bits) {
   d_variables.insert(var);
 }
 
-uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen) {
-  node = node.getKind() == kind::NOT?  node[0] : node;
-  if( !utils::isBitblastAtom( node ) ){
-    return 0;
-  }
-  Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
-  uint64_t size = utils::numNodes(atom_bb, seen);
+uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen)
+{
+  node = node.getKind() == kind::NOT ? node[0] : node;
+  if (!utils::isBitblastAtom(node)) { return 0; }
+  Node atom_bb =
+      Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
+  uint64_t size = numNodes(atom_bb, seen);
   return size;
 }
 

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 9e8a1f7dc2e9d5244d3938347f01c5b6309e37af..eaa9f463bdbb858dd48bc9d8f31f8a247d6fa609 100644 (file)
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -496,21 +496,6 @@ void intersect(const std::vector<uint32_t>& v1,
 
 /* ------------------------------------------------------------------------- */
 
-uint64_t numNodes(TNode node, NodeSet& seen)
-{
-  if (seen.find(node) != seen.end()) return 0;
-
-  uint64_t size = 1;
-  for (unsigned i = 0; i < node.getNumChildren(); ++i)
-  {
-    size += numNodes(node[i], seen);
-  }
-  seen.insert(node);
-  return size;
-}
-
-/* ------------------------------------------------------------------------- */
-
 void collectVariables(TNode node, NodeSet& vars)
 {
   if (vars.find(node) != vars.end()) return;

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 553ffaf51dd3850f35e05565828033bb10231178..1e27d75c0c85a87a65cb9fc01630df4d17060ee9 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -194,9 +194,6 @@ void intersect(const std::vector<uint32_t>& v1,
                const std::vector<uint32_t>& v2,
                std::vector<uint32_t>& intersection);
 
-/* Determine the total number of nodes that a given node consists of.  */
-uint64_t numNodes(TNode node, NodeSet& seen);
-
 /* Collect all variables under a given a node.  */
 void collectVariables(TNode node, NodeSet& vars);