From 4b8f92d23f7a75b4148f41e039f7bdc5f165babc Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Wed, 8 Jun 2016 11:52:42 -0700
Subject: Support for printing a global let map in LFSC proofs. Added a flag to
 enable/disbale this feature (enabled by default).

Also, added some infrastructure for proving rewrite rules.
---
 src/util/proof.h | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/util/proof.h')

diff --git a/src/util/proof.h b/src/util/proof.h
index fc5f7f901..b4a8a3d29 100644
--- a/src/util/proof.h
+++ b/src/util/proof.h
@@ -21,13 +21,21 @@
 #define __CVC4__PROOF_H
 
 #include <iosfwd>
+#include <ext/hash_map>
 
 namespace CVC4 {
 
+class Expr;
+class ProofLetCount;
+struct ExprHashFunction;
+
+typedef __gnu_cxx::hash_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap;
+
 class CVC4_PUBLIC Proof {
 public:
   virtual ~Proof() { }
   virtual void toStream(std::ostream& out) = 0;
+  virtual void toStream(std::ostream& out, const ProofLetMap& map) = 0;
 };/* class Proof */
 
 }/* CVC4 namespace */
-- 
cgit v1.2.3