Refactor last call for theories, only create one model when quantifiers are enabled. Fix sep.nil preregistration in TheorySep.

5 files changed, 56 insertions, 22 deletions

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 836a04afa..605537c2d 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -93,6 +93,7 @@ Node TheorySep::ppRewrite(TNode term) {
 
 //must process assertions at preprocess so that quantified assertions are processed properly
 void TheorySep::processAssertions( std::vector< Node >& assertions ) {
+  d_pp_nils.clear();
   std::map< Node, bool > visited;
   for( unsigned i=0; i<assertions.size(); i++ ){
     processAssertion( assertions[i], visited );
@@ -102,7 +103,11 @@ void TheorySep::processAssertions( std::vector< Node >& assertions ) {
 void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) {
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
-    if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){
+    if( n.getKind()==kind::SEP_NIL ){
+      if( std::find( d_pp_nils.begin(), d_pp_nils.end(), n )==d_pp_nils.end() ){
+        d_pp_nils.push_back( n );
+      }
+    }else if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){
       //get the reference type (will compute d_type_references)
       int card = 0;
       TypeNode tn = getReferenceType( n, card );
@@ -307,6 +312,13 @@ void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel )
 void TheorySep::presolve() {
   Trace("sep-pp") << "Presolving" << std::endl;
   //TODO: cleanup if incremental?
+  
+  //we must preregister all instances of sep.nil to ensure they are made equal
+  for( unsigned i=0; i<d_pp_nils.size(); i++ ){
+    std::map< TNode, bool > visited;
+    preRegisterTermRec( d_pp_nils[i], visited );
+  }
+  d_pp_nils.clear();
 }
 
 
@@ -773,6 +785,10 @@ void TheorySep::check(Effort e) {
 }
 
 
+bool TheorySep::needsCheckLastEffort() {
+  return hasFacts();
+}
+
 Node TheorySep::getNextDecisionRequest() {
   for( unsigned i=0; i<d_neg_guards.size(); i++ ){
     Node g = d_neg_guards[i];
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 852a36721..2c87e79f9 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -50,6 +50,8 @@ class TheorySep : public Theory {
 
   /** True node for predicates = false */
   Node d_false;
+  
+  std::vector< Node > d_pp_nils;
 
   Node mkAnd( std::vector< TNode >& assumptions );
 
@@ -126,6 +128,8 @@ class TheorySep : public Theory {
 
   void check(Effort e);
 
+  bool needsCheckLastEffort();
+
   private:
 
   // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
diff --git a/src/theory/theory.h b/src/theory/theory.h
index e8518b1f6..81062d67a 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -565,7 +565,11 @@ public:
    * - or call get() until done() is true.
    */
   virtual void check(Effort level = EFFORT_FULL) { }
-
+  
+  /**
+   * Needs last effort check?
+   */ 
+  virtual bool needsCheckLastEffort() { return false; }
   /**
    * T-propagate new literal assignments in the current context.
    */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 881acdddd..f6894e07b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -156,6 +156,14 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf)
 void TheoryEngine::finishInit() {
   // initialize the quantifiers engine
   d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
+  
+  //initialize the model
+  if( d_logicInfo.isQuantified() ) {
+    d_curr_model = d_quantEngine->getModel();
+  } else {
+    d_curr_model = new theory::TheoryModel(d_userContext, "DefaultModel", true);
+    d_aloc_curr_model = true;
+  }
 
   if (d_logicInfo.isQuantified()) {
     d_quantEngine->finishInit();
@@ -217,6 +225,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_masterEENotify(*this),
   d_quantEngine(NULL),
   d_curr_model(NULL),
+  d_aloc_curr_model(false),
   d_curr_model_builder(NULL),
   d_ppCache(),
   d_possiblePropagations(context),
@@ -254,7 +263,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
   }
 
   // build model information if applicable
-  d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);
   d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
 
   smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
@@ -281,7 +289,9 @@ TheoryEngine::~TheoryEngine() {
   }
 
   delete d_curr_model_builder;
-  delete d_curr_model;
+  if( d_aloc_curr_model ){
+    delete d_curr_model;
+  }
 
   delete d_quantEngine;
 
@@ -518,24 +528,30 @@ void TheoryEngine::check(Theory::Effort effort) {
 
     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
     if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
-      //calls to theories requiring the model go here
-      //FIXME: this should not be theory-specific
-      if(d_logicInfo.isTheoryEnabled(THEORY_SEP)) {
-        Assert( d_theoryTable[THEORY_SEP]!=NULL );
-        if( d_theoryTable[THEORY_SEP]->hasFacts() ){
-          // must build model at this point
-          d_curr_model_builder->buildModel(getModel(), false);
-          d_theoryTable[THEORY_SEP]->check(Theory::EFFORT_LAST_CALL);
+      //checks for theories requiring the model go at last call
+      bool builtModel = false;
+      for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
+        if( theoryId!=THEORY_QUANTIFIERS ){
+          Theory* theory = d_theoryTable[theoryId];
+          if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
+            if( theory->needsCheckLastEffort() ){
+              if( !builtModel ){
+                builtModel = true;
+                d_curr_model_builder->buildModel(d_curr_model, false);
+              }
+              theory->check(Theory::EFFORT_LAST_CALL);
+            }
+          }
         }
       }
       if( ! d_inConflict && ! needCheck() ){
         if(d_logicInfo.isQuantified()) {
           // quantifiers engine must pass effort last call check
           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
-          // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
+          // if returning incomplete or SAT, we have ensured that d_curr_model has been built with fullModel=true
         } else if(options::produceModels()) {
           // must build model at this point
-          d_curr_model_builder->buildModel(getModel(), true);
+          d_curr_model_builder->buildModel(d_curr_model, true);
         }
         Trace("theory::assertions-model") << endl;
         if (Trace.isOn("theory::assertions-model")) {
@@ -782,14 +798,7 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
 
 /* get model */
 TheoryModel* TheoryEngine::getModel() {
-  Debug("model") << "TheoryEngine::getModel()" << endl;
-  if( d_logicInfo.isQuantified() ) {
-    Debug("model") << "Get model from quantifiers engine." << endl;
-    return d_quantEngine->getModel();
-  } else {
-    Debug("model") << "Get default model." << endl;
-    return d_curr_model;
-  }
+  return d_curr_model;
 }
 
 bool TheoryEngine::presolve() {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 53c4aac77..c126e89ad 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -183,6 +183,7 @@ class TheoryEngine {
    * Default model object
    */
   theory::TheoryModel* d_curr_model;
+  bool d_aloc_curr_model;
   /**
    * Model builder object
    */