Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI.

7 files changed, 47 insertions, 48 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index c94775aec..797ca8f70 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -169,7 +169,7 @@ void FirstOrderModelIG::resetEvaluate(){
 //   each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
 int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
   ++d_eval_formulas;
-  //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
+  Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl;
   //Notice() << "Eval " << n << std::endl;
   if( n.getKind()==NOT ){
     int val = evaluate( n[0], depIndex, ri );
@@ -447,7 +447,7 @@ void FirstOrderModelIG::makeEvalUfModel( Node n ){
       d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] );
       d_uf_model_gen[op].makeModel( this, d_eval_uf_model[n] );
       //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;
-      //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );
+      //d_eval_uf_model[n].debugPrint( std::cout, d_qe->getModel(), 2 );
     }
   }
 }
@@ -578,7 +578,7 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a
 
 void FirstOrderModelFmc::processInitialize( bool ispre ) {
   if( ispre ){
-    if( options::fmfFmcInterval() && intervalOp.isNull() ){
+    if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && intervalOp.isNull() ){
       std::vector< TypeNode > types;
       for(unsigned i=0; i<2; i++){
         types.push_back(NodeManager::currentNM()->integerType());
@@ -616,7 +616,7 @@ Node FirstOrderModelFmc::getStar(TypeNode tn) {
 
 Node FirstOrderModelFmc::getStarElement(TypeNode tn) {
   Node st = getStar(tn);
-  if( options::fmfFmcInterval() && tn.isInteger() ){
+  if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && tn.isInteger() ){
     st = getInterval( st, st );
   }
   return st;
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 174e26a5a..c7d7b7415 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -60,9 +60,9 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
         return true;
       }
     }
-    if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){
+    if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){
       //for star: check if all children are defined and have generalizations
-      if( options::fmfFmcCoverSimplify() && c[index]==st ){
+      if( c[index]==st ){     ///options::fmfFmcCoverSimplify()
         //check if all children exist and are complete
         int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);
         if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){
@@ -92,7 +92,7 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>
     return d_data;
   }else{
     int minIndex = -1;
-    if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){
+    if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && inst[index].getType().isInteger() ){
       for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
         //if( !m->isInterval( it->first ) ){
         //  std::cout << "Not an interval during getGenIndex " << it->first << std::endl;
@@ -327,7 +327,7 @@ QModelBuilder( c, qe ){
 bool FullModelChecker::optBuildAtFullModel() {
   //need to build after full model has taken effect if we are constructing interval models
   //  this is because we need to have a constant in all integer equivalence classes
-  return options::fmfFmcInterval();
+  return options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL;
 }
 
 void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
@@ -443,7 +443,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
             Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl;
           }
           children.push_back(ri);
-          if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){
+          if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
             if (fm->isModelBasisTerm(ri) ) {
               ri = fm->getStar( ri.getType() );
             }else{
@@ -485,7 +485,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       }
 
 
-      if( options::fmfFmcInterval() ){
+      if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){
         convertIntervalModel( fm, op );
       }
 
@@ -1103,7 +1103,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
       }
     }else{
       if( !v.isNull() ){
-        if( options::fmfFmcInterval() && v.getType().isInteger() ){
+        if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && v.getType().isInteger() ){
           for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
             if( fm->isInRange( v, it->first ) ){
               doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
@@ -1165,7 +1165,7 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c
   Trace("fmc-debug3") << "isCompat " << c << std::endl;
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
-    if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+    if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){
       Node iv = doIntervalMeet( fm, cond[i], c[i-1], false );
       if( iv.isNull() ){
         return 0;
@@ -1184,7 +1184,7 @@ bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & co
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
     if( cond[i]!=c[i-1] ) {
-      if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+      if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){
         Node iv = doIntervalMeet( fm, cond[i], c[i-1] );
         if( !iv.isNull() ){
           cond[i] = iv;
@@ -1254,7 +1254,7 @@ Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {
 }
 
 void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {
-  Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl;
+  Trace("fmc-debug") << "Make default vec, intervals = " << (options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL) << std::endl;
   //get function symbol for f
   cond.push_back(d_quant_cond[f]);
   for (unsigned i=0; i<f[0].getNumChildren(); i++) {
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 468c78978..cb63ccd45 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -273,17 +273,15 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
       ++(d_statistics.d_num_quants_init);
     }
     //try to add it
-    if( optInstGen() ){
-      Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
-      //add model basis instantiation
-      if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){
-        d_quant_basis_match_added[f] = true;
-        return 1;
-      }else{
-        //shouldn't happen usually, but will occur if x != y is a required literal for f.
-        //Notice() << "No model basis for " << f << std::endl;
-        d_quant_basis_match_added[f] = false;
-      }
+    Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
+    //add model basis instantiation
+    if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){
+      d_quant_basis_match_added[f] = true;
+      return 1;
+    }else{
+      //shouldn't happen usually, but will occur if x != y is a required literal for f.
+      //Notice() << "No model basis for " << f << std::endl;
+      d_quant_basis_match_added[f] = false;
     }
   }
   return 0;
@@ -418,6 +416,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
         //if evaluate(...)==1, then the instantiation is already true in the model
         //  depIndex is the index of the least significant variable that this evaluation relies upon
         depIndex = riter.getNumTerms()-1;
+        Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermDatabase()->getInstConstantBody( f ) << std::endl;
         eval = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
         if( eval==1 ){
           Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 5006a8a61..f314584cd 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -37,7 +37,7 @@ 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::fmfBoundInt() ){
+  if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){
     Trace("model-engine-debug") << "...make fmc builder." << std::endl;
     d_builder = new fmcheck::FullModelChecker( c, qe );
   }else if( options::mbqiMode()==MBQI_INTERVAL ){
@@ -212,7 +212,7 @@ int ModelEngine::checkModel(){
   }
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
-  int e_max = options::mbqiMode()==MBQI_FMC ? 2 : 1;
+  int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : 1;
   for( int e=0; e<e_max; e++) {
     if (d_addedLemmas==0) {
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
@@ -230,6 +230,8 @@ int ModelEngine::checkModel(){
           if( optOneQuantPerRound() && d_addedLemmas>0 ){
             break;
           }
+        }else{
+          Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl;
         }
       }
     }
@@ -248,11 +250,12 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   d_builder->d_addedLemmas = 0;
   d_builder->d_incomplete_check = false;
   if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
+    Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl;
     d_triedLemmas += d_builder->d_triedLemmas;
     d_addedLemmas += d_builder->d_addedLemmas;
     d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check;
   }else{
-    Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
+    Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
     Debug("inst-fmf-ei") << "   Instantiation Constants: ";
     for( size_t i=0; i<f[0].getNumChildren(); i++ ){
       Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 7c4cb3651..d5c755ad2 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -65,7 +65,7 @@ typedef enum {
   /** mbqi from Section 5.4.2 of AJR thesis */
   MBQI_FMC,
   /** mbqi with integer intervals */
-  //MBQI_FMC_INTERVAL,
+  MBQI_FMC_INTERVAL,
   /** mbqi with interval abstraction of uninterpreted sorts */
   MBQI_INTERVAL,
 } MbqiMode;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index f485b981c..190c7ddc9 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -76,9 +76,8 @@ option eagerInstQuant --eager-inst-quant bool :default false
 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
 
-option cbqi --enable-cbqi/--disable-cbqi bool :default false
- turns on counterexample-based quantifier instantiation [off by default]
-/turns off counterexample-based quantifier instantiation
+option cbqi --enable-cbqi bool :default false
+ turns on counterexample-based quantifier instantiation
 
 option recurseCbqi --cbqi-recurse bool :default false
  turns on recursive counterexample-based quantifier instantiation
@@ -97,30 +96,23 @@ option finiteModelFind --finite-model-find bool :default false
 
 option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose mode for model-based quantifier instantiation
+option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
+ only add one instantiation per quantifier per round for mbqi
+option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
+ only add instantiations for one quantifier per round for mbqi 
 
-option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
- disable simple models in full model check for finite model finding
-option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true
- disable covering simplification of fmc models
-option fmfFmcInterval --fmf-fmc-interval bool :default false
- construct interval models for fmc models
-
-option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
- only add one instantiation per quantifier per round for fmf
-option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false
- only add instantiations for one quantifier per round for fmf 
 option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
 option fmfRelevantDomain --fmf-relevant-domain bool :default false
  use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
-option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true
- enable Inst-Gen instantiation techniques for finite model finding (default)
-/disable Inst-Gen instantiation techniques for finite model finding
+option fmfInstGen /--disable-fmf-inst-gen bool :default true
+ disable Inst-Gen instantiation techniques for finite model finding
 option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
  only perform Inst-Gen instantiation techniques on one quantifier per round
 option fmfFreshDistConst --fmf-fresh-dc bool :default false
  use fresh distinguished representative when applying Inst-Gen techniques
-
+option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
+ disable simple models in full model check for finite model finding
 option fmfBoundInt --fmf-bound-int bool :default false
  finite model finding on bounded integer quantification
 
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index a119bcaf6..4929fa60b 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -87,9 +87,12 @@ instgen \n\
 + Use instantiation algorithm that mimics Inst-Gen calculus. \n\
 \n\
 fmc \n\
-+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability. \n\
++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
   Modulo Theories.\n\
 \n\
+fmc-interval \n\
++ Same as fmc, but with intervals for models of integer functions.\n\
+\n\
 interval \n\
 + Use algorithm that abstracts domain elements as intervals. \n\
 \n\
@@ -166,6 +169,8 @@ inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngi
     return MBQI_INST_GEN;
   } else if(optarg ==  "fmc") {
     return MBQI_FMC;
+  } else if(optarg ==  "fmc-interval") {
+    return MBQI_FMC_INTERVAL;
   } else if(optarg ==  "interval") {
     return MBQI_INTERVAL;
   } else if(optarg ==  "help") {