Refactor last call for theories, only create one model when quantifiers are enabled...

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 836a04afad17034b8abbf23c01fac79dab500244..605537c2d7966a53abea44c02823fa192fd1ad6e 100644 (file)
--- 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 852a36721e66b3799891cebc4cbc5a03f5def31d..2c87e79f9d1743adb1f3e079edaa6163876a88a7 100644 (file)
--- 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 e8518b1f6b49d7ecb58aa514a78e8929ee44ce4e..81062d67a6f00f3d1b34615a3ca23b305d41fb61 100644 (file)
--- 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 881acddddce4ab2f6c690bfeb2b6da40189c1261..f6894e07b9ee65a59b91d7a9153349ff174dbe79 100644 (file)
--- 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 53c4aac77da9078d927a0440f3ccc856bf5991db..c126e89ad21e314281c04662254fb981cdd3e66d 100644 (file)
--- 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
    */

diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index 9d2abaa1845b21dcf87d00d6411e94856a6199f6..9744cae99deda0f09f12807a7ecd94011e534da9 100644 (file)
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -53,7 +53,8 @@ TESTS =       \
   dispose-list-4-init.smt2 \
   wand-0526-sat.smt2 \
   quant_wand.smt2 \
-  fmf-nemp-2.smt2
+  fmf-nemp-2.smt2 \
+  trees-1.smt2
 
 
 FAILING_TESTS =

diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2
new file mode 100644 (file)
index 0000000..88e875f
--- /dev/null
+++ b/test/regress/regress0/sep/trees-1.smt2
@@ -0,0 +1,41 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-sort Loc 0)
+(declare-const loc0 Loc)
+
+(declare-datatypes () ((Node (node (data Int) (left Loc) (right Loc)))))
+
+(declare-const dv Int)
+(declare-const v Loc)
+
+(declare-const dl Int)
+(declare-const l Loc)
+(declare-const dr Int)
+(declare-const r Loc)
+
+(define-fun ten-tree0 ((x Loc) (d Int)) Bool 
+(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0) (= l (as sep.nil Loc))) (and (emp loc0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
+
+(declare-const dy Int)
+(declare-const y Loc)
+(declare-const dz Int)
+(declare-const z Loc)
+
+(define-fun ord-tree0 ((x Loc) (d Int)) Bool 
+(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0) (= y (as sep.nil Loc))) (and (emp loc0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
+
+;------- f -------
+(assert (= y (as sep.nil Loc)))
+(assert (= z (as sep.nil Loc)))
+
+(assert (= dy dv))
+(assert (= dz (+ dv 10)))
+;-----------------
+
+(assert (not (= v (as sep.nil Loc))))
+
+(assert (ten-tree0 v dv))
+(assert (not (ord-tree0 v dv)))
+
+(check-sat)