From 8d3446768446f16e71dca48bdf14d4ed767756aa Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 1 Aug 2014 15:16:17 +0200
Subject: Minor cleanup from previous commit.  Better organization for how
 quantifiers modules check (introduce QuantifiersEngine::QEffort).

---
 src/theory/quantifiers/bounded_integers.cpp     |  13 +-
 src/theory/quantifiers/bounded_integers.h       |   3 +-
 src/theory/quantifiers/conjecture_generator.cpp | 197 +++++++++---------------
 src/theory/quantifiers/conjecture_generator.h   |  12 +-
 src/theory/quantifiers/instantiation_engine.cpp |  60 ++++----
 src/theory/quantifiers/instantiation_engine.h   |   3 +-
 src/theory/quantifiers/model_engine.cpp         |   9 +-
 src/theory/quantifiers/model_engine.h           |   3 +-
 src/theory/quantifiers/options                  |   4 +-
 src/theory/quantifiers/options_handlers.h       |   2 +-
 src/theory/quantifiers/quant_conflict_find.cpp  |  53 ++++---
 src/theory/quantifiers/quant_conflict_find.h    |   7 +-
 src/theory/quantifiers/rewrite_engine.cpp       |  11 +-
 src/theory/quantifiers/rewrite_engine.h         |   3 +-
 src/theory/quantifiers/term_database.cpp        |  67 ++++----
 src/theory/quantifiers/term_database.h          |   5 -
 src/theory/quantifiers_engine.cpp               |  59 +++++--
 src/theory/quantifiers_engine.h                 |  18 ++-
 18 files changed, 247 insertions(+), 282 deletions(-)

(limited to 'src')

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index d6f9704b3..57799fd8e 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -243,8 +243,13 @@ void BoundedIntegers::process( Node f, Node n, bool pol,
   }
 }
 
-void BoundedIntegers::check( Theory::Effort e ) {
-  if( e==Theory::EFFORT_LAST_CALL ){
+bool BoundedIntegers::needsCheck( Theory::Effort e ) {
+  return e==Theory::EFFORT_LAST_CALL;
+}
+
+void BoundedIntegers::check( Theory::Effort e, unsigned quant_e ) {
+  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+    Trace("bint-engine") << "---Bounded Integers---" << std::endl;
     bool addedLemma = false;
     //make sure proxies are up-to-date with range
     for( unsigned i=0; i<d_ranges.size(); i++) {
@@ -252,9 +257,7 @@ void BoundedIntegers::check( Theory::Effort e ) {
         addedLemma = true;
       }
     }
-    if( addedLemma ){
-      d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
-    }
+    Trace("bint-engine") << "   addedLemma = " << addedLemma << std::endl;
   }
 }
 
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index ac188ca65..355360e41 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -110,7 +110,8 @@ private:
 public:
   BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
 
-  void check( Theory::Effort e );
+  bool needsCheck( Theory::Effort e );
+  void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node f );
   void assertNode( Node n );
   Node getNextDecisionRequest();
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 462738cf8..a7c67a5e4 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file subgoal_generator.cpp
+/*! \file conjecture_generator.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: none
@@ -156,7 +156,7 @@ void ConjectureGenerator::doPendingAddUniversalTerms() {
       Node t = pending[i];
       TypeNode tn = t.getType();
       Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;
-      //get all equivalent terms from conjecture database
+      //get all equivalent terms based on theorem database
       std::vector< Node > eq_terms;
       d_thm_index.getEquivalentTerms( t, eq_terms );
       if( !eq_terms.empty() ){
@@ -184,6 +184,17 @@ void ConjectureGenerator::doPendingAddUniversalTerms() {
       }else{
         Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl;
       }
+      //if occurs at ground level, merge with representative of ground equality engine
+      /*
+      eq::EqualityEngine * ee = getEqualityEngine();
+      if( ee->hasTerm( t ) ){
+        TNode grt = ee->getRepresentative( t );
+        if( t!=grt ){
+          Node exp;
+          d_uequalityEngine.assertEquality( t.eqNode( grt ), true, exp );
+        }
+      }
+      */
     }
   }
 }
@@ -289,19 +300,6 @@ TermDb * ConjectureGenerator::getTermDatabase() {
   return d_quantEngine->getTermDatabase();
 }
 
-bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
-  if( e==Theory::EFFORT_FULL ){
-    //d_fullEffortCount++;
-    return d_fullEffortCount%optFullCheckFrequency()==0;
-  }else{
-    return false;
-  }
-}
-
-void ConjectureGenerator::reset_round( Theory::Effort e ) {
-
-}
-
 Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
   Assert( !tn.isNull() );
   while( d_free_var[tn].size()<=i ){
@@ -374,16 +372,19 @@ bool ConjectureGenerator::isGroundTerm( TNode n ) {
   return std::find( d_ground_terms.begin(), d_ground_terms.end(), n )!=d_ground_terms.end();
 }
 
-void ConjectureGenerator::check( Theory::Effort e ) {
-  if( e==Theory::EFFORT_FULL ){
-    bool doCheck = d_fullEffortCount%optFullCheckFrequency()==0;
-    if( d_quantEngine->hasAddedLemma() ){
-     doCheck = false;
-    }else{
-      d_fullEffortCount++;
-    }
-    if( doCheck ){
-      Trace("sg-engine") << "---Subgoal engine, effort = " << e << "--- " << std::endl;
+bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
+  return e==Theory::EFFORT_FULL;
+}
+
+void ConjectureGenerator::reset_round( Theory::Effort e ) {
+
+}
+
+void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
+  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+    d_fullEffortCount++;
+    if( d_fullEffortCount%optFullCheckFrequency()==0 ){
+      Trace("sg-engine") << "---Conjecture generator, effort = " << e << "--- " << std::endl;
       eq::EqualityEngine * ee = getEqualityEngine();
 
       Trace("sg-proc") << "Get eq classes..." << std::endl;
@@ -559,7 +560,7 @@ void ConjectureGenerator::check( Theory::Effort e ) {
       quantifiers::FirstOrderModel* m = d_quantEngine->getModel();
       for( int i=0; i<m->getNumAssertedQuantifiers(); i++ ){
         Node q = m->getAssertedQuantifier( i );
-        Trace("sg-conjecture-debug") << "Is " << q << " a relevant theorem?" << std::endl;
+        Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl;
         Node conjEq;
         if( q[1].getKind()==EQUAL ){
           bool isSubsume = false;
@@ -614,12 +615,12 @@ void ConjectureGenerator::check( Theory::Effort e ) {
         if( std::find( provenConj.begin(), provenConj.end(), q )==provenConj.end() ){
           //check each skolem variable
           bool disproven = true;
-          std::vector< Node > sk;
-          getTermDatabase()->getSkolemConstants( q, sk, true );
+          //std::vector< Node > sk;
+          //getTermDatabase()->getSkolemConstants( q, sk, true );
           Trace("sg-conjecture") << "    CONJECTURE : ";
           std::vector< Node > ce;
-          for( unsigned j=0; j<sk.size(); j++ ){
-            TNode k = sk[j];
+          for( unsigned j=0; j<getTermDatabase()->d_skolem_constants[q].size(); j++ ){
+            TNode k = getTermDatabase()->d_skolem_constants[q][j];
             TNode rk = getRepresentative( k );
             std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk );
             //check if it is a ground term
@@ -627,7 +628,7 @@ void ConjectureGenerator::check( Theory::Effort e ) {
               Trace("sg-conjecture") << "ACTIVE : " << q;
               if( Trace.isOn("sg-gen-eqc") ){
                 Trace("sg-conjecture") << " { ";
-                for( unsigned k=0; k<sk.size(); k++ ){ Trace("sg-conjecture") << sk[k] << ( j==k ? "*" : "" ) << " "; }
+                for( unsigned k=0; k<getTermDatabase()->d_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermDatabase()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; }
                 Trace("sg-conjecture") << "}";
               }
               Trace("sg-conjecture") << std::endl;
@@ -903,8 +904,8 @@ void ConjectureGenerator::check( Theory::Effort e ) {
         for( unsigned i=0; i<d_waiting_conjectures.size(); i++ ){
           Assert( d_waiting_conjectures[i].getKind()==FORALL );
           Node lem = NodeManager::currentNM()->mkNode( OR, d_waiting_conjectures[i].negate(), d_waiting_conjectures[i] );
-          d_quantEngine->getOutputChannel().lemma( lem );
-          d_quantEngine->getOutputChannel().requirePhase( d_waiting_conjectures[i], false );
+          d_quantEngine->addLemma( lem, false );
+          d_quantEngine->addRequirePhase( d_waiting_conjectures[i], false );
         }
         d_waiting_conjectures.clear();
       }
@@ -1244,20 +1245,13 @@ void ConjectureGenerator::processCandidateConjecture( unsigned cid, unsigned dep
           Trace("sg-conjecture-debug") << ", ";
         }
         Trace("sg-conjecture-debug") << it->first << " : " << it->second.size() << "/" << d_pattern_fun_id[lhs][it->first];
+        if( it->second.size()==1 ){
+          Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";
+        }
         firstTime = false;
       }
       Trace("sg-conjecture-debug") << std::endl;
     }
-    /*
-    if( getUniversalRepresentative( lhs )!=lhs ){
-      std::cout << "bad universal representative LHS : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;
-      exit(0);
-    }
-    if( getUniversalRepresentative( rhs )!=rhs ){
-      std::cout << "bad universal representative RHS : " << rhs << " " << getUniversalRepresentative( rhs ) << std::endl;
-      exit(0);
-    }
-    */
     Assert( getUniversalRepresentative( rhs )==rhs );
     Assert( getUniversalRepresentative( lhs )==lhs );
     //make universal quantified formula
@@ -1273,7 +1267,6 @@ void ConjectureGenerator::processCandidateConjecture( unsigned cid, unsigned dep
     Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );
     Node conj = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );
     conj = Rewriter::rewrite( conj );
-    Trace("sg-conjecture-debug") << "   formula is : " << conj << std::endl;
     d_waiting_conjectures.push_back( conj );
   }
 }
@@ -1331,6 +1324,8 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
         }
       }
       if( optFilterConfirmationDomain() ){
+        std::vector< TNode > vars;
+        std::vector< TNode > subs;
         for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
           Assert( d_pattern_fun_id[lhs].find( it->first )!=d_pattern_fun_id[lhs].end() );
           unsigned req = d_pattern_fun_id[lhs][it->first];
@@ -1342,6 +1337,22 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
             Trace("sg-cconj") << "  -> did not find at least " << d_pattern_fun_id[lhs][it->first] << " different values in ground substitutions for variable " << it->first << "." << std::endl;
             return false;
           }
+          if( it->second.size()==1 ){
+            vars.push_back( it->first );
+            subs.push_back( it->second[0] );
+          }
+        }
+        if( optFilterConfirmationNonCanonical() && !vars.empty() ){
+          Node slhs = lhs.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+          Node srhs = rhs.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+          TNode slhsr = getUniversalRepresentative( slhs, true );
+          TNode srhsr = getUniversalRepresentative( srhs, true );
+          if( areUniversalEqual( slhsr, srhsr ) ){
+            Trace("sg-cconj") << "  -> all ground witnesses can be proven by other theorems." << std::endl;
+            return false; 
+          }else{
+            Trace("sg-cconj-debug") << "Checked if " << slhsr << " and " << srhsr << " were equal." << std::endl;
+          }
         }
       }
     }
@@ -1353,70 +1364,27 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
         Trace("sg-cconj") << "     #witnesses for " << it->first << " : " << it->second.size() << std::endl;
       }
     }
-
-    return true;
-  }
-}
-
-
-
-bool ConjectureGenerator::processCandidateConjecture2( TNode rhs, TypeNode tn, unsigned depth ) {
-  for( unsigned j=0; j<d_rel_patterns_at_depth[tn][depth].size(); j++ ){
-    if( processCandidateConjecture2( d_rel_patterns_at_depth[tn][depth][j], rhs ) ){
-      return true;
-    }
-  }
-  return false;
-}
-
-bool ConjectureGenerator::processCandidateConjecture2( TNode lhs, TNode rhs ) {
-  if( !considerCandidateConjecture( lhs, rhs ) ){
-    return false;
-  }else{
-    Trace("sg-conjecture") << "* Candidate conjecture : " << lhs << " == " << rhs << std::endl;
-    Trace("sg-conjecture-debug") << "     LHS generalization depth : " << d_gen_depth[lhs] << std::endl;
-    if( optFilterConfirmation() || optFilterFalsification() ){
-      Trace("sg-conjecture-debug") << "     confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;
-      Trace("sg-conjecture-debug") << "     #witnesses for ";
-      bool firstTime = true;
-      for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
-        if( !firstTime ){
-          Trace("sg-conjecture-debug") << ", ";
-        }
-        Trace("sg-conjecture-debug") << it->first << " : " << it->second.size() << "/" << d_pattern_fun_id[lhs][it->first];
-        firstTime = false;
-      }
-      Trace("sg-conjecture-debug") << std::endl;
-    }
+    
+    /*
     if( getUniversalRepresentative( lhs )!=lhs ){
-      Trace("ajr-temp") << "bad universal representative : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;
+      std::cout << "bad universal representative LHS : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;
+      exit(0);
     }
-    Assert( getUniversalRepresentative( rhs )==rhs );
-    Assert( getUniversalRepresentative( lhs )==lhs );
-    //make universal quantified formula
-    Assert( std::find( d_eq_conjectures[lhs].begin(), d_eq_conjectures[lhs].end(), rhs )==d_eq_conjectures[lhs].end() );
-    d_eq_conjectures[lhs].push_back( rhs );
-    d_eq_conjectures[rhs].push_back( lhs );
-    std::vector< Node > bvs;
-    for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){
-      for( unsigned i=0; i<=it->second; i++ ){
-        bvs.push_back( getFreeVar( it->first, i ) );
-      }
+    if( getUniversalRepresentative( rhs )!=rhs ){
+      std::cout << "bad universal representative RHS : " << rhs << " " << getUniversalRepresentative( rhs ) << std::endl;
+      exit(0);
     }
-    Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );
-    Node conj = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );
-    conj = Rewriter::rewrite( conj );
-    Trace("sg-conjecture-debug") << "   formula is : " << conj << std::endl;
-    d_waiting_conjectures.push_back( conj );
+    */
+    
+    //check if still canonical representation (should be, but for efficiency this is not guarenteed)
+    if( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ){
+      Trace("sg-cconj") << "  -> after processing, not canonical." << std::endl;
+    }
+    
     return true;
   }
 }
 
-
-
-
-
-
 bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs ) {
   if( Trace.isOn("sg-cconj-debug") ){
     Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs << ", based on substituion: " << std::endl;
@@ -1807,30 +1775,6 @@ Node TermGenerator::getTerm( ConjectureGenerator * s ) {
   return Node::null();
 }
 
-/*
-int TermGenerator::getActiveChild( ConjectureGenerator * s ) {
-  if( d_status==1 || d_status==2 ){
-    return d_id;
-  }else if( d_status==5 ){
-    Node f = s->getTgFunc( d_typ, d_status_num );
-    int i = d_children.size()-1;
-    if( d_children.size()==s->d_func_args[f].size() ){
-      if( d_children.empty() ){
-        return d_id;
-      }else{
-        int cac = s->d_tg_alloc[d_children[i]].getActiveChild( s );
-        return cac==(int)d_children[i] ? d_id : cac;
-      }
-    }else if( !d_children.empty() ){
-      return s->d_tg_alloc[d_children[i]].getActiveChild( s );
-    }
-  }else{
-    Assert( false );
-  }
-  return -1;
-}
-*/
-
 void TermGenerator::debugPrint( ConjectureGenerator * s, const char * c, const char * cd ) {
   Trace(cd) << "[*" << d_id << "," << d_status << "]:";
   if( d_status==1 || d_status==2 ){
@@ -1999,11 +1943,10 @@ bool ConjectureGenerator::optFilterFalsification() { return true; }
 bool ConjectureGenerator::optFilterConfirmation() { return true; }
 bool ConjectureGenerator::optFilterConfirmationDomain() { return true; }
 bool ConjectureGenerator::optFilterConfirmationOnlyGround() { return true; }//false; }
-bool ConjectureGenerator::optWaitForFullCheck() { return true; }
+bool ConjectureGenerator::optFilterConfirmationNonCanonical() { return false; }//true; }
 unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }
 unsigned ConjectureGenerator::optFullCheckConjectures() { return 1; }
 
-
 }
 
 
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 90c76d410..afdd9e018 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file subgoal_generator.h
+/*! \file conjecture_generator.h
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: none
@@ -339,12 +339,6 @@ public:  //for property enumeration
   void addCandidateConjecture( TNode lhs, TNode rhs, unsigned depth );
   //process candidate conjecture at depth
   void processCandidateConjecture( unsigned cid, unsigned depth );
-  
-  //process candidate conjecture at depth
-  bool processCandidateConjecture2( TNode rhs, TypeNode tn, unsigned depth );
-  //process candidate conjecture 
-  bool processCandidateConjecture2( TNode lhs, TNode rhs );
-  
   //whether it should be considered
   bool considerCandidateConjecture( TNode lhs, TNode rhs );
   //notified of a substitution
@@ -381,7 +375,7 @@ public:
   /* reset at a round */
   void reset_round( Theory::Effort e );
   /* Call during quantifier engine's check */
-  void check( Theory::Effort e );
+  void check( Theory::Effort e, unsigned quant_e );
   /* Called for new quantifiers */
   void registerQuantifier( Node q );
   void assertNode( Node n );
@@ -395,7 +389,7 @@ private:
   bool optFilterConfirmation();
   bool optFilterConfirmationDomain();
   bool optFilterConfirmationOnlyGround();
-  bool optWaitForFullCheck();
+  bool optFilterConfirmationNonCanonical();   //filter if all ground confirmations are non-canonical
   unsigned optFullCheckFrequency();
   unsigned optFullCheckConjectures();
 };
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 2167c7c7d..684831773 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -31,7 +31,7 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
 
 }
 
@@ -41,18 +41,19 @@ InstantiationEngine::~InstantiationEngine() {
 }
 
 void InstantiationEngine::finishInit(){
-  //for UF terms
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
-    //if( options::cbqi() ){
-    //  addInstStrategy( new InstStrategyCheckCESolved( this, d_quantEngine ) );
-    //}
-    //these are the instantiation strategies for basic E-matching
+
+    //these are the instantiation strategies for E-matching
+    
+    //user-provided patterns
     if( options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
       d_isup = new InstStrategyUserPatterns( d_quantEngine );
       addInstStrategy( d_isup );
     }else{
       d_isup = NULL;
     }
+    
+    //auto-generated patterns
     int tstrt = Trigger::TS_ALL;
     if( options::triggerSelMode()==TRIGGER_SEL_MIN ){
       tstrt = Trigger::TS_MIN_TRIGGER;
@@ -62,26 +63,23 @@ void InstantiationEngine::finishInit(){
     d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, tstrt, 3 );
     d_i_ag->setGenerateAdditional( true );
     addInstStrategy( d_i_ag );
-    //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
+    
+    //full saturation : instantiate from relevant domain, then arbitrary terms
     if( !options::finiteModelFind() && options::fullSaturateQuant() ){
       addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) );
     }
-    //d_isup->setPriorityOver( d_i_ag );
-    //d_isup->setPriorityOver( i_agm );
-    //i_ag->setPriorityOver( i_agm );
   }
-  //for arithmetic
+  
+  //counterexample-based quantifier instantiation
   if( options::cbqi() ){
     addInstStrategy( new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ) );
-  }
-  //for datatypes
-  //if( options::cbqi() ){
   //  addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) );
-  //}
+  }
 }
 
 
 bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
+  unsigned lastWaiting = d_quantEngine->d_lemmas_waiting.size();
   //if counterexample-based quantifier instantiation is active
   if( options::cbqi() ){
     //check if any cbqi lemma has not been added yet
@@ -155,7 +153,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
       }
     }
     //do not consider another level if already added lemma at this level
-    if( d_quantEngine->hasAddedLemma() ){
+    if( d_quantEngine->d_lemmas_waiting.size()>lastWaiting ){
       d_inst_round_status = InstStrategy::STATUS_UNKNOWN;
     }
     e++;
@@ -164,14 +162,11 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   Debug("inst-engine") << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
   //Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
   if( !d_quantEngine->hasAddedLemma() ){
-    Debug("inst-engine-stuck") << "No instantiations produced at this state." << std::endl;
     Debug("inst-engine-ctrl") << "---Fail." << std::endl;
     return false;
   }else{
-    Debug("inst-engine-ctrl") << "---Done. " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
-    Trace("inst-engine") << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
-    //flush lemmas to output channel
-    d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
+    Debug("inst-engine-ctrl") << "---Done. " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting) << std::endl;
+    Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting)  << std::endl;
     return true;
   }
 }
@@ -181,17 +176,17 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){
     d_ierCounter++;
   }
   //determine if we should perform check, based on instWhenMode
-  d_performCheck = false;
+  bool performCheck = false;
   if( options::instWhenMode()==INST_WHEN_FULL ){
-    d_performCheck = ( e >= Theory::EFFORT_FULL );
+    performCheck = ( e >= Theory::EFFORT_FULL );
   }else if( options::instWhenMode()==INST_WHEN_FULL_DELAY ){
-    d_performCheck = ( e >= Theory::EFFORT_FULL ) && !d_quantEngine->getTheoryEngine()->needCheck();
+    performCheck = ( e >= Theory::EFFORT_FULL ) && !d_quantEngine->getTheoryEngine()->needCheck();
   }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){
-    d_performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+    performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
   }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){
-    d_performCheck = ( e >= Theory::EFFORT_LAST_CALL );
+    performCheck = ( e >= Theory::EFFORT_LAST_CALL );
   }else{
-    d_performCheck = true;
+    performCheck = true;
   }
   static int ierCounter2 = 0;
   if( e==Theory::EFFORT_LAST_CALL ){
@@ -199,15 +194,14 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){
     //with bounded integers, skip every other last call,
     // since matching loops may occur with infinite quantification
     if( ierCounter2%2==0 && options::fmfBoundInt() ){
-      d_performCheck = false;
+      performCheck = false;
     }
   }
-
-  return d_performCheck;
+  return performCheck;
 }
 
-void InstantiationEngine::check( Theory::Effort e ){
-  if( d_performCheck && !d_quantEngine->hasAddedLemma() ){
+void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
+  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
     Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl;
     double clSet = 0;
     if( Trace.isOn("inst-engine") ){
@@ -217,7 +211,7 @@ void InstantiationEngine::check( Theory::Effort e ){
     ++(d_statistics.d_instantiation_rounds);
     bool quantActive = false;
     Debug("quantifiers") << "quantifiers:  check:  asserted quantifiers size="
-                         << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
+                          << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
       //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 7a3528217..393f53897 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -99,7 +99,6 @@ private:
   bool d_setIncomplete;
   /** inst round counter */
   int d_ierCounter;
-  bool d_performCheck;
   /** whether each quantifier is active */
   std::map< Node, bool > d_quant_active;
   /** whether we have added cbqi lemma */
@@ -131,7 +130,7 @@ public:
   void finishInit();
 
   bool needsCheck( Theory::Effort e );
-  void check( Theory::Effort e );
+  void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node f );
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 3c2f9903e..f3d3e4bc9 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -66,8 +66,12 @@ ModelEngine::~ModelEngine() {
   delete d_builder;
 }
 
-void ModelEngine::check( Theory::Effort e ){
-  if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){
+bool ModelEngine::needsCheck( Theory::Effort e ) {
+  return e==Theory::EFFORT_LAST_CALL;
+}
+
+void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
+  if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
     int addedLemmas = 0;
     bool needsBuild = true;
     FirstOrderModel* fm = d_quantEngine->getModel();
@@ -145,7 +149,6 @@ void ModelEngine::check( Theory::Effort e ){
       }
     }else{
       //otherwise, the search will continue
-      d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
     }
   }
 }
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index caf27f691..890af1643 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -52,7 +52,8 @@ public:
   //get the builder
   QModelBuilder* getModelBuilder() { return d_builder; }
 public:
-  void check( Theory::Effort e );
+  bool needsCheck( Theory::Effort e );
+  void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node f );
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index e23e70174..71b05cec5 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -145,8 +145,8 @@ option rrOneInstPerRound --rr-one-inst-per-round bool :default false
  add one instance of rewrite rule per round
 
 option dtStcInduction --dt-stc-ind bool :default false
- apply strengthening for existential quantification over datatypes based on structural 
+ apply strengthening for existential quantification over datatypes based on structural induction
 option conjectureGen --conjecture-gen bool :default false
- generate candidate conjectures for inductive strengthening
+ generate candidate conjectures for inductive proofs
 
 endmodule
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 86d0c27e4..97eaf4aaa 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -153,7 +153,7 @@ ignore \n\
 \n\
 ";
 static const std::string triggerSelModeHelp = "\
-User pattern modes currently supported by the --trigger-sel option:\n\
+Trigger selection modes currently supported by the --trigger-sel option:\n\
 \n\
 default \n\
 + Default, consider all subterms of quantified formulas for trigger selection.\n\
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 4e4d92d28..504c3dcff 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1922,22 +1922,36 @@ void QuantConflictFind::assertDisequal( Node a, Node b ) {
 
 //-------------------------------------------------- check function
 
+bool QuantConflictFind::needsCheck( Theory::Effort level ) {
+  bool performCheck = false;
+  if( options::quantConflictFind() && !d_conflict ){
+    if( level==Theory::EFFORT_LAST_CALL ){
+      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
+    }else if( level==Theory::EFFORT_FULL ){
+      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
+    }else if( level==Theory::EFFORT_STANDARD ){
+      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
+    }
+  }
+  return performCheck;
+}
+
 void QuantConflictFind::reset_round( Theory::Effort level ) {
   d_needs_computeRelEqr = true;
 }
 
 /** check */
-void QuantConflictFind::check( Theory::Effort level ) {
-  Trace("qcf-check") << "QCF : check : " << level << std::endl;
-  if( d_conflict ){
-    Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
-    if( level>=Theory::EFFORT_FULL ){
-      Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
-      //Assert( false );
-    }
-  }else{
-    int addedLemmas = 0;
-    if( d_performCheck ){
+void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
+  if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
+    Trace("qcf-check") << "QCF : check : " << level << std::endl;
+    if( d_conflict ){
+      Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
+      if( level>=Theory::EFFORT_FULL ){
+        Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
+        //Assert( false );
+      }
+    }else{
+      int addedLemmas = 0;
       ++(d_statistics.d_inst_rounds);
       double clSet = 0;
       int prevEt = 0;
@@ -2048,7 +2062,6 @@ void QuantConflictFind::check( Theory::Effort level ) {
           }
         }
         if( addedLemmas>0 ){
-          d_quantEngine->flushLemmas();
           break;
         }
       }
@@ -2065,23 +2078,9 @@ void QuantConflictFind::check( Theory::Effort level ) {
           Trace("qcf-engine") << "  Entailment checks = " << ( currEt - prevEt ) << std::endl;
         }
       }
-    }
-    Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
-  }
-}
-
-bool QuantConflictFind::needsCheck( Theory::Effort level ) {
-  d_performCheck = false;
-  if( options::quantConflictFind() && !d_conflict ){
-    if( level==Theory::EFFORT_LAST_CALL ){
-      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
-    }else if( level==Theory::EFFORT_FULL ){
-      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
-    }else if( level==Theory::EFFORT_STANDARD ){
-      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
+      Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
     }
   }
-  return d_performCheck;
 }
 
 void QuantConflictFind::computeRelevantEqr() {
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 1f3635e78..d8f1c8e6f 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -166,7 +166,6 @@ class QuantConflictFind : public QuantifiersModule
 private:
   context::Context* d_c;
   context::CDO< bool > d_conflict;
-  bool d_performCheck;
   std::vector< Node > d_quant_order;
   std::map< Kind, Node > d_zero;
   //for storing nodes created during t-constraint solving (prevents memory leaks)
@@ -220,12 +219,12 @@ public:
   void merge( Node a, Node b );
   /** assert disequal */
   void assertDisequal( Node a, Node b );
+  /** needs check */
+  bool needsCheck( Theory::Effort level );
   /** reset round */
   void reset_round( Theory::Effort level );
   /** check */
-  void check( Theory::Effort level );
-  /** needs check */
-  bool needsCheck( Theory::Effort level );
+  void check( Theory::Effort level, unsigned quant_e );
 private:
   bool d_needs_computeRelEqr;
 public:
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 1b13d772e..7d9fa3344 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -61,8 +61,14 @@ double RewriteEngine::getPriority( Node f ) {
   //return deterministic ? 0.0 : 1.0;
 }
 
-void RewriteEngine::check( Theory::Effort e ) {
-  if( e==Theory::EFFORT_FULL ){
+bool RewriteEngine::needsCheck( Theory::Effort e ){
+  return e==Theory::EFFORT_FULL;
+  //return e>=Theory::EFFORT_LAST_CALL;
+}
+
+void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) {
+  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+  //if( e==Theory::EFFORT_FULL ){  
     Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl;
     //if( e==Theory::EFFORT_LAST_CALL ){
     //  if( !d_quantEngine->getModel()->isModelSet() ){
@@ -102,7 +108,6 @@ void RewriteEngine::check( Theory::Effort e ) {
 
     }else{
       //otherwise, the search will continue
-      d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
     }
   }
 }
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index d2108bf3e..1703a9bfc 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -54,7 +54,8 @@ private:
 public:
   RewriteEngine( context::Context* c, QuantifiersEngine* qe );
 
-  void check( Theory::Effort e );
+  bool needsCheck( Theory::Effort e );
+  void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node f );
   void assertNode( Node n );  
   /** Identify this module */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 0d5103db6..60ee5d1e9 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -144,8 +144,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
               for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
                 addedLemmas += d_op_triggers[op][i]->addTerm( n );
               }
-              //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
-              d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
             }
           }
         }
@@ -241,9 +239,9 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
         Assert( ee->hasTerm( n1 ) );
         Assert( ee->hasTerm( n2 ) );
         if( pol ){
-          return ee->areEqual( n1, n2 );
+          return n1==n2 || ee->areEqual( n1, n2 );
         }else{
-          return ee->areDisequal( n1, n2, false );
+          return n1!=n2 && ee->areDisequal( n1, n2, false );
         }
       }
     }
@@ -260,18 +258,19 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
   }else if( n.getKind()==NOT ){
     return isEntailed( n[0], subs, subsRep, !pol );
   }else if( n.getKind()==OR || n.getKind()==AND ){
+    bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( isEntailed( n[i], subs, subsRep, pol ) ){
-        if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
+        if( simPol ){
           return true;
         }
       }else{
-        if( ( !pol && n.getKind()==OR ) || ( pol && n.getKind()==AND ) ){
+        if( !simPol ){
           return false;
         }
       }
     }
-    return true;
+    return !simPol;
   }else if( n.getKind()==IFF || n.getKind()==ITE ){
     for( unsigned i=0; i<2; i++ ){
       if( isEntailed( n[0], subs, subsRep, i==0 ) ){
@@ -594,6 +593,7 @@ void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vecto
 
 Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes, std::vector< TNode >& fvs,
                                std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ) {
+  Assert( sk.empty() || sk.size()==f[0].getNumChildren() );
   //calculate the variables and substitution
   std::vector< TNode > ind_vars;
   std::vector< unsigned > ind_var_indicies;
@@ -608,19 +608,23 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes
       var_indicies.push_back( i );
     }
     Node s;
-    //make the new function symbol
-    if( argTypes.empty() ){
-      s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" );
+    //make the new function symbol or use existing
+    if( i>=sk.size() ){
+      if( argTypes.empty() ){
+        s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" );
+      }else{
+        TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() );
+        Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" );
+        //DOTHIS: set attribute on op, marking that it should not be selected as trigger
+        std::vector< Node > funcArgs;
+        funcArgs.push_back( op );
+        funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
+        s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
+      }
+      sk.push_back( s );
     }else{
-      TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() );
-      Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" );
-      //DOTHIS: set attribute on op, marking that it should not be selected as trigger
-      std::vector< Node > funcArgs;
-      funcArgs.push_back( op );
-      funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
-      s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
+      Assert( sk[i].getType()==f[0][i].getType() );
     }
-    sk.push_back( s );
   }
   Node ret;
   if( vars.empty() ){
@@ -688,9 +692,11 @@ Node TermDb::getSkolemizedBody( Node f ){
     d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars );
     //store sub quantifier information
     if( !sub.isNull() ){
-      Assert( sub[0].getNumChildren()==sub_vars.size() );
-      d_skolem_sub_quant[f] = sub;
-      d_skolem_sub_quant_vars[f].insert( d_skolem_sub_quant_vars[f].end(), sub_vars.begin(), sub_vars.end() );
+      //if we are skolemizing one at a time, we already know the skolem constants of the sub-quantified formula, store them
+      Assert( d_skolem_constants[sub].empty() );
+      for( unsigned i=0; i<sub_vars.size(); i++ ){
+        d_skolem_constants[sub].push_back( d_skolem_constants[f][sub_vars[i]] );
+      }
     }
     Assert( d_skolem_constants[f].size()==f[0].getNumChildren() );
     if( options::sortInference() ){
@@ -703,25 +709,6 @@ Node TermDb::getSkolemizedBody( Node f ){
   return d_skolem_body[ f ];
 }
 
-void TermDb::getSkolemConstants( Node f, std::vector< Node >& sk, bool expSub ) {
-  std::map< Node, std::vector< Node > >::iterator it = d_skolem_constants.find( f );
-  if( it!=d_skolem_constants.end() ){
-    sk.insert( sk.end(), it->second.begin(), it->second.end() );
-    if( expSub ){
-      std::map< Node, Node >::iterator its = d_skolem_sub_quant.find( f );
-      if( its!=d_skolem_sub_quant.end() && !its->second.isNull() ){
-        std::vector< Node > ssk;
-        getSkolemConstants( its->second, ssk, true );
-        Assert( ssk.size()==d_skolem_sub_quant_vars[f].size() );
-        for( unsigned i=0; i<d_skolem_sub_quant_vars[f].size(); i++ ){
-          sk[d_skolem_sub_quant_vars[f][i]] = ssk[i];
-        }
-      }
-    }
-    Assert( sk.size()==f[0].getNumChildren() );
-  }
-}
-
 Node TermDb::getFreeVariableForInstConstant( Node n ){
   TypeNode tn = n.getType();
   if( d_free_vars.find( tn )==d_free_vars.end() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index d63f61ca8..d6b336dfa 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -223,16 +223,11 @@ private:
 public:
   /** map from universal quantifiers to the list of skolem constants */
   std::map< Node, std::vector< Node > > d_skolem_constants;
-  /** for quantified formulas whose skolemization was strengthened by induction */
-  std::map< Node, Node > d_skolem_sub_quant;
-  std::map< Node, std::vector< unsigned > > d_skolem_sub_quant_vars;
   /** make the skolemized body f[e/x] */
   static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs,
                                 std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars );
   /** get the skolemized body */
   Node getSkolemizedBody( Node f);
-  /** get skolem constants */
-  void getSkolemConstants( Node f, std::vector< Node >& sk, bool expSub = false );
 
 //miscellaneous
 public:
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a4adf8054..f80f65723 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -167,20 +167,29 @@ void QuantifiersEngine::finishInit(){
 void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_time);
   bool needsCheck = e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
+  std::vector< QuantifiersModule* > qm;
   for( int i=0; i<(int)d_modules.size(); i++ ){
     if( d_modules[i]->needsCheck( e ) ){
+      qm.push_back( d_modules[i] );
       needsCheck = true;
     }
   }
   if( needsCheck ){
     Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
+    Trace("quant-engine-debug") << "  modules to check : ";
+    for( unsigned i=0; i<qm.size(); i++ ){
+      Trace("quant-engine-debug") << qm[i]->identify() << " ";
+    }
+    Trace("quant-engine-debug") << std::endl;
     Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
+    
     if( !getMasterEqualityEngine()->consistent() ){
       Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl;
       return;
     }
-    Trace("quant-engine-debug") << "Resetting modules..." << std::endl;
+    Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
     //reset relevant information
+    d_conflict = false;
     d_hasAddedLemma = false;
     d_term_db->reset( e );
     d_eq_query->reset();
@@ -191,12 +200,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
     for( int i=0; i<(int)d_modules.size(); i++ ){
       d_modules[i]->reset_round( e );
     }
-    Trace("quant-engine-debug") << "Done resetting modules." << std::endl;
+    Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
 
     if( e==Theory::EFFORT_LAST_CALL ){
       //if effort is last call, try to minimize model first
       if( options::finiteModelFind() ){
-        //first, check if we can minimize the model further
+        //first, check if we can minimize the model further  FIXME: remove?
         if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
           return;
         }
@@ -205,12 +214,22 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }else if( e==Theory::EFFORT_FULL ){
       ++(d_statistics.d_instantiation_rounds);
     }
-    Trace("quant-engine-debug") << "Check with modules..." << std::endl;
-    for( int i=0; i<(int)d_modules.size(); i++ ){
-      Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl;
-      d_modules[i]->check( e );
+    
+    Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
+    for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){
+      for( int i=0; i<(int)qm.size(); i++ ){
+        Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl;
+        qm[i]->check( e, quant_e );
+      }
+      //flush all current lemmas
+      flushLemmas();
+      //if we have added one, stop
+      if( d_hasAddedLemma ){
+        break;
+      }
     }
-    Trace("quant-engine-debug") << "Done check with modules." << std::endl;
+    Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
+    
     //build the model if not done so already
     //  this happens if no quantifiers are currently asserted and no model-building module is enabled
     if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
@@ -270,7 +289,7 @@ void QuantifiersEngine::registerQuantifier( Node f ){
 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
   for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
     std::set< Node > added;
-    getTermDatabase()->addTerm(*p,added);
+    getTermDatabase()->addTerm( *p, added );
   }
 }
 
@@ -323,6 +342,10 @@ Node QuantifiersEngine::getNextDecisionRequest(){
 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
   std::set< Node > added;
   getTermDatabase()->addTerm( n, added, withinQuant );
+  //maybe have triggered instantiations if we are doing eager instantiation
+  if( options::eagerInstQuant() ){
+    flushLemmas();
+  }
   //added contains also the Node that just have been asserted in this branch
   if( d_quant_rel ){
     for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
@@ -520,6 +543,10 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
   }
 }
 
+void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
+  d_phase_req_waiting[lit] = req;
+}
+
 bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){
   std::vector< Node > terms;
   //make sure there are values for each variable we are instantiating
@@ -568,7 +595,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
     }
     if( d_term_db->isEntailed( f[1], subs, false, true ) ){
       Trace("inst-add-debug") << " -> Currently entailed." << std::endl;
-      Trace("inst-add-entail") << " -> instantiation for " << f[1] << " currently entailed." << std::endl;
       return false;
     }
   }
@@ -628,18 +654,21 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool
   return addSplit( fm );
 }
 
-void QuantifiersEngine::flushLemmas( OutputChannel* out ){
+void QuantifiersEngine::flushLemmas(){
   if( !d_lemmas_waiting.empty() ){
-    if( !out ){
-      out = &getOutputChannel();
-    }
     //take default output channel if none is provided
     d_hasAddedLemma = true;
     for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){
-      out->lemma( d_lemmas_waiting[i], false, true );
+      getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
     }
     d_lemmas_waiting.clear();
   }
+  if( !d_phase_req_waiting.empty() ){
+    for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
+      getOutputChannel().requirePhase( it->first, it->second );
+    }
+    d_phase_req_waiting.clear();
+  }
 }
 
 void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 220fa0b1f..f74c478ae 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -52,7 +52,7 @@ public:
   /* reset at a round */
   virtual void reset_round( Theory::Effort e ){}
   /* Call during quantifier engine's check */
-  virtual void check( Theory::Effort e ) = 0;
+  virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
   /* Called for new quantifiers */
   virtual void registerQuantifier( Node q ) = 0;
   virtual void assertNode( Node n ) = 0;
@@ -115,6 +115,12 @@ private:
   quantifiers::RewriteEngine * d_rr_engine;
   /** subgoal generator */
   quantifiers::ConjectureGenerator * d_sg_gen;
+public: //effort levels
+  enum {
+    QEFFORT_CONFLICT,
+    QEFFORT_STANDARD,
+    QEFFORT_MODEL,
+  };
 private:
   /** list of all quantifiers seen */
   std::vector< Node > d_quants;
@@ -123,8 +129,12 @@ private:
   BoolMap d_lemmas_produced_c;
   /** lemmas waiting */
   std::vector< Node > d_lemmas_waiting;
+  /** phase requirements waiting */
+  std::map< Node, bool > d_phase_req_waiting;
   /** has added lemma this round */
   bool d_hasAddedLemma;
+  /** has a conflict been found */
+  bool d_conflict;
   /** list of all instantiations produced for each quantifier */
   std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
   std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
@@ -196,6 +206,8 @@ private:
   bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
   /** set instantiation level attr */
   void setInstantiationLevelAttr( Node n, Node qn, uint64_t level, std::vector< Node >& inst_terms );
+  /** flush lemmas */
+  void flushLemmas();
 public:
   /** get instantiation */
   Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
@@ -209,6 +221,8 @@ public:
   bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
   /** add lemma lem */
   bool addLemma( Node lem, bool doCache = true );
+  /** add require phase */
+  void addRequirePhase( Node lit, bool req );
   /** do instantiation specified by m */
   bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false );
   /** add instantiation */
@@ -219,8 +233,6 @@ public:
   bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
   /** has added lemma */
   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
-  /** flush lemmas */
-  void flushLemmas( OutputChannel* out = NULL );
   /** get number of waiting lemmas */
   int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
 public:
-- 
cgit v1.2.3