Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

1 files changed, 24 insertions, 29 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 7658f2b6b..9c09371c4 100755
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -73,7 +73,6 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       Trace("model-engine") << "---Model Engine Round---" << std::endl;
       clSet = double(clock())/double(CLOCKS_PER_SEC);
     }
-    ++(d_statistics.d_inst_rounds);
 
     Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
     //let the strong solver verify that the model is minimal
@@ -99,7 +98,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 +112,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 +198,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,13 +264,17 @@ 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;
+    d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->d_addedLemmas;
   }else{
     if( Trace.isOn("fmf-exh-inst-debug") ){
       Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
@@ -303,13 +311,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         }
         d_addedLemmas += addedLemmas;
         d_triedLemmas += triedLemmas;
-        d_statistics.d_exh_inst_lemmas += addedLemmas;
+        d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas;
       }
     }else{
       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 );
+    }
   }
 }
 
@@ -328,18 +338,3 @@ void ModelEngine::debugPrint( const char* c ){
   //d_quantEngine->getModel()->debugPrint( c );
 }
 
-ModelEngine::Statistics::Statistics():
-  d_inst_rounds("ModelEngine::Inst_Rounds", 0),
-  d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ),
-  d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 )
-{
-  smtStatisticsRegistry()->registerStat(&d_inst_rounds);
-  smtStatisticsRegistry()->registerStat(&d_exh_inst_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_mbqi_inst_lemmas);
-}
-
-ModelEngine::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
-  smtStatisticsRegistry()->unregisterStat(&d_exh_inst_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_mbqi_inst_lemmas);
-}