From 7ace6d43eeabb9ff2575f385ced5e2ed3c31ea2d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Jul 2021 08:33:23 -0500
Subject: [PATCH] Add print expression utility (#6880)

This will be used in the LFSC printer. It may be of general use to other proof printers.
---
 src/proof/print_expr.cpp | 58 +++++++++++++++++++++++++++
 src/proof/print_expr.h   | 86 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 144 insertions(+)
 create mode 100644 src/proof/print_expr.cpp
 create mode 100644 src/proof/print_expr.h

diff --git a/src/proof/print_expr.cpp b/src/proof/print_expr.cpp
new file mode 100644
index 000000000..becd9195a
--- /dev/null
+++ b/src/proof/print_expr.cpp
@@ -0,0 +1,58 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Utilities for printing expressions in proofs
+ */
+
+#include "proof/print_expr.h"
+
+namespace cvc5 {
+namespace proof {
+
+PExprStream::PExprStream(std::vector<PExpr>& stream, Node tt, Node ff)
+    : d_stream(stream), d_tt(tt), d_ff(ff)
+{
+}
+
+PExprStream& PExprStream::operator<<(const ProofNode* pn)
+{
+  d_stream.push_back(PExpr(pn));
+  return *this;
+}
+
+PExprStream& PExprStream::operator<<(Node n)
+{
+  d_stream.push_back(PExpr(n));
+  return *this;
+}
+
+PExprStream& PExprStream::operator<<(TypeNode tn)
+{
+  d_stream.push_back(PExpr(tn));
+  return *this;
+}
+
+PExprStream& PExprStream::operator<<(bool b)
+{
+  Assert(!d_tt.isNull() && !d_ff.isNull());
+  d_stream.push_back(b ? d_tt : d_ff);
+  return *this;
+}
+
+PExprStream& PExprStream::operator<<(PExpr p)
+{
+  d_stream.push_back(p);
+  return *this;
+}
+
+}  // namespace proof
+}  // namespace cvc5
diff --git a/src/proof/print_expr.h b/src/proof/print_expr.h
new file mode 100644
index 000000000..15a8bb6c2
--- /dev/null
+++ b/src/proof/print_expr.h
@@ -0,0 +1,86 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Utilities for printing expressions in proofs
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__PRINT_EXPR_H
+#define CVC5__PROOF__PRINT_EXPR_H
+
+#include <iostream>
+#include <map>
+
+#include "expr/node.h"
+#include "proof/proof_node.h"
+
+namespace cvc5 {
+namespace proof {
+
+/** 
+ * A term, type or a proof. This class is used for printing combinations of
+ * proofs terms and types.
+ */
+class PExpr
+{
+ public:
+  PExpr() : d_node(), d_pnode(nullptr), d_typeNode() {}
+  PExpr(Node n) : d_node(n), d_pnode(nullptr), d_typeNode() {}
+  PExpr(const ProofNode* pn) : d_node(), d_pnode(pn), d_typeNode() {}
+  PExpr(TypeNode tn) : d_node(), d_pnode(nullptr), d_typeNode(tn) {}
+  ~PExpr() {}
+  /** The node, if this p-exression is a node */
+  Node d_node;
+  /** The proof node, if this p-expression is a proof */
+  const ProofNode* d_pnode;
+  /** The type node, if this p-expression is a type */
+  TypeNode d_typeNode;
+};
+
+/**
+ * A stream of p-expressions, which appends p-expressions to a reference vector.
+ * That vector can then be used when printing a proof.
+ */
+class PExprStream
+{
+ public:
+   /** 
+    * Takes a reference to a stream (vector of p-expressions), and the
+    * representation true/false (tt/ff).
+    */
+  PExprStream(std::vector<PExpr>& stream,
+              Node tt = Node::null(),
+              Node ff = Node::null());
+  /** Append a proof node */
+  PExprStream& operator<<(const ProofNode* pn);
+  /** Append a node */
+  PExprStream& operator<<(Node n);
+  /** Append a type node */
+  PExprStream& operator<<(TypeNode tn);
+  /** Append a Boolean */
+  PExprStream& operator<<(bool b);
+  /** Append a pexpr */
+  PExprStream& operator<<(PExpr p);
+
+ private:
+  /** Reference to the stream */
+  std::vector<PExpr>& d_stream;
+  /** Builtin nodes for true and false */
+  Node d_tt;
+  Node d_ff;
+};
+
+}  // namespace proof
+}  // namespace cvc5
+
+#endif
-- 
2.30.2