Fix policy for merging subproofs (#6981)

This makes it so that we replace subproof A with subproof B if A and B prove the same thing, and B contains no assumptions. This is independent of the scope that A and B are in.

The previous policy replaced subproof A with subproof B if A and B prove the same thing and were in the same scope. This is not safe if A occurs in multiple scopes, where free assumptions can escape.

The new policy is more effective and safer than the previous one.

4 files changed, 69 insertions, 30 deletions

diff --git a/src/proof/proof_node_updater.cpp b/src/proof/proof_node_updater.cpp
index 2bdb54a45..561d4a761 100644
--- a/src/proof/proof_node_updater.cpp
+++ b/src/proof/proof_node_updater.cpp
@@ -69,15 +69,25 @@ void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf)
       }
     }
   }
-  std::vector<std::shared_ptr<ProofNode>> traversing;
-  processInternal(pf, d_freeAssumps, traversing);
+  processInternal(pf, d_freeAssumps);
 }
 
-void ProofNodeUpdater::processInternal(
-    std::shared_ptr<ProofNode> pf,
-    const std::vector<Node>& fa,
-    std::vector<std::shared_ptr<ProofNode>>& traversing)
+void ProofNodeUpdater::processInternal(std::shared_ptr<ProofNode> pf,
+                                       std::vector<Node>& fa)
 {
+  // Note that processInternal uses a single scope; fa is updated based on
+  // the current free assumptions of the proof nodes on the stack.
+
+  // The list of proof nodes we are currently traversing beneath. This is used
+  // for checking for cycles in the overall proof.
+  std::vector<std::shared_ptr<ProofNode>> traversing;
+  // Map from formulas to (closed) proof nodes that prove that fact
+  std::map<Node, std::shared_ptr<ProofNode>> resCache;
+  // Map from formulas to non-closed proof nodes that prove that fact. These
+  // are replaced by proofs in the above map when applicable.
+  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> resCacheNcWaiting;
+  // Map from proof nodes to whether they contain assumptions
+  std::unordered_map<const ProofNode*, bool> cfaMap;
   Trace("pf-process") << "ProofNodeUpdater::process" << std::endl;
   std::unordered_map<std::shared_ptr<ProofNode>, bool> visited;
   std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it;
@@ -85,10 +95,6 @@ void ProofNodeUpdater::processInternal(
   std::shared_ptr<ProofNode> cur;
   visit.push_back(pf);
   std::map<Node, std::shared_ptr<ProofNode>>::iterator itc;
-  // A cache from formulas to proof nodes that are in the current scope.
-  // Notice that we make a fresh recursive call to process if the current
-  // rule is SCOPE below.
-  std::map<Node, std::shared_ptr<ProofNode>> resCache;
   Node res;
   do
   {
@@ -106,6 +112,9 @@ void ProofNodeUpdater::processInternal(
           // already have a proof, merge it into this one
           visited[cur] = true;
           d_pnm->updateNode(cur.get(), itc->second.get());
+          // does not contain free assumptions since the range of resCache does
+          // not contain free assumptions
+          cfaMap[cur.get()] = false;
           continue;
         }
       }
@@ -121,7 +130,7 @@ void ProofNodeUpdater::processInternal(
         // no further changes should be made to cur according to the callback
         Trace("pf-process-debug")
             << "...marked to not continue update." << std::endl;
-        runFinalize(cur, fa, resCache);
+        runFinalize(cur, fa, resCache, resCacheNcWaiting, cfaMap);
         continue;
       }
       traversing.push_back(cur);
@@ -131,16 +140,10 @@ void ProofNodeUpdater::processInternal(
       // allows us to properly track the assumptions in scope, which is
       // important for example to merge or to determine updates based on free
       // assumptions.
-      if (cur->getRule() == PfRule::SCOPE && cur != pf)
+      if (cur->getRule() == PfRule::SCOPE)
       {
-        std::vector<Node> nfa;
-        nfa.insert(nfa.end(), fa.begin(), fa.end());
         const std::vector<Node>& args = cur->getArguments();
-        nfa.insert(nfa.end(), args.begin(), args.end());
-        Trace("pfnu-debug2") << "Process new scope with " << args << std::endl;
-        // Process in new call separately
-        processInternal(cur, nfa, traversing);
-        continue;
+        fa.insert(fa.end(), args.begin(), args.end());
       }
       const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
       // now, process children
@@ -163,7 +166,13 @@ void ProofNodeUpdater::processInternal(
       traversing.pop_back();
       visited[cur] = true;
       // finalize the node
-      runFinalize(cur, fa, resCache);
+      if (cur->getRule() == PfRule::SCOPE)
+      {
+        const std::vector<Node>& args = cur->getArguments();
+        Assert(fa.size() >= args.size());
+        fa.resize(fa.size() - args.size());
+      }
+      runFinalize(cur, fa, resCache, resCacheNcWaiting, cfaMap);
     }
   } while (!visit.empty());
   Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl;
@@ -227,13 +236,34 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
 void ProofNodeUpdater::runFinalize(
     std::shared_ptr<ProofNode> cur,
     const std::vector<Node>& fa,
-    std::map<Node, std::shared_ptr<ProofNode>>& resCache)
+    std::map<Node, std::shared_ptr<ProofNode>>& resCache,
+    std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& resCacheNcWaiting,
+    std::unordered_map<const ProofNode*, bool>& cfaMap)
 {
   if (d_mergeSubproofs)
   {
     Node res = cur->getResult();
-    // cache result if we are merging subproofs
-    resCache[res] = cur;
+    // cache the result if we don't contain an assumption
+    if (!expr::containsAssumption(cur.get(), cfaMap))
+    {
+      // cache result if we are merging subproofs
+      resCache[res] = cur;
+      // go back and merge into the non-closed proofs of the same fact
+      std::map<Node, std::vector<std::shared_ptr<ProofNode>>>::iterator itnw =
+          resCacheNcWaiting.find(res);
+      if (itnw != resCacheNcWaiting.end())
+      {
+        for (std::shared_ptr<ProofNode>& ncp : itnw->second)
+        {
+          d_pnm->updateNode(ncp.get(), cur.get());
+        }
+        resCacheNcWaiting.erase(res);
+      }
+    }
+    else
+    {
+      resCacheNcWaiting[res].push_back(cur);
+    }
   }
   if (d_debugFreeAssumps)
   {
diff --git a/src/proof/proof_node_updater.h b/src/proof/proof_node_updater.h
index 6b8841e67..603583715 100644
--- a/src/proof/proof_node_updater.h
+++ b/src/proof/proof_node_updater.h
@@ -122,12 +122,8 @@ class ProofNodeUpdater
    * @param fa The assumptions of the scope that fa is a subproof of with
    * respect to the original proof. For example, if (SCOPE P :args (A B)), we
    * may call this method on P with fa = { A, B }.
-   * @param traversing The list of proof nodes we are currently traversing
-   * beneath. This is used for checking for cycles in the overall proof.
    */
-  void processInternal(std::shared_ptr<ProofNode> pf,
-                       const std::vector<Node>& fa,
-                       std::vector<std::shared_ptr<ProofNode>>& traversing);
+  void processInternal(std::shared_ptr<ProofNode> pf, std::vector<Node>& fa);
   /**
    * Update proof node cur based on the callback. This modifies curr using
    * ProofNodeManager::updateNode based on the proof node constructed to
@@ -141,11 +137,15 @@ class ProofNodeUpdater
   /**
    * Finalize the node cur. This is called at the moment that it is established
    * that cur will appear in the final proof. We do any final debug checking
-   * and add it to the results cache resCache if we are merging subproofs.
+   * and add it to resCache/resCacheNcWaiting if we are merging subproofs, where
+   * these map result formulas to proof nodes with/without assumptions.
    */
   void runFinalize(std::shared_ptr<ProofNode> cur,
                    const std::vector<Node>& fa,
-                   std::map<Node, std::shared_ptr<ProofNode>>& resCache);
+                   std::map<Node, std::shared_ptr<ProofNode>>& resCache,
+                   std::map<Node, std::vector<std::shared_ptr<ProofNode>>>&
+                       resCacheNcWaiting,
+                   std::unordered_map<const ProofNode*, bool>& cfaMap);
   /** Are we debugging free assumptions? */
   bool d_debugFreeAssumps;
   /** The initial free assumptions */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 87512e35b..2f807d939 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2193,6 +2193,7 @@ set(regress_1_tests
   regress1/strings/norn-simp-rew-sat.smt2
   regress1/strings/nt6-dd.smt2
   regress1/strings/nterm-re-inter-sigma.smt2
+  regress1/strings/open-pf-merge.smt2
   regress1/strings/pierre150331.smt2
   regress1/strings/policy_variable.smt2
   regress1/strings/pre_ctn_no_skolem_share.smt2
diff --git a/test/regress/regress1/strings/open-pf-merge.smt2 b/test/regress/regress1/strings/open-pf-merge.smt2
new file mode 100644
index 000000000..645ea4797
--- /dev/null
+++ b/test/regress/regress1/strings/open-pf-merge.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-const x String)
+(declare-const y String)
+(assert (not (str.prefixof "ab" x)))
+(assert (and (str.prefixof y (str.substr x 1 (str.len x))) (str.prefixof "bb" y)))
+(assert (str.prefixof "a" x))
+(check-sat)