diff options
author | mudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu> | 2020-02-03 12:44:34 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-03 12:44:34 -0600 |
commit | 25ee78ea4a4111ca7e72e9d81cb7f23f3d1c2fb7 (patch) | |
tree | 1abea753035b49c0dded334158f02531c03138c0 | |
parent | dd67f7c0250a0725f2afc9fa38d3fca219eb2088 (diff) |
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>
-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) |