[proofs] Alethe: Implementation of Printer (#7674)

Adds an implementation file of the Alethe printer with function stubs to be filled in in further PRs.

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

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 224af6a092d37195516c2d39a526f39a112cf77f..025f499e6952f8bc69ae3b1cd93ee18b73f87f25 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -224,6 +224,7 @@ libcvc5_add_sources(
   proof/alethe/alethe_post_processor.cpp
   proof/alethe/alethe_post_processor.h
   proof/alethe/alethe_printer.h
+  proof/alethe/alethe_printer.cpp
   proof/alethe/alethe_proof_rule.cpp
   proof/alethe/alethe_proof_rule.h
   prop/cadical.cpp

diff --git a/src/proof/alethe/alethe_printer.cpp b/src/proof/alethe/alethe_printer.cpp
new file mode 100644 (file)
index 0000000..49b2716
--- /dev/null
+++ b/src/proof/alethe/alethe_printer.cpp
@@ -0,0 +1,62 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Hanna Lachnitt
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The module for printing Alethe proof nodes.
+ */
+
+#include "proof/alethe/alethe_printer.h"
+
+#include <iostream>
+#include <unordered_map>
+
+#include "proof/alethe/alethe_proof_rule.h"
+
+namespace cvc5 {
+
+namespace proof {
+
+AletheProofPrinter::AletheProofPrinter() {}
+
+void AletheProofPrinter::print(std::ostream& out,
+                               std::shared_ptr<ProofNode> pfn)
+{
+  Trace("alethe-printer") << "- Print proof in Alethe format. " << std::endl;
+  std::unordered_map<Node, std::string> assumptions;
+  const std::vector<Node>& args = pfn->getArguments();
+  // Special handling for the first scope
+  // Print assumptions and add them to the list but do not print anchor.
+  for (size_t i = 3, size = args.size(); i < size; i++)
+  {
+    Trace("alethe-printer") << "... print assumption " << args[i] << std::endl;
+    out << "(assume a" << i - 3 << " " << args[i] << ")\n";
+    assumptions[args[i]] = "a" + std::to_string(i - 3);
+  }
+
+  // Then, print the rest of the proof node
+  uint32_t start_t = 1;
+  printInternal(out, pfn->getChildren()[0], assumptions, {}, "", 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::string current_prefix,
+    uint32_t& current_step_id)
+{
+  return "";
+}
+
+}  // namespace proof
+
+}  // namespace cvc5