diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-22 17:40:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-22 17:40:22 -0500 |
commit | 9c02423e90cf9cb8509d4ca6565acba06e6f9b2d (patch) | |
tree | 8030c67f89b083b695900ade8d8a5d413b569f0f /src/theory/quantifiers_engine.cpp | |
parent | 810bd1f79ca8416a24d21f72a18b29689d6b57f6 (diff) |
More unused code elimination (#2358)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 17 |
1 files changed, 1 insertions, 16 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8c43e98ff..a5cd95d29 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -135,7 +135,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; if( options::relevantTriggers() ){ - d_quant_rel = new quantifiers::QuantRelevance(false); + d_quant_rel = new quantifiers::QuantRelevance; d_util.push_back(d_quant_rel); }else{ d_quant_rel = NULL; @@ -563,9 +563,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( e==Theory::EFFORT_LAST_CALL ){ - //if effort is last call, try to minimize model first - //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); - //if( ufss && !ufss->minimize() ){ return; } ++(d_statistics.d_instantiation_rounds_lc); }else if( e==Theory::EFFORT_FULL ){ ++(d_statistics.d_instantiation_rounds); @@ -908,18 +905,6 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within { d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n); } - - // added contains also the Node that just have been asserted in this - // branch - if (d_quant_rel) - { - for (std::set<Node>::iterator i = added.begin(), end = added.end(); - i != end; - i++) - { - d_quant_rel->setRelevance( i->getOperator(), 0 ); - } - } } } } |