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 | |
| parent | eb27070783709a410e6655ba9af6da6de5b0da9d (diff) | |
Limit duplicate propagating instances to avoid exponential behavior in QuantConflictFind.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 4 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 93cd4be91..ec93b96fc 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2069,7 +2069,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { } }else{ Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; - //Assert( false ); + //this should only happen if the algorithm generates the same propagating instance twice this round + //in this case, break to avoid exponential behavior + break; } } //clean up assigned @@ -2082,6 +2084,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl; } } + Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; if( d_conflict ){ break; } 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{ |