diff options
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index f021fff28..2cc244a34 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -34,9 +34,23 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) { d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + IteSkolemMap& imap = assertions->getIteSkolemMap(); // Remove all of the ITE occurrences and normalize - d_preprocContext->getIteRemover()->run( - assertions->ref(), assertions->getIteSkolemMap(), true); + for (unsigned i = 0, size = assertions->size(); i < size; ++i) + { + std::vector<theory::TrustNode> newAsserts; + std::vector<Node> newSkolems; + TrustNode trn = d_preprocContext->getIteRemover()->run( + (*assertions)[i], newAsserts, newSkolems, true); + // process + assertions->replace(i, trn.getNode()); + Assert(newSkolems.size() == newAsserts.size()); + for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) + { + imap[newSkolems[j]] = assertions->size(); + assertions->ref().push_back(newAsserts[j].getNode()); + } + } for (unsigned i = 0, size = assertions->size(); i < size; ++i) { assertions->replace(i, Rewriter::rewrite((*assertions)[i])); |