diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-18 10:05:32 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-18 10:05:32 -0500 |
| commit | 22c24eeffd7dc0e44533ccd8c2c6dc91eb77f2f3 (patch) | |
| tree | c524aa83ebdd80ae911b697e243146aa25f99025 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
| parent | eb27070783709a410e6655ba9af6da6de5b0da9d (diff) | |
Limit duplicate propagating instances to avoid exponential behavior in QuantConflictFind.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index c10ba944b..b0340d630 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -305,6 +305,10 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { } childrenChanged = childrenChanged || c!=body[i]; } + //if( body.getKind()==ITE && isLiteral( body[0] ) ){ + // ret = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ), + // NodeManager::currentNM()->mkNode( OR, body[0], body[2] ) ); + //} if( childrenChanged ){ return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children ); }else{ |