From 25ee78ea4a4111ca7e72e9d81cb7f23f3d1c2fb7 Mon Sep 17 00:00:00 2001
From: mudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu>
Date: Mon, 3 Feb 2020 12:44:34 -0600
Subject: [PATCH] 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>
---
 src/theory/sets/cardinality_extension.cpp     | 30 ++++++++++++-------
 test/regress/CMakeLists.txt                   |  1 +
 .../regress1/sets/finite-type/bug3663.smt2    |  8 +++++
 3 files changed, 28 insertions(+), 11 deletions(-)
 create mode 100644 test/regress/regress1/sets/finite-type/bug3663.smt2

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()));
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index aeca8e720..20272de2b 100644
--- 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
index 000000000..5aef5d15d
--- /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)
-- 
2.30.2