diff options
author | Andres Noetzli <noetzli@amazon.com> | 2021-04-02 15:43:15 -0700 |
---|---|---|
committer | Andres Noetzli <noetzli@amazon.com> | 2021-04-02 17:59:17 -0700 |
commit | fc6336a011e099bfeff9c9ddd134f7aa6dad47b8 (patch) | |
tree | 43a98b7dd3ad2c942967c019a3a33f9095d27b3e /src/preprocessing/util/ite_utilities.cpp | |
parent | fba1437c772b6733ce678b93b5ef7d95e366c82d (diff) |
Remove template argument from `NodeBuilder`an/refactor/NodeBuilder
Currently, `NodeBuilder` takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the `d_inlineNvChildSpace` array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a `NodeValue` on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the `NodeBuilder` code to a source file for faster compilation.
CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s
Diffstat (limited to 'src/preprocessing/util/ite_utilities.cpp')
-rw-r--r-- | src/preprocessing/util/ite_utilities.cpp | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index a3ad701a8..7826c207b 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -401,7 +401,7 @@ Node ITECompressor::compressBooleanITEs(Node toCompress) } } - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); Node curr = toCompress; while (curr.getKind() == kind::ITE && (curr[1] == d_false || curr[2] == d_false) @@ -465,7 +465,7 @@ Node ITECompressor::compressTerm(Node toCompress) } } - NodeBuilder<> nb(toCompress.getKind()); + NodeBuilder nb(toCompress.getKind()); if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -504,7 +504,7 @@ Node ITECompressor::compressBoolean(Node toCompress) else { bool ta = ite::isTheoryAtom(toCompress); - NodeBuilder<> nb(toCompress.getKind()); + NodeBuilder nb(toCompress.getKind()); if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << (toCompress.getOperator()); @@ -906,7 +906,7 @@ Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar) return d_replaceOverCache[p]; } - NodeBuilder<> builder(n.getKind()); + NodeBuilder builder(n.getKind()); if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << n.getOperator(); @@ -1207,7 +1207,7 @@ Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite) } else { - NodeBuilder<> nb(kind::OR); + NodeBuilder nb(kind::OR); NodeVec::const_iterator it = intersection.begin(), end = intersection.end(); for (; it != end; ++it) { @@ -1332,7 +1332,7 @@ Node ITESimplifier::simpConstants(TNode simpContext, if (iteNode.getKind() == kind::ITE) { - NodeBuilder<> builder(kind::ITE); + NodeBuilder builder(kind::ITE); builder << iteNode[0]; unsigned i = 1; for (; i < iteNode.getNumChildren(); ++i) @@ -1428,7 +1428,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) return simpVar; } - NodeBuilder<> builder(c.getKind()); + NodeBuilder builder(c.getKind()); if (c.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << c.getOperator(); @@ -1584,7 +1584,7 @@ Node ITESimplifier::simpITE(TNode assertion) if (stackHead.d_children_added) { // Children have been processed, so substitute - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); @@ -1731,7 +1731,7 @@ Node ITECareSimplifier::substitute(TNode e, return e; } - NodeBuilder<> builder(e.getKind()); + NodeBuilder builder(e.getKind()); if (e.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << e.getOperator(); |