Model building into quantifiers engine. Simplify axiom-inst mode.

11 files changed, 110 insertions, 109 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index d6dac6f14..353b6d1c4 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -740,7 +740,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
     //debug the model
     debugModel( fm );
   }else{
-    fm->initialize( d_considerAxioms );
+    fm->initialize();
     //process representatives
     fm->d_rep_id.clear();
     fm->d_domain.clear();
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 0a0d4eba8..07fea3cca 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -74,7 +74,7 @@ Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
   }
 }
 
-void FirstOrderModel::initialize( bool considerAxioms ) {
+void FirstOrderModel::initialize() {
   processInitialize( true );
   //this is called after representatives have been chosen and the equality engine has been built
   //for each quantifier, collect all operators we care about
@@ -86,10 +86,8 @@ void FirstOrderModel::initialize( bool considerAxioms ) {
       }
     }
     processInitializeQuantifier( f );
-    if( considerAxioms || !f.hasAttribute(AxiomAttribute()) ){
-      //initialize relevant models within bodies of all quantifiers
-      initializeModelForTerm( f[1] );
-    }
+    //initialize relevant models within bodies of all quantifiers
+    initializeModelForTerm( f[1] );
   }
   processInitialize( false );
 }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 6ad04a1e6..0b282d5a5 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -78,7 +78,7 @@ public:
   virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
   virtual FirstOrderModelAbs * asFirstOrderModelAbs() { return NULL; }
   // initialize the model
-  void initialize( bool considerAxioms = true );
+  void initialize();
   virtual void processInitialize( bool ispre ) = 0;
   /** mark model set */
   void markModelSet() { d_isModelSet = true; }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 64ebb6cda..3148901da 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -335,7 +335,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
   if( fullModel==optBuildAtFullModel() ){
     Trace("fmc") << "---Full Model Check reset() " << std::endl;
-    fm->initialize( d_considerAxioms );
+    fm->initialize();
     d_quant_models.clear();
     d_rep_ids.clear();
     d_star_insts.clear();
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index cbff2b581..f6392a0b2 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -36,7 +36,7 @@ using namespace CVC4::theory::quantifiers;
 
 QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) :
 TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe( qe ){
-  d_considerAxioms = true;
+
 }
 
 bool QModelBuilder::isQuantifierActive( Node f ) {
@@ -161,7 +161,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
         Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
       }else{
         //initialize model
-        fm->initialize( d_considerAxioms );
+        fm->initialize();
         //analyze the functions
         Trace("model-engine-debug") << "Analyzing model..." << std::endl;
         analyzeModel( fm );
@@ -382,7 +382,7 @@ QModelBuilderIG::Statistics::~Statistics(){
 }
 
 bool QModelBuilderIG::isQuantifierActive( Node f ){
-  return d_qe->hasOwnership( f ) && ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end();
+  return d_qe->hasOwnership( f ) && d_quant_sat.find( f )==d_quant_sat.end();
 }
 
 bool QModelBuilderIG::isTermActive( Node n ){
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 4b0046089..3e4471fa4 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -44,8 +44,6 @@ public:
   virtual bool optUseModel();
   //whether to construct model at fullModel = true
   virtual bool optBuildAtFullModel() { return false; }
-  //consider axioms
-  bool d_considerAxioms;
   /** number of lemmas generated while building model */
   //is the exhaustive instantiation incomplete?
   bool d_incomplete_check;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 92361f68a..eede5c3a8 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -52,86 +52,50 @@ bool ModelEngine::needsCheck( Theory::Effort e ) {
   return e==Theory::EFFORT_LAST_CALL;
 }
 
+bool ModelEngine::needsModel( Theory::Effort e ) {
+  return true;  
+}
+
 void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
   if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
     int addedLemmas = 0;
-    bool needsBuild = true;
     FirstOrderModel* fm = d_quantEngine->getModel();
-    quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
-    if( fm->getNumAssertedQuantifiers()>0 ){
-      //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
-      //quantifiers are initialized, we begin an instantiation round
-      double clSet = 0;
-      if( Trace.isOn("model-engine") ){
-        clSet = double(clock())/double(CLOCKS_PER_SEC);
-      }
-      ++(d_statistics.d_inst_rounds);
-      Assert( mb!=NULL );
-      bool buildAtFullModel = mb->optBuildAtFullModel();
-      needsBuild = !buildAtFullModel;
-      //two effort levels: first try exhaustive instantiation without axioms, then with.
-      int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
-      for( int effort=startEffort; effort<2; effort++ ){
-        // for effort = 0, we only instantiate non-axioms
-        // for effort = 1, we instantiate everything
-        if( addedLemmas==0 ){
-          Trace("model-engine") << "---Model Engine Round---" << std::endl;
-          //initialize the model
-          Trace("model-engine-debug") << "Build model..." << std::endl;
-          mb->d_considerAxioms = effort>=1;
-          mb->d_addedLemmas = 0;
-          mb->buildModel( fm, buildAtFullModel );
-          addedLemmas += (int)mb->d_addedLemmas;
-          //if builder has lemmas, add and return
-          if( addedLemmas==0 ){
-            Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
-            //let the strong solver verify that the model is minimal
-            //for debugging, this will if there are terms in the model that the strong solver was not notified of
-            uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
-            if( !ufss || ufss->debugModel( fm ) ){
-              Trace("model-engine-debug") << "Check model..." << std::endl;
-              d_incomplete_check = false;
-              //print debug
-              Debug("fmf-model-complete") << std::endl;
-              debugPrint("fmf-model-complete");
-              //successfully built an acceptable model, now check it
-              addedLemmas += checkModel();
-            }else{
-              addedLemmas++;
-            }
-          }
-        }
-        if( addedLemmas==0 ){
-          //if we have not added lemmas yet and axiomInstMode=trust, then we are done
-          if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
-            //we must return unknown if an axiom is asserted
-            if( effort==0 ){
-              d_incomplete_check = true;
-            }
-            break;
-          }
-        }
-      }
-      if( Trace.isOn("model-engine") ){
-        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-        Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
-      }
+
+    //the following will test that the model satisfies all asserted universal quantifiers by 
+    // (model-based) exhaustive instantiation.
+    double clSet = 0;
+    if( Trace.isOn("model-engine") ){
+      Trace("model-engine") << "---Model Engine Round---" << std::endl;
+      clSet = double(clock())/double(CLOCKS_PER_SEC);
+    }
+    ++(d_statistics.d_inst_rounds);
+
+    Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
+    //let the strong solver verify that the model is minimal
+    //for debugging, this will if there are terms in the model that the strong solver was not notified of
+    uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
+    if( !ufss || ufss->debugModel( fm ) ){
+      Trace("model-engine-debug") << "Check model..." << std::endl;
+      d_incomplete_check = false;
+      //print debug
+      Debug("fmf-model-complete") << std::endl;
+      debugPrint("fmf-model-complete");
+      //successfully built an acceptable model, now check it
+      addedLemmas += checkModel();
     }else{
-      Trace("model-engine-debug") << "No quantified formulas asserted." << std::endl;
+      addedLemmas++;
+    }
+      
+    if( Trace.isOn("model-engine") ){
+      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
     }
+
     if( addedLemmas==0 ){
       Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
       //CVC4 will answer SAT or unknown
       Trace("fmf-consistent") << std::endl;
       debugPrint("fmf-consistent");
-      if( options::produceModels() && needsBuild ){
-        // finish building the model
-        mb->buildModel( fm, true );
-      }
-      //if the check was incomplete, we must set incomplete flag
-      if( d_incomplete_check ){
-        d_quantEngine->getOutputChannel().setIncomplete();
-      }
     }else{
       //otherwise, the search will continue
     }
@@ -173,6 +137,7 @@ bool ModelEngine::optOneQuantPerRound(){
 int ModelEngine::checkModel(){
   FirstOrderModel* fm = d_quantEngine->getModel();
   quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
+  Assert( mb!=NULL );
 
   //flatten the representatives
   //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
@@ -216,32 +181,46 @@ 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 : ( 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++ ){
-        Node f = fm->getAssertedQuantifier( i );
-        //determine if we should check this quantifier
-        if( mb->isQuantifierActive( f ) ){
-          exhaustiveInstantiate( f, e );
-          if( Trace.isOn("model-engine-warn") ){
-            if( d_addedLemmas>10000 ){
-              Debug("fmf-exit") << std::endl;
-              debugPrint("fmf-exit");
-              exit( 0 );
+  //default : 1 : conj,axiom
+  //priority : 0 : conj, 1 : axiom
+  //trust : 0 : conj
+  int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
+  for( int effort=startEffort; effort<2; effort++ ){
+    // FMC uses two sub-effort levels
+    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++ ){
+          Node f = fm->getAssertedQuantifier( i );
+          bool isAx = getTermDatabase()->isQAttrAxiom( f );
+          //determine if we should check this quantifier
+          if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){
+            exhaustiveInstantiate( f, e );
+            if( Trace.isOn("model-engine-warn") ){
+              if( d_addedLemmas>10000 ){
+                Debug("fmf-exit") << std::endl;
+                debugPrint("fmf-exit");
+                exit( 0 );
+              }
             }
+            if( optOneQuantPerRound() && d_addedLemmas>0 ){
+              break;
+            }
+          }else{
+            Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl;
           }
-          if( optOneQuantPerRound() && d_addedLemmas>0 ){
-            break;
-          }
-        }else{
-          Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl;
         }
       }
     }
+    if( d_addedLemmas==0 && options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
+      //set incomplete
+      if( effort==0 ){
+        d_quantEngine->getOutputChannel().setIncomplete();
+      }
+      break;
+    }
   }
   //print debug information
-  Trace("model-engine-debug") << "Instantiate axioms : " << ( mb->d_considerAxioms ? "yes" : "no" ) << std::endl;
   Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
   Trace("model-engine") << d_totalLemmas << std::endl;
   return d_addedLemmas;
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 6929188bc..8c53084f0 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -48,6 +48,7 @@ public:
   virtual ~ModelEngine();
 public:
   bool needsCheck( Theory::Effort e );
+  bool needsModel( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node f );
   void assertNode( Node f );
diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp
index fd3a76a52..5dd6316b3 100644
--- a/src/theory/quantifiers/qinterval_builder.cpp
+++ b/src/theory/quantifiers/qinterval_builder.cpp
@@ -943,7 +943,7 @@ void QIntervalBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
     //debug the model
     debugModel( fm );
   }else{
-    fm->initialize( d_considerAxioms );
+    fm->initialize();
     //process representatives
     fm->d_rep_id.clear();
     fm->d_max.clear();
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 09cae8eca..135f3547a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -256,7 +256,7 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
 void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_time);
   bool needsCheck = false;
-  bool needsBuildModel = false;
+  bool needsModel = false;
   std::vector< QuantifiersModule* > qm;
   if( d_model->getNumAssertedQuantifiers()>0 ){
     needsCheck = e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
@@ -264,9 +264,13 @@ void QuantifiersEngine::check( Theory::Effort e ){
       if( d_modules[i]->needsCheck( e ) ){
         qm.push_back( d_modules[i] );
         needsCheck = true;
+        if( d_modules[i]->needsModel( e ) ){
+          needsModel = true;
+        }
       }
     }
   }
+  bool defaultBuildModel = false;
   if( needsCheck ){
     Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
     Trace("quant-engine-debug") << "  modules to check : ";
@@ -319,15 +323,34 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
     for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){
-      for( int i=0; i<(int)qm.size(); i++ ){
-        Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
-        qm[i]->check( e, quant_e );
+      bool success = true;
+      //build the model if any module requested it
+      if( quant_e==QEFFORT_MODEL && needsModel ){
+        Assert( d_builder!=NULL );
+        Trace("quant-engine-debug") << "Build model, fullModel = " <<  d_builder->optBuildAtFullModel() << "..." << std::endl;
+        d_builder->d_addedLemmas = 0;
+        d_builder->buildModel( d_model, d_builder->optBuildAtFullModel() );
+        //we are done if model building was unsuccessful
+        if( d_builder->d_addedLemmas>0 ){
+          success = false;
+        }
+      }
+      if( success ){
+        //check each module
+        for( int i=0; i<(int)qm.size(); i++ ){
+          Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
+          qm[i]->check( e, quant_e );
+        }
       }
       //flush all current lemmas
       flushLemmas();
       //if we have added one, stop
       if( d_hasAddedLemma ){
         break;
+      //otherwise, complete the model generation if necessary
+      }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() && !d_builder->optBuildAtFullModel() ){
+        Trace("quant-engine-debug") << "Build completed model..." << std::endl;
+        d_builder->buildModel( d_model, true );
       }
     }
     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
@@ -336,7 +359,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     //  this happens if no quantifiers are currently asserted and no model-building module is enabled
     if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
       if( options::produceModels() && !d_model->isModelSet() ){
-        needsBuildModel = true;
+        defaultBuildModel = true;
       }
       if( Trace.isOn("inst-per-quant") ){
         for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
@@ -354,11 +377,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
   }else{
     if( e==Theory::EFFORT_LAST_CALL && options::produceModels() ){
-      needsBuildModel = true;
+      defaultBuildModel = true;
     }
   }
 
-  if( needsBuildModel ){
+  if( defaultBuildModel ){
     Trace("quant-engine-debug") << "Build the model..." << std::endl;
     d_te->getModelBuilder()->buildModel( d_model, true );
     Trace("quant-engine-debug") << "Done building the model." << std::endl;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index ee905ad09..75b55ca4a 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -53,6 +53,8 @@ public:
   virtual void finishInit() {}
   /* whether this module needs to check this round */
   virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
+  /* whether this module needs a model built */
+  virtual bool needsModel( Theory::Effort e ) { return false; }
   /* reset at a round */
   virtual void reset_round( Theory::Effort e ){}
   /* Call during quantifier engine's check */