1 files changed, 86 insertions, 0 deletions
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