\r
//-------------------------------------------------- check function\r
\r
+bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
+ bool performCheck = false;\r
+ if( options::quantConflictFind() && !d_conflict ){\r
+ if( level==Theory::EFFORT_LAST_CALL ){\r
+ performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;\r
+ }else if( level==Theory::EFFORT_FULL ){\r
+ performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;\r
+ }else if( level==Theory::EFFORT_STANDARD ){\r
+ performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;\r
+ }\r
+ }\r
+ return performCheck;\r
+}\r
+\r
void QuantConflictFind::reset_round( Theory::Effort level ) {\r
d_needs_computeRelEqr = true;\r
}\r
\r
/** check */\r
-void QuantConflictFind::check( Theory::Effort level ) {\r
- Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
- if( d_conflict ){\r
- Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
- if( level>=Theory::EFFORT_FULL ){\r
- Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;\r
- //Assert( false );\r
- }\r
- }else{\r
- int addedLemmas = 0;\r
- if( d_performCheck ){\r
+void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {\r
+ if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){\r
+ Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
+ if( d_conflict ){\r
+ Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
+ if( level>=Theory::EFFORT_FULL ){\r
+ Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;\r
+ //Assert( false );\r
+ }\r
+ }else{\r
+ int addedLemmas = 0;\r
++(d_statistics.d_inst_rounds);\r
double clSet = 0;\r
int prevEt = 0;\r
}\r
}\r
if( addedLemmas>0 ){\r
- d_quantEngine->flushLemmas();\r
break;\r
}\r
}\r
Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl;\r
}\r
}\r
- }\r
- Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
- }\r
-}\r
-\r
-bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
- d_performCheck = false;\r
- if( options::quantConflictFind() && !d_conflict ){\r
- if( level==Theory::EFFORT_LAST_CALL ){\r
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;\r
- }else if( level==Theory::EFFORT_FULL ){\r
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;\r
- }else if( level==Theory::EFFORT_STANDARD ){\r
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;\r
+ Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
}\r
}\r
- return d_performCheck;\r
}\r
\r
void QuantConflictFind::computeRelevantEqr() {\r