Properly handle user cardinality constraints for uf-ss=none. (#1068)

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 6d4d96a873c0e8c0a533ebe558340d8abf6f922c..981e3e2acb6f65c34bff5062d49950a45e397769 100644 (file)
--- 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 {