1 files changed, 80 insertions, 25 deletions

diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index da10c33a0..546d419fc 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -17,7 +17,7 @@
 
 #include "cvc4_private.h"
 
-#pragma once 
+#pragma once
 
 #include <set>
 #include <vector>
@@ -29,6 +29,61 @@ namespace CVC4 {
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
 typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
 
+typedef std::pair<Node, Node> NodePair;
+typedef std::set<NodePair> NodePairSet;
+
+
+struct ProofLetCount {
+  static unsigned counter;
+  static void resetCounter() { counter = 0; }
+  static unsigned newId() { return ++counter; }
+
+  unsigned count;
+  unsigned id;
+  ProofLetCount()
+    : count(0)
+    , id(-1)
+  {}
+
+  void increment() { ++count; }
+  ProofLetCount(unsigned i)
+    : count(1)
+    , id(i)
+  {}
+
+  ProofLetCount(const ProofLetCount& other)
+    : count(other.count)
+    , id (other.id)
+  {}
+
+  bool operator==(const ProofLetCount &other) const {
+    return other.id == id && other.count == count;
+  }
+
+  ProofLetCount& operator=(const ProofLetCount &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 std::vector<LetOrderElement> Bindings;
+
 namespace utils {
 
 std::string toLFSCKind(Kind kind);
@@ -42,7 +97,7 @@ inline unsigned getExtractLow(Expr node) {
 }
 
 inline unsigned getSize(Type type) {
-  BitVectorType bv(type); 
+  BitVectorType bv(type);
   return bv.getSize();
 }
 
@@ -60,8 +115,8 @@ inline Expr mkFalse() {
   return NodeManager::currentNM()->toExprManager()->mkConst<bool>(false);
 }
 inline BitVector mkBitVectorOnes(unsigned size) {
-  Assert(size > 0); 
-  return BitVector(1, Integer(1)).signExtend(size - 1); 
+  Assert(size > 0);
+  return BitVector(1, Integer(1)).signExtend(size - 1);
 }
 
 inline Expr mkExpr(Kind k , Expr expr) {
@@ -73,16 +128,16 @@ inline Expr mkExpr(Kind k , Expr e1, Expr e2) {
 inline Expr mkExpr(Kind k , std::vector<Expr>& children) {
   return NodeManager::currentNM()->toExprManager()->mkExpr(k, children);
 }
-  
-  
+
+
 inline Expr mkOnes(unsigned size) {
-  BitVector val = mkBitVectorOnes(size); 
-  return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); 
+  BitVector val = mkBitVectorOnes(size);
+  return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
 }
 
 inline Expr mkConst(unsigned size, unsigned int value) {
   BitVector val(size, value);
-  return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); 
+  return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
 }
 
 inline Expr mkConst(const BitVector& value) {
@@ -92,14 +147,14 @@ inline Expr mkConst(const BitVector& value) {
 inline Expr mkOr(const std::vector<Expr>& nodes) {
   std::set<Expr> all;
   all.insert(nodes.begin(), nodes.end());
-  Assert(all.size() != 0 ); 
+  Assert(all.size() != 0 );
 
   if (all.size() == 1) {
     // All the same, or just one
     return nodes[0];
   }
-  
-  
+
+
   NodeBuilder<> disjunction(kind::OR);
   std::set<Expr>::const_iterator it = all.begin();
   std::set<Expr>::const_iterator it_end = all.end();
@@ -109,23 +164,23 @@ inline Expr mkOr(const std::vector<Expr>& nodes) {
   }
 
   Node res = disjunction;
-  return res.toExpr(); 
+  return res.toExpr();
 }/* mkOr() */
 
-                 
+
 inline Expr mkAnd(const std::vector<Expr>& conjunctions) {
   std::set<Expr> all;
   all.insert(conjunctions.begin(), conjunctions.end());
 
   if (all.size() == 0) {
-    return mkTrue(); 
+    return mkTrue();
   }
-  
+
   if (all.size() == 1) {
     // All the same, or just one
     return conjunctions[0];
   }
-  
+
 
   NodeBuilder<> conjunction(kind::AND);
   std::set<Expr>::const_iterator it = all.begin();
@@ -135,7 +190,7 @@ inline Expr mkAnd(const std::vector<Expr>& conjunctions) {
     ++ it;
   }
 
-  Node res = conjunction; 
+  Node res = conjunction;
   return res.toExpr();
 }/* mkAnd() */
 
@@ -144,14 +199,14 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) {
   all.insert(children.begin(), children.end());
 
   if (all.size() == 0) {
-    return mkTrue(); 
+    return mkTrue();
   }
-  
+
   if (all.size() == 1) {
     // All the same, or just one
     return children[0];
   }
-  
+
 
   NodeBuilder<> res(kind);
   std::set<Expr>::const_iterator it = all.begin();
@@ -165,13 +220,13 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) {
 }/* mkSortedNode() */
 
 inline const bool getBit(Expr expr, unsigned i) {
-  Assert (i < utils::getSize(expr) && 
-          expr.isConst()); 
+  Assert (i < utils::getSize(expr) &&
+          expr.isConst());
   Integer bit = expr.getConst<BitVector>().extract(i, i).getValue();
-  return (bit == 1u); 
+  return (bit == 1u);
 }
 
-void collectAtoms(TNode node, NodeSet& seen);
+void collectAtoms(TNode node, std::set<Node>& seen);
 
 
 }