Optimizations and fixes for computing whether a type is finite (#2179)

8 files changed, 100 insertions, 44 deletions

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index d6cf12d41..6616f470f 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -83,46 +83,81 @@ bool TypeNode::isInterpretedFinite()
   if (!getAttribute(IsInterpretedFiniteComputedAttr()))
   {
     bool isInterpretedFinite = false;
-    if (getCardinality().isFinite())
+    if (isSort())
+    {
+      // If the finite model finding flag is set, we treat uninterpreted sorts
+      // as finite. If it is not set, we treat them implicitly as infinite
+      // sorts (that is, their cardinality is not constrained to be finite).
+      isInterpretedFinite = options::finiteModelFind();
+    }
+    else if (isBitVector() || isFloatingPoint())
     {
       isInterpretedFinite = true;
     }
-    else if (options::finiteModelFind())
+    else if (isDatatype())
     {
-      if( isSort() ){
-        isInterpretedFinite = true;
-      }else if( isDatatype() ){
-        TypeNode tn = *this;
-        const Datatype& dt = getDatatype();
-        isInterpretedFinite = dt.isInterpretedFinite(tn.toType());
-      }else if( isArray() ){
-        isInterpretedFinite =
-            getArrayIndexType().isInterpretedFinite()
-            && getArrayConstituentType().isInterpretedFinite();
-      }else if( isSet() ) {
-        isInterpretedFinite = getSetElementType().isInterpretedFinite();
+      TypeNode tn = *this;
+      const Datatype& dt = getDatatype();
+      isInterpretedFinite = dt.isInterpretedFinite(tn.toType());
+    }
+    else if (isArray())
+    {
+      TypeNode tnc = getArrayConstituentType();
+      if (!tnc.isInterpretedFinite())
+      {
+        // arrays with consistuent type that is infinite are infinite
+        isInterpretedFinite = false;
       }
-      else if (isFunction())
+      else if (getArrayIndexType().isInterpretedFinite())
       {
+        // arrays with both finite consistuent and index types are finite
         isInterpretedFinite = true;
-        if (!getRangeType().isInterpretedFinite())
-        {
-          isInterpretedFinite = false;
-        }
-        else
+      }
+      else
+      {
+        // If the consistuent type of the array has cardinality one, then the
+        // array type has cardinality one, independent of the index type.
+        isInterpretedFinite = tnc.getCardinality().isOne();
+      }
+    }
+    else if (isSet())
+    {
+      isInterpretedFinite = getSetElementType().isInterpretedFinite();
+    }
+    else if (isFunction())
+    {
+      isInterpretedFinite = true;
+      TypeNode tnr = getRangeType();
+      if (!tnr.isInterpretedFinite())
+      {
+        isInterpretedFinite = false;
+      }
+      else
+      {
+        std::vector<TypeNode> argTypes = getArgTypes();
+        for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
         {
-          std::vector<TypeNode> argTypes = getArgTypes();
-          for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
+          if (!argTypes[i].isInterpretedFinite())
           {
-            if (!argTypes[i].isInterpretedFinite())
-            {
-              isInterpretedFinite = false;
-              break;
-            }
+            isInterpretedFinite = false;
+            break;
           }
         }
+        if (!isInterpretedFinite)
+        {
+          // similar to arrays, functions are finite if their range type
+          // has cardinality one, regardless of the arguments.
+          isInterpretedFinite = tnr.getCardinality().isOne();
+        }
       }
     }
+    else
+    {
+      // by default, compute the exact cardinality for the type and check
+      // whether it is finite. This should be avoided in general, since
+      // computing cardinalities for types can be highly expensive.
+      isInterpretedFinite = getCardinality().isFinite();
+    }
     setAttribute(IsInterpretedFiniteAttr(), isInterpretedFinite);
     setAttribute(IsInterpretedFiniteComputedAttr(), true);
     return isInterpretedFinite;
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 8e954ddc0..8c7414fa7 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -638,6 +638,15 @@ header = "options/quantifiers_options.h"
   help       = "mode for which types of bounds to minimize via first decision heuristics"
 
 [[option]]
+  name       = "fmfTypeCompletionThresh"
+  category   = "regular"
+  long       = "fmf-type-completion-thresh=N"
+  type       = "int"
+  default    = "1000"
+  read_only  = true
+  help       = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted"
+
+[[option]]
   name       = "quantConflictFind"
   category   = "regular"
   long       = "quant-cf"
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 49132dc46..d95a5763c 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -568,7 +568,9 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
           unsigned c1 = deq_child[0][i];
           unsigned c2 = deq_child[1][i];
           TypeNode tnc = children[c1].getType();
-          if (tnc == children[c2].getType() && !tnc.getCardinality().isOne())
+          // we may only apply this symmetry breaking scheme (which introduces
+          // disequalities) if the types are infinite.
+          if (tnc == children[c2].getType() && !tnc.isInterpretedFinite())
           {
             Node sym_lem_deq = children[c1].eqNode(children[c2]).negate();
             // notice that this symmetry breaking still allows for
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index e3b48a4da..cf690af57 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -202,7 +202,9 @@ void TheoryDatatypes::check(Effort e) {
             Trace("datatypes-debug") << "No constructor..." << std::endl;
             Type tt = tn.toType();
             const Datatype& dt = ((DatatypeType)tt).getDatatype();
-            Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite( tt ) << " " << dt.isInterpretedFinite( tt ) << " " << dt.isRecursiveSingleton( tt ) << std::endl;
+            Trace("datatypes-debug")
+                << "Datatype " << dt << " is " << dt.isInterpretedFinite(tt)
+                << " " << dt.isRecursiveSingleton(tt) << std::endl;
             bool continueProc = true;
             if( dt.isRecursiveSingleton( tt ) ){
               Trace("datatypes-debug") << "Check recursive singleton..." << std::endl;
@@ -263,7 +265,13 @@ void TheoryDatatypes::check(Effort e) {
                   if( consIndex==-1 ){
                     consIndex = j;
                   }
-                  if( !dt[ j ].isInterpretedFinite( tt ) ) {
+                  Trace("datatypes-debug") << j << " compute finite..."
+                                           << std::endl;
+                  bool ifin = dt[j].isInterpretedFinite(tt);
+                  Trace("datatypes-debug") << "...returned " << ifin
+                                           << std::endl;
+                  if (!ifin)
+                  {
                     if( !eqc || !eqc->d_selectors ){
                       needSplit = false;
                     }
@@ -1752,8 +1760,6 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
         tt = exp[0];
       }
       const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
-      //must be finite or have a selector
-      //if( eqc->d_selectors || dt[ index ].isFinite() ){
       //instantiate this equivalence class
       eqc->d_inst = true;
       Node tt_cons = getInstantiateCons( tt, dt, index );
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 4a69a9442..afe6e182f 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -171,7 +171,6 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
    Debug("dt-enum") << "datatype is " << d_type << std::endl;
    Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton( d_type.toType() );
-   Debug("dt-enum") << " " << d_datatype.isFinite( d_type.toType() ) << std::endl;
    Debug("dt-enum") << " " << d_datatype.isInterpretedFinite( d_type.toType() ) << std::endl;
 
    if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index f05246ddb..6763a0ad3 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -136,7 +136,8 @@ void ModelEngine::registerQuantifier( Node f ){
     for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
       TypeNode tn = f[0][i].getType();
       if( !tn.isSort() ){
-        if( !tn.getCardinality().isFinite() ){
+        if (!tn.isInterpretedFinite())
+        {
           if( tn.isInteger() ){
             if( !options::fmfBound() ){
               canHandle = false;
diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp
index 58558d302..34b9d7e81 100644
--- a/src/theory/quantifiers/term_enumeration.cpp
+++ b/src/theory/quantifiers/term_enumeration.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/term_enumeration.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
@@ -109,15 +110,19 @@ bool TermEnumeration::mayComplete(TypeNode tn)
   if (it == d_may_complete.end())
   {
     bool mc = false;
-    if (isClosedEnumerableType(tn) && tn.getCardinality().isFinite()
-        && !tn.getCardinality().isLargeFinite())
+    if (isClosedEnumerableType(tn) && tn.isInterpretedFinite())
     {
-      Node card = NodeManager::currentNM()->mkConst(
-          Rational(tn.getCardinality().getFiniteCardinality()));
-      Node oth = NodeManager::currentNM()->mkConst(Rational(1000));
-      Node eq = NodeManager::currentNM()->mkNode(LEQ, card, oth);
-      eq = Rewriter::rewrite(eq);
-      mc = eq.isConst() && eq.getConst<bool>();
+      Cardinality c = tn.getCardinality();
+      if (!c.isLargeFinite())
+      {
+        NodeManager* nm = NodeManager::currentNM();
+        Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
+        // check if less than fixed upper bound, default 1000
+        Node oth = nm->mkConst(Rational(options::fmfTypeCompletionThresh()));
+        Node eq = nm->mkNode(LEQ, card, oth);
+        eq = Rewriter::rewrite(eq);
+        mc = eq.isConst() && eq.getConst<bool>();
+      }
     }
     d_may_complete[tn] = mc;
     return mc;
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index b45f6bcc2..956468e30 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -135,8 +135,7 @@ class CVC4_PUBLIC Cardinality {
   /** Returns true iff this cardinality is finite. */
   bool isFinite() const { return d_card > 0; }
   /** Returns true iff this cardinality is one */
-  bool isOne() const { return d_card == 1; }
-
+  bool isOne() const { return d_card == 2; }
   /**
    * Returns true iff this cardinality is finite and large (i.e.,
    * at the ceiling of representable finite cardinalities).