diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-11 11:13:33 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-11 11:13:33 -0800 |
commit | c9e58c9cf4b90e42d314b92054a010513da1502a (patch) | |
tree | b45f6d2126bb764172af306c8e2b4f94732b7c9f /src/theory/bv/lazy_bitblaster.cpp | |
parent | 544cf41c1a5c1a3c8514c21d426ad66e578e67b0 (diff) |
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.
Diffstat (limited to 'src/theory/bv/lazy_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 38 |
1 files changed, 31 insertions, 7 deletions
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; } |