Improvements to sets + cardinality + quantifiers (#2200)

2 files changed, 24 insertions, 10 deletions

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 7b5244a04..49954c111 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -533,6 +533,7 @@ void TheorySetsPrivate::fullEffortCheck(){
     d_bop_index.clear();
     d_op_list.clear();
     d_card_enabled = false;
+    d_t_card_enabled.clear();
     d_rels_enabled = false;
     d_eqc_to_card_term.clear();
 
@@ -622,12 +623,23 @@ void TheorySetsPrivate::fullEffortCheck(){
         }else if( n.getKind()==kind::CARD ){
           d_card_enabled = true;
           TypeNode tnc = n[0].getType().getSetElementType();
+          d_t_card_enabled[tnc] = true;
           if( tnc.isInterpretedFinite() ){
             std::stringstream ss;
-            ss << "ERROR: cannot use cardinality on sets with finite element type." << std::endl;
+            ss << "ERROR: cannot use cardinality on sets with finite element "
+                  "type (term is "
+               << n << ")." << std::endl;
             throw LogicException(ss.str());
             //TODO: extend approach for this case
           }
+          // if we do not handle the kind, set incomplete
+          Kind nk = n[0].getKind();
+          if (nk == kind::UNIVERSE_SET || d_rels->isRelationKind(nk))
+          {
+            d_full_check_incomplete = true;
+            Trace("sets-incomplete")
+                << "Sets : incomplete because of " << n << "." << std::endl;
+          }
           Node r = d_equalityEngine.getRepresentative( n[0] );
           if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){
             d_eqc_to_card_term[ r ] = n;
@@ -1037,6 +1049,12 @@ void TheorySetsPrivate::checkCardBuildGraph( std::vector< Node >& lemmas ) {
 }
 
 void TheorySetsPrivate::registerCardinalityTerm( Node n, std::vector< Node >& lemmas ){
+  TypeNode tnc = n.getType().getSetElementType();
+  if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end())
+  {
+    // if no cardinality constraints for sets of this type, we can ignore
+    return;
+  }
   if( d_card_processed.find( n )==d_card_processed.end() ){
     d_card_processed.insert( n );
     Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
@@ -1724,16 +1742,10 @@ void TheorySetsPrivate::check(Theory::Effort level) {
         fullEffortCheck();
         if( !d_conflict && !d_sentLemma ){
           //invoke relations solver
-          d_rels->check(level);  
-          if( d_card_enabled && ( d_rels_enabled || options::setsExt() ) ){
-            //if cardinality constraints are enabled,
-            //  then model construction may fail in there are relational operators, or universe set.
-            // TODO: should internally check model, return unknown if fail
-            d_full_check_incomplete = true;
-            Trace("sets-incomplete") << "Sets : incomplete because of extended operators." << std::endl;
-          }
+          d_rels->check(level);
         }
-        if( d_full_check_incomplete ){
+        if (!d_conflict && !d_sentLemma && d_full_check_incomplete)
+        {
           d_external.d_out->setIncomplete();
         }
       }
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 57a7aaf65..31aec85c3 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -141,6 +141,8 @@ private:
   //cardinality
 private:
   bool d_card_enabled;
+  /** element types of sets for which cardinality is enabled */
+  std::map<TypeNode, bool> d_t_card_enabled;
   bool d_rels_enabled;
   std::map< Node, Node > d_eqc_to_card_term;
   NodeSet d_card_processed;