Fix cardinality of uninterpreted types when univset is not used (#3663)

* Fixed bug 3662

* format

* small change

* added bug3663.smt2 file

* throw Logic Exception

* throw Logic Exception

* ;EXIT: 1

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

1 files changed, 19 insertions, 11 deletions

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index a1c91c517..babe1bd03 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -84,11 +84,29 @@ void CardinalityExtension::checkFiniteTypes()
 void CardinalityExtension::checkFiniteType(TypeNode& t)
 {
   Assert(t.isInterpretedFinite());
-  NodeManager* nm = NodeManager::currentNM();
+
+  // get the cardinality of the finite type t
+  Cardinality card = t.getCardinality();
+
+  // cardinality of an interpreted finite type t is infinite when t
+  // is infinite without --fmf
+
+  if (card.isInfinite())
+  {
+    // TODO (#1123): support uninterpreted sorts with --finite-model-find
+    std::stringstream message;
+    message << "The cardinality " << card << " of the finite type " << t
+            << " is not supported yet.";
+    throw LogicException(message.str());
+  }
+
   // get the universe set (as univset (Set t))
+  NodeManager* nm = NodeManager::currentNM();
   Node univ = d_state.getUnivSet(nm->mkSetType(t));
   std::map<Node, Node>::iterator it = d_univProxy.find(univ);
+
   Node proxy;
+
   if (it == d_univProxy.end())
   {
     // Force cvc4 to build the cardinality graph for the universe set
@@ -102,16 +120,6 @@ void CardinalityExtension::checkFiniteType(TypeNode& t)
 
   // get all equivalent classes of type t
   vector<Node> representatives = d_state.getSetsEqClasses(t);
-  // get the cardinality of the finite type t
-  Cardinality card = t.getCardinality();
-  if (!card.isFinite())
-  {
-    // TODO (#1123): support uninterpreted sorts with --finite-model-find
-    std::stringstream message;
-    message << "The cardinality " << card << " of the finite type " << t
-            << " is not supported yet." << endl;
-    Assert(false) << message.str().c_str();
-  }
 
   Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality()));