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 /src/theory | |
| parent | 327fe83f2e0533d53902645364180bc51ff20dcc (diff) | |
Apply empty splits more aggressively in sets+cardinality (#2907)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 7 |
1 files changed, 6 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; |