Add Lfsc print channel utilities (#7123)

These are utilities used for two-pass printing of LFSC proofs.

3 files changed, 291 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5c898b654..4484f9447 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -182,6 +182,8 @@ libcvc5_add_sources(
   proof/lfsc/lfsc_list_sc_node_converter.h
   proof/lfsc/lfsc_node_converter.cpp
   proof/lfsc/lfsc_node_converter.h
+  proof/lfsc/lfsc_print_channel.cpp
+  proof/lfsc/lfsc_print_channel.h
   proof/lfsc/lfsc_util.cpp
   proof/lfsc/lfsc_util.h
   proof/method_id.cpp
diff --git a/src/proof/lfsc/lfsc_print_channel.cpp b/src/proof/lfsc/lfsc_print_channel.cpp
new file mode 100644
index 000000000..36fd8831b
--- /dev/null
+++ b/src/proof/lfsc/lfsc_print_channel.cpp
@@ -0,0 +1,161 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Print channels for LFSC proofs.
+ */
+
+#include "proof/lfsc/lfsc_print_channel.h"
+
+#include <sstream>
+
+#include "proof/lfsc/lfsc_util.h"
+
+namespace cvc5 {
+namespace proof {
+
+LfscPrintChannelOut::LfscPrintChannelOut(std::ostream& out) : d_out(out) {}
+void LfscPrintChannelOut::printNode(TNode n)
+{
+  d_out << " ";
+  printNodeInternal(d_out, n);
+}
+
+void LfscPrintChannelOut::printTypeNode(TypeNode tn)
+{
+  d_out << " ";
+  printTypeNodeInternal(d_out, tn);
+}
+
+void LfscPrintChannelOut::printHole() { d_out << " _ "; }
+void LfscPrintChannelOut::printTrust(TNode res, PfRule src)
+{
+  d_out << std::endl << "(trust ";
+  printNodeInternal(d_out, res);
+  d_out << ") ; from " << src << std::endl;
+}
+
+void LfscPrintChannelOut::printOpenRule(const ProofNode* pn)
+{
+  d_out << std::endl << "(";
+  printRule(d_out, pn);
+}
+
+void LfscPrintChannelOut::printOpenLfscRule(LfscRule lr)
+{
+  d_out << std::endl << "(" << lr;
+}
+
+void LfscPrintChannelOut::printCloseRule(size_t nparen)
+{
+  for (size_t i = 0; i < nparen; i++)
+  {
+    d_out << ")";
+  }
+}
+
+void LfscPrintChannelOut::printProofId(size_t id)
+{
+  d_out << " ";
+  printProofId(d_out, id);
+}
+void LfscPrintChannelOut::printAssumeId(size_t id)
+{
+  d_out << " ";
+  printAssumeId(d_out, id);
+}
+
+void LfscPrintChannelOut::printEndLine() { d_out << std::endl; }
+
+void LfscPrintChannelOut::printNodeInternal(std::ostream& out, Node n)
+{
+  // due to use of special names in the node converter, we must clean symbols
+  std::stringstream ss;
+  n.toStream(ss, -1, 0, Language::LANG_SMTLIB_V2_6);
+  std::string s = ss.str();
+  cleanSymbols(s);
+  out << s;
+}
+
+void LfscPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn)
+{
+  // due to use of special names in the node converter, we must clean symbols
+  std::stringstream ss;
+  tn.toStream(ss, Language::LANG_SMTLIB_V2_6);
+  std::string s = ss.str();
+  cleanSymbols(s);
+  out << s;
+}
+
+void LfscPrintChannelOut::printRule(std::ostream& out, const ProofNode* pn)
+{
+  if (pn->getRule() == PfRule::LFSC_RULE)
+  {
+    const std::vector<Node>& args = pn->getArguments();
+    out << getLfscRule(args[0]);
+    return;
+  }
+  // Otherwise, convert to lower case
+  std::stringstream ss;
+  ss << pn->getRule();
+  std::string rname = ss.str();
+  std::transform(
+      rname.begin(), rname.end(), rname.begin(), [](unsigned char c) {
+        return std::tolower(c);
+      });
+  out << rname;
+}
+
+void LfscPrintChannelOut::printId(std::ostream& out, size_t id)
+{
+  out << "__t" << id;
+}
+
+void LfscPrintChannelOut::printProofId(std::ostream& out, size_t id)
+{
+  out << "__p" << id;
+}
+
+void LfscPrintChannelOut::printAssumeId(std::ostream& out, size_t id)
+{
+  out << "__a" << id;
+}
+
+void LfscPrintChannelOut::cleanSymbols(std::string& s)
+{
+  size_t start_pos = 0;
+  while ((start_pos = s.find("(_ ", start_pos)) != std::string::npos)
+  {
+    s.replace(start_pos, 3, "(");
+    start_pos += 1;
+  }
+  start_pos = 0;
+  while ((start_pos = s.find("__LFSC_TMP", start_pos)) != std::string::npos)
+  {
+    s.replace(start_pos, 10, "");
+  }
+}
+
+LfscPrintChannelPre::LfscPrintChannelPre(LetBinding& lbind) : d_lbind(lbind) {}
+
+void LfscPrintChannelPre::printNode(TNode n) { d_lbind.process(n); }
+void LfscPrintChannelPre::printTrust(TNode res, PfRule src)
+{
+  d_lbind.process(res);
+}
+
+void LfscPrintChannelPre::printOpenRule(const ProofNode* pn)
+{
+
+}
+
+}  // namespace proof
+}  // namespace cvc5
diff --git a/src/proof/lfsc/lfsc_print_channel.h b/src/proof/lfsc/lfsc_print_channel.h
new file mode 100644
index 000000000..655fa192c
--- /dev/null
+++ b/src/proof/lfsc/lfsc_print_channel.h
@@ -0,0 +1,128 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Print channels for LFSC proofs.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H
+#define CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H
+
+#include <iostream>
+#include <map>
+
+#include "expr/node.h"
+#include "printer/let_binding.h"
+#include "proof/lfsc/lfsc_util.h"
+#include "proof/proof_node.h"
+
+namespace cvc5 {
+namespace proof {
+
+/**
+ * LFSC proofs are printed in two phases: the first phase computes the
+ * letification of terms in the proof as well as other information that is
+ * required for printing the preamble of the proof. The second phase prints the
+ * proof to an output stream. This is the base class for these two phases.
+ */
+class LfscPrintChannel
+{
+ public:
+  LfscPrintChannel() {}
+  virtual ~LfscPrintChannel() {}
+  /** Print node n */
+  virtual void printNode(TNode n) {}
+  /** Print type node n */
+  virtual void printTypeNode(TypeNode tn) {}
+  /** Print a hole */
+  virtual void printHole() {}
+  /**
+   * Print an application of the trusting the result res, whose source is the
+   * given proof rule.
+   */
+  virtual void printTrust(TNode res, PfRule src) {}
+  /** Print the opening of the rule of proof rule pn, e.g. "(and_elim ". */
+  virtual void printOpenRule(const ProofNode* pn) {}
+  /** Print the opening of LFSC rule lr, e.g. "(cong " */
+  virtual void printOpenLfscRule(LfscRule lr) {}
+  /** Print the closing of # nparen proof rules */
+  virtual void printCloseRule(size_t nparen = 1) {}
+  /** Print a letified proof with the given identifier */
+  virtual void printProofId(size_t id) {}
+  /** Print a proof assumption with the given identifier */
+  virtual void printAssumeId(size_t id) {}
+  /** Print an end line */
+  virtual void printEndLine() {}
+};
+
+/** Prints the proof to output stream d_out */
+class LfscPrintChannelOut : public LfscPrintChannel
+{
+ public:
+  LfscPrintChannelOut(std::ostream& out);
+  void printNode(TNode n) override;
+  void printTypeNode(TypeNode tn) override;
+  void printHole() override;
+  void printTrust(TNode res, PfRule src) override;
+  void printOpenRule(const ProofNode* pn) override;
+  void printOpenLfscRule(LfscRule lr) override;
+  void printCloseRule(size_t nparen = 1) override;
+  void printProofId(size_t id) override;
+  void printAssumeId(size_t id) override;
+  void printEndLine() override;
+  //------------------- helper methods
+  /**
+   * Print node to stream in the expected format of LFSC.
+   */
+  static void printNodeInternal(std::ostream& out, Node n);
+  /**
+   * Print type node to stream in the expected format of LFSC.
+   */
+  static void printTypeNodeInternal(std::ostream& out, TypeNode tn);
+  static void printRule(std::ostream& out, const ProofNode* pn);
+  static void printId(std::ostream& out, size_t id);
+  static void printProofId(std::ostream& out, size_t id);
+  static void printAssumeId(std::ostream& out, size_t id);
+  //------------------- end helper methods
+ private:
+  /**
+   * Replaces "(_ " with "(" to eliminate indexed symbols
+   * Replaces "__LFSC_TMP" with ""
+   */
+  static void cleanSymbols(std::string& s);
+  /** The output stream */
+  std::ostream& d_out;
+};
+
+/**
+ * Run on the proof before it is printed, and does two preparation steps:
+ * - Computes the letification of nodes that appear in the proof.
+ * - Computes the set of DSL rules that appear in the proof.
+ */
+class LfscPrintChannelPre : public LfscPrintChannel
+{
+ public:
+  LfscPrintChannelPre(LetBinding& lbind);
+  void printNode(TNode n) override;
+  void printTrust(TNode res, PfRule src) override;
+  void printOpenRule(const ProofNode* pn) override;
+
+ private:
+  /** The let binding */
+  LetBinding& d_lbind;
+};
+
+}  // namespace proof
+}  // namespace cvc5
+
+#endif