From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 9 Sep 2016 19:14:09 +0000 (-0500)
Subject: Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow... 
X-Git-Tag: cvc5-1.0.0~6028^2~59
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a97944b850f201fd692aa870e830b8fa0369c541;p=cvc5.git

Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow sep disequal card constants when type is monotonic.  Update logics on sep regressions.
---

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 462995bec..606e33d75 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -310,7 +310,7 @@ option cbqiInnermost --cbqi-innermost bool :read-write :default true
 option cbqiNestedQE --cbqi-nested-qe bool :default false
  process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation
  
-option quantEpr --quant-epr bool :default false
+option quantEpr --quant-epr bool :default false :read-write
  infer whether in effectively propositional fragment, use for cbqi
  
 ### local theory extensions options 
diff --git a/src/options/sep_options b/src/options/sep_options
index 043355bda..fecf4401e 100644
--- a/src/options/sep_options
+++ b/src/options/sep_options
@@ -12,8 +12,6 @@ option sepExp --sep-exp bool :default false
  experimental flag for sep
 option sepMinimalRefine --sep-min-refine bool :default false
  only add refinement lemmas for minimal (innermost) assertions
-option sepPreciseBound --sep-prec-bound bool :default false
- calculate precise bounds for labels
 option sepDisequalC --sep-deq-c bool :default true
  assume cardinality elements are distinct
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9c8838113..93e62f79d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1690,6 +1690,7 @@ void SmtEngine::setDefaults() {
     //disable modes not supported by incremental
     options::sortInference.set( false );
     options::ufssFairnessMonotone.set( false );
+    options::quantEpr.set( false );
   }
   if( d_logic.hasCardinalityConstraints() ){
     //must have finite model finding on
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 316357ef2..7c1fd82d3 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -19,6 +19,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/datatypes/theory_datatypes.h"
+#include "theory/sep/theory_sep.h"
 #include "theory/quantifiers/alpha_equivalence.h"
 #include "theory/quantifiers/ambqi_builder.h"
 #include "theory/quantifiers/bounded_integers.h"
@@ -113,11 +114,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   }
 
   if( options::quantEpr() ){
-    if( !options::incrementalSolving() ){
-      d_qepr = new QuantEPR;
-    }else{
-      d_qepr = NULL;
-    }
+    Assert( !options::incrementalSolving() );
+    d_qepr = new QuantEPR;
   }else{
     d_qepr = NULL;
   }
@@ -367,6 +365,9 @@ void QuantifiersEngine::ppNotifyAssertions( std::vector< Node >& assertions ) {
       }
     }
     if( d_qepr!=NULL ){
+      //must handle sources of other new constants e.g. separation logic
+      //FIXME: cleanup
+      ((sep::TheorySep*)getTheoryEngine()->theoryOf( THEORY_SEP ))->initializeBounds();
       d_qepr->finishInit(); 
     }
   }
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 8ab92368a..eefc0e779 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -26,6 +26,7 @@
 #include "smt/logic_exception.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/term_database.h"
+#include "options/quantifiers_options.h"
 
 using namespace std;
 
@@ -45,6 +46,7 @@ TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel
 {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
+  d_bounds_init = false;
   
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::SEP_PTO);
@@ -126,43 +128,6 @@ void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
   }
 }
 
-void TheorySep::preRegisterTermRec(TNode t, std::map< TNode, bool >& visited ) {
-  if( visited.find( t )==visited.end() ){
-    visited[t] = true;
-    Trace("sep-prereg-debug") << "Preregister : " << t << std::endl;
-    if( t.getKind()==kind::SEP_NIL ){
-      Trace("sep-prereg") << "Preregister nil : " << t << std::endl;
-      //per type, all nil variable references are equal
-      TypeNode tn = t.getType();
-      std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn );
-      if( it==d_nil_ref.end() ){
-        Trace("sep-prereg") << "...set as reference." << std::endl;
-        setNilRef( tn, t );
-      }else{
-        Node nr = it->second;
-        Trace("sep-prereg") << "...reference is " << nr << "." << std::endl;
-        if( t!=nr ){
-          if( d_reduce.find( t )==d_reduce.end() ){
-            d_reduce.insert( t );
-            Node lem = NodeManager::currentNM()->mkNode( tn.isBoolean() ? kind::IFF : kind::EQUAL, t, nr );
-            Trace("sep-lemma") << "Sep::Lemma: nil ref eq : " << lem << std::endl;
-            d_out->lemma( lem );
-          }
-        }
-      }
-    }else{
-      for( unsigned i=0; i<t.getNumChildren(); i++ ){
-        preRegisterTermRec( t[i], visited );
-      }
-    }
-  }
-}
-
-void TheorySep::preRegisterTerm(TNode term){
-  std::map< TNode, bool > visited;
-  preRegisterTermRec( term, visited );
-}
-
 
 void TheorySep::propagate(Effort e){
 
@@ -234,14 +199,12 @@ void TheorySep::computeCareGraph() {
 /////////////////////////////////////////////////////////////////////////////
 
 
-void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel )
-{
+void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ){
   // Send the equality engine information to the model
   m->assertEqualityEngine( &d_equalityEngine );
- 
 }
 
-void TheorySep::postProcessModel(TheoryModel* m) {
+void TheorySep::postProcessModel( TheoryModel* m ){
   Trace("sep-model") << "Printing model for TheorySep..." << std::endl;
   
   std::vector< Node > sep_children;
@@ -253,11 +216,9 @@ void TheorySep::postProcessModel(TheoryModel* m) {
     Assert( d_loc_to_data_type.find( it->first )!=d_loc_to_data_type.end() );
     Trace("sep-model") << "Model for heap, type = " << it->first << " with data type " << d_loc_to_data_type[it->first] << " : " << std::endl;
     TypeEnumerator te_range( d_loc_to_data_type[it->first] );
-    //m->d_comment_str << "Model for heap, type = " << it->first << " : " << std::endl;
     computeLabelModel( it->second, d_tmodel );
     if( d_label_model[it->second].d_heap_locs_model.empty() ){
       Trace("sep-model") << "  [empty]" << std::endl;
-      //m->d_comment_str << "  [empty]" << std::endl;
     }else{
       for( unsigned j=0; j<d_label_model[it->second].d_heap_locs_model.size(); j++ ){
         Assert( d_label_model[it->second].d_heap_locs_model[j].getKind()==kind::SINGLETON );
@@ -266,20 +227,17 @@ void TheorySep::postProcessModel(TheoryModel* m) {
         Assert( l.isConst() );
         pto_children.push_back( l );
         Trace("sep-model") << " " << l << " -> ";
-        //m->d_comment_str << "  " << l << " -> ";
         if( d_pto_model[l].isNull() ){
           Trace("sep-model") << "_";
           //m->d_comment_str << "_";
           pto_children.push_back( *te_range );
         }else{
           Trace("sep-model") << d_pto_model[l];
-          //m->d_comment_str << d_pto_model[l];
           Node vpto = d_valuation.getModel()->getRepresentative( d_pto_model[l] );
           Assert( vpto.isConst() );
           pto_children.push_back( vpto );
         }
         Trace("sep-model") << std::endl;
-        //m->d_comment_str << std::endl;
         sep_children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_PTO, pto_children ) );
       }
     }
@@ -288,8 +246,6 @@ void TheorySep::postProcessModel(TheoryModel* m) {
     m_neq = NodeManager::currentNM()->mkNode( nil.getType().isBoolean() ? kind::IFF : kind::EQUAL, nil, vnil );
     Trace("sep-model") << "sep.nil = " << vnil << std::endl;
     Trace("sep-model") << std::endl;
-    //m->d_comment_str << "sep.nil = " << vnil << std::endl;
-    //m->d_comment_str << std::endl;
     if( sep_children.empty() ){
       TypeEnumerator te_domain( it->first );
       m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain );
@@ -299,8 +255,6 @@ void TheorySep::postProcessModel(TheoryModel* m) {
       m_heap = NodeManager::currentNM()->mkNode( kind::SEP_STAR, sep_children );
     }
     m->setHeapModel( m_heap, m_neq );
-    //m->d_comment_str << m->d_sep_heap << std::endl;
-    //m->d_comment_str << m->d_sep_nil_eq << std::endl;
   }
   Trace("sep-model") << "Finished printing model for TheorySep." << std::endl;
 }
@@ -314,10 +268,17 @@ 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 );
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = d_pp_nils.begin(); it != d_pp_nils.end(); ++it ){
+    Trace("sep-pp") << it->second.size() << " nil references of type " << it->first << std::endl;
+    if( !it->second.empty() ){
+      setNilRef( it->first, it->second[0] );
+      //ensure all instances of sep.nil are made equal
+      for( unsigned i=1; i<it->second.size(); i++ ){
+        Node lem = NodeManager::currentNM()->mkNode( it->first.isBoolean() ? kind::IFF : kind::EQUAL, it->second[i], it->second[0] );
+        Trace("sep-lemma") << "Sep::Lemma: nil ref eq : " << lem << std::endl;
+        d_out->lemma( lem );
+      }
+    }
   }
   d_pp_nils.clear();
 }
@@ -392,28 +353,6 @@ void TheorySep::check(Effort e) {
               TypeNode tn = getReferenceType( s_atom );
               Assert( d_reference_bound.find( tn )!=d_reference_bound.end() );
               c_lems.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, s_lbl, d_reference_bound[tn] ) );
-              if( options::sepPreciseBound() ){
-                //more precise bound
-                Trace("sep-bound") << "Propagate Bound(" << s_lbl << ") = ";
-                Assert( d_lbl_reference_bound.find( s_lbl )!=d_lbl_reference_bound.end() );
-                for( unsigned j=0; j<d_lbl_reference_bound[s_lbl].size(); j++ ){
-                  Trace("sep-bound") << d_lbl_reference_bound[s_lbl][j] << " ";
-                }
-                Trace("sep-bound") << std::endl << "  to children of " << s_atom << std::endl;
-                //int rb_start = 0;
-                for( unsigned j=0; j<s_atom.getNumChildren(); j++ ){
-                  Node c_lbl = getLabel( s_atom, j, s_lbl );
-                  std::vector< Node > bound_loc;
-                  bound_loc.insert( bound_loc.end(), d_references[s_atom][j].begin(), d_references[s_atom][j].end() );
-                  //carry all locations for now
-                  bound_loc.insert( bound_loc.end(), d_lbl_reference_bound[s_lbl].begin(), d_lbl_reference_bound[s_lbl].end() );
-                  //Trace("sep-bound") << std::endl;
-                  Node bound_v = mkUnion( tn, bound_loc );
-                  Trace("sep-bound") << "  ...bound value : " << bound_v << std::endl;
-                  children.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, c_lbl, bound_v ) );
-                }     
-                Trace("sep-bound") << "Done propagate Bound(" << s_lbl << ")" << std::endl;        
-              }
               std::vector< Node > labels;
               getLabelChildren( s_atom, s_lbl, children, labels );
               Node empSet = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType()));
@@ -845,10 +784,10 @@ TypeNode TheorySep::getDataType( Node n ) {
 
 //must process assertions at preprocess so that quantified assertions are processed properly
 void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) {
-  //dummy sort in case heap loc/data is unconstrained
   d_pp_nils.clear();
   std::map< Node, bool > visited;
   for( unsigned i=0; i<assertions.size(); i++ ){
+    Trace("sep-pp") << "Process assertion : " << assertions[i] << std::endl;
     processAssertion( assertions[i], visited );
   }
   //if data type is unconstrained, assume a fresh uninterpreted sort
@@ -865,8 +804,9 @@ void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) {
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
     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 );
+      TypeNode tn = n.getType();
+      if( std::find( d_pp_nils[tn].begin(), d_pp_nils[tn].end(), n )==d_pp_nils[tn].end() ){
+        d_pp_nils[tn].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)
@@ -887,7 +827,7 @@ TypeNode TheorySep::computeReferenceType( Node atom, int& card, int index ) {
   std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index );
   if( it==d_reference_type[atom].end() ){
     card = 0;
-    TypeNode tn;      
+    TypeNode tn;
     if( index==-1 && ( atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND ) ){
       for( unsigned i=0; i<atom.getNumChildren(); i++ ){
         int cardc = 0;
@@ -947,7 +887,13 @@ TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node
       TypeNode tn1 = n[0].getType();
       TypeNode tn2 = n[1].getType();
       if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){
-        d_reference_bound_invalid[tn1] = true;
+        if( options::quantEpr() && n[0].getKind()==kind::BOUND_VARIABLE ){
+          // still valid : bound on heap models will include Herbrand universe of n[0].getType()
+          d_reference_bound_fv[tn1] = true;
+        }else{
+          d_reference_bound_invalid[tn1] = true;
+          Trace("sep-bound") << "reference cannot be bound (due to quantified pto)." << std::endl;
+        }
       }else{
         if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), n[0] )==d_references[atom][index].end() ){
           d_references[atom][index].push_back( n[0] );
@@ -976,6 +922,14 @@ TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node
       }
       visited[n] = card;
       return tn;
+    }else if( n.getKind()==kind::SEP_NIL ){
+      TypeNode tn = n.getType();
+      TypeNode tnd;
+      registerRefDataTypes( tn, tnd, n );
+      if( std::find( d_pp_nils[tn].begin(), d_pp_nils[tn].end(), n )==d_pp_nils[tn].end() ){
+        d_pp_nils[tn].push_back( n );
+      }
+      return tn;
     }else{
       card = 0;
       TypeNode otn;
@@ -998,6 +952,12 @@ TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node
 }
 
 void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){
+  //separation logic is effectively enabled when we find at least one spatial constraint occurs in the input
+  if( options::incrementalSolving() ){
+    std::stringstream ss;
+    ss << "ERROR: cannot use separation logic in incremental mode." << std::endl;
+    throw LogicException(ss.str());
+  }
   std::map< TypeNode, TypeNode >::iterator itt = d_loc_to_data_type.find( tn1 );
   if( itt==d_loc_to_data_type.end() ){
     if( !d_loc_to_data_type.empty() ){
@@ -1035,9 +995,55 @@ void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){
   }
 }
 
+void TheorySep::initializeBounds() {
+  if( !d_bounds_init ){
+    Trace("sep-bound")  << "Initialize sep bounds..." << std::endl;
+    d_bounds_init = true;
+    for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){
+      TypeNode tn = it->first;
+      Trace("sep-bound")  << "Initialize bounds for " << tn << "..." << std::endl;
+      QuantEPR * qepr = getLogicInfo().isQuantified() ? getQuantifiersEngine()->getQuantEPR() : NULL;
+      //if pto had free variable reference      
+      if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){
+        if( d_reference_bound_fv.find( tn )!=d_reference_bound_fv.end() ){
+          //include Herbrand universe of tn
+          if( qepr && qepr->isEPR( tn ) ){
+            for( unsigned j=0; j<qepr->d_consts[tn].size(); j++ ){
+              Node k = qepr->d_consts[tn][j];
+              if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), k )==d_type_references[tn].end() ){
+                d_type_references[tn].push_back( k );
+              }
+            }
+          }else{
+            d_reference_bound_invalid[tn] = true;
+            Trace("sep-bound") << "reference cannot be bound (due to non-EPR variable)." << std::endl;
+          }
+        }
+      }
+      unsigned n_emp = 0;
+      if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){ 
+        n_emp = d_card_max[tn]>d_card_max[TypeNode::null()] ? d_card_max[tn] : d_card_max[TypeNode::null()];  
+      }else if( d_type_references[tn].empty() ){
+        //must include at least one constant
+        n_emp = 1;
+      }
+      Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." << std::endl;
+      for( unsigned r=0; r<n_emp; r++ ){
+        Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
+        d_type_references_card[tn].push_back( e );
+        //must include this constant back into EPR handling
+        if( qepr && qepr->isEPR( tn ) ){
+          qepr->d_consts[tn].push_back( e );
+        }
+      }
+    }
+  }
+}
+
 Node TheorySep::getBaseLabel( TypeNode tn ) {
   std::map< TypeNode, Node >::iterator it = d_base_label.find( tn );
   if( it==d_base_label.end() ){
+    initializeBounds();
     Trace("sep") << "Make base label for " << tn << std::endl;
     std::stringstream ss;
     ss << "__Lb";
@@ -1051,35 +1057,45 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
     ss2 << "__Lu";
     d_reference_bound[tn] = NodeManager::currentNM()->mkSkolem( ss2.str(), ltn, "" );
     d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), d_type_references[tn].end() );
+
+    //check whether monotonic (elements can be added to tn without effecting satisfiability)
+    bool tn_is_monotonic = true;
+    if( tn.isSort() ){
+      //TODO: use monotonicity inference
+      tn_is_monotonic = !getLogicInfo().isQuantified();
+    }else{
+      tn_is_monotonic = tn.getCardinality().isInfinite();
+    }
     //add a reference type for maximum occurrences of empty in a constraint
-    unsigned n_emp = d_card_max[tn]>d_card_max[TypeNode::null()] ? d_card_max[tn] : d_card_max[TypeNode::null()];
-    for( unsigned r=0; r<n_emp; r++ ){
-      Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
-      //d_type_references_all[tn].push_back( NodeManager::currentNM()->mkSkolem( "e", NodeManager::currentNM()->mkRefType(tn) ) );
-      if( options::sepDisequalC() ){
+    if( options::sepDisequalC() && tn_is_monotonic ){
+      for( unsigned r=0; r<d_type_references_card[tn].size(); r++ ){
+        Node e = d_type_references_card[tn][r];
         //ensure that it is distinct from all other references so far
         for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){
           Node eq = NodeManager::currentNM()->mkNode( e.getType().isBoolean() ? kind::IFF : kind::EQUAL, e, d_type_references_all[tn][j] );
           d_out->lemma( eq.negate() );
         }
+        d_type_references_all[tn].push_back( e );
       }
-      d_type_references_all[tn].push_back( e );
-      d_lbl_reference_bound[d_base_label[tn]].push_back( e );
+    }else{
+      //break symmetries TODO
+    
+      d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begin(), d_type_references_card[tn].end() );
     }
-    //construct bound
-    d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] );
-    Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl;
+    Assert( !d_type_references_all[tn].empty() );
+    
+    if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){      
+      //construct bound
+      d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] );
+      Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl;
 
-    if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){
       Node slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_reference_bound[tn], d_reference_bound_max[tn] );
       Trace("sep-lemma") << "Sep::Lemma: reference bound for " << tn << " : " << slem << std::endl;
       d_out->lemma( slem );
-    }else{
-      Trace("sep-bound") << "reference cannot be bound (possibly due to quantified pto)." << std::endl;
+      //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
+      //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl;
+      //d_out->lemma( slem );
     }
-    //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
-    //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl;
-    //d_out->lemma( slem );
     
     //assert that nil ref is not in base label
     Node nr = getNilRef( tn );
@@ -1373,7 +1389,6 @@ void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) {
         Assert( false );
       }
     }
-    //end hack
     for( unsigned j=0; j<d_label_model[lbl].d_heap_locs_model.size(); j++ ){
       Node u = d_label_model[lbl].d_heap_locs_model[j];
       Assert( u.getKind()==kind::SINGLETON );
@@ -1387,7 +1402,8 @@ void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) {
         //TypeNode tn = u.getType().getRefConstituentType();
         TypeNode tn = u.getType();
         Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << ", cref type " << tn << std::endl;
-        Assert( d_type_references_all.find( tn )!=d_type_references_all.end() && !d_type_references_all[tn].empty() );
+        Assert( d_type_references_all.find( tn )!=d_type_references_all.end() );
+        Assert( !d_type_references_all[tn].empty() );
         tt = d_type_references_all[tn][0];
       }else{
         tt = itm->second;
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 32aa065b7..4f60c5781 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -51,7 +51,10 @@ class TheorySep : public Theory {
   /** True node for predicates = false */
   Node d_false;
   
-  std::vector< Node > d_pp_nils;
+  //whether bounds have been initialized
+  bool d_bounds_init;
+  
+  std::map< TypeNode, std::vector< Node > > d_pp_nils;
 
   Node mkAnd( std::vector< TNode >& assumptions );
 
@@ -88,10 +91,8 @@ class TheorySep : public Theory {
   /** Explain why this literal is true by adding assumptions */
   void explain(TNode literal, std::vector<TNode>& assumptions);
 
-  void preRegisterTermRec(TNode t, std::map< TNode, bool >& visited );
   public:
 
-  void preRegisterTerm(TNode t);
   void propagate(Effort e);
   Node explain(TNode n);
 
@@ -220,11 +221,11 @@ class TheorySep : public Theory {
   std::map< TypeNode, Node > d_reference_bound;
   std::map< TypeNode, Node > d_reference_bound_max;
   std::map< TypeNode, bool > d_reference_bound_invalid;
+  std::map< TypeNode, bool > d_reference_bound_fv;
   std::map< TypeNode, std::vector< Node > > d_type_references;
+  std::map< TypeNode, std::vector< Node > > d_type_references_card;
   std::map< TypeNode, std::vector< Node > > d_type_references_all;
   std::map< TypeNode, unsigned > d_card_max;
-  //bounds for labels
-  std::map< Node, std::vector< Node > > d_lbl_reference_bound;
   //for empty argument
   std::map< TypeNode, Node > d_emp_arg;
   //map from ( atom, label, child index ) -> label
@@ -299,6 +300,7 @@ public:
     return &d_equalityEngine;
   }
 
+  void initializeBounds();
 };/* class TheorySep */
 
 }/* CVC4::theory::sep namespace */
diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index 6078bfa19..7bcd700bd 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -56,7 +56,8 @@ TESTS =	\
   fmf-nemp-2.smt2 \
   trees-1.smt2 \
   wand-false.smt2 \
-  dup-nemp.smt2
+  dup-nemp.smt2 \
+  emp2-quant-unsat.smt2
 
 
 FAILING_TESTS =
diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2
index d3245e33f..ebe52fa46 100644
--- a/test/regress/regress0/sep/chain-int.smt2
+++ b/test/regress/regress0/sep/chain-int.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2
index a0fc5a187..f68434f33 100755
--- a/test/regress/regress0/sep/crash1220.smt2
+++ b/test/regress/regress0/sep/crash1220.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/dispose-list-4-init.smt2 b/test/regress/regress0/sep/dispose-list-4-init.smt2
index 766354cd9..b3e2088b1 100644
--- a/test/regress/regress0/sep/dispose-list-4-init.smt2
+++ b/test/regress/regress0/sep/dispose-list-4-init.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 
 (declare-sort Loc 0)
 
diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2
index 009561128..98348f617 100644
--- a/test/regress/regress0/sep/dup-nemp.smt2
+++ b/test/regress/regress0/sep/dup-nemp.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 (declare-sort Loc 0)
 (declare-const l Loc)
diff --git a/test/regress/regress0/sep/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2
new file mode 100644
index 000000000..52d99d8c0
--- /dev/null
+++ b/test/regress/regress0/sep/emp2-quant-unsat.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --quant-epr
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun u () U)
+
+(assert (sep (not (emp u)) (not (emp u))))
+
+(assert (forall ((x U) (y U)) (= x y)))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2
index 2981606d8..b857aec2a 100644
--- a/test/regress/regress0/sep/loop-1220.smt2
+++ b/test/regress/regress0/sep/loop-1220.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index e1e21dd10..a0766a7e0 100644
--- a/test/regress/regress0/sep/nemp.smt2
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (assert (not (emp 0)))
 (check-sat)
diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2
index 0c93719c9..c807757d1 100755
--- a/test/regress/regress0/sep/nspatial-simp.smt2
+++ b/test/regress/regress0/sep/nspatial-simp.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun x () Int)
 
diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2
index b0dece248..28ed5c47b 100644
--- a/test/regress/regress0/sep/pto-01.smt2
+++ b/test/regress/regress0/sep/pto-01.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2
index f0b6d2dee..ab1cea0c8 100644
--- a/test/regress/regress0/sep/pto-02.smt2
+++ b/test/regress/regress0/sep/pto-02.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 
diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2
index 1734c93bb..9b0afda7a 100644
--- a/test/regress/regress0/sep/pto-04.smt2
+++ b/test/regress/regress0/sep/pto-04.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x1 Int)
diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2
index c3330f036..a93fc4db8 100644
--- a/test/regress/regress0/sep/sep-01.smt2
+++ b/test/regress/regress0/sep/sep-01.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2
index 403bcf077..6f190d964 100644
--- a/test/regress/regress0/sep/sep-02.smt2
+++ b/test/regress/regress0/sep/sep-02.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-03.smt2 b/test/regress/regress0/sep/sep-03.smt2
index 427c44b50..8dce5acc7 100644
--- a/test/regress/regress0/sep/sep-03.smt2
+++ b/test/regress/regress0/sep/sep-03.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-find2.smt2 b/test/regress/regress0/sep/sep-find2.smt2
index 26a27eb22..356f866c1 100644
--- a/test/regress/regress0/sep/sep-find2.smt2
+++ b/test/regress/regress0/sep/sep-find2.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x1 Int)
diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2
index 8ddbdd05f..ab12c6461 100644
--- a/test/regress/regress0/sep/sep-neg-1refine.smt2
+++ b/test/regress/regress0/sep/sep-neg-1refine.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-neg-nstrict.smt2 b/test/regress/regress0/sep/sep-neg-nstrict.smt2
index 1a69336a8..425e5ce3c 100644
--- a/test/regress/regress0/sep/sep-neg-nstrict.smt2
+++ b/test/regress/regress0/sep/sep-neg-nstrict.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2
index e71e6a51a..7ada6ff06 100644
--- a/test/regress/regress0/sep/sep-neg-nstrict2.smt2
+++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-neg-simple.smt2 b/test/regress/regress0/sep/sep-neg-simple.smt2
index 191e7527f..7b6fc69e9 100644
--- a/test/regress/regress0/sep/sep-neg-simple.smt2
+++ b/test/regress/regress0/sep/sep-neg-simple.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-neg-swap.smt2 b/test/regress/regress0/sep/sep-neg-swap.smt2
index f89a9c0ac..53f890b0d 100644
--- a/test/regress/regress0/sep/sep-neg-swap.smt2
+++ b/test/regress/regress0/sep/sep-neg-swap.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-nterm-again.smt2 b/test/regress/regress0/sep/sep-nterm-again.smt2
index 9b4afe36a..3e595b5e9 100644
--- a/test/regress/regress0/sep/sep-nterm-again.smt2
+++ b/test/regress/regress0/sep/sep-nterm-again.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-nterm-val-model.smt2 b/test/regress/regress0/sep/sep-nterm-val-model.smt2
index 0178134cb..d4fb0fd52 100644
--- a/test/regress/regress0/sep/sep-nterm-val-model.smt2
+++ b/test/regress/regress0/sep/sep-nterm-val-model.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2
index 772acd981..9522e2420 100644
--- a/test/regress/regress0/sep/sep-plus1.smt2
+++ b/test/regress/regress0/sep/sep-plus1.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2
index 6cdf51294..cedbb53eb 100755
--- a/test/regress/regress0/sep/sep-simp-unc.smt2
+++ b/test/regress/regress0/sep/sep-simp-unc.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun x () U)
diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
index fb58b9d10..9239fb770 100644
--- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
+++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-sort U 0)
diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2
index 0c0b6a9a3..70927ad82 100644
--- a/test/regress/regress0/sep/simple-neg-sat.smt2
+++ b/test/regress/regress0/sep/simple-neg-sat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
index ed3187a96..10e509e05 100644
--- a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
+++ b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2
index 1731174fa..1a9e76a8a 100644
--- a/test/regress/regress0/sep/split-find-unsat.smt2
+++ b/test/regress/regress0/sep/split-find-unsat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2
index 0c0ee72ad..fa0aab591 100644
--- a/test/regress/regress0/sep/wand-0526-sat.smt2
+++ b/test/regress/regress0/sep/wand-0526-sat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
 (declare-fun y () Int)
 (declare-fun u () Int)
diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2
index 9b4871323..1d799c8c9 100644
--- a/test/regress/regress0/sep/wand-crash.smt2
+++ b/test/regress/regress0/sep/wand-crash.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (assert (wand (emp 0) (emp 0)))
 (check-sat)
diff --git a/test/regress/regress0/sep/wand-false.smt2 b/test/regress/regress0/sep/wand-false.smt2
index 642c0a8aa..65500f775 100644
--- a/test/regress/regress0/sep/wand-false.smt2
+++ b/test/regress/regress0/sep/wand-false.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun x () Int)
 (assert (wand (pto x x) false))
diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2
index e8ee4252c..0db7330d1 100644
--- a/test/regress/regress0/sep/wand-nterm-simp.smt2
+++ b/test/regress/regress0/sep/wand-nterm-simp.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
 (assert (wand (emp x) (pto x 3)))
 (check-sat)
diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2
index c317e8736..cce0f79e3 100644
--- a/test/regress/regress0/sep/wand-nterm-simp2.smt2
+++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (emp x)))
diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2
index df4bfa6d8..120683f74 100755
--- a/test/regress/regress0/sep/wand-simp-sat.smt2
+++ b/test/regress/regress0/sep/wand-simp-sat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (pto x 1)))
 (check-sat)
diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2
index 059e91317..c684d16ad 100755
--- a/test/regress/regress0/sep/wand-simp-sat2.smt2
+++ b/test/regress/regress0/sep/wand-simp-sat2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (pto x 3)))
diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2
index 95bc85537..c9851661a 100755
--- a/test/regress/regress0/sep/wand-simp-unsat.smt2
+++ b/test/regress/regress0/sep/wand-simp-unsat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (pto x 3)))
 (assert (emp x))