From c59aefd26d391cb01f0e27b050e553afe49a69d8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 29 Mar 2019 08:38:30 -0500
Subject: [PATCH] Apply empty splits more aggressively in sets+cardinality
 (#2907)

---
 src/theory/sets/theory_sets_private.cpp   |  7 +++++-
 test/regress/CMakeLists.txt               |  1 +
 test/regress/regress1/sets/issue2904.smt2 | 27 +++++++++++++++++++++++
 3 files changed, 34 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress1/sets/issue2904.smt2

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f77d89254..aaa66046e 100644
--- 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 b5bccae23..55c777f80 100644
--- 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
index 000000000..13ca789f6
--- /dev/null
+++ b/test/regress/regress1/sets/issue2904.smt2
@@ -0,0 +1,27 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+; conjecture set nonempty(~b & ~c)
+
+(declare-fun n () Int)
+(declare-fun f () Int)
+(declare-fun m () Int)
+
+(declare-fun b () (Set Int))
+(declare-fun c () (Set Int))
+(declare-fun UNIVERALSET () (Set Int))
+(assert (subset b UNIVERALSET))
+(assert (subset c UNIVERALSET))
+
+(assert (> n 0))
+(assert (= (card UNIVERALSET) n))
+(assert (= (card b) m))
+(assert (= (card c) (- f m)))
+(assert (>= m 0))
+(assert (>= f m))
+(assert (> n (+ (* 2 f) m)))
+
+
+(assert (>= (card (setminus UNIVERALSET (intersection (setminus UNIVERALSET b) (setminus UNIVERALSET c)))) n))
+
+(check-sat)
-- 
2.30.2