[proofs] Alethe: Removed Steps that are Double-Printed (#7754)

This PR fixes that some steps are printed more than once. To this end, it deletes that the reference maps in which the steps are stored are constant and optimizes where the steps are added to the maps. It also stores ProofNodes instead of Nodes in the maps.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

diff --git a/src/proof/alethe/alethe_printer.cpp b/src/proof/alethe/alethe_printer.cpp
index cb4696af9e5aa88fcf358ab3e9faf0669af35491..2fd898bfdecfeb0364de7a3dc5f893b8de0b8d36 100644 (file)
--- a/src/proof/alethe/alethe_printer.cpp
+++ b/src/proof/alethe/alethe_printer.cpp
@@ -43,22 +43,20 @@ void AletheProofPrinter::print(std::ostream& out,
 
   // Then, print the rest of the proof node
   uint32_t start_t = 1;
-  printInternal(out, pfn->getChildren()[0], assumptions, {}, "", start_t);
+  std::unordered_map<std::shared_ptr<ProofNode>, std::string> steps = {};
+  printInternal(out, pfn->getChildren()[0], assumptions, steps, "", start_t);
 }
 
 std::string AletheProofPrinter::printInternal(
     std::ostream& out,
     std::shared_ptr<ProofNode> pfn,
-    const std::unordered_map<Node, std::string>& assumptions,
-    const std::unordered_map<Node, std::string>& steps,
+    std::unordered_map<Node, std::string>& assumptions,
+    std::unordered_map<std::shared_ptr<ProofNode>, std::string>& steps,
     std::string current_prefix,
     uint32_t& current_step_id)
 {
   int step_id = current_step_id;
-  std::vector<std::string> current_assumptions;
   const std::vector<Node>& args = pfn->getArguments();
-  std::unordered_map<Node, std::string> new_assumptions = assumptions;
-  std::unordered_map<Node, std::string> new_steps = steps;
 
   // If the proof node is untranslated a problem might have occured during
   // postprocessing
@@ -74,20 +72,43 @@ std::string AletheProofPrinter::printInternal(
   // Get the alethe proof rule
   AletheRule arule = getAletheRule(args[0]);
 
+  // Assumptions are printed at the anchor and therefore have to be in the list
+  // of assumptions when an assume is reached.
+  if (arule == AletheRule::ASSUME)
+  {
+    Trace("alethe-printer")
+        << "... reached assumption " << pfn->getResult() << " " << arule << " "
+        << " / " << args << " " << std::endl;
+
+    auto it = assumptions.find(args[2]);
+    Assert(it != assumptions.end())
+        << "Assumption has not been printed yet! " << args[2] << "/"
+        << assumptions << std::endl;
+    Trace("alethe-printer")
+        << "... found assumption in list " << it->second << ": " << args[2]
+        << "/" << assumptions << std::endl;
+    return it->second;
+  }
+
+  // If the current step is already printed return its id
+  auto it = steps.find(pfn);
+  if (it != steps.end())
+  {
+    Trace("alethe-printer")
+        << "... step is already printed " << it->second << " "
+        << pfn->getResult() << " " << arule << " / " << args << std::endl;
+    return it->second;
+  }
+  std::vector<std::string> current_assumptions;
+  std::unordered_map<Node, std::string> assumptions_before_subproof =
+      assumptions;
+  std::unordered_map<std::shared_ptr<ProofNode>, std::string>
+      steps_before_subproof = steps;
+
   // In case the rule is an anchor it is printed before its children.
   if (arule == AletheRule::ANCHOR_SUBPROOF || arule == AletheRule::ANCHOR_BIND)
   {
-    // Look up if subproof has already been printed
-    auto it = steps.find(args[2]);
-    if (it != steps.end())
-    {
-      Trace("alethe-printer")
-          << "... subproof is already printed " << pfn->getResult() << " "
-          << arule << " / " << args << std::endl;
-      return it->second;
-    }
-
-    // Otherwise, print anchor
+    // Print anchor
     std::string current_t =
         current_prefix + "t" + std::to_string(current_step_id);
     Trace("alethe-printer")
@@ -129,48 +150,19 @@ std::string AletheProofPrinter::printInternal(
         Trace("alethe-printer")
             << "... print assumption " << args[i] << std::endl;
         out << "(assume " << assumption_name << " " << args[i] << ")\n";
-        new_assumptions[args[i]] = assumption_name;
+        assumptions[args[i]] = assumption_name;
         current_assumptions.push_back(assumption_name);
       }
     }
   }
 
-  // Assumptions are printed at the anchor and therefore have to be in the list
-  // of assumptions when an assume is reached.
-  else if (arule == AletheRule::ASSUME)
-  {
-    Trace("alethe-printer")
-        << "... reached assumption " << pfn->getResult() << " " << arule << " "
-        << " / " << args << " " << std::endl;
-
-    auto it = assumptions.find(args[2]);
-    if (it != assumptions.end())
-    {
-      Trace("alethe-printer") << "... found assumption in list "
-                              << ": " << args[2] << "/" << assumptions
-                              << "     " << it->second << std::endl;
-      return it->second;
-    }
-
-    Trace("alethe-printer") << "... printing failed! Encountered assumption "
-                               "that has not been printed! "
-                            << args[2] << "/" << assumptions << std::endl;
-    return "";
-  }
-
   // Print children
   std::vector<std::string> child_prefixes;
-
   const std::vector<std::shared_ptr<ProofNode>>& children = pfn->getChildren();
   for (const std::shared_ptr<ProofNode>& child : children)
   {
-    std::string child_prefix = printInternal(out,
-                                             child,
-                                             new_assumptions,
-                                             new_steps,
-                                             current_prefix,
-                                             current_step_id);
-    new_steps[args[2]] = child_prefix;
+    std::string child_prefix = printInternal(
+        out, child, assumptions, steps, current_prefix, current_step_id);
     child_prefixes.push_back(child_prefix);
   }
 
@@ -183,7 +175,15 @@ std::string AletheProofPrinter::printInternal(
     current_prefix.pop_back();
     out << "(step " << current_prefix << " " << args[2] << " :rule " << arule;
 
-    new_steps[args[2]] = current_prefix;
+    // Reset steps array to the steps before the subproof since steps inside the
+    // subproof cannot be accessed anymore
+    steps = steps_before_subproof;
+    assumptions = assumptions_before_subproof;
+
+    // Add to map of printed steps
+    steps[pfn] = current_prefix;
+    Trace("alethe-printer") << "... add to steps " << pfn->getArguments()[2]
+                            << " " << current_prefix << std::endl;
 
     // Reset step id to the number before the subproof + 1
     current_step_id = step_id + 1;
@@ -204,23 +204,21 @@ std::string AletheProofPrinter::printInternal(
     return current_prefix;
   }
 
-  // If the current step is already printed return its id
-  auto it = new_steps.find(args[2]);
-  if (it != new_steps.end())
-  {
-    Trace("alethe-printer")
-        << "... step is already printed " << pfn->getResult() << " " << arule
-        << " / " << args << std::endl;
-    return it->second;
-  }
-
+  // Otherwise, the step is a normal step
   // Print current step
-  Trace("alethe-printer") << "... print node " << pfn->getResult() << " "
-                          << arule << " / " << args << std::endl;
   std::string current_t =
       current_prefix + "t" + std::to_string(current_step_id);
-  out << "(step " << current_t << " " << args[2] << " :rule " << arule;
+  Trace("alethe-printer") << "... print node " << current_t << " "
+                          << pfn->getResult() << " " << arule << " / " << args
+                          << std::endl;
+
+  // Add to map of printed steps
+  steps[pfn] = current_t;
+  Trace("alethe-printer") << "... add to steps " << pfn->getArguments()[2]
+                          << " " << current_t << std::endl;
   current_step_id++;
+
+  out << "(step " << current_t << " " << args[2] << " :rule " << arule;
   if (args.size() > 3)
   {
     out << " :args (";

diff --git a/src/proof/alethe/alethe_printer.h b/src/proof/alethe/alethe_printer.h
index 22fcb64990bbe58ebd4aef320caded1f6b331405..f96c5f7d96a0a48f78d426c191c8ba4421ebe06b 100644 (file)
--- a/src/proof/alethe/alethe_printer.h
+++ b/src/proof/alethe/alethe_printer.h
@@ -69,8 +69,8 @@ class AletheProofPrinter
   std::string printInternal(
       std::ostream& out,
       std::shared_ptr<ProofNode> pfn,
-      const std::unordered_map<Node, std::string>& assumptions,
-      const std::unordered_map<Node, std::string>& steps,
+      std::unordered_map<Node, std::string>& assumptions,
+      std::unordered_map<std::shared_ptr<ProofNode>, std::string>& steps,
       std::string current_prefix,
       uint32_t& current_step_id);
 };