From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Sep 2017 09:50:59 +0000 (+0200)
Subject: Properly handle user cardinality constraints for uf-ss=none. (#1068)
X-Git-Tag: cvc5-1.0.0~5650
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8a68cca2f9cf76b42187c39d09a4a40bd19622c1;p=cvc5.git

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 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 {