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 /src/theory/sets | |
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>
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/cardinality_extension.cpp | 30 |
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())); |