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, 9 insertions, 0 deletions

diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 62036ced0..788526b80 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -141,6 +141,10 @@ public:
   virtual void printAtomMapping(const std::set<Node>& atoms,
                                 std::ostream& os,
                                 std::ostream& paren) = 0;
+  virtual void printAtomMapping(const std::set<Node>& atoms,
+                           std::ostream& os,
+                           std::ostream& paren,
+                           ProofLetMap &letMap) = 0;
 
   virtual void printClause(const prop::SatClause& clause,
                            std::ostream& os,
@@ -169,6 +173,11 @@ public:
                         std::ostream& os,
                         std::ostream& paren);
 
+  void printAtomMapping(const std::set<Node>& atoms,
+                        std::ostream& os,
+                        std::ostream& paren,
+                        ProofLetMap &letMap);
+
   void printClause(const prop::SatClause& clause,
                    std::ostream& os,
                    std::ostream& paren);