From e43b45b42ee786f4dd103aa68d67915504c1f59c Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Dec 2016 14:09:57 -0600
Subject: [PATCH] Added cardinality to cvc language, fixes bug 753. Throw logic
 exception when using cardinality on sets with finite element type.

---
 src/parser/cvc/Cvc.g                    | 13 +++++++++++++
 src/printer/cvc/cvc_printer.cpp         |  4 ++--
 src/theory/sets/theory_sets_private.cpp |  7 +++++++
 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)
 
-- 
2.30.2