Modify strategy in sets+cardinality (#2909)

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index aaa66046ebaaf263ee651d156c86c1d60d36c3da..a62a235c31fda2c55be17d86e96f472d3e042fa8 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -700,9 +700,11 @@ void TheorySetsPrivate::fullEffortCheck(){
           checkUpwardsClosure( lemmas );
           flushLemmas( lemmas );
           if( !hasProcessed() ){
-            std::vector< Node > intro_sets;
-            //for cardinality
-            if( d_card_enabled ){
+            checkDisequalities(lemmas);
+            flushLemmas(lemmas);
+            if (!hasProcessed() && d_card_enabled)
+            {
+              // for cardinality
               checkCardBuildGraph( lemmas );
               flushLemmas( lemmas );
               if( !hasProcessed() ){
@@ -712,28 +714,24 @@ void TheorySetsPrivate::fullEffortCheck(){
                   checkCardCycles( lemmas );
                   flushLemmas( lemmas );
                   if( !hasProcessed() ){
+                    std::vector<Node> intro_sets;
                     checkNormalForms( lemmas, intro_sets );
                     flushLemmas( lemmas );
+                    if (!hasProcessed() && !intro_sets.empty())
+                    {
+                      Assert(intro_sets.size() == 1);
+                      Trace("sets-intro")
+                          << "Introduce term : " << intro_sets[0] << std::endl;
+                      Trace("sets-intro") << "  Actual Intro : ";
+                      debugPrintSet(intro_sets[0], "sets-nf");
+                      Trace("sets-nf") << std::endl;
+                      Node k = getProxy(intro_sets[0]);
+                      d_sentLemma = true;
+                    }
                   }
                 }
               }
             }
-            if( !hasProcessed() ){
-              checkDisequalities( lemmas );
-              flushLemmas( lemmas );
-              if( !hasProcessed() ){
-                //introduce splitting on venn regions (absolute last resort)
-                if( d_card_enabled && !hasProcessed() && !intro_sets.empty() ){
-                  Assert( intro_sets.size()==1 );
-                  Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl;
-                  Trace("sets-intro") << "  Actual Intro : ";
-                  debugPrintSet( intro_sets[0], "sets-nf" );
-                  Trace("sets-nf") << std::endl;
-                  Node k = getProxy( intro_sets[0] );
-                  d_sentLemma = true;
-                }
-              }
-            }
           }
         }
       }
@@ -1491,17 +1489,24 @@ void TheorySetsPrivate::checkNormalForm( Node eqc, std::vector< Node >& intro_se
         Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
       }else{
         Trace("sets-nf") << "failed to build N " << eqc << std::endl;
-        Assert( false );
       }
     }else{
       // must ensure disequal from empty
-      if (!eqc.isConst() && !ee_areDisequal(eqc, emp_set))
+      if (!eqc.isConst() && !ee_areDisequal(eqc, emp_set)
+          && (d_pol_mems[0].find(eqc) == d_pol_mems[0].end()
+              || d_pol_mems[0][eqc].empty()))
       {
+        Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
         split(eqc.eqNode(emp_set));
+        success = false;
+      }
+      else
+      {
+        // normal form is this equivalence class
+        d_nf[eqc].push_back(eqc);
+        Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }"
+                         << std::endl;
       }
-      //normal form is this equivalence class
-      d_nf[eqc].push_back( eqc );
-      Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }" << std::endl;
     }
     if( success ){
       //send to parents