From f08aa56f710b46da5c2b5157c102062e9a39e0b9 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Jul 2022 11:26:00 -0500
Subject: [PATCH] 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.
---
 src/theory/sep/theory_sep.cpp                 | 27 +++++++++++++++++-
 src/theory/sep/theory_sep.h                   |  8 ++++--
 test/regress/cli/CMakeLists.txt               |  1 +
 .../regress0/sep/issue8863-downwards-pto.smt2 | 28 +++++++++++++++++++
 4 files changed, 60 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/cli/regress0/sep/issue8863-downwards-pto.smt2

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index d86bea6b4..73fe3eda1 100644
--- 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 8abfd5a5a..f6e40f972 100644
--- 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 c8efaad52..d4fd132cd 100644
--- 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
index 000000000..b2cca9564
--- /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) 
+
-- 
2.30.2