Refactor setIncomplete in quantifiers.

1 files changed, 22 insertions, 11 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 7658f2b6b..7f560b74c 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -99,7 +99,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
     }
 
     if( addedLemmas==0 ){
-      Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
+      Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl;
       //CVC4 will answer SAT or unknown
       if( Trace.isOn("fmf-consistent") ){
         Trace("fmf-consistent") << std::endl;
@@ -113,6 +113,10 @@ bool ModelEngine::checkComplete() {
   return !d_incomplete_check;
 }
 
+bool ModelEngine::checkCompleteFor( Node q ) {
+  return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end();
+}
+
 void ModelEngine::registerQuantifier( Node f ){
   if( Trace.isOn("fmf-warn") ){
     bool canHandle = true;
@@ -195,17 +199,18 @@ int ModelEngine::checkModel(){
   // FMC uses two sub-effort levels
   int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
   for( int e=0; e<e_max; e++) {
+    d_incomplete_quants.clear();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-      Node f = fm->getAssertedQuantifier( i, true );
-      Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
+      Node q = fm->getAssertedQuantifier( i, true );
+      Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
       //determine if we should check this quantifier
-      if( considerQuantifiedFormula( f ) ){
-        exhaustiveInstantiate( f, e );
+      if( considerQuantifiedFormula( q ) ){
+        exhaustiveInstantiate( q, e );
         if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
           break;
         }
       }else{
-        Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
+        Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
       }
     }
     if( d_addedLemmas>0 ){
@@ -260,12 +265,16 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
   mb->d_triedLemmas = 0;
   mb->d_addedLemmas = 0;
-  mb->d_incomplete_check = false;
-  if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
-    Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
+  int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort );
+  if( retEi!=0 ){
+    if( retEi<0 ){
+      Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
+      d_incomplete_quants.push_back( f );
+    }else{
+      Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
+    }
     d_triedLemmas += mb->d_triedLemmas;
     d_addedLemmas += mb->d_addedLemmas;
-    d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
     d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
   }else{
     if( Trace.isOn("fmf-exh-inst-debug") ){
@@ -309,7 +318,9 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
       Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
-    d_incomplete_check = d_incomplete_check || riter.isIncomplete();
+    if( riter.isIncomplete() ){
+      d_incomplete_quants.push_back( f );
+    }
   }
 }