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/prop/theory_proxy.cpp | |
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/prop/theory_proxy.cpp')
-rw-r--r-- | src/prop/theory_proxy.cpp | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 8e54064e1..c604c47f7 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -172,22 +172,26 @@ CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; } theory::TrustNode TheoryProxy::preprocessLemma( theory::TrustNode trn, std::vector<theory::TrustNode>& newLemmas, - std::vector<Node>& newSkolems, - bool doTheoryPreprocess) + std::vector<Node>& newSkolems) { - return d_tpp.preprocessLemma( - trn, newLemmas, newSkolems, doTheoryPreprocess, true); + return d_tpp.preprocessLemma(trn, newLemmas, newSkolems); } theory::TrustNode TheoryProxy::preprocess( TNode node, std::vector<theory::TrustNode>& newLemmas, - std::vector<Node>& newSkolems, - bool doTheoryPreprocess) + std::vector<Node>& newSkolems) { - theory::TrustNode pnode = - d_tpp.preprocess(node, newLemmas, newSkolems, doTheoryPreprocess, true); - return pnode; + return d_tpp.preprocess(node, newLemmas, newSkolems); +} + +theory::TrustNode TheoryProxy::removeItes( + TNode node, + std::vector<theory::TrustNode>& newLemmas, + std::vector<Node>& newSkolems) +{ + RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas(); + return rtf.run(node, newLemmas, newSkolems, true); } void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); } |