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.

1 files changed, 8 insertions, 0 deletions

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 */