Unifying the definitions of ClauseId to a single source of truth.

9 files changed, 32 insertions, 34 deletions

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index e067f0bce..a018d8bc5 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -15,9 +15,10 @@
 ** \todo document this file
 **/
 
-
 #include "proof/bitvector_proof.h" 
+
 #include "options/bv_options.h"
+#include "proof/clause_id.h"
 #include "proof/proof_utils.h"
 #include "proof/sat_proof_implementation.h"
 #include "prop/bvminisat/bvminisat.h"
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 884a67856..31c976a63 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -16,11 +16,13 @@
  **/
 
 #include "proof/cnf_proof.h"
-#include "proof/theory_proof.h"
+
+#include "proof/clause_id.h"
 #include "proof/proof_manager.h"
-#include "prop/sat_solver_types.h"
-#include "prop/minisat/minisat.h"
+#include "proof/theory_proof.h"
 #include "prop/cnf_stream.h"
+#include "prop/minisat/minisat.h"
+#include "prop/sat_solver_types.h"
 
 using namespace CVC4::prop;
 
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 675bd9b9d..e5a80b428 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -26,9 +26,8 @@
 #include <iosfwd>
 
 #include "context/cdhashmap.h"
+#include "proof/clause_id.h"
 #include "proof/sat_proof.h"
-#include "proof/sat_proof.h"
-#include "util/proof.h"
 #include "util/proof.h"
 
 namespace CVC4 {
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index b90d589b8..93752d3cf 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -15,20 +15,17 @@
  ** \todo document this file
  **/
 
-#include "context/context.h"
-
 #include "proof/proof_manager.h"
-#include "proof/cnf_proof.h"
-#include "proof/theory_proof.h"
+
+#include "base/cvc4_assert.h"
+#include "context/context.h"
+#include "options/bv_options.h"
 #include "proof/bitvector_proof.h"
+#include "proof/clause_id.h"
+#include "proof/cnf_proof.h"
 #include "proof/proof_utils.h"
 #include "proof/sat_proof_implementation.h"
-#include "options/bv_options.h"
-
-#include "util/proof.h"
-#include "util/hash.h"
-
-#include "base/cvc4_assert.h"
+#include "proof/theory_proof.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt_util/node_visitor.h"
@@ -38,7 +35,8 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/valuation.h"
-
+#include "util/hash.h"
+#include "util/proof.h"
 
 namespace CVC4 {
 
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 96c4e1d61..58a2f45f7 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -23,6 +23,7 @@
 #include <map>
 
 #include "expr/node.h"
+#include "proof/clause_id.h"
 #include "proof/proof.h"
 #include "theory/logic_info.h"
 #include "theory/substitutions.h"
@@ -46,7 +47,6 @@ namespace prop {
 
 class SmtEngine;
 
-typedef unsigned ClauseId;
 const ClauseId ClauseIdEmpty(-1);
 const ClauseId ClauseIdUndef(-2);  
 const ClauseId ClauseIdError(-3);
@@ -96,8 +96,6 @@ typedef __gnu_cxx::hash_set<Node, NodeHashFunction > NodeSet;
 typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction > NodeToNodes;
 typedef std::hash_set<ClauseId> IdHashSet;
 
-typedef unsigned ClauseId;
-
 enum ProofRule {
   RULE_GIVEN,       /* input assertion */
   RULE_DERIVED,     /* a "macro" rule */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index cd42ab85b..ccb81b9ad 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -20,21 +20,22 @@
 #define __CVC4__SAT__PROOF_H
 
 #include <stdint.h>
+
 #include <ext/hash_map>
 #include <ext/hash_set>
 #include <iosfwd>
 #include <set>
 #include <sstream>
 #include <vector>
+
 #include "expr/expr.h"
+#include "proof/clause_id.h"
 #include "proof/proof_manager.h"
 #include "util/proof.h"
 #include "util/statistics_registry.h"
 
-
 namespace CVC4 {
 
-
 class CnfProof;
 
 /**
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 92645e105..d786eef76 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -19,12 +19,13 @@
 #ifndef __CVC4__SAT__PROOF_IMPLEMENTATION_H
 #define __CVC4__SAT__PROOF_IMPLEMENTATION_H
 
-#include "proof/sat_proof.h"
+#include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
-#include "prop/minisat/minisat.h"
+#include "proof/sat_proof.h"
 #include "prop/bvminisat/bvminisat.h"
-#include "prop/minisat/core/Solver.h"
 #include "prop/bvminisat/core/Solver.h"
+#include "prop/minisat/core/Solver.h"
+#include "prop/minisat/minisat.h"
 #include "prop/sat_solver_types.h"
 #include "smt/smt_statistics_registry.h"
 
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 6679cf896..6a77faab7 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -14,18 +14,18 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
+#include "proof/theory_proof.h"
 
 #include "base/cvc4_assert.h"
 #include "context/context.h"
 #include "options/bv_options.h"
 #include "proof/array_proof.h"
 #include "proof/bitvector_proof.h"
-#include "proof/cnf_proof.h"
+#include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
 #include "proof/proof_manager.h"
 #include "proof/proof_utils.h"
 #include "proof/sat_proof.h"
-#include "proof/theory_proof.h"
 #include "proof/uf_proof.h"
 #include "prop/sat_solver_types.h"
 #include "smt/smt_engine.h"
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index d997d6e23..d14704760 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -21,20 +21,19 @@
 #ifndef __CVC4__THEORY_PROOF_H
 #define __CVC4__THEORY_PROOF_H
 
-#include "util/proof.h"
-#include "expr/expr.h"
-#include "prop/sat_solver_types.h"
 #include <ext/hash_set>
 #include <iosfwd>
 
+#include "expr/expr.h"
+#include "proof/clause_id.h"
+#include "prop/sat_solver_types.h"
+#include "util/proof.h"
 
 namespace CVC4 {
 
 namespace theory {
 class Theory;
-}
-
-typedef unsigned ClauseId;
+} /* namespace CVC4::theory */
 
 struct LetCount {
   static unsigned counter;
@@ -88,7 +87,6 @@ typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap;
 typedef std::vector<LetOrderElement> Bindings; 
 
 class TheoryProof;
-typedef unsigned ClauseId;
 
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
 typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable;