Make --var-elim-quant true by default. Add rewrite engine to quantifiers module.

1 files changed, 1 insertions, 8 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 32deb9e47..0f756dcc0 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -168,14 +168,6 @@ int ModelEngine::checkModel(){
       }
     }
   }
-  //full model checking: construct models for all functions
-  /*
-  if( d_fmc.isActive() ){
-    for (std::map< Node, uf::UfModelTreeGenerator >::iterator it = fm->d_uf_model_gen.begin(); it != fm->d_uf_model_gen.end(); ++it) {
-      d_fmc.getModel(fm, it->first);
-    }
-  }
-  */
   //compute the relevant domain if necessary
   //if( optUseRelevantDomain() ){
   //}
@@ -227,6 +219,7 @@ int ModelEngine::checkModel(){
 
 int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   int addedLemmas = 0;
+  //first check if the builder can do the exhaustive instantiation
   if( !d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort, addedLemmas ) ){
     Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
     Debug("inst-fmf-ei") << "   Instantiation Constants: ";