From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 12 Dec 2014 11:03:26 +0000 (+0100)
Subject: Add cvc parsing support for cardinality constraints.  Bug fix for enumerating element... 
X-Git-Tag: cvc5-1.0.0~6462
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fafb7f90f35941a72957dcc9ca5e45afd066cf04;p=cvc5.git

Add cvc parsing support for cardinality constraints.  Bug fix for enumerating elements to meet cardinality lower bounds.
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 2b442015a..0c356ca57 100644
--- 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 28ea995d9..05fea6b5e 100644
--- 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] ) ){