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

6 files changed, 16 insertions, 10 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 936778e0d..54e3f2e8b 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -19,6 +19,7 @@
 #include "prop/bvminisat/bvminisat.h"
 
 #include "prop/bvminisat/simp/SimpSolver.h"
+#include "proof/clause_id.h"
 #include "proof/sat_proof.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index ec8c3455a..20724efd2 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -21,6 +21,7 @@
 #pragma once
 
 #include "context/cdo.h"
+#include "proof/clause_id.h"
 #include "prop/bvminisat/simp/SimpSolver.h"
 #include "prop/sat_solver.h"
 #include "util/statistics_registry.h"
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 2100160de..d626a5d15 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -30,11 +30,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "mtl/Sort.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
-#include "theory/interrupted.h"
-#include "proof/proof_manager.h"
 #include "proof/bitvector_proof.h"
+#include "proof/clause_id.h"
+#include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
 #include "proof/sat_proof_implementation.h"
+#include "theory/interrupted.h"
 #include "util/utility.h"
 
 namespace CVC4 {
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 019c09bcd..555495149 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -21,20 +21,21 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef BVMinisat_Solver_h
 #define BVMinisat_Solver_h
 
+#include <ext/hash_set>
+#include <vector>
+
+#include "context/context.h"
+#include "proof/clause_id.h"
+#include "proof/sat_proof.h"
 #include "prop/bvminisat/core/SolverTypes.h"
-#include "prop/bvminisat/mtl/Vec.h"
-#include "prop/bvminisat/mtl/Heap.h"
 #include "prop/bvminisat/mtl/Alg.h"
+#include "prop/bvminisat/mtl/Heap.h"
+#include "prop/bvminisat/mtl/Vec.h"
 #include "prop/bvminisat/utils/Options.h"
-#include "context/cdhashmap.h"
-#include "proof/sat_proof.h"
 
-#include <ext/hash_set>
-#include <vector>
 
 namespace CVC4 {
 
-typedef unsigned ClauseId;
 namespace BVMinisat {
 class Solver;
 }
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 311ed1dd1..cb5929320 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -23,8 +23,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "mtl/Sort.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
-#include "utils/System.h"
+#include "proof/clause_id.h"
 #include "proof/proof.h"
+#include "utils/System.h"
 
 namespace CVC4 {
 namespace BVMinisat {
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 5f6f46b91..9854bf77d 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -22,6 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define BVMinisat_SimpSolver_h
 
 #include "context/context.h"
+#include "proof/clause_id.h"
 #include "prop/bvminisat/core/Solver.h"
 #include "prop/bvminisat/mtl/Queue.h"
 #include "util/statistics_registry.h"