From bd6f48ec9ecdd0547b77e9e8a49d3028f4281fe0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 Sep 2020 14:43:24 -0500 Subject: 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. --- test/regress/regress0/arith/issue3480.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress0') 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) -- cgit v1.2.3