diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 15 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 7 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 6 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 22 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 15 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 14 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 14 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 5 | ||||
-rw-r--r-- | src/prop/options | 31 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 39 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 9 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 8 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 18 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 6 |
15 files changed, 94 insertions, 117 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index ca7228ee8..5a37da27c 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -18,19 +18,20 @@ 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 "core/Solver.h" + #include <math.h> -#include "mtl/Sort.h" -#include "core/Solver.h" #include <vector> #include <iostream> -#include "util/output.h" -#include "util/utility.h" -#include "util/exception.h" -#include "theory/bv/options.h" -#include "smt/options.h" +#include "base/exception.h" +#include "base/output.h" +#include "mtl/Sort.h" +#include "options/bv_options.h" +#include "options/smt_options.h" #include "theory/interrupted.h" +#include "util/utility.h" namespace CVC4 { namespace BVMinisat { diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index e7e489985..c5b185c95 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -18,11 +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 "mtl/Sort.h" #include "simp/SimpSolver.h" + +#include "mtl/Sort.h" +#include "options/bv_options.h" +#include "options/smt_options.h" #include "utils/System.h" -#include "theory/bv/options.h" -#include "smt/options.h" namespace CVC4 { namespace BVMinisat { diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 707f62e34..bef8e0a70 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -21,10 +21,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_SimpSolver_h #define BVMinisat_SimpSolver_h -#include "prop/bvminisat/mtl/Queue.h" -#include "prop/bvminisat/core/Solver.h" -#include "util/statistics_registry.h" #include "context/context.h" +#include "expr/statistics_registry.h" +#include "prop/bvminisat/core/Solver.h" +#include "prop/bvminisat/mtl/Queue.h" namespace CVC4 { namespace BVMinisat { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index b0b135b04..ffbc67cc4 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -15,23 +15,23 @@ ** A CNF converter that takes in asserts and has the side effect ** of given an equisatisfiable stream of assertions to PropEngine. **/ +#include <queue> -#include "prop/cnf_stream.h" -#include "prop/prop_engine.h" -#include "theory/theory_engine.h" -#include "theory/theory.h" -#include "expr/node.h" -#include "util/cvc4_assert.h" -#include "util/output.h" -#include "expr/command.h" +#include "base/cvc4_assert.h" +#include "base/output.h" #include "expr/expr.h" -#include "prop/theory_proxy.h" -#include "theory/bv/options.h" +#include "expr/node.h" +#include "options/bv_options.h" #include "proof/proof_manager.h" #include "proof/sat_proof.h" +#include "prop/cnf_stream.h" #include "prop/minisat/minisat.h" +#include "prop/prop_engine.h" +#include "prop/theory_proxy.h" #include "smt/smt_engine_scope.h" -#include <queue> +#include "smt_util/command.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 5dc618899..4c431a9b1 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -22,16 +22,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <iostream> -#include "prop/minisat/mtl/Sort.h" -#include "prop/minisat/core/Solver.h" - -#include "prop/theory_proxy.h" -#include "prop/minisat/minisat.h" -#include "prop/options.h" -#include "util/output.h" -#include "expr/command.h" +#include "base/output.h" +#include "options/prop_options.h" #include "proof/proof_manager.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" +#include "smt_util/command.h" using namespace CVC4::prop; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index b5895de6e..3ed828f7c 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -25,16 +25,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <iostream> -#include "prop/minisat/mtl/Vec.h" -#include "prop/minisat/mtl/Heap.h" +#include "base/output.h" +#include "context/context.h" +#include "prop/minisat/core/SolverTypes.h" #include "prop/minisat/mtl/Alg.h" +#include "prop/minisat/mtl/Heap.h" +#include "prop/minisat/mtl/Vec.h" #include "prop/minisat/utils/Options.h" -#include "prop/minisat/core/SolverTypes.h" - -#include "context/context.h" +#include "smt_util/command.h" #include "theory/theory.h" -#include "util/output.h" -#include "expr/command.h" + namespace CVC4 { class SatProof; diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 0df5eb123..b0d78242c 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define Minisat_SolverTypes_h #include <assert.h> -#include "util/output.h" +#include "base/output.h" #include "prop/minisat/mtl/IntTypes.h" #include "prop/minisat/mtl/Alg.h" #include "prop/minisat/mtl/Vec.h" diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 53ab2eccf..23a740a26 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -17,13 +17,14 @@ **/ #include "prop/minisat/minisat.h" + +#include "options/decision_options.h" +#include "options/prop_options.h" +#include "options/smt_options.h" #include "prop/minisat/simp/SimpSolver.h" -#include "prop/options.h" -#include "smt/options.h" -#include "decision/options.h" -using namespace CVC4; -using namespace CVC4::prop; +namespace CVC4 { +namespace prop { //// DPllMinisatSatSolver @@ -270,3 +271,6 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ d_statMaxLiterals.setData(d_minisat->max_literals); d_statTotLiterals.setData(d_minisat->tot_literals); } + +} /* namespace CVC4::prop */ +} /* namespace CVC4 */ diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 8408503e2..235c97e8f 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -18,11 +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 "options/prop_options.h" +#include "proof/proof.h" #include "prop/minisat/mtl/Sort.h" #include "prop/minisat/simp/SimpSolver.h" #include "prop/minisat/utils/System.h" -#include "prop/options.h" -#include "proof/proof.h" + using namespace CVC4; using namespace CVC4::Minisat; diff --git a/src/prop/options b/src/prop/options deleted file mode 100644 index 65bb44de6..000000000 --- a/src/prop/options +++ /dev/null @@ -1,31 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module PROP "prop/options.h" SAT layer - -option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate options::greater_equal(0.0) options::less_equal(1.0) - sets the frequency of random decisions in the sat solver (P=0.0 by default) -option satRandomSeed random-seed --random-seed=S uint32_t :default 0 :read-write - sets the random seed for the sat solver - -option satVarDecay double :default 0.95 :predicate options::less_equal(1.0) options::greater_equal(0.0) - variable activity decay factor for Minisat -option satClauseDecay double :default 0.999 :predicate options::less_equal(1.0) options::greater_equal(0.0) - clause activity decay factor for Minisat -option satRestartFirst --restart-int-base=N unsigned :default 25 - sets the base restart interval for the sat solver (N=25 by default) -option satRestartInc --restart-int-inc=F double :default 3.0 :predicate options::greater_equal(0.0) - sets the restart interval increase factor for the sat solver (F=3.0 by default) - -option sat_refine_conflicts --refine-conflicts bool :default false - refine theory conflict clauses (default false) - -option minisatUseElim --minisat-elimination bool :default true :read-write - use Minisat elimination - -option minisatDumpDimacs --minisat-dump-dimacs bool :default false - instead of solving minisat dumps the asserted clauses in Dimacs format - -endmodule diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 794e36e2c..499cf1b56 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -14,31 +14,32 @@ ** Implementation of the propositional engine of CVC4. **/ -#include "prop/cnf_stream.h" #include "prop/prop_engine.h" -#include "prop/theory_proxy.h" -#include "prop/sat_solver.h" -#include "prop/sat_solver_factory.h" -#include "proof/proof_manager.h" +#include <iomanip> +#include <map> +#include <utility> + +#include "base/cvc4_assert.h" +#include "base/output.h" #include "decision/decision_engine.h" -#include "decision/options.h" +#include "expr/expr.h" +#include "expr/resource_manager.h" +#include "expr/result.h" +#include "options/decision_options.h" +#include "options/main_options.h" +#include "options/options.h" +#include "options/smt_options.h" +#include "proof/proof_manager.h" +#include "proof/proof_manager.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver.h" +#include "prop/sat_solver_factory.h" +#include "prop/theory_proxy.h" +#include "smt_util/command.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" -#include "proof/proof_manager.h" -#include "util/cvc4_assert.h" -#include "options/options.h" -#include "smt/options.h" -#include "main/options.h" -#include "util/output.h" -#include "util/result.h" -#include "util/resource_manager.h" -#include "expr/expr.h" -#include "expr/command.h" -#include <utility> -#include <map> -#include <iomanip> using namespace std; using namespace CVC4::context; diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 768f07108..57ff3c5c0 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -21,13 +21,14 @@ #ifndef __CVC4__PROP_ENGINE_H #define __CVC4__PROP_ENGINE_H +#include <sys/time.h> + +#include "base/modal_exception.h" #include "expr/node.h" +#include "expr/result.h" #include "options/options.h" -#include "util/result.h" -#include "util/unsafe_interrupt_exception.h" -#include "smt/modal_exception.h" #include "proof/proof_manager.h" -#include <sys/time.h> +#include "util/unsafe_interrupt_exception.h" namespace CVC4 { diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 50d308541..960881844 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -19,12 +19,14 @@ #ifndef __CVC4__PROP__SAT_SOLVER_H #define __CVC4__PROP__SAT_SOLVER_H -#include <string> #include <stdint.h> -#include "util/statistics_registry.h" + +#include <string> + #include "context/cdlist.h" -#include "prop/sat_solver_types.h" #include "expr/node.h" +#include "expr/statistics_registry.h" +#include "prop/sat_solver_types.h" namespace CVC4 { namespace prop { diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 9c6da703a..386b12391 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -14,19 +14,19 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "prop/theory_proxy.h" +#include "context/context.h" +#include "decision/decision_engine.h" +#include "expr/expr_stream.h" +#include "expr/statistics_registry.h" +#include "options/decision_options.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" -#include "prop/theory_proxy.h" -#include "context/context.h" -#include "theory/theory_engine.h" +#include "smt_util/lemma_input_channel.h" +#include "smt_util/lemma_output_channel.h" #include "theory/rewriter.h" -#include "expr/expr_stream.h" -#include "decision/decision_engine.h" -#include "decision/options.h" -#include "util/lemma_input_channel.h" -#include "util/lemma_output_channel.h" -#include "util/statistics_registry.h" +#include "theory/theory_engine.h" namespace CVC4 { namespace prop { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 90ad558f5..413b4941d 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -23,12 +23,10 @@ // Optional blocks below will be unconditionally included #define __CVC4_USE_MINISAT -#include "theory/theory.h" -#include "util/statistics_registry.h" - #include "context/cdqueue.h" - +#include "expr/statistics_registry.h" #include "prop/sat_solver.h" +#include "theory/theory.h" namespace CVC4 { |