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: 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 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'src/parser')

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]
-- 
cgit v1.2.3