summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am37
-rw-r--r--src/proof/bitvector_proof.cpp3
-rw-r--r--src/proof/cnf_proof.cpp8
-rw-r--r--src/proof/cnf_proof.h3
-rw-r--r--src/proof/proof_manager.cpp20
-rw-r--r--src/proof/proof_manager.h4
-rw-r--r--src/proof/sat_proof.h5
-rw-r--r--src/proof/sat_proof_implementation.h7
-rw-r--r--src/proof/theory_proof.cpp4
-rw-r--r--src/proof/theory_proof.h12
-rw-r--r--src/prop/bvminisat/bvminisat.cpp1
-rw-r--r--src/prop/bvminisat/bvminisat.h1
-rw-r--r--src/prop/bvminisat/core/Solver.cc5
-rw-r--r--src/prop/bvminisat/core/Solver.h15
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.cc3
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.h1
-rw-r--r--src/prop/cnf_stream.cpp6
-rw-r--r--src/prop/minisat/core/Solver.cc5
-rw-r--r--src/prop/minisat/core/Solver.h2
-rw-r--r--src/prop/minisat/minisat.cpp1
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc4
-rw-r--r--src/prop/minisat/simp/SimpSolver.h1
-rw-r--r--src/prop/sat_solver.h3
23 files changed, 81 insertions, 70 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index 068e30256..703f82614 100644
--- 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 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;
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"
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index d54848d26..9bc352f9b 100644
--- 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 b7fb1603d..b13448bb2 100644
--- 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 777fb1093..99c47e045 100644
--- 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 739d9087a..bfbf9da6f 100644
--- 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 5bdaea950..9b551fa70 100644
--- 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 a19bec1ef..a995c1357 100644
--- 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 1383308a3..99e981220 100644
--- 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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback