Add option to interleave enumerative instantiation with other strategies.

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index a55dfda84a64ad4719a84b227d40ad2c0c912155..eb1ce56eff41574a253ec5bdcf9921dfb1f076da 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -460,12 +460,34 @@ FullSaturation::FullSaturation( QuantifiersEngine* qe ) : QuantifiersModule( qe
 
 }
 
+bool FullSaturation::needsCheck( Theory::Effort e ){
+  if( options::fullSaturateInst() ){
+    if( d_quantEngine->getInstWhenNeedsCheck( e ) ){
+      return true;
+    }
+  }
+  if( options::fullSaturateQuant() ){
+    if( e>=Theory::EFFORT_LAST_CALL ){
+      return true;
+    }
+  }
+  return false;
+}
+
 void FullSaturation::reset_round( Theory::Effort e ) {
 
 }
 
 void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
-  if( quant_e==QuantifiersEngine::QEFFORT_LAST_CALL ){
+  bool doCheck = false;
+  if( options::fullSaturateInst() ){
+    //we only add when interleaved with other strategies
+    doCheck = quant_e==QuantifiersEngine::QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
+  }
+  if( options::fullSaturateQuant() && !doCheck ){
+    doCheck = quant_e==QuantifiersEngine::QEFFORT_LAST_CALL;
+  }
+  if( doCheck ){
     double clSet = 0;
     if( Trace.isOn("fs-engine") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 5163653cfbc282a50723e0f2e1ced923b55bb51a..c6a0be03b8aebaffff707a7dd036585b68e44691 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -114,6 +114,7 @@ private:
 public:
   FullSaturation( QuantifiersEngine* qe );
   ~FullSaturation(){}
+  bool needsCheck( Theory::Effort e );
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node q );

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index cd5f90a37938874935fbb985608007a74cd781af..9e8d02d30041b8f83e07d12e5f5eb859c7063826 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -102,10 +102,12 @@ option internalReps --quant-internal-reps bool :default true
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
 
-option fullSaturateQuant --full-saturate-quant bool :default false
+option fullSaturateQuant --full-saturate-quant bool :default false :read-write
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
 option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
  whether to use relevant domain first for full saturation instantiation strategy
+option fullSaturateInst --fs-inst bool :default false
+ interleave full saturate instantiation with other techniques
 
 option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose literal matching mode

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2c2e4ea5b50e2bb3c62edb634bb0e29d393121e4..622ef5a52a916f562890d510eb0c6f9ecc4dab6e 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -94,6 +94,7 @@ d_presolve_cache_wic(u){
   d_hasAddedLemma = false;
 
   bool needsBuilder = false;
+  bool needsRelDom = false;
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
@@ -107,11 +108,6 @@ d_presolve_cache_wic(u){
   }else{
     d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
   }
-  if( options::fullSaturateQuant() ){
-    d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
-  }else{
-    d_rel_dom = NULL;
-  }
   if( options::relevantTriggers() ){
     d_quant_rel = new QuantRelevance( false );
   }else{
@@ -191,15 +187,21 @@ d_presolve_cache_wic(u){
   }else{
     d_uee = NULL;
   }
-  
   //full saturation : instantiate from relevant domain, then arbitrary terms
-  if( options::fullSaturateQuant() ){
+  if( options::fullSaturateQuant() || options::fullSaturateInst() ){
     d_fs = new quantifiers::FullSaturation( this );
     d_modules.push_back( d_fs );
+    needsRelDom = true;
   }else{
     d_fs = NULL;
   }
 
+  if( needsRelDom ){
+    d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
+  }else{
+    d_rel_dom = NULL;
+  }
+  
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
     if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||