projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 134ce17) | patch
Eliminate recursion from the internals of term formula removal (#5701)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 21 Dec 2020 14:53:41 +0000 (08:53 -0600)
committerGitHub <noreply@github.com>
Mon, 21 Dec 2020 14:53:41 +0000 (08:53 -0600)
commite32908362d75acad3cce28cf725eb781d1556e6f
tree0124387fe79f59798180b7a440959e18e70adf1etree
parent134ce1704c4f2467a0c5eeef2127afd140d44cc4commit | 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.
src/smt/term_formula_removal.cpp diff | blob | history
src/smt/term_formula_removal.h diff | blob | history
src/theory/theory_preprocessor.cpp diff | blob | history
test/regress/regress1/nl/nl_uf_lalt.smt2 diff | blob | history