diff options
| -rw-r--r-- | src/theory/sets/cardinality_extension.cpp | 30 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sets/finite-type/bug3663.smt2 | 8 |
3 files changed, 28 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())); 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) |