diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-16 09:03:45 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-16 09:03:45 -0600 |
commit | 3a3735d58ddac7ecfac80dad35da963901f15f55 (patch) | |
tree | 1aa213359a6637f571f22f3db7434bb75a8fc93e /src/preprocessing/passes/ite_removal.cpp | |
parent | 5b90fdad09209da667cc281f5425300a4b2bb9c9 (diff) |
Move ownership of term formula removal to theory preprocessor (#5670)
This is work towards refactoring ITE removal (more generally, term formula removal) so that it happens at a configurable time, preferably post-CNF conversion.
This moves the TermFormulaRemover to the TheoryPreprocessor and changes several interfaces as a consequence of this move.
The next step will move the TheoryPreprocessor inside prop::TheoryProxy.
There are no behavior changes to solving in this PR. One aspect of CheckModels is simplified.
Diffstat (limited to 'src/preprocessing/passes/ite_removal.cpp')
-rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 27 |
1 files changed, 23 insertions, 4 deletions
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index a75b6f5ad..3531497e8 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -18,6 +18,7 @@ #include "preprocessing/passes/ite_removal.h" #include "theory/rewriter.h" +#include "theory/theory_preprocessor.h" namespace CVC4 { namespace preprocessing { @@ -25,6 +26,7 @@ namespace passes { using namespace CVC4::theory; +// TODO (project #42): note this preprocessing pass is deprecated IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "ite-removal") { @@ -36,19 +38,36 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) IteSkolemMap& imap = assertions->getIteSkolemMap(); // Remove all of the ITE occurrences and normalize + theory::TheoryPreprocessor* tpp = + d_preprocContext->getTheoryEngine()->getTheoryPreprocess(); for (unsigned i = 0, size = assertions->size(); i < size; ++i) { + Node assertion = (*assertions)[i]; std::vector<theory::TrustNode> newAsserts; std::vector<Node> newSkolems; - TrustNode trn = d_preprocContext->getIteRemover()->run( - (*assertions)[i], newAsserts, newSkolems, true); - // process - assertions->replaceTrusted(i, trn); + // TODO (project #42): this will call the prop engine + TrustNode trn = tpp->preprocess(assertion, newAsserts, newSkolems, false); + if (!trn.isNull()) + { + // process + assertions->replaceTrusted(i, trn); + // rewritten assertion has a dependence on the node (old pf architecture) + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(trn.getNode(), assertion); + } + } Assert(newSkolems.size() == newAsserts.size()); for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) { imap[newSkolems[j]] = assertions->size(); assertions->pushBackTrusted(newAsserts[j]); + // new assertions have a dependence on the node (old pf architecture) + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(newAsserts[j].getProven(), + assertion); + } } } for (unsigned i = 0, size = assertions->size(); i < size; ++i) |