Add cvc parsing support for cardinality constraints. Bug fix for enumerating element...

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 2b442015aabd64d3eb8fde2299f322f0f9c7704d..0c356ca579bc5b96906deddf517952d87f94cb21 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -213,6 +213,8 @@ tokens {
   STOINTEGER_TOK = 'TO_INTEGER';
   STOSTRING_TOK = 'TO_STRING';
   STORE_TOK = 'TO_RE';
+  
+  FMF_CARD_TOK = 'HAS_CARD';
 
   // these are parsed by special NUMBER_OR_RANGEOP rule, below
   DECIMAL_LITERAL;
@@ -291,7 +293,8 @@ int getOperatorPrecedence(int type) {
   case LT_TOK:
   case GEQ_TOK:
   case GT_TOK:
-  case MEMBER_TOK: return 25;
+  case MEMBER_TOK: 
+  case FMF_CARD_TOK: return 25;
   case EQUAL_TOK:
   case DISEQUAL_TOK: return 26;
   case NOT_TOK: return 27;
@@ -331,6 +334,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 FMF_CARD_TOK: return kind::CARDINALITY_CONSTRAINT;
 
     // arithmeticBinop
   case PLUS_TOK: return kind::PLUS;
@@ -1455,6 +1459,7 @@ comparisonBinop[unsigned& op]
   | LT_TOK
   | LEQ_TOK
   | MEMBER_TOK
+  | FMF_CARD_TOK
   ;
 
 arithmeticBinop[unsigned& op]

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 28ea995d9f5cd0539a4d737c2ecf0eabf127cb40..05fea6b5e23ba6f9045a3142110ca57dfc4e447f 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1417,11 +1417,11 @@ bool StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){
     }
   }
   int nReps = m->d_rep_set.d_type_reps.find( d_type )==m->d_rep_set.d_type_reps.end() ? 0 : (int)m->d_rep_set.d_type_reps[d_type].size();
-  if( nReps!=d_maxNegCard ){
+  if( nReps!=(d_maxNegCard+1) ){
     Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
     Trace("uf-ss-warn") << "   Max neg cardinality : " << d_maxNegCard << std::endl;
     Trace("uf-ss-warn") << "   # Reps : " << nReps << std::endl;
-    if( d_maxNegCard>nReps ){
+    if( d_maxNegCard>=nReps ){
       /*
       for( unsigned i=0; i<d_fresh_aloc_reps.size(); i++ ){
         if( add>0 && !m->d_equalityEngine->hasTerm( d_fresh_aloc_reps[i] ) ){