diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-07 11:50:59 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-07 11:50:59 +0200 |
| commit | 8a68cca2f9cf76b42187c39d09a4a40bd19622c1 (patch) | |
| tree | e238ce80d9273cf086c972bc5b60e9a51a67567e | |
| parent | 15486098da0e2131ca4299b9fdea1510008a60c4 (diff) | |
Properly handle user cardinality constraints for uf-ss=none. (#1068)
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 6d4d96a87..981e3e2ac 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -125,13 +125,18 @@ void TheoryUF::check(Effort level) { d_equalityEngine.assertEquality(atom, polarity, fact); } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { if( d_thss == NULL ){ - std::stringstream ss; - ss << "Cardinality constraint " << atom << " was asserted, but the logic does not allow it." << std::endl; - ss << "Try using a logic containing \"UFC\"." << std::endl; - throw Exception( ss.str() ); + if( !getLogicInfo().hasCardinalityConstraints() ){ + std::stringstream ss; + ss << "Cardinality constraint " << atom << " was asserted, but the logic does not allow it." << std::endl; + ss << "Try using a logic containing \"UFC\"." << std::endl; + throw Exception( ss.str() ); + }else{ + // support for cardinality constraints is not enabled, set incomplete + d_out->setIncomplete(); + } } //needed for models - if( options::produceModels() && ( atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT || options::ufssMode()!=UF_SS_FULL ) ){ + if( options::produceModels() ){ d_equalityEngine.assertPredicate(atom, polarity, fact); } } else { |