Simplify and fix computation of free assumptions (cvc5#10660)

The previous version cached visited independent of context, which would lead to a proof node being skipped in a "free" context when it had already been visited in a bound context.

This led to incorrect unsat cores in a development branch for one regression.

src/proof/proof_node_algorithm.cpp

@@ -39,30 +39,9 @@ void getFreeAssumptionsMap(
     std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
 {
   // proof should not be cyclic
-  // visited set false after preorder traversal, true after postorder traversal
-  std::unordered_map<ProofNode*, bool> visited;
-  std::unordered_map<ProofNode*, bool>::iterator it;
+  std::unordered_set<ProofNode*> visited;
+  std::unordered_set<ProofNode*>::iterator it;
   std::vector<std::shared_ptr<ProofNode>> visit;
-  std::vector<std::shared_ptr<ProofNode>> traversing;
-  // Maps a bound assumption to the number of bindings it is under
-  // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at
-  // (ASSUME x), and x would be mapped to 1.
-  //
-  // This map is used to track which nodes are in scope while traversing the
-  // DAG. The in-scope assumptions are keys in the map. They're removed when
-  // their binding count drops to zero. Let's annotate the above example to
-  // serve as an illustration:
-  //
-  //   (SCOPE0 (SCOPE1 (ASSUME x) (x y)) (y))
-  //
-  // This is how the map changes during the traversal:
-  //   after  previsiting SCOPE0: { y: 1 }
-  //   after  previsiting SCOPE1: { y: 2, x: 1 }
-  //   at                 ASSUME: { y: 2, x: 1 } (so x is in scope!)
-  //   after postvisiting SCOPE1: { y: 1 }
-  //   after postvisiting SCOPE2: {}
-  //
-  std::unordered_map<Node, uint32_t> scopeDepth;
   std::shared_ptr<ProofNode> cur;
   visit.push_back(pn);
   do
@@ -73,65 +52,36 @@ void getFreeAssumptionsMap(
     const std::vector<Node>& cargs = cur->getArguments();
     if (it == visited.end())
     {
+      visited.insert(cur.get());
       ProofRule id = cur->getRule();
       if (id == ProofRule::ASSUME)
       {
-        visited[cur.get()] = true;
         Assert(cargs.size() == 1);
         Node f = cargs[0];
-        if (!scopeDepth.count(f))
-        {
-          amap[f].push_back(cur);
-        }
+        amap[f].push_back(cur);
       }
       else
       {
-        if (id == ProofRule::SCOPE)
-        {
-          // mark that its arguments are bound in the current scope
-          for (const Node& a : cargs)
-          {
-            scopeDepth[a] += 1;
-          }
-          // will need to unbind the variables below
-        }
-        // The following loop cannot be merged with the loop above because the
-        // same subproof
-        visited[cur.get()] = false;
-        visit.push_back(cur);
-        traversing.push_back(cur);
         const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
-        for (const std::shared_ptr<ProofNode>& cp : cs)
-        {
-          if (std::find(traversing.begin(), traversing.end(), cp)
-              != traversing.end())
-          {
-            Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use "
-                           "--proof-check=eager)"
-                        << std::endl;
-          }
-          visit.push_back(cp);
-        }
-      }
-    }
-    else if (!it->second)
-    {
-      Assert(!traversing.empty());
-      traversing.pop_back();
-      visited[cur.get()] = true;
-      if (cur->getRule() == ProofRule::SCOPE)
-      {
-        // unbind its assumptions
-        for (const Node& a : cargs)
+        if (id == ProofRule::SCOPE)
         {
-          auto scopeCt = scopeDepth.find(a);
-          Assert(scopeCt != scopeDepth.end());
-          scopeCt->second -= 1;
-          if (scopeCt->second == 0)
+          // make a recursive call, which is bound in depth by the number of
+          // nested SCOPE (never expected to be more than 1 or 2).
+          std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amapTmp;
+          expr::getFreeAssumptionsMap(cs[0], amapTmp);
+          for (std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
+                   a : amapTmp)
           {
-            scopeDepth.erase(scopeCt);
+            if (std::find(cargs.begin(), cargs.end(), a.first) == cargs.end())
+            {
+              std::vector<std::shared_ptr<ProofNode>>& pfs = amap[a.first];
+              pfs.insert(pfs.end(), a.second.begin(), a.second.end());
+            }
           }
+          continue;
         }
+        // traverse on children
+        visit.insert(visit.end(), cs.begin(), cs.end());
       }
     }
   } while (!visit.empty());

src/prop/prop_engine.cpp

@@ -764,7 +764,9 @@ void PropEngine::getUnsatCore(std::vector<Node>& core)
     // need to connect the SAT proof to the CNF proof becuase we need the
     // preprocessed input as leaves, not the clauses derived from them.
     std::shared_ptr<ProofNode> pfn = getProof();
+    Trace("unsat-core") << "Proof is " << *pfn.get() << std::endl;
     expr::getFreeAssumptions(pfn.get(), core);
+    Trace("unsat-core") << "Core is " << core << std::endl;
   }
 }