From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Sun, 11 Feb 2018 19:13:33 +0000 (-0800)
Subject: Move (unrecursified) bv::utils::numNodes to lazy_bitblaster.cpp. (#1594)
X-Git-Tag: cvc5-1.0.0~5292
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c9e58c9cf4b90e42d314b92054a010513da1502a;p=cvc5.git

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 cc4f52d8d..6cd4a3314 100644
--- 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 9e8a1f7dc..eaa9f463b 100644
--- 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 553ffaf51..1e27d75c0 100644
--- 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);