Added cardinality to cvc language, fixes bug 753. Throw logic exception when using...

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1b1137a9d6d7a0373106cfb47187df1c6db135ca..8d76a5122e191421b499ff7c9cc51b4a721c35be 100644 (file)
--- 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 4f0d4b6644eb7a6180261967129dcf5ab49eb75b..58d0ea6c0ebe3702078ee44729a87dc59a1e5440 100644 (file)
--- 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 b52c225aa4d14bb63a9b3713cbbbe44eaa529dd4..c658220057500d776ce5d14f7620bb26c56bf0d7 100644 (file)
--- 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 f68b9b036528b7fab2b2588c7b05926d2002a996..ab597350e59ec53d6f4f76a399c1ab85f41cfb9d 100644 (file)
--- 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)