Modify lemma vs fact policy for datatype equalities (#5115)

This changes the lemma vs fact policy for datatype equalities. Previously, datatype equalities were sent as lemmas unless they were over datatypes that were composed of datatypes only. This is now changed so that equalities that do not involve direct subterms with finite non-datatype types are kept internal.

The primary type of equality that this targets are "Instantiate" equalities, e.g. the conclusion of:
(is-cons x) => x = (cons (head x) (tail x))
These equalities have been observed to generate large amounts of new terms for many benchmarks.

With this PR, the the challenging Facebook benchmark goes from 2 min 45 sec -> 29 sec. If the instantiate rule is disabled altogether, it still correctly solves, and is faster (~14 seconds), which however is not correct in general.

This change triggered two other issues:
(1) A relations benchmark involving transitive closure now times out. This has been a common issue for the relations solver and should be revisited.
(2) A potential issue with doPendingLemmas in InferenceManagerBuffer was uncovered. In rare cases, we can be re-entrant into this method since OutputChannel::lemma may trigger further preregistration of terms, which can trigger a recursive call to doPendingLemmas in the case of datatypes, which causes a segfault due to corrupting an iterator. This PR adds a simple guard for this method.

This PR also fixes some existing issues in computing cardinality for parametric datatypes.

3 files changed, 33 insertions, 1 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c7bf666d6..fc2167a4a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -415,6 +415,7 @@ set(regress_0_tests
   regress0/datatypes/datatype3.cvc
   regress0/datatypes/datatype4.cvc
   regress0/datatypes/dt-2.6.smt2
+  regress0/datatypes/dt-different-params.smt2
   regress0/datatypes/dt-match-pat-param-2.6.smt2
   regress0/datatypes/dt-param-2.6.smt2
   regress0/datatypes/dt-param-2.6-print.smt2
@@ -426,6 +427,7 @@ set(regress_0_tests
   regress0/datatypes/issue1433.smt2
   regress0/datatypes/issue2838.cvc
   regress0/datatypes/jsat-2.6.smt2
+  regress0/datatypes/list-bool.smt2
   regress0/datatypes/model-subterms-min.smt2
   regress0/datatypes/mutually-recursive.cvc
   regress0/datatypes/pair-bool-bool.cvc
@@ -1676,7 +1678,6 @@ set(regress_1_tests
   regress1/rels/rel_pressure_0.cvc
   regress1/rels/rel_tc_10_1.cvc
   regress1/rels/rel_tc_4.cvc
-  regress1/rels/rel_tc_4_1.cvc
   regress1/rels/rel_tc_5_1.cvc
   regress1/rels/rel_tc_6.cvc
   regress1/rels/rel_tc_9_1.cvc
@@ -2519,6 +2520,8 @@ set(regression_disabled_tests
   # doing a coverage build with LFSC.
   regress1/quantifiers/set3.smt2
   regress1/rels/garbage_collect.cvc
+  # times out after dt fact update due to overly eager splitting for tclosure
+  regress1/rels/rel_tc_4_1.cvc
   regress1/sets/setofsets-disequal.smt2
   regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
   regress1/simple-rdl-definefun.smt2
diff --git a/test/regress/regress0/datatypes/dt-different-params.smt2 b/test/regress/regress0/datatypes/dt-different-params.smt2
new file mode 100644
index 000000000..f73d82dc9
--- /dev/null
+++ b/test/regress/regress0/datatypes/dt-different-params.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes ((Data 1)) ((par (T) ((data (first T))))))
+
+(declare-fun q1 () (Data Int))
+(declare-fun q2 () (Data Int))
+(declare-fun q3 () (Data Int))
+
+(assert (distinct q1 q2 q3))
+
+(declare-fun p1 () (Data Bool))
+(declare-fun p2 () (Data Bool))
+(declare-fun p3 () (Data Bool))
+
+(assert (distinct p1 p2 p3))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/list-bool.smt2 b/test/regress/regress0/datatypes/list-bool.smt2
new file mode 100644
index 000000000..adc7ad95a
--- /dev/null
+++ b/test/regress/regress0/datatypes/list-bool.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((list 0)) (
+((cons (head Bool) (tail list)) (nil))
+))
+(declare-fun x1 () list)
+(declare-fun x2 () list)
+(declare-fun x3 () list)
+(assert (= (tail x1) nil))
+(assert (= (tail x2) nil))
+(assert (= (tail x3) nil))
+(assert (distinct x1 x2 x3 nil))
+(check-sat)