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

2 files changed, 21 insertions, 1 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