Add options --full-saturate-quant and --mbqi=trust. Other minor changes.

7 files changed, 30 insertions, 15 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 199d3233c..9a3c07c5e 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -52,7 +52,7 @@ void InstantiationEngine::finishInit(){
     i_ag->setGenerateAdditional( true );
     addInstStrategy( i_ag );
     //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
-    if( !options::finiteModelFind() ){
+    if( !options::finiteModelFind() && options::fullSaturateQuant() ){
       addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) );
     }
     //d_isup->setPriorityOver( i_ag );
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 9fe0407e5..738cfed60 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -37,7 +37,8 @@ ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
 QuantifiersModule( qe ){
 
   Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
-  if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){
+  if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
+      options::mbqiMode()==MBQI_TRUST || options::fmfBoundInt() ){
     Trace("model-engine-debug") << "...make fmc builder." << std::endl;
     d_builder = new fmcheck::FullModelChecker( c, qe );
   }else if( options::mbqiMode()==MBQI_INTERVAL ){
@@ -204,7 +205,7 @@ int ModelEngine::checkModel(){
   }
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
-  int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : 1;
+  int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
   for( int e=0; e<e_max; e++) {
     if (d_addedLemmas==0) {
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index b37e48ec3..89e10b175 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -70,6 +70,8 @@ typedef enum {
   MBQI_FMC_INTERVAL,
   /** mbqi with interval abstraction of uninterpreted sorts */
   MBQI_INTERVAL,
+  /** mbqi trust (produce no instantiations) */
+  MBQI_TRUST,
 } MbqiMode;
 
 typedef enum {
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 2041a91b8..f9cabe62b 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -72,6 +72,9 @@ option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :de
  
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
+ 
+option fullSaturateQuant --full-saturate-quant bool :default true
+ when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
 
 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/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 06f5d7600..492155e02 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -226,6 +226,8 @@ inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngi
     return MBQI_FMC_INTERVAL;
   } else if(optarg ==  "interval") {
     return MBQI_INTERVAL;
+  } else if(optarg ==  "trust") {
+    return MBQI_TRUST;
   } else if(optarg ==  "help") {
     puts(mbqiModeHelp.c_str());
     exit(1);
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a454d8334..36410bd50 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -54,7 +54,8 @@ d_lemmas_produced_c(u){
 
   //the model object
   if( options::mbqiMode()==quantifiers::MBQI_FMC ||
-      options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){
+      options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ||
+      options::mbqiMode()==quantifiers::MBQI_TRUST ){
     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
   }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
     d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" );
@@ -452,18 +453,23 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
   return false;
 }
 
-bool QuantifiersEngine::addLemma( Node lem ){
-  Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
-  lem = Rewriter::rewrite(lem);
-  if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
-    //d_curr_out->lemma( lem );
-    d_lemmas_produced_c[ lem ] = true;
+bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
+  if( doCache ){
+    Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
+    lem = Rewriter::rewrite(lem);
+    if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
+      //d_curr_out->lemma( lem );
+      d_lemmas_produced_c[ lem ] = true;
+      d_lemmas_waiting.push_back( lem );
+      Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
+      return true;
+    }else{
+      Debug("inst-engine-debug") << "Duplicate." << std::endl;
+      return false;
+    }
+  }else{
     d_lemmas_waiting.push_back( lem );
-    Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
     return true;
-  }else{
-    Debug("inst-engine-debug") << "Duplicate." << std::endl;
-    return false;
   }
 }
 
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index fd51e4fb1..fbc501aec 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -86,6 +86,7 @@ class QuantifiersEngine {
   friend class quantifiers::InstantiationEngine;
   friend class quantifiers::ModelEngine;
   friend class quantifiers::RewriteEngine;
+  friend class quantifiers::QuantConflictFind;
   friend class inst::InstMatch;
 private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
@@ -210,7 +211,7 @@ public:
   /** exist instantiation ? */
   bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
   /** add lemma lem */
-  bool addLemma( Node lem );
+  bool addLemma( Node lem, bool doCache = true );
   /** do instantiation specified by m */
   bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false );
   /** add instantiation */