Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix for sygus.

1 files changed, 10 insertions, 6 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 1d6676464..ce780a29b 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -35,7 +35,7 @@ using namespace CVC4::theory::inst;
 //Model Engine constructor
 ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
 QuantifiersModule( qe ),
-d_incomplete_check(false),
+d_incomplete_check(true),
 d_addedLemmas(0),
 d_triedLemmas(0),
 d_totalLemmas(0)
@@ -55,6 +55,10 @@ unsigned ModelEngine::needsModel( Theory::Effort e ) {
   return QuantifiersEngine::QEFFORT_MODEL;  
 }
 
+void ModelEngine::reset_round( Theory::Effort e ) {
+  d_incomplete_check = true;
+}
+
 void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
   if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
     int addedLemmas = 0;
@@ -95,16 +99,16 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       //CVC4 will answer SAT or unknown
       Trace("fmf-consistent") << std::endl;
       debugPrint("fmf-consistent");
-      //if the check was incomplete, we must set incomplete flag
-      if( d_incomplete_check ){
-        d_quantEngine->getOutputChannel().setIncomplete();
-      }
     }else{
       //otherwise, the search will continue
     }
   }
 }
 
+bool ModelEngine::checkComplete() {
+  return !d_incomplete_check;
+}
+
 void ModelEngine::registerQuantifier( Node f ){
   if( Trace.isOn("fmf-warn") ){
     bool canHandle = true;
@@ -218,7 +222,7 @@ int ModelEngine::checkModel(){
     if( d_addedLemmas==0 && options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
       //set incomplete
       if( effort==0 ){
-        d_quantEngine->getOutputChannel().setIncomplete();
+        d_incomplete_check = true;
       }
       break;
     }