diff options
| author | Tim King <taking@cs.nyu.edu> | 2017-11-18 16:27:46 -0800 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-18 18:27:46 -0600 |
| commit | 6f95e3c711d39b531eb0a8ac0e098c89a5737ce2 (patch) | |
| tree | f30496e445b710b5a1fa1dae5a5cad0911648857 /src/theory/quantifiers/rewrite_engine.cpp | |
| parent | a7524f1f72c324dae36bd4a461d31e5e26fdca15 (diff) | |
Names the Effort enum of QuantConflictFind class. (#1354)
* Changes the Effort level of QuantConflictFind to an enum class. Adding a third value to the enum to indicate not being set. Minor refactoring related to this change. Resolves CID 1172043.
* Fixing a missed assertion. Fixing a few compiler warnings.
* Switching back to an enum from an enum class.
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 2c85bceb8..337d61976 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -119,7 +119,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { if( qcf ){ //reset QCF module qcf->computeRelevantEqr(); - qcf->setEffort( QuantConflictFind::effort_conflict ); + qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT); //get the proper quantifiers info std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f ); if( it!=d_qinfo.end() ){ |