Synchronize conjecture generation with E-matching. Minor fix to --full-saturate-quant.

6 files changed, 49 insertions, 37 deletions

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 06552196d..2f8822b53 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -352,7 +352,8 @@ bool ConjectureGenerator::isGroundTerm( TNode n ) {
 }

 

 bool ConjectureGenerator::needsCheck( Theory::Effort e ) {

-  return e==Theory::EFFORT_FULL;

+  // synchonized with instantiation engine

+  return d_quantEngine->getInstWhenNeedsCheck( e );

 }

 

 bool ConjectureGenerator::hasEnumeratedUf( Node n ) {

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 8918a6dac..b9e8aef09 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -530,12 +530,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
                   //skip inst constant nodes
                   while( nv<maxs[index] && nv<=max_i &&
                          r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
-                    childIndex[index]++;
-                    nv = childIndex[index]+1;
+                    nv++;
                   }
                 }
                 if( nv<maxs[index] && nv<=max_i ){
-                  childIndex[index]++;
+                  childIndex[index] = nv;
                   index++;
                 }else{
                   childIndex.pop_back();
@@ -545,8 +544,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
             }
             success = index>=0;
             if( success ){
-              Trace("inst-alg-rd") << "Try instantiation..." << std::endl;
-              index--;
+              Trace("inst-alg-rd") << "Try instantiation { ";
+              for( unsigned j=0; j<childIndex.size(); j++ ){
+                Trace("inst-alg-rd") << childIndex[j] << " ";
+              }
+              Trace("inst-alg-rd") << "}" << std::endl;
               //try instantiation
               std::vector< Node > terms;
               for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
@@ -560,6 +562,8 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
                 Trace("inst-alg-rd") << "Success!" << std::endl;
                 ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
                 return STATUS_UNKNOWN;
+              }else{
+                index--;
               }
             }
           }while( success );
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index ade6d4313..b53919aaf 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_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ){
 
 }
 
@@ -178,37 +178,11 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
 }
 
 bool InstantiationEngine::needsCheck( Theory::Effort e ){
-  if( e==Theory::EFFORT_FULL ){
-    d_ierCounter++;
-  }
-  //determine if we should perform check, based on instWhenMode
-  bool performCheck = false;
-  if( options::instWhenMode()==INST_WHEN_FULL ){
-    performCheck = ( e >= Theory::EFFORT_FULL );
-  }else if( options::instWhenMode()==INST_WHEN_FULL_DELAY ){
-    performCheck = ( e >= Theory::EFFORT_FULL ) && !d_quantEngine->getTheoryEngine()->needCheck();
-  }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){
-    performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
-  }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){
-    performCheck = ( e >= Theory::EFFORT_LAST_CALL );
-  }else{
-    performCheck = true;
-  }
-  static int ierCounter2 = 0;
-  if( e==Theory::EFFORT_LAST_CALL ){
-    ierCounter2++;
-    //with bounded integers, skip every other last call,
-    // since matching loops may occur with infinite quantification
-    if( ierCounter2%2==0 && options::fmfBoundInt() ){
-      performCheck = false;
-    }
-  }
-  return performCheck;
+  return d_quantEngine->getInstWhenNeedsCheck( e );
 }
 
 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") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 2fa37ac35..2d427ae0a 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -84,8 +84,6 @@ private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   /** whether the instantiation engine should set incomplete if it cannot answer SAT */
   bool d_setIncomplete;
-  /** inst round counter */
-  int d_ierCounter;
   /** whether each quantifier is active */
   std::map< Node, bool > d_quant_active;
   /** whether we have added cbqi lemma */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4dc8df09d..d6c6f4667 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -171,8 +171,9 @@ d_lemmas_produced_c(u){
     d_builder = NULL;
   }
 
-  //options
   d_total_inst_count_debug = 0;
+  d_ierCounter = 0;
+  d_ierCounter_lc = 0;
 }
 
 QuantifiersEngine::~QuantifiersEngine(){
@@ -251,6 +252,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
     return;
   }
+  if( e==Theory::EFFORT_FULL ){
+    d_ierCounter++;
+  }else if( e==Theory::EFFORT_LAST_CALL ){
+    d_ierCounter_lc++;
+  }
   bool needsCheck = false;
   bool needsModel = false;
   bool needsFullModel = false;
@@ -825,6 +831,30 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool
   return addSplit( fm );
 }
 
+bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
+  //determine if we should perform check, based on instWhenMode
+  bool performCheck = false;
+  if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){
+    performCheck = ( e >= Theory::EFFORT_FULL );
+  }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
+    performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
+  }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
+    performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+  }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
+    performCheck = ( e >= Theory::EFFORT_LAST_CALL );
+  }else{
+    performCheck = true;
+  }
+  if( e==Theory::EFFORT_LAST_CALL ){
+    //with bounded integers, skip every other last call,
+    // since matching loops may occur with infinite quantification
+    if( d_ierCounter_lc%2==0 && options::fmfBoundInt() ){
+      performCheck = false;
+    }
+  }
+  return performCheck;
+}
+
 void QuantifiersEngine::flushLemmas(){
   if( !d_lemmas_waiting.empty() ){
     //take default output channel if none is provided
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 2b466b96b..ac782a536 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -169,6 +169,9 @@ private:
   std::map< Node, int > d_total_inst_debug;
   std::map< Node, int > d_temp_inst_debug;
   int d_total_inst_count_debug;
+  /** inst round counters */
+  int d_ierCounter;
+  int d_ierCounter_lc;
 private:
   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
 public:
@@ -273,6 +276,8 @@ public:
   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
   /** get number of waiting lemmas */
   int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
+  /** get needs check */
+  bool getInstWhenNeedsCheck( Theory::Effort e );
   /** set instantiation level attr */
   static void setInstantiationLevelAttr( Node n, uint64_t level );
   /** is term eligble for instantiation? */