update from the master

1 files changed, 62 insertions, 51 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 4b173c833..0bbca88eb 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file model_engine.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): Francois Bobot
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of model engine class
  **/
@@ -62,6 +62,7 @@ void ModelEngine::reset_round( Theory::Effort e ) {
 
 void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
   if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
+    Assert( !d_quantEngine->inConflict() );
     int addedLemmas = 0;
     FirstOrderModel* fm = d_quantEngine->getModel();
 
@@ -82,8 +83,10 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       Trace("model-engine-debug") << "Check model..." << std::endl;
       d_incomplete_check = false;
       //print debug
-      Trace("fmf-model-complete") << std::endl;
-      debugPrint("fmf-model-complete");
+      if( Trace.isOn("fmf-model-complete") ){
+        Trace("fmf-model-complete") << std::endl;
+        debugPrint("fmf-model-complete");
+      }
       //successfully built an acceptable model, now check it
       addedLemmas += checkModel();
     }else{
@@ -98,10 +101,10 @@ 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;
       //CVC4 will answer SAT or unknown
-      Trace("fmf-consistent") << std::endl;
-      debugPrint("fmf-consistent");
-    }else{
-      //otherwise, the search will continue
+      if( Trace.isOn("fmf-consistent") ){
+        Trace("fmf-consistent") << std::endl;
+        debugPrint("fmf-consistent");
+      }
     }
   }
 }
@@ -178,49 +181,51 @@ int ModelEngine::checkModel(){
   d_addedLemmas = 0;
   d_totalLemmas = 0;
   //for statistics
-  for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-    Node f = fm->getAssertedQuantifier( i );
-    int totalInst = 1;
-    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-      TypeNode tn = f[0][i].getType();
-      if( fm->d_rep_set.hasType( tn ) ){
-        totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+  if( Trace.isOn("model-engine") ){
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node f = fm->getAssertedQuantifier( i );
+      int totalInst = 1;
+      for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
+        TypeNode tn = f[0][j].getType();
+        if( fm->d_rep_set.hasType( tn ) ){
+          totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+        }
       }
+      d_totalLemmas += totalInst;
     }
-    d_totalLemmas += totalInst;
   }
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
   // 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++) {
-    if (d_addedLemmas==0) {
-      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-        Node f = fm->getAssertedQuantifier( i );
-        Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
-        //determine if we should check this quantifier
-        if( considerQuantifiedFormula( f ) ){
-          exhaustiveInstantiate( f, e );
-          if( Trace.isOn("model-engine-warn") ){
-            if( d_addedLemmas>10000 ){
-              Debug("fmf-exit") << std::endl;
-              debugPrint("fmf-exit");
-              exit( 0 );
-            }
-          }
-          if( optOneQuantPerRound() && d_addedLemmas>0 ){
-            break;
-          }
-        }else{
-          Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
+    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;
+      //determine if we should check this quantifier
+      if( considerQuantifiedFormula( f ) ){
+        exhaustiveInstantiate( f, e );
+        if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
+          break;
         }
+      }else{
+        Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
       }
     }
+    if( d_addedLemmas>0 ){
+      break;
+    }else{
+      Assert( !d_quantEngine->inConflict() );
+    }
   }
 
   //print debug information
-  Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
-  Trace("model-engine") << d_totalLemmas << std::endl;
+  if( d_quantEngine->inConflict() ){
+    Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl;
+  }else{
+    Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
+    Trace("model-engine") << d_totalLemmas << std::endl;
+  }
   return d_addedLemmas;
 }
 
@@ -266,15 +271,17 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
     d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
   }else{
-    Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
-    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-      Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+    if( Trace.isOn("fmf-exh-inst-debug") ){
+      Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
+      for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+        Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+      }
+      Trace("fmf-exh-inst-debug") << std::endl;
     }
-    Trace("fmf-exh-inst-debug") << std::endl;
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
-      Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl;
+      Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.d_incomplete << "..." << std::endl;
       if( !riter.d_incomplete ){
         int triedLemmas = 0;
         int addedLemmas = 0;
@@ -287,8 +294,11 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           triedLemmas++;
           //add as instantiation
-          if( d_quantEngine->addInstantiation( f, m ) ){
+          if( d_quantEngine->addInstantiation( f, m, true ) ){
             addedLemmas++;
+            if( d_quantEngine->inConflict() ){
+              break;
+            }
           }else{
             Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
           }
@@ -299,6 +309,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         d_statistics.d_exh_inst_lemmas += addedLemmas;
       }
     }else{
+      Trace("fmf-exh-inst") << "...exhaustive instantiation failed to set, incomplete=" << riter.d_incomplete << "..." << std::endl;
       Assert( riter.d_incomplete );
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
@@ -308,15 +319,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
 
 void ModelEngine::debugPrint( const char* c ){
   Trace( c ) << "Quantifiers: " << std::endl;
-  for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-    Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     Trace( c ) << "   ";
-    if( !d_quantEngine->getModelBuilder()->isQuantifierActive( f ) ){
+    if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){
       Trace( c ) << "*Inactive* ";
     }else{
       Trace( c ) << "           ";
     }
-    Trace( c ) << f << std::endl;
+    Trace( c ) << q << std::endl;
   }
   //d_quantEngine->getModel()->debugPrint( c );
 }