From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 28 Apr 2022 12:27:32 +0000 (-0500)
Subject: Make labelled separation logic asserts preserve labels (#8671)
X-Git-Tag: cvc5-1.0.1~211
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=449666e08ff5cc09fb950b6408d9362338c3d132;p=cvc5.git

Make labelled separation logic asserts preserve labels (#8671)

This is a first step towards fixing #8659.

The issue is that when two labels are equal, we assume they refer to subheaps of the same heap. This is incorrect for magic wand. This ensures we preserve labels, a further PR will ensure that syntactic equality on labels (instead of semantic equality) is used for knowing when two pto constraints must be unified. This means that SEP_LABEL nodes should never be rewritten.
---

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index d3a79b8e3..f298c6b85 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -312,6 +312,7 @@ const char* toString(InferenceId i)
     case InferenceId::SEP_LABEL_INTRO: return "SEP_LABEL_INTRO";
     case InferenceId::SEP_LABEL_DEF: return "SEP_LABEL_DEF";
     case InferenceId::SEP_EMP: return "SEP_EMP";
+    case InferenceId::SEP_POS_PTO_SINGLETON: return "SEP_POS_PTO_SINGLETON";
     case InferenceId::SEP_POS_REDUCTION: return "SEP_POS_REDUCTION";
     case InferenceId::SEP_NEG_REDUCTION: return "SEP_NEG_REDUCTION";
     case InferenceId::SEP_REFINEMENT: return "SEP_REFINEMENT";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 51ce478c4..034eeacc1 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -449,6 +449,8 @@ enum class InferenceId
   SEP_LABEL_DEF,
   // lemma for sep.emp
   SEP_EMP,
+  // lemma for positive labelled PTO
+  SEP_POS_PTO_SINGLETON,
   // positive reduction for sep constraint
   SEP_POS_REDUCTION,
   // negative reduction for sep constraint
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 47447ba78..bc65f3451 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -285,8 +285,25 @@ bool TheorySep::preNotifyFact(
       d_spatial_assertions.push_back(fact);
     }
   }
+  if (!slbl.isNull() && satom.getKind() == SEP_PTO)
+  {
+    if (polarity)
+    {
+      NodeManager* nm = NodeManager::currentNM();
+      // (SEP_LABEL (sep.pto x y) L) => L = (set.singleton x)
+      Node s = nm->mkSingleton(slbl.getType().getSetElementType(), satom[0]);
+      Node eq = slbl.eqNode(s);
+      TrustNode trn =
+          d_im.mkLemmaExp(eq, PfRule::THEORY_INFERENCE, {fact}, {fact}, {eq});
+      d_im.addPendingLemma(trn.getNode(),
+                           InferenceId::SEP_POS_PTO_SINGLETON,
+                           LemmaProperty::NONE,
+                           trn.getGenerator());
+    }
+    return false;
+  }
   // assert to equality if non-spatial or a labelled pto
-  if (!isSpatial || (!slbl.isNull() && satom.getKind() == SEP_PTO))
+  if (!isSpatial)
   {
     return false;
   }
@@ -1330,33 +1347,49 @@ Node TheorySep::getLabel( Node atom, int child, Node lbl ) {
 
 Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) {
   Assert(n.getKind() != kind::SEP_LABEL);
-  if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP ){
-    return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl );
-  }else if( !n.getType().isBoolean() || n.getNumChildren()==0 ){
-    return n;
-  }else{
-    std::map< Node, Node >::iterator it = visited.find( n );
-    if( it==visited.end() ){
-      std::vector< Node > children;
-      if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        children.push_back( n.getOperator() );
-      }
-      bool childChanged = false;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node aln = applyLabel( n[i], lbl, visited );
-        children.push_back( aln );
-        childChanged = childChanged || aln!=n[i];
-      }
-      Node ret = n;
-      if( childChanged ){
-        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-      visited[n] = ret;
-      return ret;
-    }else{
-      return it->second;
+  NodeManager* nm = NodeManager::currentNM();
+  Kind k = n.getKind();
+  std::map<Node, Node>::iterator it = visited.find(n);
+  if (it != visited.end())
+  {
+    return it->second;
+  }
+  Node ret;
+  if (k == kind::SEP_STAR || k == kind::SEP_WAND || k == kind::SEP_PTO)
+  {
+    ret = nm->mkNode(kind::SEP_LABEL, n, lbl);
+  }
+  else if (k == kind::SEP_EMP)
+  {
+    // (SEP_LABEL sep.emp L) is the same as (= L set.empty)
+    ret = lbl.eqNode(nm->mkConst(EmptySet(lbl.getType())));
+  }
+  else if (n.getType().isBoolean() && n.getNumChildren() > 0)
+  {
+    ret = n;
+    std::vector<Node> children;
+    if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      children.push_back(n.getOperator());
+    }
+    bool childChanged = false;
+    for (const Node& nc : n)
+    {
+      Node aln = applyLabel(nc, lbl, visited);
+      children.push_back(aln);
+      childChanged = childChanged || aln != nc;
+    }
+    if (childChanged)
+    {
+      ret = nm->mkNode(n.getKind(), children);
     }
   }
+  else
+  {
+    ret = n;
+  }
+  visited[n] = ret;
+  return ret;
 }
 
 Node TheorySep::instantiateLabel(Node n,
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 3073c2a44..b7db57b5c 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -284,6 +284,9 @@ class TheorySep : public Theory {
   Node getNilRef( TypeNode tn );
   void setNilRef( TypeNode tn, Node n );
   Node getLabel( Node atom, int child, Node lbl );
+  /**
+   * Apply label lbl to all top-level spatial assertions, recursively, in n.
+   */
   Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited );
   void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels );
 
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 248461bf4..ad9b63666 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -100,26 +100,6 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
   Trace("sep-postrewrite") << "Sep::postRewrite start " << node << std::endl;
   Node retNode = node;
   switch (node.getKind()) {
-    case kind::SEP_LABEL: {
-      if( node[0].getKind()==kind::SEP_PTO ){
-        // TODO(project##230): Find a safe type for the singleton operator
-        Node s = NodeManager::currentNM()->mkSingleton(node[0][0].getType(),
-                                                       node[0][0]);
-        if( node[1]!=s ){
-          Node c1 = node[1].eqNode( s );
-          Node c2 = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, node[0][0], node[0][1] ), s );
-          retNode = NodeManager::currentNM()->mkNode( kind::AND, c1, c2 );
-        }
-      }
-      if( node[0].getKind()==kind::SEP_EMP ){
-        retNode = node[1].eqNode(
-            NodeManager::currentNM()->mkConst(EmptySet(node[1].getType())));
-      }
-      break;
-    }
-    case kind::SEP_PTO: {
-      break;
-    }
     case kind::SEP_STAR: {
       //flatten
       std::vector< Node > s_children;