Make isClosedEnumerable a member of TypeNode (#2434)

6 files changed, 34 insertions, 87 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index b90d98ca6..46649154e 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -29,7 +29,6 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
 
@@ -1645,7 +1644,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
 
 
 Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){
-  d_closed_enum_type = qe->getTermEnumeration()->isClosedEnumerableType(tn);
+  d_closed_enum_type = tn.isClosedEnumerable();
 }
 
 bool Instantiator::processEqualTerm(CegInstantiator* ci,
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 69f89021b..0dc704219 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1088,7 +1088,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       vec.push_back( 0 );
       TypeNode tn = n[i].getType();
-      if (te->isClosedEnumerableType(tn))
+      if (tn.isClosedEnumerable())
       {
         types.push_back( tn );
       }else{
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 1e3116f43..0eec40de2 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -317,7 +317,7 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
   if (d_model_basis_term.find(tn) == d_model_basis_term.end())
   {
     Node mbt;
-    if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+    if (tn.isClosedEnumerable())
     {
       mbt = d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
     }
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index eab05f454..24f418b0c 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -491,7 +491,7 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)
 
 Node Instantiate::getTermForType(TypeNode tn)
 {
-  if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+  if (tn.isClosedEnumerable())
   {
     return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
   }
diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp
index 34b9d7e81..8e3219768 100644
--- a/src/theory/quantifiers/term_enumeration.cpp
+++ b/src/theory/quantifiers/term_enumeration.cpp
@@ -53,84 +53,38 @@ Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index)
   return d_enum_terms[tn][index];
 }
 
-bool TermEnumeration::isClosedEnumerableType(TypeNode tn)
-{
-  std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
-      d_typ_closed_enum.find(tn);
-  if (it == d_typ_closed_enum.end())
-  {
-    d_typ_closed_enum[tn] = true;
-    bool ret = true;
-    if (tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction())
-    {
-      ret = false;
-    }
-    else if (tn.isSet())
-    {
-      ret = isClosedEnumerableType(tn.getSetElementType());
-    }
-    else if (tn.isDatatype())
-    {
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      for (unsigned i = 0; i < dt.getNumConstructors(); i++)
-      {
-        for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
-        {
-          TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
-          if (tn != ctn && !isClosedEnumerableType(ctn))
-          {
-            ret = false;
-            break;
-          }
-        }
-        if (!ret)
-        {
-          break;
-        }
-      }
-    }
-    
-    // other parametric sorts go here
-    
-    d_typ_closed_enum[tn] = ret;
-    return ret;
-  }
-  else
-  {
-    return it->second;
-  }
-}
-
-// checks whether a type is closed enumerable and is reasonably small enough (<1000)
-// such that all of its domain elements can be enumerated
 bool TermEnumeration::mayComplete(TypeNode tn)
 {
   std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
       d_may_complete.find(tn);
   if (it == d_may_complete.end())
   {
-    bool mc = false;
-    if (isClosedEnumerableType(tn) && tn.isInterpretedFinite())
-    {
-      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>();
-      }
-    }
+    // cache
+    bool mc = mayComplete(tn, options::fmfTypeCompletionThresh());
     d_may_complete[tn] = mc;
     return mc;
   }
-  else
+  return it->second;
+}
+
+bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard)
+{
+  bool mc = false;
+  if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
   {
-    return it->second;
+    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
+      Node oth = nm->mkConst(Rational(maxCard));
+      Node eq = nm->mkNode(LEQ, card, oth);
+      eq = Rewriter::rewrite(eq);
+      mc = eq.isConst() && eq.getConst<bool>();
+    }
   }
+  return mc;
 }
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h
index cede77dbe..cf25335f4 100644
--- a/src/theory/quantifiers/term_enumeration.h
+++ b/src/theory/quantifiers/term_enumeration.h
@@ -42,25 +42,19 @@ class TermEnumeration
   ~TermEnumeration() {}
   /** get i^th term for type tn */
   Node getEnumerateTerm(TypeNode tn, unsigned i);
-  /** is closed enumerable type
-   *
-   * This returns true if this type has an enumerator that produces
-   * constants that are handled by ground theory solvers.
-   * Examples of types that are not closed enumerable are:
-   * (1) uninterpreted sorts,
-   * (2) arrays,
-   * (3) codatatypes,
-   * (4) parametric sorts involving any of the above.
-   */
-  bool isClosedEnumerableType(TypeNode tn);
   /** may complete type
    *
-   * Returns true if the type tn is closed 
-   * enumerable, and is small enough
-   * for finite model finding to enumerate it,
-   * by some heuristic (current cardinality < 1000).
+   * Returns true if the type tn is closed enumerable, is interpreted as a
+   * finite type, and has cardinality less than some reasonable value
+   * (currently < 1000). This method caches the results of whether each type
+   * may be completed.
    */
   bool mayComplete(TypeNode tn);
+  /**
+   * Static version of the above method where maximum cardinality is
+   * configurable.
+   */
+  static bool mayComplete(TypeNode tn, unsigned cardMax);
 
  private:
   /** ground terms enumerated for types */