diff options
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-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 { |