From 449666e08ff5cc09fb950b6408d9362338c3d132 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Apr 2022 07:27:32 -0500 Subject: [PATCH] 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. --- src/theory/inference_id.cpp | 1 + src/theory/inference_id.h | 2 + src/theory/sep/theory_sep.cpp | 85 ++++++++++++++++++-------- src/theory/sep/theory_sep.h | 3 + src/theory/sep/theory_sep_rewriter.cpp | 20 ------ 5 files changed, 65 insertions(+), 46 deletions(-) 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; imkNode( n.getKind(), children ); - } - visited[n] = ret; - return ret; - }else{ - return it->second; + NodeManager* nm = NodeManager::currentNM(); + Kind k = n.getKind(); + std::map::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 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; -- 2.30.2