diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-28 08:25:38 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-28 08:25:38 -0600 |
| commit | 4cd2d73366aba081a38900ddc2f4f172ce9ed2f8 (patch) | |
| tree | 6a7d612d6f3c66d24099fddccd6d2d761f96688a /src/preprocessing | |
| parent | e986a322232ac3edcd139ec7b424291ea3d5033a (diff) | |
Always theory-preprocess lemmas (#5817)
This PR makes it so that theory-preprocessing is always called on lemmas. It simplifies the proof production in the theory preprocessor accordingly.
Additionally, it ensures that our theory-preprocessor is run on lemmas that are generated from term formula removal. Previously, this was not the case and in fact certain lemmas (e.g. literals within witness terms that are not in preprocessed form) would escape and be asserted to TheoryEngine. This was uncovered by a unit test failure, the corresponding regression is added in this PR.
It adds a new interface removeItes to PropEngine which is required for the (deprecated) preprocessing pass removeItes.
This PR now makes the lemma propery PREPROCESS obsolete. Further simplification is possible after this PR in non-linear arithmetic and quantifiers, where it is not necessary to distinguish 2 caches for preprocessed vs. non-preprocessed lemmas.
Diffstat (limited to 'src/preprocessing')
| -rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 7 | ||||
| -rw-r--r-- | src/preprocessing/passes/theory_preprocess.cpp | 8 |
2 files changed, 2 insertions, 13 deletions
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 91af2a5b8..66a32472b 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -44,16 +44,11 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) Node assertion = (*assertions)[i]; std::vector<theory::TrustNode> newAsserts; std::vector<Node> newSkolems; - TrustNode trn = pe->preprocess(assertion, newAsserts, newSkolems, false); + TrustNode trn = pe->removeItes(assertion, newAsserts, newSkolems); if (!trn.isNull()) { // process assertions->replaceTrusted(i, trn); - // rewritten assertion has a dependence on the node (old pf architecture) - if (options::unsatCores() && !options::proofNew()) - { - ProofManager::currentPM()->addDependence(trn.getNode(), assertion); - } } Assert(newSkolems.size() == newAsserts.size()); for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 6c751f864..4552d13fc 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -41,17 +41,11 @@ PreprocessingPassResult TheoryPreprocess::applyInternal( Node assertion = (*assertions)[i]; std::vector<theory::TrustNode> newAsserts; std::vector<Node> newSkolems; - TrustNode trn = - propEngine->preprocess(assertion, newAsserts, newSkolems, true); + TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems); 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++) |