Options merge. This commit:

1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)

The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:

* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important.  If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***

Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).

Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double).  For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).

Benefits of the new options system include:

1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose

I've taken lots of care not to break anything.  Hopefully, I've succeeded in that.

14 files changed, 607 insertions, 33 deletions

diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 5e6b18c19..f109e0ed2 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -22,5 +22,8 @@ libprop_la_SOURCES = \
 	sat_solver_registry.h \
 	sat_solver_registry.cpp
 
+EXTRA_DIST = \
+	options_handlers.h
+
 SUBDIRS = minisat bvminisat
 
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 94f3a6b74..293ddd657 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -27,7 +27,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "util/output.h"
 #include "util/utility.h"
-#include "util/options.h"
+
+#include "theory/bv/options.h"
 
 using namespace BVMinisat;
 
@@ -423,7 +424,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
         out_btlevel       = level(var(p));
     }
 
-    if (out_learnt.size() > 0 && clause_all_marker && CVC4::Options::current()->bitvectorShareLemmas) {
+    if (out_learnt.size() > 0 && clause_all_marker && CVC4::options::bitvectorShareLemmas()) {
       notify->notify(out_learnt);
     }
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 485ddbb55..b498f1e40 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -202,7 +202,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
 
   // If it's a theory literal, need to store it for back queries
   if ( theoryLiteral || d_fullLitToNodeMap ||
-       ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ||
+       ( CVC4_USE_REPLAY && options::replayLog() != NULL ) ||
        (Dump.isOn("clauses")) ) {
     d_nodeCache[lit] = node;
     d_nodeCache[~lit] = node.notNode();
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 4c5743c7c..675bc8f4e 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "prop/theory_proxy.h"
 #include "prop/minisat/minisat.h"
+#include "prop/options.h"
 #include "util/output.h"
 #include "expr/command.h"
 #include "proof/proof_manager.h"
@@ -1079,7 +1080,7 @@ lbool Solver::search(int nof_conflicts)
                            (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
             }
 
-            if (theoryConflict && Options::current()->sat_refine_conflicts) {
+            if (theoryConflict && options::sat_refine_conflicts()) {
               check_type = CHECK_FINAL_FAKE;
             } else {
               check_type = CHECK_WITH_THEORY;
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 6fa698bd0..464a41d74 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -18,6 +18,9 @@
 
 #include "prop/minisat/minisat.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;
@@ -106,26 +109,26 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory
 
   d_context = context;
 
-  if( Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL ) {
+  if( options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ) {
     Notice() << "minisat: Incremental solving is disabled"
              << " unless using internal decision strategy." << std::endl;
   }
 
   // Create the solver
   d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
-                                      Options::current()->incrementalSolving || 
-                                      Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL );
+                                      options::incrementalSolving() ||
+                                      options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL );
   // Setup the verbosity
-  d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1;
+  d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;
 
   // Setup the random decision parameters
-  d_minisat->random_var_freq = Options::current()->satRandomFreq;
-  d_minisat->random_seed = Options::current()->satRandomSeed;
+  d_minisat->random_var_freq = options::satRandomFreq();
+  d_minisat->random_seed = options::satRandomSeed();
   // Give access to all possible options in the sat solver
-  d_minisat->var_decay = Options::current()->satVarDecay;
-  d_minisat->clause_decay = Options::current()->satClauseDecay;
-  d_minisat->restart_first = Options::current()->satRestartFirst;
-  d_minisat->restart_inc = Options::current()->satRestartInc;
+  d_minisat->var_decay = options::satVarDecay();
+  d_minisat->clause_decay = options::satClauseDecay();
+  d_minisat->restart_first = options::satRestartFirst();
+  d_minisat->restart_inc = options::satRestartInc();
 
   d_statistics.init(d_minisat);
 }
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 8da3856ff..bf04cec8d 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #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 Minisat;
 using namespace CVC4;
@@ -52,7 +53,7 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* c
   , simp_garbage_frac  (opt_simp_garbage_frac)
   , use_asymm          (opt_use_asymm)
   , use_rcheck         (opt_use_rcheck)
-  , use_elim           (!enableIncremental)
+  , use_elim           (options::minisatUseElim() && !enableIncremental)
   , merges             (0)
   , asymm_lits         (0)
   , eliminated_vars    (0)
@@ -63,6 +64,12 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* c
   , bwdsub_assigns     (0)
   , n_touched          (0)
 {
+    if(options::minisatUseElim() &&
+       options::minisatUseElim.wasSetByUser() &&
+       enableIncremental) {
+        WarningOnce() << "Incremental mode incompatible with --minisat-elimination" << std::endl;
+    }
+
     vec<Lit> dummy(1,lit_Undef);
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
     bwdsub_tmpunit        = ca.alloc(0, dummy);
diff --git a/src/prop/options b/src/prop/options
new file mode 100644
index 000000000..c3c2674c4
--- /dev/null
+++ b/src/prop/options
@@ -0,0 +1,31 @@
+#
+# 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 - --show-sat-solvers void :handler CVC4::prop::showSatSolvers :handler-include "prop/options_handlers.h"
+ show all available SAT solvers
+
+option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate greater_equal(0.0) 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 double :default 91648253 :read-write
+ sets the random seed for the sat solver
+
+option satVarDecay double :default 0.95 :predicate less_equal(1.0) greater_equal(0.0)
+ variable activity decay factor for Minisat
+option satClauseDecay double :default 0.999 :predicate less_equal(1.0) 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 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
+ refine theory conflict clauses
+
+option minisatUseElim --minisat-elimination bool :default true
+ use Minisat elimination
+
+endmodule
diff --git a/src/prop/options_handlers.h b/src/prop/options_handlers.h
new file mode 100644
index 000000000..efcb8d911
--- /dev/null
+++ b/src/prop/options_handlers.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROP__OPTIONS_HANDLERS_H
+#define __CVC4__PROP__OPTIONS_HANDLERS_H
+
+#include "prop/sat_solver_factory.h"
+#include <string>
+#include <vector>
+
+namespace CVC4 {
+namespace prop {
+
+inline void showSatSolvers(std::string option, SmtEngine* smt) {
+  std::vector<std::string> solvers;
+  SatSolverFactory::getSolverIds(solvers);
+  printf("Available SAT solvers: ");
+  for (unsigned i = 0; i < solvers.size(); ++ i) {
+    if (i > 0) {
+      printf(", ");
+    }
+    printf("%s", solvers[i].c_str());
+  }
+  printf("\n");
+  exit(0);
+}
+
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PROP__OPTIONS_HANDLERS_H */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 0f138eb65..54309cd01 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -23,10 +23,12 @@
 #include "prop/sat_solver_factory.h"
 
 #include "decision/decision_engine.h"
+#include "decision/options.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
 #include "util/Assert.h"
-#include "util/options.h"
+#include "options/options.h"
+#include "smt/options.h"
 #include "util/output.h"
 #include "util/result.h"
 #include "expr/expr.h"
@@ -80,8 +82,8 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) :
   d_cnfStream = new CVC4::prop::TseitinCnfStream
     (d_satSolver, registrar, 
      // fullLitToNode Map = 
-     Options::current()->threads > 1 || 
-     Options::current()->decisionMode == Options::DECISION_STRATEGY_RELEVANCY);
+     options::threads() > 1 || 
+     options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY);
 
   d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream));
 
@@ -165,7 +167,7 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
   // TODO This currently ignores conflicts (a dangerous practice).
   d_theoryEngine->presolve();
 
-  if(Options::current()->preprocessOnly) {
+  if(options::preprocessOnly()) {
     millis = resource = 0;
     return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
   }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index dcfc5a9df..2d4e08db7 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -24,7 +24,7 @@
 #define __CVC4__PROP_ENGINE_H
 
 #include "expr/node.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/result.h"
 #include "smt/modal_exception.h"
 #include <sys/time.h>
diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp
new file mode 100644
index 000000000..ca41eac2f
--- /dev/null
+++ b/src/prop/sat_module.cpp
@@ -0,0 +1,478 @@
+/*********************                                                        */
+/*! \file sat.cpp
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: dejan, taking, mdeters, lianah
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "prop/prop_engine.h"
+#include "prop/sat_module.h"
+#include "context/context.h"
+#include "theory/theory_engine.h"
+#include "expr/expr_stream.h"
+#include "prop/sat.h"
+
+// DPLLT Minisat
+#include "prop/minisat/simp/SimpSolver.h"
+
+// BV Minisat
+#include "prop/bvminisat/simp/SimpSolver.h"
+
+
+using namespace std; 
+
+namespace CVC4 {
+namespace prop {
+
+string SatLiteral::toString() {
+  ostringstream os;
+  os << (isNegated()? "~" : "") << getSatVariable() << " ";
+  return os.str(); 
+}
+
+MinisatSatSolver::MinisatSatSolver() :
+  d_minisat(new BVMinisat::SimpSolver())
+{
+  d_statistics.init(d_minisat); 
+}
+
+MinisatSatSolver::~MinisatSatSolver() {
+  delete d_minisat; 
+}
+
+void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
+  Debug("sat::minisat") << "Add clause " << clause <<"\n"; 
+  BVMinisat::vec<BVMinisat::Lit> minisat_clause;
+  toMinisatClause(clause, minisat_clause);
+  // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
+  //   d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true); 
+  // }
+  d_minisat->addClause(minisat_clause);
+}
+
+SatVariable MinisatSatSolver::newVar(bool freeze){
+  return d_minisat->newVar(true, true, freeze);
+}
+
+void MinisatSatSolver::markUnremovable(SatLiteral lit){
+  d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
+}
+ 
+void MinisatSatSolver::interrupt(){
+  d_minisat->interrupt(); 
+}
+
+SatLiteralValue MinisatSatSolver::solve(){
+  return toSatLiteralValue(d_minisat->solve()); 
+}
+
+SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){
+  Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
+  if(resource == 0) {
+    d_minisat->budgetOff();
+  } else {
+    d_minisat->setConfBudget(resource);
+  }
+  BVMinisat::vec<BVMinisat::Lit> empty;
+  unsigned long conflictsBefore = d_minisat->conflicts;
+  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
+  d_minisat->clearInterrupt();
+  resource = d_minisat->conflicts - conflictsBefore;
+  Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
+  return result;
+}
+
+SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){
+  Debug("sat::minisat") << "Solve with assumptions ";
+  context::CDList<SatLiteral>::const_iterator it = assumptions.begin();
+  BVMinisat::vec<BVMinisat::Lit> assump; 
+  for(; it!= assumptions.end(); ++it) {
+    SatLiteral lit = *it;
+    Debug("sat::minisat") << lit <<" "; 
+    assump.push(toMinisatLit(lit)); 
+  }
+  Debug("sat::minisat") <<"\n";
+  
+ SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump));
+ return result;
+}
+
+
+void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
+  // TODO add assertion to check the call was after an unsat call
+  for (int i = 0; i < d_minisat->conflict.size(); ++i) {
+    unsatCore.push_back(toSatLiteral(d_minisat->conflict[i])); 
+  }
+}
+
+SatLiteralValue MinisatSatSolver::value(SatLiteral l){
+    Unimplemented();
+    return SatValUnknown; 
+}
+
+SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){
+    Unimplemented();
+    return SatValUnknown; 
+}
+
+void MinisatSatSolver::unregisterVar(SatLiteral lit) {
+  // this should only be called when user context is implemented
+  // in the BVSatSolver 
+  Unreachable();
+}
+
+void MinisatSatSolver::renewVar(SatLiteral lit, int level) {
+  // this should only be called when user context is implemented
+  // in the BVSatSolver 
+
+  Unreachable(); 
+}
+
+int MinisatSatSolver::getAssertionLevel() const {
+  // we have no user context implemented so far
+  return 0;
+}
+
+// converting from internal Minisat representation
+
+SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) {
+  if (var == var_Undef) {
+    return undefSatVariable; 
+  }
+  return SatVariable(var);
+}
+
+BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
+  if (lit == undefSatLiteral) {
+    return BVMinisat::lit_Undef;
+  }
+  return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated()); 
+}
+
+SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
+  if (lit == BVMinisat::lit_Undef) {
+    return undefSatLiteral; 
+  }
+  
+  return SatLiteral(SatVariable(BVMinisat::var(lit)),
+                    BVMinisat::sign(lit)); 
+}
+
+SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) {
+  if(res) return SatValTrue;
+  else return SatValFalse; 
+}
+
+SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
+  if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue;
+  if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown;
+  Assert(res == (BVMinisat::lbool((uint8_t)1)));
+  return SatValFalse; 
+}
+
+void MinisatSatSolver::toMinisatClause(SatClause& clause,
+                                           BVMinisat::vec<BVMinisat::Lit>& minisat_clause) {
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    minisat_clause.push(toMinisatLit(clause[i])); 
+  }
+  Assert(clause.size() == (unsigned)minisat_clause.size()); 
+}
+
+void MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
+                                       SatClause& sat_clause) {
+  for (int i = 0; i < clause.size(); ++i) {
+    sat_clause.push_back(toSatLiteral(clause[i])); 
+  }
+  Assert((unsigned)clause.size() == sat_clause.size()); 
+}
+
+
+// Satistics for MinisatSatSolver
+
+MinisatSatSolver::Statistics::Statistics() :
+  d_statStarts("theory::bv::bvminisat::starts"),
+  d_statDecisions("theory::bv::bvminisat::decisions"),
+  d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"),
+  d_statPropagations("theory::bv::bvminisat::propagations"),
+  d_statConflicts("theory::bv::bvminisat::conflicts"),
+  d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"),
+  d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"),
+  d_statMaxLiterals("theory::bv::bvminisat::max_literals"),
+  d_statTotLiterals("theory::bv::bvminisat::tot_literals"),
+  d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars")
+{
+  StatisticsRegistry::registerStat(&d_statStarts);
+  StatisticsRegistry::registerStat(&d_statDecisions);
+  StatisticsRegistry::registerStat(&d_statRndDecisions);
+  StatisticsRegistry::registerStat(&d_statPropagations);
+  StatisticsRegistry::registerStat(&d_statConflicts);
+  StatisticsRegistry::registerStat(&d_statClausesLiterals);
+  StatisticsRegistry::registerStat(&d_statLearntsLiterals);
+  StatisticsRegistry::registerStat(&d_statMaxLiterals);
+  StatisticsRegistry::registerStat(&d_statTotLiterals);
+  StatisticsRegistry::registerStat(&d_statEliminatedVars);
+}
+
+MinisatSatSolver::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_statStarts);
+  StatisticsRegistry::unregisterStat(&d_statDecisions);
+  StatisticsRegistry::unregisterStat(&d_statRndDecisions);
+  StatisticsRegistry::unregisterStat(&d_statPropagations);
+  StatisticsRegistry::unregisterStat(&d_statConflicts);
+  StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
+  StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
+  StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
+  StatisticsRegistry::unregisterStat(&d_statTotLiterals);
+  StatisticsRegistry::unregisterStat(&d_statEliminatedVars);
+}
+    
+void MinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
+  d_statStarts.setData(minisat->starts);
+  d_statDecisions.setData(minisat->decisions);
+  d_statRndDecisions.setData(minisat->rnd_decisions);
+  d_statPropagations.setData(minisat->propagations);
+  d_statConflicts.setData(minisat->conflicts);
+  d_statClausesLiterals.setData(minisat->clauses_literals);
+  d_statLearntsLiterals.setData(minisat->learnts_literals);
+  d_statMaxLiterals.setData(minisat->max_literals);
+  d_statTotLiterals.setData(minisat->tot_literals);
+  d_statEliminatedVars.setData(minisat->eliminated_vars);
+}
+
+
+
+//// DPllMinisatSatSolver
+
+DPLLMinisatSatSolver::DPLLMinisatSatSolver() :
+  d_minisat(NULL), 
+  d_theoryProxy(NULL),
+  d_context(NULL)
+{}
+
+DPLLMinisatSatSolver::~DPLLMinisatSatSolver() {
+  delete d_minisat; 
+}
+
+SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) {
+  if (var == var_Undef) {
+    return undefSatVariable; 
+  }
+  return SatVariable(var);
+}
+
+Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) {
+  if (lit == undefSatLiteral) {
+    return Minisat::lit_Undef;
+  }
+  return Minisat::mkLit(lit.getSatVariable(), lit.isNegated()); 
+}
+
+SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
+  if (lit == Minisat::lit_Undef) {
+    return undefSatLiteral; 
+  }
+  
+  return SatLiteral(SatVariable(Minisat::var(lit)),
+                    Minisat::sign(lit)); 
+}
+
+SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
+  if(res) return SatValTrue;
+  else return SatValFalse; 
+}
+
+SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
+  if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue;
+  if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown;
+  Assert(res == (Minisat::lbool((uint8_t)1)));
+  return SatValFalse; 
+}
+
+
+void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause,
+                                           Minisat::vec<Minisat::Lit>& minisat_clause) {
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    minisat_clause.push(toMinisatLit(clause[i])); 
+  }
+  Assert(clause.size() == (unsigned)minisat_clause.size()); 
+}
+
+void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
+                                       SatClause& sat_clause) {
+  for (int i = 0; i < clause.size(); ++i) {
+    sat_clause.push_back(toSatLiteral(clause[i])); 
+  }
+  Assert((unsigned)clause.size() == sat_clause.size()); 
+}
+
+
+void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
+{
+
+  d_context = context;
+  
+  // Create the solver
+  d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
+                                      options::incrementalSolving());
+  // Setup the verbosity
+  d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;
+
+  // Setup the random decision parameters
+  d_minisat->random_var_freq = options::satRandomFreq();
+  d_minisat->random_seed = options::satRandomSeed();
+  // Give access to all possible options in the sat solver
+  d_minisat->var_decay = options::satVarDecay();
+  d_minisat->clause_decay = options::satClauseDecay();
+  d_minisat->restart_first = options::satRestartFirst();
+  d_minisat->restart_inc = options::satRestartInc();
+
+  d_statistics.init(d_minisat);
+}
+
+void DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) {
+  Minisat::vec<Minisat::Lit> minisat_clause;
+  toMinisatClause(clause, minisat_clause); 
+  d_minisat->addClause(minisat_clause, removable);
+}
+
+SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) {
+  return d_minisat->newVar(true, true, theoryAtom);
+}
+
+  
+SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
+  Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
+  if(resource == 0) {
+    d_minisat->budgetOff();
+  } else {
+    d_minisat->setConfBudget(resource);
+  }
+  Minisat::vec<Minisat::Lit> empty;
+  unsigned long conflictsBefore = d_minisat->conflicts;
+  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
+  d_minisat->clearInterrupt();
+  resource = d_minisat->conflicts - conflictsBefore;
+  Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
+  return result;
+}
+
+SatLiteralValue DPLLMinisatSatSolver::solve() {
+  d_minisat->budgetOff();
+  return toSatLiteralValue(d_minisat->solve()); 
+}
+
+
+void DPLLMinisatSatSolver::interrupt() {
+  d_minisat->interrupt();
+}
+
+SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) {
+  return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
+}
+
+SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
+  return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
+}
+
+bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
+  return true;
+}
+
+/** Incremental interface */ 
+  
+int DPLLMinisatSatSolver::getAssertionLevel() const {
+  return d_minisat->getAssertionLevel(); 
+}
+  
+void DPLLMinisatSatSolver::push() {
+  d_minisat->push();
+}
+
+void DPLLMinisatSatSolver::pop(){
+  d_minisat->pop();
+}
+
+void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) {
+  d_minisat->unregisterVar(toMinisatLit(lit));
+}
+
+void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) {
+  d_minisat->renewVar(toMinisatLit(lit), level);
+}
+
+/// Statistics for DPLLMinisatSatSolver
+
+DPLLMinisatSatSolver::Statistics::Statistics() :
+  d_statStarts("sat::starts"),
+  d_statDecisions("sat::decisions"),
+  d_statRndDecisions("sat::rnd_decisions"),
+  d_statPropagations("sat::propagations"),
+  d_statConflicts("sat::conflicts"),
+  d_statClausesLiterals("sat::clauses_literals"),
+  d_statLearntsLiterals("sat::learnts_literals"),
+  d_statMaxLiterals("sat::max_literals"),
+  d_statTotLiterals("sat::tot_literals")
+{
+  StatisticsRegistry::registerStat(&d_statStarts);
+  StatisticsRegistry::registerStat(&d_statDecisions);
+  StatisticsRegistry::registerStat(&d_statRndDecisions);
+  StatisticsRegistry::registerStat(&d_statPropagations);
+  StatisticsRegistry::registerStat(&d_statConflicts);
+  StatisticsRegistry::registerStat(&d_statClausesLiterals);
+  StatisticsRegistry::registerStat(&d_statLearntsLiterals);
+  StatisticsRegistry::registerStat(&d_statMaxLiterals);
+  StatisticsRegistry::registerStat(&d_statTotLiterals);
+}
+DPLLMinisatSatSolver::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_statStarts);
+  StatisticsRegistry::unregisterStat(&d_statDecisions);
+  StatisticsRegistry::unregisterStat(&d_statRndDecisions);
+  StatisticsRegistry::unregisterStat(&d_statPropagations);
+  StatisticsRegistry::unregisterStat(&d_statConflicts);
+  StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
+  StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
+  StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
+  StatisticsRegistry::unregisterStat(&d_statTotLiterals);
+}
+void DPLLMinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
+  d_statStarts.setData(d_minisat->starts);
+  d_statDecisions.setData(d_minisat->decisions);
+  d_statRndDecisions.setData(d_minisat->rnd_decisions);
+  d_statPropagations.setData(d_minisat->propagations);
+  d_statConflicts.setData(d_minisat->conflicts);
+  d_statClausesLiterals.setData(d_minisat->clauses_literals);
+  d_statLearntsLiterals.setData(d_minisat->learnts_literals);
+  d_statMaxLiterals.setData(d_minisat->max_literals);
+  d_statTotLiterals.setData(d_minisat->tot_literals);
+}
+
+
+/*
+  
+  SatSolverFactory
+  
+ */
+
+MinisatSatSolver* SatSolverFactory::createMinisat() {
+  return new MinisatSatSolver(); 
+}
+
+DPLLMinisatSatSolver* SatSolverFactory::createDPLLMinisat(){
+  return new DPLLMinisatSatSolver(); 
+} 
+
+
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index c30f18d29..ac80e4422 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -23,7 +23,6 @@
 
 #include <string>
 #include <stdint.h>
-#include "util/options.h"
 #include "util/stats.h"
 #include "context/cdlist.h"
 #include "prop/sat_solver_types.h"
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 10d2aee8c..9ed2202fe 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -25,6 +25,7 @@
 #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"
 
@@ -94,7 +95,7 @@ SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) {
   if(stopSearch) {
     Trace("decision") << "  ***  Decision Engine stopped search *** " << std::endl;
   }
-  return Options::current()->decisionOptions.stopOnly ? undefSatLiteral : ret;
+  return options::decisionStopOnly() ? undefSatLiteral : ret;
 }
 
 bool TheoryProxy::theoryNeedCheck() const {
@@ -115,10 +116,10 @@ void TheoryProxy::notifyRestart() {
 
   static uint32_t lemmaCount = 0;
 
-  if(Options::current()->lemmaInputChannel != NULL) {
-    while(Options::current()->lemmaInputChannel->hasNewLemma()) {
+  if(options::lemmaInputChannel() != NULL) {
+    while(options::lemmaInputChannel()->hasNewLemma()) {
       Debug("shared") << "shared" << std::endl;
-      Expr lemma = Options::current()->lemmaInputChannel->getNewLemma();
+      Expr lemma = options::lemmaInputChannel()->getNewLemma();
       Node asNode = lemma.getNode();
       asNode = theory::Rewriter::rewrite(asNode);
 
@@ -142,10 +143,10 @@ void TheoryProxy::notifyRestart() {
 
 void TheoryProxy::notifyNewLemma(SatClause& lemma) {
   Assert(lemma.size() > 0);
-  if(Options::current()->lemmaOutputChannel != NULL) {
+  if(options::lemmaOutputChannel() != NULL) {
     if(lemma.size() == 1) {
       // cannot share units yet
-      //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr());
+      //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr());
     } else {
       NodeBuilder<> b(kind::OR);
       for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) {
@@ -155,7 +156,7 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) {
 
       if(d_shared.find(n) == d_shared.end()) {
         d_shared.insert(n);
-        Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr());
+        options::lemmaOutputChannel()->notifyNewLemma(n.toExpr());
       } else {
         Debug("shared") <<"drop new " << n << std::endl;
       }
@@ -165,8 +166,8 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) {
 
 SatLiteral TheoryProxy::getNextReplayDecision() {
 #ifdef CVC4_REPLAY
-  if(Options::current()->replayStream != NULL) {
-    Expr e = Options::current()->replayStream->nextExpr();
+  if(options::replayStream() != NULL) {
+    Expr e = options::replayStream()->nextExpr();
     if(!e.isNull()) { // we get null node when out of decisions to replay
       // convert & return
       return d_cnfStream->getLiteral(e);
@@ -179,9 +180,9 @@ SatLiteral TheoryProxy::getNextReplayDecision() {
 
 void TheoryProxy::logDecision(SatLiteral lit) {
 #ifdef CVC4_REPLAY
-  if(Options::current()->replayLog != NULL) {
+  if(options::replayLog() != NULL) {
     Assert(lit != undefSatLiteral, "logging an `undef' decision ?!");
-    *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl;
+    *options::replayLog() << d_cnfStream->getNode(lit) << std::endl;
   }
 #endif /* CVC4_REPLAY */
 }
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 26357886c..e8da202bd 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -26,7 +26,6 @@
 #define __CVC4_USE_MINISAT
 
 #include "theory/theory.h"
-#include "util/options.h"
 #include "util/stats.h"
 
 #include "context/cdqueue.h"