* 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>
void CardinalityExtension::checkFiniteType(TypeNode& t)
{
Assert(t.isInterpretedFinite());
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))
// 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 univ = d_state.getUnivSet(nm->mkSetType(t));
std::map<Node, Node>::iterator it = d_univProxy.find(univ);
if (it == d_univProxy.end())
{
// Force cvc4 to build the cardinality graph for the universe set
if (it == d_univProxy.end())
{
// Force cvc4 to build the cardinality graph for the universe set
// get all equivalent classes of type t
vector<Node> representatives = d_state.getSetsEqClasses(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()));
Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality()));
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/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
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
--- /dev/null
+;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)