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.

2 files changed, 69 insertions, 49 deletions

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 7eec52b19..8e86ba49d 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -153,60 +153,39 @@ Cardinality DTypeConstructor::getCardinality(TypeNode t) const
 
 bool DTypeConstructor::isFinite(TypeNode t) const
 {
-  Assert(isResolved());
-
-  TNode self = d_constructor;
-  // is this already in the cache ?
-  if (self.getAttribute(DTypeFiniteComputedAttr()))
-  {
-    return self.getAttribute(DTypeFiniteAttr());
-  }
-  std::vector<TypeNode> instTypes;
-  std::vector<TypeNode> paramTypes;
-  bool isParam = t.isParametricDatatype();
-  if (isParam)
-  {
-    paramTypes = t.getDType().getParameters();
-    instTypes = TypeNode(t).getParamTypes();
-  }
-  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
-  {
-    TypeNode tc = getArgType(i);
-    if (isParam)
-    {
-      tc = tc.substitute(paramTypes.begin(),
-                         paramTypes.end(),
-                         instTypes.begin(),
-                         instTypes.end());
-    }
-    if (!tc.isFinite())
-    {
-      self.setAttribute(DTypeFiniteComputedAttr(), true);
-      self.setAttribute(DTypeFiniteAttr(), false);
-      return false;
-    }
-  }
-  self.setAttribute(DTypeFiniteComputedAttr(), true);
-  self.setAttribute(DTypeFiniteAttr(), true);
-  return true;
+  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
+  return cinfo.first == CardinalityType::FINITE;
 }
 
 bool DTypeConstructor::isInterpretedFinite(TypeNode t) const
 {
-  Assert(isResolved());
-  TNode self = d_constructor;
-  // is this already in the cache ?
-  if (self.getAttribute(DTypeUFiniteComputedAttr()))
+  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
+  return cinfo.first != CardinalityType::INFINITE;
+}
+
+bool DTypeConstructor::hasFiniteExternalArgType(TypeNode t) const
+{
+  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
+  return cinfo.second;
+}
+
+std::pair<DTypeConstructor::CardinalityType, bool>
+DTypeConstructor::computeCardinalityInfo(TypeNode t) const
+{
+  std::map<TypeNode, std::pair<CardinalityType, bool> >::iterator it =
+      d_cardInfo.find(t);
+  if (it != d_cardInfo.end())
   {
-    return self.getAttribute(DTypeUFiniteAttr());
+    return it->second;
   }
+  std::pair<CardinalityType, bool> ret(CardinalityType::FINITE, false);
   std::vector<TypeNode> instTypes;
   std::vector<TypeNode> paramTypes;
   bool isParam = t.isParametricDatatype();
   if (isParam)
   {
     paramTypes = t.getDType().getParameters();
-    instTypes = TypeNode(t).getParamTypes();
+    instTypes = t.getParamTypes();
   }
   for (unsigned i = 0, nargs = getNumArgs(); i < nargs; i++)
   {
@@ -218,16 +197,30 @@ bool DTypeConstructor::isInterpretedFinite(TypeNode t) const
                          instTypes.begin(),
                          instTypes.end());
     }
-    if (!tc.isInterpretedFinite())
+    if (tc.isFinite())
+    {
+      // do nothing
+    }
+    else if (tc.isInterpretedFinite())
+    {
+      if (ret.first == CardinalityType::FINITE)
+      {
+        // not simply finite, it depends on uninterpreted sorts being finite
+        ret.first = CardinalityType::INTERPRETED_FINITE;
+      }
+    }
+    else
     {
-      self.setAttribute(DTypeUFiniteComputedAttr(), true);
-      self.setAttribute(DTypeUFiniteAttr(), false);
-      return false;
+      // infinite implies the constructor is infinite cardinality
+      ret.first = CardinalityType::INFINITE;
+      continue;
     }
+    // if the argument is (interpreted) finite and external, set the flag
+    // for indicating it has a finite external argument
+    ret.second = ret.second || !tc.isDatatype();
   }
-  self.setAttribute(DTypeUFiniteComputedAttr(), true);
-  self.setAttribute(DTypeUFiniteAttr(), true);
-  return true;
+  d_cardInfo[t] = ret;
+  return ret;
 }
 
 bool DTypeConstructor::isResolved() const { return !d_tester.isNull(); }
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
index fc414c756..2dba895e9 100644
--- a/src/expr/dtype_cons.h
+++ b/src/expr/dtype_cons.h
@@ -158,6 +158,13 @@ class DTypeConstructor
    * only be called for resolved constructors.
    */
   bool isInterpretedFinite(TypeNode t) const;
+  /**
+   * Has finite external argument type. This returns true if this constructor
+   * has an argument type that is not a datatype and is interpreted as a
+   * finite type. This function can only be called for resolved constructors.
+   *
+   */
+  bool hasFiniteExternalArgType(TypeNode t) const;
 
   /**
    * Returns true iff this constructor has already been
@@ -229,6 +236,17 @@ class DTypeConstructor
   void toStream(std::ostream& out) const;
 
  private:
+  /** Constructor cardinality type */
+  enum class CardinalityType
+  {
+    // the constructor is finite
+    FINITE,
+    // the constructor is interpreted-finite (finite under the assumption that
+    // uninterpreted sorts are finite)
+    INTERPRETED_FINITE,
+    // the constructor is infinte
+    INFINITE
+  };
   /** resolve
    *
    * This resolves (initializes) the constructor. For details
@@ -286,6 +304,13 @@ class DTypeConstructor
                          std::vector<TypeNode>& processing,
                          std::map<TypeNode, Node>& gt,
                          bool isValue) const;
+  /**
+   * Compute cardinality info, returns a pair where its first component is
+   * an identifier indicating the cardinality type of this constructor for
+   * type t, and a Boolean indicating whether the constructor has any arguments
+   * that have finite external type.
+   */
+  std::pair<CardinalityType, bool> computeCardinalityInfo(TypeNode t) const;
   /** compute shared selectors
    * This computes the maps d_sharedSelectors and d_sharedSelectorIndex.
    */
@@ -324,6 +349,8 @@ class DTypeConstructor
    * its argument index for this constructor.
    */
   mutable std::map<TypeNode, std::map<Node, unsigned> > d_sharedSelectorIndex;
+  /**  A cache for computeCardinalityInfo. */
+  mutable std::map<TypeNode, std::pair<CardinalityType, bool> > d_cardInfo;
 }; /* class DTypeConstructor */
 
 /**