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 {