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

diff --git a/src/Makefile.am b/src/Makefile.am
index 068e30256137fb9a4bf54bc2e35db4f7f3068655..703f826148803d4a98f4d1e0b4e232f725013f96 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -76,35 +76,36 @@ libcvc4_la_SOURCES = \
        printer/cvc/cvc_printer.cpp \
        printer/tptp/tptp_printer.h \
        printer/tptp/tptp_printer.cpp \
+       proof/array_proof.h \
+       proof/bitvector_proof.cpp \
+       proof/bitvector_proof.h \
+       proof/clause_id.h \
+       proof/cnf_proof.cpp \
+       proof/cnf_proof.h \
        proof/proof.h \
+       proof/proof_manager.cpp \
+       proof/proof_manager.h \
+       proof/proof_utils.cpp \
+       proof/proof_utils.h \
        proof/sat_proof.h \
        proof/sat_proof_implementation.h \
-       proof/cnf_proof.h \
-       proof/cnf_proof.cpp \
-       proof/theory_proof.h \
        proof/theory_proof.cpp \
-       proof/uf_proof.h \
+       proof/theory_proof.h \
        proof/uf_proof.cpp \
-       proof/array_proof.h \
-       proof/bitvector_proof.h \
-       proof/bitvector_proof.cpp \
-       proof/proof_manager.h \
-       proof/proof_manager.cpp \
-       proof/proof_utils.h \
-       proof/proof_utils.cpp \
+       proof/uf_proof.h \
        proof/unsat_core.cpp \
        proof/unsat_core.h \
-       prop/registrar.h \
+       prop/cnf_stream.cpp \
+       prop/cnf_stream.h \
        prop/prop_engine.cpp \
        prop/prop_engine.h \
-       prop/theory_proxy.h \
-       prop/theory_proxy.cpp \
-       prop/cnf_stream.h \
-       prop/cnf_stream.cpp \
+       prop/registrar.h \
        prop/sat_solver.h \
-       prop/sat_solver_types.h \
-       prop/sat_solver_factory.h \
        prop/sat_solver_factory.cpp \
+       prop/sat_solver_factory.h \
+       prop/sat_solver_types.h \
+       prop/theory_proxy.cpp \
+       prop/theory_proxy.h \
        smt/boolean_terms.cpp \
        smt/boolean_terms.h \
        smt/command.cpp \

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index e067f0bce5dcfedf51010539b3592514dc0dfccc..a018d8bc53fa047ce5c0504ee9b7e56a184acdcb 100644 (file)
--- 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 884a67856cd6d479ed4c6a7b71c125fb29eb836f..31c976a63da16c44d53c7fc7bca0fc644c65771b 100644 (file)
--- 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 675bd9b9d757eb7b77dbce8d0e4c41838ed923ba..e5a80b428377cc7612281b3b434014fde5c1ccaa 100644 (file)
--- 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 b90d589b8cb3d601abf7e04d22ed174f610e5107..93752d3cf7d33a697f4e7d717fa8006c9e271d8f 100644 (file)
--- 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 96c4e1d61852bf5512d64bef2385e753304377b5..58a2f45f7fa733d68b502626e4d532f5dab6f196 100644 (file)
--- 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 cd42ab85b16cb2db4d0e7971cf5d2a28f80d4d31..ccb81b9ad469293732802e4a2b11dff23d255425 100644 (file)
--- 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 92645e1054449e9100b6140e7136e49038279498..d786eef76e5563478f3bad8b2272b15e206345c6 100644 (file)
--- 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 6679cf896e5dbf466b25e79eac298b728051c3eb..6a77faab7ce71eb4f35010c7c80c475ea2fe16a2 100644 (file)
--- 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 d997d6e23130c7e3e2f116e7adb5c55e26a67bef..d1470476000ddf74a61401bb1593b62a5fab4e4b 100644 (file)
--- 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;

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 936778e0d7cbbf90687c8d5a61777b014d4bfb52..54e3f2e8ba6a54855c443d9ee9c4760c0d949c1c 100644 (file)
--- 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 ec8c3455adff4293a9a5334a28c0e9f4cd1f43e8..20724efd2751e9d15a89a241857e5b4bcba4cd90 100644 (file)
--- 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 2100160de6f1a90192cf44aec7bfa1821a9af6f5..d626a5d153c5dc183590b624e73bec27fafa230f 100644 (file)
--- 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 019c09bcd90a60e66c27dbddfb50257ce7e1489b..5554951497b5ae88b9fc7b2dac8b2540145b1a90 100644 (file)
--- 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 311ed1dd12e07f9daae1a2f868c95a2e35cb6791..cb5929320afbe8766278f737d2c71eddc4951b64 100644 (file)
--- 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 5f6f46b91817a723443135a9886158e3cf0e33e9..9854bf77d62ee1e58c90efe501e1e81037bcd92c 100644 (file)
--- 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"

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index d54848d2603995dd2e1eef48e75d2934cfab6e94..9bc352f9b54373f70dc0e77b9b2dc7fa4d0fad90 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -15,6 +15,8 @@
  ** A CNF converter that takes in asserts and has the side effect
  ** of given an equisatisfiable stream of assertions to PropEngine.
  **/
+#include "prop/cnf_stream.h"
+
 #include <queue>
 
 #include "base/cvc4_assert.h"
@@ -22,10 +24,10 @@
 #include "expr/expr.h"
 #include "expr/node.h"
 #include "options/bv_options.h"
+#include "proof/clause_id.h"
+#include "proof/cnf_proof.h"
 #include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
-#include "proof/cnf_proof.h"
-#include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b7fb1603d839d4e233b507eff384bc515916bb05..b13448bb23cc61303a7f950c3420fac8b1221120 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -18,21 +18,22 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "prop/minisat/core/Solver.h"
+
 #include <math.h>
 
 #include <iostream>
 
 #include "base/output.h"
 #include "options/prop_options.h"
+#include "proof/clause_id.h"
 #include "proof/proof_manager.h"
 #include "proof/sat_proof_implementation.h"
 #include "proof/sat_proof.h"
-#include "prop/minisat/core/Solver.h"
 #include "prop/minisat/minisat.h"
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/theory_proxy.h"
 
-
 using namespace CVC4::prop;
 
 namespace CVC4 {

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 777fb1093b7ed850db9ca64237c0d0fcd2d84cbf..99c47e045d42a049e4d6148df30f585eb8b59a52 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "base/output.h"
 #include "context/context.h"
+#include "proof/clause_id.h"
 #include "prop/minisat/core/SolverTypes.h"
 #include "prop/minisat/mtl/Alg.h"
 #include "prop/minisat/mtl/Heap.h"
@@ -43,7 +44,6 @@ namespace prop {
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
-typedef unsigned ClauseId;
 
 namespace CVC4 {
 namespace Minisat {

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 739d9087afd395da2a0083d7673cfb65c95b8d38..bfbf9da6f6a043fb7a579ec8b142d2f5d702ed77 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -23,6 +23,7 @@
 #include "options/prop_options.h"
 #include "options/smt_options.h"
 #include "prop/minisat/simp/SimpSolver.h"
+#include "proof/clause_id.h"
 #include "proof/sat_proof.h"
 #include "util/statistics_registry.h"
 

diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 5bdaea95090bc4cd0485199caccb6aaccacbe1b9..9b551fa708b7a72723fa452c320c081e5beafa2c 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -18,10 +18,12 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "prop/minisat/simp/SimpSolver.h"
+
 #include "options/prop_options.h"
+#include "proof/clause_id.h"
 #include "proof/proof.h"
 #include "prop/minisat/mtl/Sort.h"
-#include "prop/minisat/simp/SimpSolver.h"
 #include "prop/minisat/utils/System.h"
 
 using namespace CVC4;

diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index a19bec1efe65c476125973e4b4133befb2ca525c..a995c1357df3046e3b8d85e8c4edc980b3c10ee4 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "cvc4_private.h"
 
+#include "proof/clause_id.h"
 #include "prop/minisat/mtl/Queue.h"
 #include "prop/minisat/core/Solver.h"
 

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 1383308a34ad6124965fe58dada0078147507361..99e9812204d2f58dc767752c0adbdb99ac2b0ea2 100644 (file)
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -26,6 +26,7 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
 #include "util/statistics_registry.h"
 
@@ -37,8 +38,6 @@ namespace prop {
 
 class TheoryProxy;
 
-typedef unsigned ClauseId;
-
 class SatSolver {
 
 public: