Refactor setIncomplete in quantifiers.

20 files changed, 138 insertions, 80 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 97116dee4..2ccc17e55 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -836,7 +836,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
 //--------------------model checking---------------------------------------
 
 //do exhaustive instantiation
-bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
+int AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
   Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl;
   if (effort==0) {
     FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();
@@ -868,9 +868,10 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in
       d_addedLemmas += lem;
       Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl;
     }
-    return quantValid;
+    return quantValid ? 1 : 0;
+  }else{
+    return 1;
   }
-  return true;
 }
 
 bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) {
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 3669d38b7..0adaef638 100644
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -93,7 +93,7 @@ public:
   //process build model
   void processBuildModel(TheoryModel* m, bool fullModel);
   //do exhaustive instantiation
-  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
+  int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
 };
 
 }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index be608aeaa..72057e734 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -589,7 +589,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
 }
 
 
-bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
+int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
   Assert( !d_qe->inConflict() );
   if( optUseModel() ){
@@ -723,15 +723,15 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
           if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
             if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){
               //something went wrong, resort to exhaustive instantiation
-              return false;
+              return 0;
             }
           }
         }
       }
     }
-    return true;
+    return 1;
   }else{
-    return false;
+    return 0;
   }
 }
 
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 411b7a5eb..7d21b4185 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -139,7 +139,7 @@ public:
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
 
-  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+  int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
 
   Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
 
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 82f45916c..9ee62964b 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -285,6 +285,15 @@ bool InstStrategyCbqi::checkComplete() {
   }
 }
 
+bool InstStrategyCbqi::checkCompleteFor( Node q ) {
+  std::map< Node, int >::iterator it = d_do_cbqi.find( q );
+  if( it!=d_do_cbqi.end() ){
+    return it->second>0;
+  }else{
+    return false;
+  }
+}
+
 Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){
   std::map< Node, Node >::iterator it = visited.find( n );
   if( it==visited.end() ){
@@ -334,7 +343,7 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis
 
 void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
-    if( !options::cbqiAll() ){
+    if( d_do_cbqi[q]==2 ){
       //take full ownership of the quantified formula
       d_quantEngine->setOwner( q, this );
       
@@ -512,43 +521,49 @@ int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
 }
 
 bool InstStrategyCbqi::doCbqi( Node q ){
-  std::map< Node, bool >::iterator it = d_do_cbqi.find( q );
+  std::map< Node, int >::iterator it = d_do_cbqi.find( q );
   if( it==d_do_cbqi.end() ){
-    bool ret = true;
+    int ret = 2;
     if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
       //if has an instantiation pattern, don't do it
       if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
         for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
           if( q[2][i].getKind()==INST_PATTERN ){
-            ret = false;
+            ret = 0;
           }
         }
       }
-      if( ret ){
-        if( options::cbqiAll() ){
-          ret = true;
-        }else{
-          //if quantifier has a non-handled variable, then do not use cbqi
-          //if quantifier has an APPLY_UF term, then do not use cbqi
-          //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
-          int ncbqiv = hasNonCbqiVariable( q );
-          if( ncbqiv==1 ){
-            //all variables imply this will be handled regardless of body (e.g. for EPR)
-            ret = true;
-          }else if( ncbqiv==0 ){
-            std::map< Node, bool > visited;
-            ret = !hasNonCbqiOperator( q[1], visited );
-          }else{
-            ret = false;
+      if( ret!=0 ){
+        //if quantifier has a non-handled variable, then do not use cbqi
+        //if quantifier has an APPLY_UF term, then do not use cbqi unless EPR
+        int ncbqiv = hasNonCbqiVariable( q );
+        if( ncbqiv==0 || ncbqiv==1 ){
+          std::map< Node, bool > visited;
+          if( hasNonCbqiOperator( q[1], visited ) ){
+            if( ncbqiv==1 ){
+              //all variables are fully handled, this implies this will be handlable regardless of body (e.g. for EPR)
+              //  so, try but not exclusively
+              ret = 1;
+            }else{
+              //cannot be handled
+              ret = 0;
+            }
           }
+        }else{
+          // unhandled variable type
+          ret = 0;
+        }
+        if( ret==0 && options::cbqiAll() ){
+          //try but not exclusively
+          ret = 1;
         }
       }
     }
     Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
     d_do_cbqi[q] = ret;
-    return ret;
+    return ret!=0;
   }else{
-    return it->second;
+    return it->second!=0;
   }
 }
 
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 18f4f4a31..eab267747 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -48,8 +48,8 @@ protected:
   std::map< Node, bool > d_active_quant;
   /** whether we have instantiated quantified formulas */
   //NodeSet d_added_inst;
-  /** whether to do cbqi for this quantified formula */
-  std::map< Node, bool > d_do_cbqi;
+  /** whether to do cbqi for this quantified formula 0 : no, 2 : yes, 1 : yes but not exclusively, -1 : heuristically */
+  std::map< Node, int > d_do_cbqi;
   /** register ce lemma */
   bool registerCbqiLemma( Node q );
   virtual void registerCounterexampleLemma( Node q, Node lem );
@@ -103,6 +103,7 @@ public:
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();
+  bool checkCompleteFor( Node q );
   void preRegisterQuantifier( Node q );
   void registerQuantifier( Node q );
   /** get next decision request */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index db597d031..f46d08f08 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -151,19 +151,9 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
   }
 }
 
-bool InstantiationEngine::checkComplete() {
-  if( !options::finiteModelFind() ){
-    for( unsigned i=0; i<d_quants.size(); i++ ){
-      if( isIncomplete( d_quants[i] ) ){
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
-bool InstantiationEngine::isIncomplete( Node q ) {
-  return true;
+bool InstantiationEngine::checkCompleteFor( Node q ) {
+  //TODO?
+  return false;
 }
 
 void InstantiationEngine::preRegisterQuantifier( Node q ) {
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index d2b3740a1..79963cb45 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -78,7 +78,7 @@ public:
   bool needsCheck( Theory::Effort e );
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
-  bool checkComplete();
+  bool checkCompleteFor( Node q );
   void preRegisterQuantifier( Node q );
   void registerQuantifier( Node q );
   Node explain(TNode n){ return Node::null(); }
diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 94abf3c90..04a6bc9c8 100644
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -66,6 +66,8 @@ public:
   void check( Theory::Effort e, unsigned quant_e );
   /* Called for new quantifiers */
   void registerQuantifier( Node q ) {}
+  /* check complete */
+  bool checkComplete() { return !d_wasInvoked; }
   void assertNode( Node n ) {}
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const { return "LtePartialInst"; }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 7bbe06108..b30c2addb 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -391,7 +391,7 @@ bool QModelBuilderIG::isTermActive( Node n ){
 
 
 //do exhaustive instantiation
-bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
+int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   if( optUseModel() ){
     RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
@@ -470,10 +470,9 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
       }
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
-    d_incomplete_check = riter.isIncomplete();
-    return true;
+    return riter.isIncomplete() ? -1 : 1;
   }else{
-    return false;
+    return 0;
   }
 }
 
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index e4f9529a8..9b89e5ef6 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -38,13 +38,14 @@ public:
   virtual ~QModelBuilder() throw() {}
   // is quantifier active?
   virtual bool isQuantifierActive( Node f );
-  //do exhaustive instantiation
-  virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
+  //do exhaustive instantiation  
+  // 0 :  failed, but resorting to true exhaustive instantiation may work
+  // >0 : success
+  // <0 : failed
+  virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
   //whether to construct model
   virtual bool optUseModel();
   /** number of lemmas generated while building model */
-  //is the exhaustive instantiation incomplete?
-  bool d_incomplete_check;
   int d_addedLemmas;
   int d_triedLemmas;
   /** exist instantiation ? */
@@ -142,7 +143,7 @@ public:
   // is quantifier active?
   bool isQuantifierActive( Node f );
   //do exhaustive instantiation
-  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+  int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
 
   //temporary stats
   int d_numQuantSat;
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 );
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 12f18aa08..8575792b4 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -42,6 +42,8 @@ private:
   //temporary statistics
   //is the exhaustive instantiation incomplete?
   bool d_incomplete_check;
+  // set of quantified formulas for which check was incomplete
+  std::vector< Node > d_incomplete_quants;
   int d_addedLemmas;
   int d_triedLemmas;
   int d_totalLemmas;
@@ -54,6 +56,7 @@ public:
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();
+  bool checkCompleteFor( Node q );
   void registerQuantifier( Node f );
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 35b3e1f9e..df8533135 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -73,6 +73,11 @@ bool QuantDSplit::needsCheck( Theory::Effort e ) {
   return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
 }
 
+bool QuantDSplit::checkCompleteFor( Node q ) {
+  // true if we split q
+  return d_added_split.find( q )!=d_added_split.end();
+}
+
 /* Call during quantifier engine's check */
 void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
   //add lemmas ASAP (they are a reduction)
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index d36824998..3e3b08814 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -43,6 +43,7 @@ public:
   /* Called for new quantifiers */
   void registerQuantifier( Node q ) {}
   void assertNode( Node n ) {}
+  bool checkCompleteFor( Node q );
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const { return "QuantDSplit"; }
 };
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index c3ddfacff..f4284a8ab 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -429,7 +429,7 @@ void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& vi
         for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
           TypeNode tn = n[0][i].getType();
           if( d_non_epr.find( tn )==d_non_epr.end() ){
-            Trace("quant-epr") << "Sort " << tn << " is non-EPR because of nested quantification." << std::endl;
+            Trace("quant-epr") << "Sort " << tn << " is non-EPR because of nested or possible existential quantification." << std::endl;
             d_non_epr[tn] = true;
           }
         }
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index d8e57b1ca..3ff21aa6e 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -51,8 +51,10 @@ public:
   virtual void reset_round( Theory::Effort e ){}
   /* Call during quantifier engine's check */
   virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
-  /* check was complete (e.g. no lemmas implies a model) */
+  /* check was complete, return false if there is no way to answer "SAT", true if maybe can answer "SAT" */
   virtual bool checkComplete() { return true; }
+  /* check was complete for quantified formula q (e.g. no lemmas implies a model) */
+  virtual bool checkCompleteFor( Node q ) { return false; }
   /* Called for new quantified formulas */
   virtual void preRegisterQuantifier( Node q ) { }
   /* Called for new quantifiers after owners are finalized */
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 3add7a9d7..a2a2e99c6 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -295,6 +295,11 @@ void RewriteEngine::assertNode( Node n ) {
 
 }
 
+bool RewriteEngine::checkCompleteFor( Node q ) { 
+  // by semantics of rewrite rules, saturation -> SAT 
+  return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end();
+}
+
 Node RewriteEngine::getInstConstNode( Node n, Node q ) {
   std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n );
   if( it==d_inst_const_node[q].end() ){
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 8d0678724..ef3337e53 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -56,6 +56,7 @@ public:
   void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node f );
   void assertNode( Node n );
+  bool checkCompleteFor( Node q );
   /** Identify this module */
   std::string identify() const { return "RewriteEngine"; }
 };
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e48c6eafe..fbfdb856e 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -219,7 +219,6 @@ void QuantifiersEngine::finishInit(){
     d_sg_gen = new quantifiers::ConjectureGenerator( this, c );
     d_modules.push_back( d_sg_gen );
   }
-  //maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
     d_inst_engine = new quantifiers::InstantiationEngine( this );
     d_modules.push_back(  d_inst_engine );
@@ -395,13 +394,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
   d_conflict = false;
   d_hasAddedLemma = false;
   bool setIncomplete = false;
-  if( e==Theory::EFFORT_LAST_CALL ){
-    //sources of incompleteness
-    if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){
-      Trace("quant-engine-debug") << "Set incomplete due to LTE partial instantiation." << std::endl;
-      setIncomplete = true;
-    }
-  }
   bool usedModelBuilder = false;
 
   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
@@ -544,20 +536,49 @@ void QuantifiersEngine::check( Theory::Effort e ){
           }
         }else if( quant_e==QEFFORT_MODEL ){
           if( e==Theory::EFFORT_LAST_CALL ){
+            //sources of incompleteness
             if( !d_recorded_inst.empty() ){
+              Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl;
               setIncomplete = true;
             }
             //if we have a chance not to set incomplete
             if( !setIncomplete ){
               setIncomplete = false;
               //check if we should set the incomplete flag
-              for( unsigned i=0; i<qm.size(); i++ ){
-                if( !qm[i]->checkComplete() ){
-                  Trace("quant-engine-debug") << "Set incomplete because " << qm[i]->identify().c_str() << " was incomplete." << std::endl;
+              for( unsigned i=0; i<d_modules.size(); i++ ){
+                if( !d_modules[i]->checkComplete() ){
+                  Trace("quant-engine-debug") << "Set incomplete because " << d_modules[i]->identify().c_str() << " was incomplete." << std::endl;
                   setIncomplete = true;
                   break;
                 }
               }
+              if( !setIncomplete ){
+                //look at individual quantified formulas, one module must claim completeness for each one
+                for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
+                  bool hasCompleteM = false;
+                  Node q = d_model->getAssertedQuantifier( i );
+                  QuantifiersModule * qmd = getOwner( q );
+                  if( qmd!=NULL ){
+                    hasCompleteM = qmd->checkCompleteFor( q );
+                  }else{
+                    for( unsigned j=0; j<d_modules.size(); j++ ){
+                      if( d_modules[j]->checkCompleteFor( q ) ){
+                        qmd = d_modules[j];
+                        hasCompleteM = true;
+                        break;
+                      }
+                    }
+                  }
+                  if( !hasCompleteM ){
+                    Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl;
+                    setIncomplete = true;
+                    break;
+                  }else{
+                    Assert( qmd!=NULL );
+                    Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl;
+                  }
+                }
+              }
             }
             //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
             if( !setIncomplete ){