diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-12-12 12:03:26 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-12-12 12:03:32 +0100 |
| commit | fafb7f90f35941a72957dcc9ca5e45afd066cf04 (patch) | |
| tree | fa53d7bacd16dcfce96f9a3ce5f994dfcb980bed /src | |
| parent | 69c092f9e2ac6d9628f4de3e0038c1f021b3c7c6 (diff) | |
Add cvc parsing support for cardinality constraints. Bug fix for enumerating elements to meet cardinality lower bounds.
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 7 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 4 |
2 files changed, 8 insertions, 3 deletions
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] ) ){ |