diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-17 14:43:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-17 14:43:24 -0500 |
| commit | bd6f48ec9ecdd0547b77e9e8a49d3028f4281fe0 (patch) | |
| tree | 5791023f7abd0c3c79d4224d974ae8229847d8c1 /test/regress/regress0/arith | |
| parent | 92cdcc09e9a8bece8053c3aba9e68d0028b41a8e (diff) | |
Reduce recursion in term formula removal (#5052)
This reduces the use of recursion in term formula removal module. The recursion depth is now limited to the number of term positions on a path where a formula must be removed, instead of being limited to the overall formula depth. This PR also fixes some documentation.
Notice for its main cache d_tfCache, this class uses a CDInsertHashMap (instead of a CDHashMap) which does not allow inserting more than once, hence an auxliary "processedChildren" vector had to be introduced to track whether we have processed children. It's not clear to me whether we should just use the more standard CDHashMap, which would simplify this.
One non-linear arithmetic regression went unsat -> unknown, I added --nl-ext-tplanes to fix this.
This should fix #4889. It is possible to further reduce the recursion in this pass, which can be done on a followup PR if needed.
Diffstat (limited to 'test/regress/regress0/arith')
| -rw-r--r-- | test/regress/regress0/arith/issue3480.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/arith/issue3480.smt2 b/test/regress/regress0/arith/issue3480.smt2 index 74ce8d32b..ef4ad7179 100644 --- a/test/regress/regress0/arith/issue3480.smt2 +++ b/test/regress/regress0/arith/issue3480.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --theoryof-mode=type --quiet +; COMMAND-LINE: --theoryof-mode=type --quiet --nl-ext-tplanes (set-logic QF_NIA) (declare-fun a () Int) (declare-fun b () Int) |