Merging proof branch

1 files changed, 7 insertions, 0 deletions

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index c74aac237..c6454b652 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -34,6 +34,8 @@
 
 namespace CVC4 {
 
+class SmtGlobals;
+
 // forward declarations
 namespace Minisat {
   class Solver;
@@ -136,6 +138,8 @@ class ProofManager {
 
   std::set<Type> d_printedTypes;
 
+  std::map<std::string, std::string> d_rewriteFilters;
+
 protected:
   LogicInfo d_logic;
 
@@ -224,6 +228,9 @@ public:
   void markPrinted(const Type& type);
   bool wasPrinted(const Type& type) const;
 
+  void addRewriteFilter(const std::string &original, const std::string &substitute);
+  void clearRewriteFilters();
+
 };/* class ProofManager */
 
 class LFSCProof : public Proof {