diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-29 08:38:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-29 08:38:30 -0500 |
| commit | c59aefd26d391cb01f0e27b050e553afe49a69d8 (patch) | |
| tree | 5da0ac0bd5814ec93f3fde9ffed99046cd4d75c5 | |
| parent | 327fe83f2e0533d53902645364180bc51ff20dcc (diff) | |
Apply empty splits more aggressively in sets+cardinality (#2907)
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 7 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sets/issue2904.smt2 | 27 |
3 files changed, 34 insertions, 1 deletions
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)
|