diff options
Diffstat (limited to 'src/preprocessing/util/ite_utilities.cpp')
-rw-r--r-- | src/preprocessing/util/ite_utilities.cpp | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index c72da1621..c9bf283ac 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -130,13 +130,13 @@ bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const } /* returns false if an assertion is discovered to be equal to false. */ -bool ITEUtilities::compress(std::vector<Node>& assertions) +bool ITEUtilities::compress(AssertionPipeline* assertionsToPreprocess) { if (d_compressor == NULL) { d_compressor = new ITECompressor(d_containsVisitor.get()); } - return d_compressor->compress(assertions); + return d_compressor->compress(assertionsToPreprocess); } Node ITEUtilities::simplifyWithCare(TNode e) @@ -527,17 +527,18 @@ Node ITECompressor::compressBoolean(Node toCompress) } } -bool ITECompressor::compress(std::vector<Node>& assertions) +bool ITECompressor::compress(AssertionPipeline* assertionsToPreprocess) { reset(); - d_assertions = &assertions; - d_incoming.computeReachability(assertions); + d_assertions = assertionsToPreprocess; + d_incoming.computeReachability(assertionsToPreprocess->ref()); ++(d_statistics.d_compressCalls); Chat() << "Computed reachability" << endl; bool nofalses = true; + const std::vector<Node>& assertions = assertionsToPreprocess->ref(); size_t original_size = assertions.size(); Chat() << "compressing " << original_size << endl; for (size_t i = 0; i < original_size && nofalses; ++i) @@ -545,7 +546,8 @@ bool ITECompressor::compress(std::vector<Node>& assertions) Node assertion = assertions[i]; Node compressed = compressBoolean(assertion); Node rewritten = theory::Rewriter::rewrite(compressed); - assertions[i] = rewritten; + // replace + assertionsToPreprocess->replace(i, rewritten); Assert(!d_contains->containsTermITE(rewritten)); nofalses = (rewritten != d_false); |