Apply empty splits more aggressively in sets+cardinality (#2907)

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f77d892548a9ae2a8f634e3f13135a4243df33a0..aaa66046ebaaf263ee651d156c86c1d60d36c3da 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1380,8 +1380,8 @@ void TheorySetsPrivate::checkNormalForm( Node eqc, std::vector< Node >& intro_se
 
     Assert( d_nf.find( eqc )==d_nf.end() );
     bool success = true;
+    Node emp_set = getEmptySet(tn);
     if( !base.isNull() ){
-      Node emp_set = getEmptySet( tn );
       for( unsigned j=0; j<comps.size(); j++ ){
         //compare if equal
         std::vector< Node > c;
@@ -1494,6 +1494,11 @@ void TheorySetsPrivate::checkNormalForm( Node eqc, std::vector< Node >& intro_se
         Assert( false );
       }
     }else{
+      // must ensure disequal from empty
+      if (!eqc.isConst() && !ee_areDisequal(eqc, emp_set))
+      {
+        split(eqc.eqNode(emp_set));
+      }
       //normal form is this equivalence class
       d_nf[eqc].push_back( eqc );
       Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }" << std::endl;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b5bccae237b34bad0e0aee3703865a437d72133b..55c777f80452a413a0cb154dcb032180f24b2e3d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1494,6 +1494,7 @@ set(regress_1_tests
   regress1/sets/fuzz31811.smt2
   regress1/sets/insert_invariant_37_2.smt2
   regress1/sets/issue2568.smt2
+  regress1/sets/issue2904.smt2
   regress1/sets/lemmabug-ListElts317minimized.smt2
   regress1/sets/remove_check_free_31_6.smt2
   regress1/sets/sets-disequal.smt2

diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2
new file mode 100644 (file)
index 0000000..13ca789
--- /dev/null
+++ b/test/regress/regress1/sets/issue2904.smt2
@@ -0,0 +1,27 @@
+(set-logic ALL_SUPPORTED)\r
+(set-info :status unsat)\r
+\r
+; conjecture set nonempty(~b & ~c)\r
+\r
+(declare-fun n () Int)\r
+(declare-fun f () Int)\r
+(declare-fun m () Int)\r
+\r
+(declare-fun b () (Set Int))\r
+(declare-fun c () (Set Int))\r
+(declare-fun UNIVERALSET () (Set Int))\r
+(assert (subset b UNIVERALSET))\r
+(assert (subset c UNIVERALSET))\r
+\r
+(assert (> n 0))\r
+(assert (= (card UNIVERALSET) n))\r
+(assert (= (card b) m))\r
+(assert (= (card c) (- f m)))\r
+(assert (>= m 0))\r
+(assert (>= f m))\r
+(assert (> n (+ (* 2 f) m)))\r
+\r
+\r
+(assert (>= (card (setminus UNIVERALSET (intersection (setminus UNIVERALSET b) (setminus UNIVERALSET c)))) n))\r
+\r
+(check-sat)\r