Fix pto handling for heaps that are not a subset of the base heap (#8942)

These require a downwards rule to be compatible with our propagation rules for pto.

Fixes #8863.

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index d86bea6b46400137712649b49271054eaf595969..73fe3eda14bdc247a9d6427a1bbf70dd4b3611c1 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -44,7 +44,6 @@ namespace sep {
 
 TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_SEP, env, out, valuation),
-      d_lemmas_produced_c(userContext()),
       d_bounds_init(false),
       d_state(env, valuation),
       d_im(env, *this, d_state, "theory::sep::"),
@@ -410,6 +409,25 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
       {
         conc = slbl.eqNode(ss);
       }
+      // if we are not a part of the root label, we require applying downwards
+      // closure, e.g. (SEP_LABEL (pto x y) A) =>
+      // (or (SEP_LABEL (pto x y) B) (SEP_LABEL (pto x y) C)) where
+      // A is the disjoint union of B and C.
+      if (!sharesRootLabel(slbl, d_base_label))
+      {
+        std::map<Node, std::vector<Node> >::iterator itc =
+            d_childrenMap.find(slbl);
+        if (itc != d_childrenMap.end())
+        {
+          std::vector<Node> disjs;
+          for (const Node& c : itc->second)
+          {
+            disjs.push_back(nm->mkNode(SEP_LABEL, satom, c));
+          }
+          Node conc2 = nm->mkNode(OR, disjs);
+          conc = conc.isNull() ? conc2 : nm->mkNode(AND, conc, conc2);
+        }
+      }
       // note semantics of sep.nil is enforced globally
     }
     else if (satom.getKind() == SEP_EMP)
@@ -1277,7 +1295,14 @@ Node TheorySep::getLabel( Node atom, int child, Node lbl ) {
 
 void TheorySep::makeDisjointHeap(Node parent, const std::vector<Node>& children)
 {
+  Trace("sep-debug") << "disjoint heap: " << parent << " for " << children
+                     << std::endl;
   Assert(children.size() >= 2);
+  if (!sharesRootLabel(parent, d_base_label))
+  {
+    Assert(d_childrenMap.find(parent) == d_childrenMap.end());
+    d_childrenMap[parent] = children;
+  }
   // remember parent relationships
   for (const Node& c : children)
   {

diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 8abfd5a5aee67cbcf551817586940e6d6f79d85e..f6e40f97292ea6f098dfbdd5b1226d871fbaf998 100644 (file)
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -47,9 +47,6 @@ class TheorySep : public Theory {
   /////////////////////////////////////////////////////////////////////////////
 
  private:
-  /** all lemmas sent */
-  NodeSet d_lemmas_produced_c;
-
   /** True node for predicates = true */
   Node d_true;
 
@@ -248,6 +245,11 @@ class TheorySep : public Theory {
    * if sep.wand constraints are present.
    */
   std::map<Node, std::vector<Node> > d_parentMap;
+  /**
+   * Maps label sets to their direct children. This map is only stored for
+   * labels with children that do not share a root label with the base label.
+   */
+  std::map<Node, std::vector<Node> > d_childrenMap;
 
   /**
    * This sends the lemmas:

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index c8efaad52e4974326e052ffa75cc22d2a8a1ccf0..d4fd132cdf7bbfc1931a7545cb7abec39c330714 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1210,6 +1210,7 @@ set(regress_0_tests
   regress0/sep/issue5343-err.smt2
   regress0/sep/issue8659-wand-diff-heaps.smt2
   regress0/sep/issue8841-neg-prop.smt2
+  regress0/sep/issue8863-downwards-pto.smt2
   regress0/sep/nemp.smt2
   regress0/sep/nil-no-elim.smt2
   regress0/sep/nspatial-simp.smt2

diff --git a/test/regress/cli/regress0/sep/issue8863-downwards-pto.smt2 b/test/regress/cli/regress0/sep/issue8863-downwards-pto.smt2
new file mode 100644 (file)
index 0000000..b2cca95
--- /dev/null
+++ b/test/regress/cli/regress0/sep/issue8863-downwards-pto.smt2
@@ -0,0 +1,28 @@
+(set-logic ALL) 
+(set-info :status unsat)
+ 
+(declare-sort Loc 0) 
+(declare-heap (Loc Loc)) 
+ 
+(declare-const z Loc) 
+(declare-const y Loc) 
+(declare-const x Loc) 
+ 
+(assert 
+  (sep 
+    (not (wand 
+      sep.emp 
+      (not (pto x z)) 
+    ))  
+    (distinct y z) 
+    (distinct y x) 
+    (distinct z x) 
+  ) 
+) 
+ 
+(assert 
+  (pto x y) 
+) 
+ 
+(check-sat) 
+