Add a few options to separation logic and sets. Minor changes to separation logic, change syntax for empty heap constraint.

4 files changed, 101 insertions, 20 deletions

diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds
index 6c4ad33db..318442ba5 100644
--- a/src/theory/sep/kinds
+++ b/src/theory/sep/kinds
@@ -21,7 +21,7 @@ constant SEP_NIL_REF \
 
 variable SEP_NIL "separation nil"
 
-operator SEP_EMP 1 "separation empty heap"
+operator SEP_EMP 2 "separation empty heap"
 operator SEP_PTO 2 "points to relation"
 operator SEP_STAR 2: "separation star"
 operator SEP_WAND 2 "separation magic wand"
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index e2cd4f9dc..680bd8536 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -265,7 +265,8 @@ void TheorySep::postProcessModel( TheoryModel* m ){
     Trace("sep-model") << std::endl;
     if( sep_children.empty() ){
       TypeEnumerator te_domain( it->first );
-      m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain );
+      TypeEnumerator te_range( d_loc_to_data_type[it->first] );
+      m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain, *te_range );
     }else if( sep_children.size()==1 ){
       m_heap = sep_children[0];
     }else{
@@ -311,6 +312,7 @@ void TheorySep::check(Effort e) {
 
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
+    /*
     if( atom.getKind()==kind::SEP_EMP ){
       TypeNode tn = atom[0].getType();
       if( d_emp_arg.find( tn )==d_emp_arg.end() ){
@@ -319,6 +321,7 @@ void TheorySep::check(Effort e) {
         //normalize argument TODO
       }
     }
+    */
     TNode s_atom = atom.getKind()==kind::SEP_LABEL ? atom[0] : atom;
     TNode s_lbl = atom.getKind()==kind::SEP_LABEL ? atom[1] : TNode::null();
     bool is_spatial = s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_EMP;
@@ -410,7 +413,6 @@ void TheorySep::check(Effort e) {
               //Node ssn = NodeManager::currentNM()->mkNode( kind::EQUAL, s_atom[0], getNilRef(s_atom[0].getType()) ).negate();
               //conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn );
               
-              /* TODO?
             }else if( s_atom.getKind()==kind::SEP_EMP ){
               //conc = s_lbl.eqNode( NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())) );
               Node lem;
@@ -427,7 +429,7 @@ void TheorySep::check(Effort e) {
               }
               Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl;
               d_out->lemma( lem );
-              */
+
             }else{
               //labeled emp should be rewritten
               Assert( false );
@@ -546,6 +548,12 @@ void TheorySep::check(Effort e) {
           if( d_pto_model.find( vv )==d_pto_model.end() ){
             Trace("sep-process") << "Pto : " << s_atom[0] << " (" << vv << ") -> " << s_atom[1] << std::endl;
             d_pto_model[vv] = s_atom[1];
+            
+            //replace this on pto-model since this term is more relevant
+            TypeNode vtn = vv.getType();
+            if( std::find( d_type_references_all[vtn].begin(), d_type_references_all[vtn].end(), s_atom[0] )!=d_type_references_all[vtn].end() ){
+              d_tmodel[vv] = s_atom[0];
+            }
           }
         }
       }else{
@@ -991,7 +999,7 @@ TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node
       return tn1;
     }else if( n.getKind()==kind::SEP_EMP ){
       TypeNode tn = n[0].getType();
-      TypeNode tnd;
+      TypeNode tnd = n[1].getType();
       registerRefDataTypes( tn, tnd, atom );
       card = 1;
       visited[n] = card;
@@ -1110,6 +1118,8 @@ void TheorySep::initializeBounds() {
         //must include at least one constant
         n_emp = 1;
       }
+      Trace("sep-bound") << "Card maximums : " << d_card_max[tn] << " " << d_card_max[TypeNode::null()] << std::endl;
+      Trace("sep-bound") << "Type reference size : " << d_type_references[tn].size() << std::endl;
       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" );
@@ -1321,6 +1331,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
         std::vector< Node > children;
         children.resize( n.getNumChildren() );
         Assert( d_label_map[n].find( lbl )!=d_label_map[n].end() );
+        std::map< int, Node > mvals;
         for( std::map< int, Node >::iterator itl = d_label_map[n][lbl].begin(); itl != d_label_map[n][lbl].end(); ++itl ){
           Node sub_lbl = itl->second;
           int sub_index = itl->first;
@@ -1339,6 +1350,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
             lbl_mval = d_label_model[sub_lbl].getValue( rtn );
           }
           Trace("sep-inst-debug") << "Sublabel value is " << lbl_mval  << std::endl;
+          mvals[sub_index] = lbl_mval;
           children[sub_index] = instantiateLabel( n[sub_index], o_lbl, sub_lbl, lbl_mval, visited, pto_model, rtn, active_lbl, ind+1 );
           if( children[sub_index].isNull() ){
             return Node::null();
@@ -1346,14 +1358,18 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
         }
         Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn.toType()));
         if( n.getKind()==kind::SEP_STAR ){
+
           //disjoint contraints
+          std::vector< Node > conj;
+          std::vector< Node > bchildren;
+          bchildren.insert( bchildren.end(), children.begin(), children.end() );
           Node vsu;
           std::vector< Node > vs;
           for( std::map< int, Node >::iterator itl = d_label_map[n][lbl].begin(); itl != d_label_map[n][lbl].end(); ++itl ){
             Node sub_lbl = itl->second;
             Node lbl_mval = d_label_model[sub_lbl].getValue( rtn );
             for( unsigned j=0; j<vs.size(); j++ ){
-              children.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval, vs[j] ).eqNode( empSet ) );
+              bchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval, vs[j] ).eqNode( empSet ) );
             }
             vs.push_back( lbl_mval );
             if( vsu.isNull() ){
@@ -1362,11 +1378,32 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
               vsu = NodeManager::currentNM()->mkNode( kind::UNION, vsu, lbl_mval );
             }
           }
-          children.push_back( vsu.eqNode( lbl ) );
+          bchildren.push_back( vsu.eqNode( lbl ) );
           
-          //return the lemma
-          Assert( children.size()>1 );
-          return NodeManager::currentNM()->mkNode( kind::AND, children );      
+          Assert( bchildren.size()>1 );
+          conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, bchildren ) );
+
+          if( options::sepChildRefine() ){
+            //child-specific refinements (TODO: use ?)
+            for( unsigned i=0; i<children.size(); i++ ){
+              std::vector< Node > tchildren;
+              Node mval = mvals[i];
+              tchildren.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, mval, lbl ) );            
+              tchildren.push_back( children[i] );
+              std::vector< Node > rem_children;
+              for( unsigned j=0; j<children.size(); j++ ){
+                if( j!=i ){
+                  rem_children.push_back( n[j] );
+                }
+              }
+              std::map< Node, Node > rvisited;
+              Node rem = rem_children.size()==1 ? rem_children[0] : NodeManager::currentNM()->mkNode( kind::SEP_STAR, rem_children );
+              rem = applyLabel( rem, NodeManager::currentNM()->mkNode( kind::SETMINUS, lbl, mval ), rvisited );
+              tchildren.push_back( rem );
+              conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, tchildren ) );
+            }
+          }
+          return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::OR, conj );
         }else{
           std::vector< Node > wchildren;
           //disjoint constraints
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 3e74bd61e..48523cd06 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -17,6 +17,8 @@
 
 #include "expr/attribute.h"
 #include "theory/sep/theory_sep_rewriter.h"
+#include "theory/quantifiers/quant_util.h"
+#include "options/sep_options.h"
 
 namespace CVC4 {
 namespace theory {
@@ -160,18 +162,57 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
   return RewriteResponse(node==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
 
-
-/*
-RewriteResponse TheorySepRewriter::preRewrite(TNode node) {
-  if( node.getKind()==kind::SEP_EMP ){
-    Trace("sep-prerewrite") << "Sep::preRewrite emp star " << std::endl;
-    return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkNode( kind::SEP_EMP, NodeManager::currentNM()->mkConst( true ) ) );
+Node TheorySepRewriter::preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited ) {
+  std::map< Node, Node >::iterator it = visited[pol].find( n );
+  if( it==visited[pol].end() ){
+    Trace("ajr-temp") << "Pre-skolem emp " << n << " with pol " << pol << std::endl;
+    Node ret = n;
+    if( n.getKind()==kind::SEP_EMP ){
+      if( !pol ){
+        TypeNode tnx = n[0].getType();
+        TypeNode tny = n[1].getType();
+        Node x = NodeManager::currentNM()->mkSkolem( "ex", tnx, "skolem location for negated emp" );
+        Node y = NodeManager::currentNM()->mkSkolem( "ey", tny, "skolem data for negated emp" );
+        return NodeManager::currentNM()->mkNode( kind::SEP_STAR, 
+                 NodeManager::currentNM()->mkNode( kind::SEP_PTO, x, y ),
+                 NodeManager::currentNM()->mkConst( true ) ).negate();
+      }
+    }else if( n.getKind()!=kind::FORALL && n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      bool childChanged = false;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( n.getOperator() );
+      }
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        bool newPol, newHasPol;
+        QuantPhaseReq::getPolarity( n, i, true, pol, newHasPol, newPol );
+        Node nc = n[i];
+        if( newHasPol ){
+          nc = preSkolemEmp( n[i], newPol, visited );
+          childChanged = childChanged || nc!=n[i];
+        }
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        return NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }
+    visited[pol][n] = ret;
+    return n;
   }else{
-    Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl;
-    return RewriteResponse(REWRITE_DONE, node);
+    return it->second;
+  }
+}
+
+Node TheorySepRewriter::preprocess( Node n ) {
+  if( options::sepPreSkolemEmp() ){
+    bool pol = true;
+    std::map< bool, std::map< Node, Node > > visited;
+    n = preSkolemEmp( n, pol, visited );
   }
+  return n;
 }
-*/
+
 
 }/* CVC4::theory::sep namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h
index 02adbebe5..58b79c7fd 100644
--- a/src/theory/sep/theory_sep_rewriter.h
+++ b/src/theory/sep/theory_sep_rewriter.h
@@ -43,7 +43,10 @@ public:
 
   static inline void init() {}
   static inline void shutdown() {}
-
+private:
+  static Node preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited );
+public:
+  static Node preprocess( Node n );
 };/* class TheorySepRewriter */
 
 }/* CVC4::theory::sep namespace */