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.

2 files changed, 38 insertions, 0 deletions

diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index 9df87e9b5..4a7d977ca 100644
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -35,6 +35,7 @@ cvc4_add_api_test(smt2_compliance)
 # cvc4_add_api_test(statistics)
 cvc4_add_api_test(two_solvers)
 cvc4_add_api_test(issue5074)
+cvc4_add_api_test(issue4889)
 
 # if we've built using libedit, then we want the interactive shell tests
 if (USE_EDITLINE)
diff --git a/test/api/issue4889.cpp b/test/api/issue4889.cpp
new file mode 100644
index 000000000..b09b639a9
--- /dev/null
+++ b/test/api/issue4889.cpp
@@ -0,0 +1,37 @@
+/*********************                                                        */
+/*! \file issue4889.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Test for issue #4889
+ **/
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+int main()
+{
+#ifdef CVC4_USE_SYMFPU
+  Solver slv;
+  Sort sort_int = slv.getIntegerSort();
+  Sort sort_array = slv.mkArraySort(sort_int, sort_int);
+  Sort sort_fp128 = slv.mkFloatingPointSort(15, 113);
+  Sort sort_fp32 = slv.mkFloatingPointSort(8, 24);
+  Sort sort_bool = slv.getBooleanSort();
+  Term const0 = slv.mkConst(sort_fp32, "_c0");
+  Term const1 = slv.mkConst(sort_fp32, "_c2");
+  Term const2 = slv.mkConst(sort_bool, "_c4");
+  Term ite = slv.mkTerm(ITE, const2, const1, const0);
+  Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1);
+  Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem);
+  slv.checkSatAssuming(isnan);
+#endif
+  return 0;
+}