diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-19 13:57:46 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-19 19:57:46 +0000 |
commit | 90cc5b0eccafd2f571b3bc388095bf8976cb8d18 (patch) | |
tree | 8ff93c1ceb88634d6bfc1b74bf12c47b283e8ca2 /src/preprocessing/passes/ite_simp.cpp | |
parent | e67777928ed8c73f6dfc802b5844c95d135c5127 (diff) |
Remove n-ary builder (#7671)
Adds the only usage of this file into ite_simp.cpp, where it is specialized for AND.
This is work towards eliminating arithmetic subtyping (that utility had an unused and ambiguous use of mkConst(CONST_RATIONAL, ...)).
Diffstat (limited to 'src/preprocessing/passes/ite_simp.cpp')
-rw-r--r-- | src/preprocessing/passes/ite_simp.cpp | 84 |
1 files changed, 82 insertions, 2 deletions
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 433bca568..14ed9df07 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -22,7 +22,6 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_statistics_registry.h" -#include "smt_util/nary_builder.h" #include "theory/arith/arith_ite_utils.h" #include "theory/theory_engine.h" @@ -34,6 +33,87 @@ namespace cvc5 { namespace preprocessing { namespace passes { +Node mkAssocAnd(const std::vector<Node>& children) +{ + NodeManager* nm = NodeManager::currentNM(); + if (children.size() == 0) + { + return nm->mkConst(true); + } + else if (children.size() == 1) + { + return children[0]; + } + else + { + const uint32_t max = kind::metakind::getMaxArityForKind(kind::AND); + const uint32_t min = kind::metakind::getMinArityForKind(kind::AND); + + Assert(min <= children.size()); + + unsigned int numChildren = children.size(); + if (numChildren <= max) + { + return nm->mkNode(kind::AND, children); + } + + typedef std::vector<Node>::const_iterator const_iterator; + const_iterator it = children.begin(); + const_iterator end = children.end(); + + /* The new top-level children and the children of each sub node */ + std::vector<Node> newChildren; + std::vector<Node> subChildren; + + while (it != end && numChildren > max) + { + /* Grab the next max children and make a node for them. */ + for (const_iterator next = it + max; it != next; ++it, --numChildren) + { + subChildren.push_back(*it); + } + Node subNode = nm->mkNode(kind::AND, subChildren); + newChildren.push_back(subNode); + subChildren.clear(); + } + + /* If there's children left, "top off" the Expr. */ + if (numChildren > 0) + { + /* If the leftovers are too few, just copy them into newChildren; + * otherwise make a new sub-node */ + if (numChildren < min) + { + for (; it != end; ++it) + { + newChildren.push_back(*it); + } + } + else + { + for (; it != end; ++it) + { + subChildren.push_back(*it); + } + Node subNode = nm->mkNode(kind::AND, subChildren); + newChildren.push_back(subNode); + } + } + + /* It's inconceivable we could have enough children for this to fail + * (more than 2^32, in most cases?). */ + AlwaysAssert(newChildren.size() <= max) + << "Too many new children in mkAssociative"; + + /* It would be really weird if this happened (it would require + * min > 2, for one thing), but let's make sure. */ + AlwaysAssert(newChildren.size() >= min) + << "Too few new children in mkAssociative"; + + return nm->mkNode(kind::AND, newChildren); + } +} + /* -------------------------------------------------------------------------- */ namespace { @@ -71,7 +151,7 @@ void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess, assertionsToPreprocess->resize(before); size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1; intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]); - Node newLast = cvc5::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); + Node newLast = mkAssocAnd(intoConjunction); assertionsToPreprocess->replace(lastBeforeItes, newLast); Assert(assertionsToPreprocess->size() == before); } |