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, 26 insertions, 63 deletions

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 352cc1b53..f6f00fa11 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -35,57 +35,8 @@ namespace theory {
 class Theory;
 } /* namespace CVC4::theory */
 
-struct LetCount {
-  static unsigned counter;
-  static void resetCounter() { counter = 0; }
-  static unsigned newId() { return ++counter; }
-
-  unsigned count;
-  unsigned id;
-  LetCount()
-    : count(0)
-    , id(-1)
-  {}
-
-  void increment() { ++count; }
-  LetCount(unsigned i)
-    : count(1)
-    , id(i)
-  {}
-  LetCount(const LetCount& other)
-    : count(other.count)
-    , id (other.id)
-  {}
-  bool operator==(const LetCount &other) const {
-    return other.id == id && other.count == count;
-  }
-  LetCount& operator=(const LetCount &rhs) {
-    if (&rhs == this) return *this;
-    id = rhs.id;
-    count = rhs.count;
-    return *this;
-  }
-};
-
-struct LetOrderElement {
-  Expr expr;
-  unsigned id;
-  LetOrderElement(Expr e, unsigned i)
-    : expr(e)
-    , id(i)
-  {}
-
-  LetOrderElement()
-    : expr()
-    , id(-1)
-  {}
-};
-
 typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
 
-typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap;
-typedef std::vector<LetOrderElement> Bindings;
-
 class TheoryProof;
 
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
@@ -118,7 +69,7 @@ public:
    */
   virtual void printLetTerm(Expr term, std::ostream& os) = 0;
   virtual void printBoundTerm(Expr term, std::ostream& os,
-                              const LetMap& map) = 0;
+                              const ProofLetMap& map) = 0;
 
   /**
    * Print the proof representation of the given sort.
@@ -168,7 +119,7 @@ public:
    * @param paren
    */
   virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os,
-                                 std::ostream& paren) = 0;
+                                 std::ostream& paren, ProofLetMap& map) = 0;
 
   /**
    * Register theory atom (ensures all terms and atoms are declared).
@@ -192,40 +143,43 @@ public:
   void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
 
   virtual void treatBoolsAsFormulas(bool value) {};
+
+  virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
 };
 
 class LFSCTheoryProofEngine : public TheoryProofEngine {
-  LetMap d_letMap;
-  void printTheoryTerm(Expr term, std::ostream& os, const LetMap& map);
-  void bind(Expr term, LetMap& map, Bindings& let_order);
+  void bind(Expr term, ProofLetMap& map, Bindings& let_order);
 public:
   LFSCTheoryProofEngine()
     : TheoryProofEngine() {}
 
+  void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map);
+
   void registerTermsFromAssertions();
   void printSortDeclarations(std::ostream& os, std::ostream& paren);
   void printTermDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printCoreTerm(Expr term, std::ostream& os, const LetMap& map);
+  virtual void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printLetTerm(Expr term, std::ostream& os);
-  virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map);
+  virtual void printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printAssertions(std::ostream& os, std::ostream& paren);
   virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTheoryLemmas(const IdToSatClause& lemmas,
                                  std::ostream& os,
-                                 std::ostream& paren);
+                                 std::ostream& paren,
+                                 ProofLetMap& map);
   virtual void printSort(Type type, std::ostream& os);
 
   void performExtraRegistrations();
 
   void treatBoolsAsFormulas(bool value);
+  void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os);
 
 private:
   static void dumpTheoryLemmas(const IdToSatClause& lemmas);
 
   // TODO: this function should be moved into the BV prover.
-  void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren);
 
   std::map<Node, std::string> d_assertionToRewrite;
 };
@@ -247,7 +201,7 @@ public:
    * @param term expresion representing term
    * @param os output stream
    */
-  void printTerm(Expr term, std::ostream& os, const LetMap& map) {
+  void printTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
     d_proofEngine->printBoundTerm(term, os, map);
   }
   /**
@@ -256,7 +210,7 @@ public:
    * @param term expresion representing term
    * @param os output stream
    */
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
+  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
   /**
    * Print the proof representation of the given type that belongs to some theory.
    *
@@ -279,7 +233,10 @@ public:
    *
    * @param os output stream
    */
-  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma,
+                                     std::ostream& os,
+                                     std::ostream& paren,
+                                     const ProofLetMap& map);
   /**
    * Print the sorts declarations for this theory.
    *
@@ -321,6 +278,12 @@ public:
    * @param term
    */
   virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+  /**
+   * Print a proof for the equivalence of n1 and n2.
+   *
+   * @param term
+   */
+  virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
 
   virtual void treatBoolsAsFormulas(bool value) {}
 };
@@ -333,7 +296,7 @@ public:
 
   virtual void registerTerm(Expr term);
 
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
+  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
 
   virtual void printOwnedSort(Type type, std::ostream& os) = 0;
   virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0;
@@ -348,7 +311,7 @@ public:
   LFSCBooleanProof(TheoryProofEngine* proofEngine)
     : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true)
   {}
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
   virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);