Refactoring of model engine to separate individual implementations of model builder. Begin work on interval models for integers. Other minor cleanup.

1 files changed, 50 insertions, 137 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 0f756dcc0..c0fe23b94 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -22,8 +22,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 
-#define EVAL_FAIL_SKIP_MULTIPLE
-
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -67,6 +65,7 @@ void ModelEngine::check( Theory::Effort e ){
         //initialize the model
         Trace("model-engine-debug") << "Build model..." << std::endl;
         d_builder->d_considerAxioms = effort>=1;
+        d_builder->d_addedLemmas = 0;
         d_builder->buildModel( fm, false );
         addedLemmas += (int)d_builder->d_addedLemmas;
         //if builder has lemmas, add and return
@@ -127,28 +126,12 @@ void ModelEngine::assertNode( Node f ){
 
 }
 
-bool ModelEngine::optOneInstPerQuantRound(){
-  return options::fmfOneInstPerRound();
-}
-
-bool ModelEngine::optUseRelevantDomain(){
-  return options::fmfRelevantDomain();
-}
-
 bool ModelEngine::optOneQuantPerRound(){
   return options::fmfOneQuantPerRound();
 }
 
-bool ModelEngine::optExhInstEvalSkipMultiple(){
-#ifdef EVAL_FAIL_SKIP_MULTIPLE
-  return true;
-#else
-  return false;
-#endif
-}
 
 int ModelEngine::checkModel(){
-  int addedLemmas = 0;
   FirstOrderModel* fm = d_quantEngine->getModel();
   //for debugging
   if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
@@ -168,39 +151,41 @@ int ModelEngine::checkModel(){
       }
     }
   }
-  //compute the relevant domain if necessary
-  //if( optUseRelevantDomain() ){
-  //}
+  //relevant domain?
+
   d_triedLemmas = 0;
-  d_testLemmas = 0;
-  d_relevantLemmas = 0;
+  d_addedLemmas = 0;
   d_totalLemmas = 0;
+  //for statistics
+  for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+    Node f = fm->getAssertedQuantifier( i );
+    int totalInst = 1;
+    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+      TypeNode tn = f[0][i].getType();
+      if( fm->d_rep_set.hasType( tn ) ){
+        totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+      }
+    }
+    d_totalLemmas += totalInst;
+  }
+
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
   int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1;
   for( int e=0; e<e_max; e++) {
-    if (addedLemmas==0) {
+    if (d_addedLemmas==0) {
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node f = fm->getAssertedQuantifier( i );
-        //keep track of total instantiations for statistics
-        int totalInst = 1;
-        for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-          TypeNode tn = f[0][i].getType();
-          if( fm->d_rep_set.hasType( tn ) ){
-            totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
-          }
-        }
-        d_totalLemmas += totalInst;
         //determine if we should check this quantifier
         if( d_builder->isQuantifierActive( f ) ){
-          addedLemmas += exhaustiveInstantiate( f, e );
+          exhaustiveInstantiate( f, e );
           if( Trace.isOn("model-engine-warn") ){
-            if( addedLemmas>10000 ){
+            if( d_addedLemmas>10000 ){
               Debug("fmf-exit") << std::endl;
               debugPrint("fmf-exit");
               exit( 0 );
             }
           }
-          if( optOneQuantPerRound() && addedLemmas>0 ){
+          if( optOneQuantPerRound() && d_addedLemmas>0 ){
             break;
           }
         }
@@ -210,17 +195,23 @@ int ModelEngine::checkModel(){
   //print debug information
   if( Trace.isOn("model-engine") ){
     Trace("model-engine") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
-    Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
-    Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+    Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
+    Trace("model-engine") << d_totalLemmas << std::endl;
   }
-  d_statistics.d_exh_inst_lemmas += addedLemmas;
-  return addedLemmas;
+  d_statistics.d_exh_inst_lemmas += d_addedLemmas;
+  return d_addedLemmas;
 }
 
-int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
-  int addedLemmas = 0;
+void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   //first check if the builder can do the exhaustive instantiation
-  if( !d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort, addedLemmas ) ){
+  d_builder->d_triedLemmas = 0;
+  d_builder->d_addedLemmas = 0;
+  d_builder->d_incomplete_check = false;
+  if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
+    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;
     Debug("inst-fmf-ei") << "   Instantiation Constants: ";
     for( size_t i=0; i<f[0].getNumChildren(); i++ ){
@@ -230,97 +221,31 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
-      FirstOrderModelIG * fmig = NULL;
-      if( !options::fmfFullModelCheck() ){
-        fmig = (FirstOrderModelIG*)d_quantEngine->getModel();
-        Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
-        fmig->resetEvaluate();
-      }
       Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
-      int tests = 0;
       int triedLemmas = 0;
-      while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
-        for( int i=0; i<(int)riter.d_index.size(); i++ ){
-          Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl;
-        }
-        d_testLemmas++;
-        int eval = 0;
-        int depIndex;
-        if( d_builder->optUseModel() && fmig ){
-          //see if instantiation is already true in current model
-          Debug("fmf-model-eval") << "Evaluating ";
-          riter.debugPrintSmall("fmf-model-eval");
-          Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
-          tests++;
-          //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;
-          eval = fmig->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
-          if( eval==1 ){
-            Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
-          }else{
-            Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
-          }
+      int addedLemmas = 0;
+      while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+        //instantiation was not shown to be true, construct the match
+        InstMatch m;
+        for( int i=0; i<riter.getNumTerms(); i++ ){
+          m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
         }
-        if( eval==1 ){
-          //instantiation is already true -> skip
-          riter.increment2( depIndex );
+        Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+        triedLemmas++;
+        //add as instantiation
+        if( d_quantEngine->addInstantiation( f, m ) ){
+          addedLemmas++;
         }else{
-          //instantiation was not shown to be true, construct the match
-          InstMatch m;
-          for( int i=0; i<riter.getNumTerms(); i++ ){
-            m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
-          }
-          Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
-          triedLemmas++;
-          d_triedLemmas++;
-          //add as instantiation
-          if( d_quantEngine->addInstantiation( f, m ) ){
-            addedLemmas++;
-            //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
-            if( eval==-1 && optExhInstEvalSkipMultiple() ){
-              riter.increment2( depIndex );
-            }else{
-              riter.increment();
-            }
-          }else{
-            Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
-            riter.increment();
-          }
+          Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
         }
+        riter.increment();
       }
-      //print debugging information
-      if( fmig ){
-        d_statistics.d_eval_formulas += fmig->d_eval_formulas;
-        d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
-        d_statistics.d_eval_lits += fmig->d_eval_lits;
-        d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
-      }
-      int relevantInst = 1;
-      for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-        relevantInst = relevantInst * (int)riter.d_domain[i].size();
-      }
-      d_relevantLemmas += relevantInst;
-      Trace("inst-fmf-ei") << "Finished: " << std::endl;
-      //Debug("inst-fmf-ei") << "   Inst Total: " << totalInst << std::endl;
-      Trace("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
-      Trace("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
-      Trace("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
-      Trace("inst-fmf-ei") << "   # Tests: " << tests << std::endl;
-      if( addedLemmas>1000 ){
-        Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
-        //Trace("model-engine-warn") << "   Inst Total: " << totalInst << std::endl;
-        Trace("model-engine-warn") << "   Inst Relevant: " << relevantInst << std::endl;
-        Trace("model-engine-warn") << "   Inst Tried: " << triedLemmas << std::endl;
-        Trace("model-engine-warn") << "   Inst Added: " << addedLemmas << std::endl;
-        Trace("model-engine-warn") << "   # Tests: " << tests << std::endl;
-        Trace("model-engine-warn") << std::endl;
-      }
+      d_addedLemmas += addedLemmas;
+      d_triedLemmas += triedLemmas;
     }
-     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+    //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
     d_incomplete_check = d_incomplete_check || riter.d_incomplete;
   }
-  return addedLemmas;
 }
 
 void ModelEngine::debugPrint( const char* c ){
@@ -340,26 +265,14 @@ void ModelEngine::debugPrint( const char* c ){
 
 ModelEngine::Statistics::Statistics():
   d_inst_rounds("ModelEngine::Inst_Rounds", 0),
-  d_eval_formulas("ModelEngine::Eval_Formulas", 0 ),
-  d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ),
-  d_eval_lits("ModelEngine::Eval_Lits", 0 ),
-  d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ),
   d_exh_inst_lemmas("ModelEngine::Exhaustive_Instantiation_Lemmas", 0 )
 {
   StatisticsRegistry::registerStat(&d_inst_rounds);
-  StatisticsRegistry::registerStat(&d_eval_formulas);
-  StatisticsRegistry::registerStat(&d_eval_uf_terms);
-  StatisticsRegistry::registerStat(&d_eval_lits);
-  StatisticsRegistry::registerStat(&d_eval_lits_unknown);
   StatisticsRegistry::registerStat(&d_exh_inst_lemmas);
 }
 
 ModelEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_inst_rounds);
-  StatisticsRegistry::unregisterStat(&d_eval_formulas);
-  StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
-  StatisticsRegistry::unregisterStat(&d_eval_lits);
-  StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
   StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas);
 }