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>

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index a1c91c5172e16faeff16375c72248bbd7101a152..babe1bd03a497e41111bdaf9134ec6fb0022c628 100644 (file)
--- 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()));
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index aeca8e7205fe7c61bbb4ad7746a7bef286cf2650..20272de2b8a5d155ee525422b70da2433f4f5934 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1598,6 +1598,7 @@ set(regress_1_tests
   regress1/sets/comp-pos-member.smt2
   regress1/sets/copy_check_heap_access_33_4.smt2
   regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2
+  regress1/sets/finite-type/bug3663.smt2
   regress1/sets/finite-type/sets-card-arrcolor.smt2
   regress1/sets/finite-type/sets-card-arrunit.smt2
   regress1/sets/finite-type/sets-card-bool-1.smt2

diff --git a/test/regress/regress1/sets/finite-type/bug3663.smt2 b/test/regress/regress1/sets/finite-type/bug3663.smt2
new file mode 100644 (file)
index 0000000..5aef5d1
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/bug3663.smt2
@@ -0,0 +1,8 @@
+;EXIT: 1
+;EXPECT: (error "The cardinality beth[0] of the finite type a is not supported yet.")
+(set-logic ALL)
+(set-option :fmf-fun true)
+(declare-sort a 0)
+(declare-const b (Set a))
+(assert (= (card b) 0))
+(check-sat)