diff options
| -rw-r--r-- | src/parser/cvc/Cvc.g | 13 | ||||
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 4 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 7 | ||||
| -rw-r--r-- | test/regress/regress0/sets/Makefile.am | 3 |
4 files changed, 24 insertions, 3 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 1b1137a9d..8d76a5122 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -242,6 +242,7 @@ tokens { //REGEXP_EMPTY_TOK //REGEXP_SIGMA_TOK + SETS_CARD_TOK = 'CARD'; FMF_CARD_TOK = 'HAS_CARD'; @@ -328,6 +329,7 @@ int getOperatorPrecedence(int type) { case GEQ_TOK: case GT_TOK: case MEMBER_TOK: + case SETS_CARD_TOK: case FMF_CARD_TOK: return 25; case EQUAL_TOK: case DISEQUAL_TOK: return 26; @@ -371,6 +373,7 @@ Kind getOperatorKind(int type, bool& negate) { case LT_TOK: return kind::LT; case LEQ_TOK: return kind::LEQ; case MEMBER_TOK: return kind::MEMBER; + case SETS_CARD_TOK: return kind::CARD; case FMF_CARD_TOK: return kind::CARDINALITY_CONSTRAINT; // arithmeticBinop @@ -2012,8 +2015,18 @@ stringTerm[CVC4::Expr& f] | str[s] { f = MK_CONST(CVC4::String(s)); } + | setsTerm[f] + ; + +setsTerm[CVC4::Expr& f] +@init { +} + /* Sets prefix operators */ + : SETS_CARD_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::CARD, f); } | simpleTerm[f] ; + /** Parses a simple term. */ simpleTerm[CVC4::Expr& f] diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 4f0d4b664..58d0ea6c0 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -819,9 +819,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; } case kind::CARD: { - out << "||"; + out << "CARD("; toStream(out, n[0], depth, types, false); - out << "||"; + out << ")"; return; break; } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index b52c225aa..c65822005 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -576,6 +576,13 @@ void TheorySetsPrivate::fullEffortCheck(){ d_set_eqc_list[eqc].push_back( n ); }else if( n.getKind()==kind::CARD ){ d_card_enabled = true; + TypeNode tn = n[0].getType().getSetElementType(); + if( tn.isInterpretedFinite() ){ + std::stringstream ss; + ss << "ERROR: cannot use cardinality on sets with finite element type." << std::endl; + throw LogicException(ss.str()); + //TODO: extend approach for this case + } Node r = d_equalityEngine.getRepresentative( n[0] ); if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){ d_eqc_to_card_term[ r ] = n; diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index f68b9b036..ab597350e 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -63,7 +63,8 @@ TESTS = \ union-1b.smt2 \ union-2.smt2 \ dt-simp-mem.smt2 \ - card3-ground.smt2 + card3-ground.smt2 \ + card-3sets.cvc EXTRA_DIST = $(TESTS) |