Merging proof branch

1 files changed, 28 insertions, 25 deletions

diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index da10c33a0..8c734c892 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,9 @@ 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;
+
 namespace utils {
 
 std::string toLFSCKind(Kind kind);
@@ -42,7 +45,7 @@ inline unsigned getExtractLow(Expr node) {
 }
 
 inline unsigned getSize(Type type) {
-  BitVectorType bv(type); 
+  BitVectorType bv(type);
   return bv.getSize();
 }
 
@@ -60,8 +63,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 +76,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 +95,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 +112,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 +138,7 @@ inline Expr mkAnd(const std::vector<Expr>& conjunctions) {
     ++ it;
   }
 
-  Node res = conjunction; 
+  Node res = conjunction;
   return res.toExpr();
 }/* mkAnd() */
 
@@ -144,14 +147,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 +168,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);
 
 
 }