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, 40 insertions, 1 deletions

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index c6454b652..14793f380 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -22,6 +22,7 @@
 #include <iosfwd>
 #include <map>
 #include "proof/proof.h"
+#include "proof/proof_utils.h"
 #include "proof/skolemization_manager.h"
 #include "util/proof.h"
 #include "expr/node.h"
@@ -115,6 +116,30 @@ enum ProofRule {
   RULE_ARRAYS_ROW,  /* arrays, read-over-write */
 };/* enum ProofRules */
 
+class RewriteLogEntry {
+public:
+  RewriteLogEntry(unsigned ruleId, Node original, Node result)
+    : d_ruleId(ruleId), d_original(original), d_result(result) {
+  }
+
+  unsigned getRuleId() const {
+    return d_ruleId;
+  }
+
+  Node getOriginal() const {
+    return d_original;
+  }
+
+  Node getResult() const {
+    return d_result;
+  }
+
+private:
+  unsigned d_ruleId;
+  Node d_original;
+  Node d_result;
+};
+
 class ProofManager {
   CoreSatProof*  d_satProof;
   CnfProof*      d_cnfProof;
@@ -140,6 +165,8 @@ class ProofManager {
 
   std::map<std::string, std::string> d_rewriteFilters;
 
+  std::vector<RewriteLogEntry> d_rewriteLog;
+
 protected:
   LogicInfo d_logic;
 
@@ -231,6 +258,16 @@ public:
   void addRewriteFilter(const std::string &original, const std::string &substitute);
   void clearRewriteFilters();
 
+  static void registerRewrite(unsigned ruleId, Node original, Node result);
+  static void clearRewriteLog();
+
+  std::vector<RewriteLogEntry> getRewriteLog();
+  void dumpRewriteLog() const;
+
+  void printGlobalLetMap(std::set<Node>& atoms,
+                         ProofLetMap& letMap,
+                         std::ostream& out,
+                         std::ostringstream& paren);
 };/* class ProofManager */
 
 class LFSCProof : public Proof {
@@ -242,13 +279,15 @@ class LFSCProof : public Proof {
   // FIXME: hack until we get preprocessing
   void printPreprocessedAssertions(const NodeSet& assertions,
                                    std::ostream& os,
-                                   std::ostream& paren);
+                                   std::ostream& paren,
+                                   ProofLetMap& globalLetMap);
 public:
   LFSCProof(SmtEngine* smtEngine,
             LFSCCoreSatProof* sat,
             LFSCCnfProof* cnf,
             LFSCTheoryProofEngine* theory);
   virtual void toStream(std::ostream& out);
+  virtual void toStream(std::ostream& out, const ProofLetMap& map);
   virtual ~LFSCProof() {}
 };/* class LFSCProof */