diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-21 08:53:41 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-21 08:53:41 -0600 |
| commit | e32908362d75acad3cce28cf725eb781d1556e6f (patch) | |
| tree | 0124387fe79f59798180b7a440959e18e70adf1e /src/theory/theory_preprocessor.cpp | |
| parent | 134ce1704c4f2467a0c5eeef2127afd140d44cc4 (diff) | |
Eliminate recursion from the internals of term formula removal (#5701)
This makes all recursion (applying term formula removal on lemmas introduced by term formula removal) optionally happen at the top level call.
This is in preparation for making term formula removal lazier, in which case we will only apply one step of term formula removal at a time.
One QF_UFNIA regression times out due to changing the search, an option is changed for this benchmark.
Diffstat (limited to 'src/theory/theory_preprocessor.cpp')
| -rw-r--r-- | src/theory/theory_preprocessor.cpp | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 179ecc130..7c917dff5 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -100,14 +100,13 @@ TrustNode TheoryPreprocessor::preprocess(TNode node, ppNode = tpp.getNode(); } - // Remove the ITEs - TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems); - Node rtfNode = ttfr.getNode(); + // Remove the ITEs, fixed point + TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, true); + Node rtfNode = ttfr.isNull() ? ppNode : ttfr.getNode(); if (Debug.isOn("lemma-ites")) { - Debug("lemma-ites") << "removed ITEs from lemma: " << ttfr.getNode() - << endl; + Debug("lemma-ites") << "removed ITEs from lemma: " << rtfNode << endl; Debug("lemma-ites") << " + now have the following " << newLemmas.size() << " lemma(s):" << endl; for (size_t i = 0, lsize = newLemmas.size(); i <= lsize; ++i) |