diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-23 15:09:25 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-23 15:09:25 +0100 |
| commit | 8beb91c3113dae4a858a30c7a21387e833d60527 (patch) | |
| tree | 3779a2c309adb7c6200f709244f90a5d0ac554da /src/theory/quantifiers_engine.cpp | |
| parent | 973cbd67611a2943714fd9544d098ec1472a40b8 (diff) | |
Decouple counter-example guided quantifier instantiation from Sygus.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a475a8912..888cdbce0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -899,11 +899,9 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ // doing literal-based matching (consider polarity of literals) for( int i=0; i<(int)nodes.size(); i++ ){ Node prev = nodes[i]; - bool nodeChanged = false; if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){ bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] ); nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) ); - nodeChanged = true; } //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){ // Node req = qe->getPhaseReqEquality( f, trNodes[i] ); |