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.

9 files changed, 269 insertions, 35 deletions

diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am
index 4f454e9bf..5f62568ee 100644
--- a/src/decision/Makefile.am
+++ b/src/decision/Makefile.am
@@ -6,6 +6,8 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 noinst_LTLIBRARIES = libdecision.la
 
 libdecision_la_SOURCES = \
+	decision_mode.h \
+	decision_mode.cpp \
 	decision_engine.h \
 	decision_engine.cpp \
 	decision_strategy.h \
@@ -13,3 +15,6 @@ libdecision_la_SOURCES = \
 	justification_heuristic.cpp \
 	relevancy.h \
 	relevancy.cpp
+
+EXTRA_DIST = \
+	options_handlers.h
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index b42f69b7f..2832a9577 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -21,7 +21,10 @@
 #include "decision/relevancy.h"
 
 #include "expr/node.h"
-#include "util/options.h"
+#include "decision/options.h"
+#include "decision/decision_mode.h"
+
+#include "smt/options.h"
 
 using namespace std;
 
@@ -49,24 +52,23 @@ void DecisionEngine::init()
   d_engineState = 1;
 
   Trace("decision-init") << "DecisionEngine::init()" << std::endl;
-  const Options* options = Options::current();
-  if(options->incrementalSolving) return;
+  if(options::incrementalSolving()) return;
 
   Trace("decision-init") << " * options->decisionMode: " 
-                         << options->decisionMode << std:: endl;
-  Trace("decision-init") << " * options->decisionOptions.stopOnly: "
-                         << ((options->decisionOptions).stopOnly) << std::endl;
+                         << options::decisionMode() << std:: endl;
+  Trace("decision-init") << " * options->decisionStopOnly: "
+                         << options::decisionStopOnly() << std::endl;
 
-  if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
-  if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
+  if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { }
+  if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) {
     ITEDecisionStrategy* ds = 
       new decision::JustificationHeuristic(this, d_satContext);
     enableStrategy(ds);
     d_needIteSkolemMap.push_back(ds);
   }
-  if(options->decisionMode == Options::DECISION_STRATEGY_RELEVANCY) {
+  if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) {
     RelevancyStrategy* ds = 
-      new decision::Relevancy(this, d_satContext, options->decisionOptions);
+      new decision::Relevancy(this, d_satContext);
     enableStrategy(ds);
     d_needIteSkolemMap.push_back(ds);
     d_relevancyStrategy = ds;
diff --git a/src/decision/decision_mode.cpp b/src/decision/decision_mode.cpp
new file mode 100644
index 000000000..c4bb58b93
--- /dev/null
+++ b/src/decision/decision_mode.cpp
@@ -0,0 +1,40 @@
+/*********************                                                        */
+/*! \file decision_mode.cpp
+ ** \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 "decision/decision_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) {
+  switch(mode) {
+  case decision::DECISION_STRATEGY_INTERNAL:
+    out << "DECISION_STRATEGY_INTERNAL";
+    break;
+  case decision::DECISION_STRATEGY_JUSTIFICATION:
+    out << "DECISION_STRATEGY_JUSTIFICATION";
+    break;
+  default:
+    out << "DecisionMode:UNKNOWN![" << unsigned(mode) << "]";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
diff --git a/src/decision/decision_mode.h b/src/decision/decision_mode.h
new file mode 100644
index 000000000..f6dba32ea
--- /dev/null
+++ b/src/decision/decision_mode.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file decision_mode.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** 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__SMT__DECISION_MODE_H
+#define __CVC4__SMT__DECISION_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+namespace decision {
+
+/** Enumeration of decision strategies */
+enum DecisionMode {
+
+  /**
+   * Decision engine doesn't do anything. Use sat solver's internal
+   * heuristics
+   */
+  DECISION_STRATEGY_INTERNAL,
+
+  /**
+   * Use the justification heuristic
+   */
+  DECISION_STRATEGY_JUSTIFICATION,
+
+  /**
+   * Use may-relevancy.
+   */
+  DECISION_STRATEGY_RELEVANCY
+
+};/* enum DecisionMode */
+
+}/* CVC4::decision namespace */
+
+std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__DECISION_MODE_H */
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index ee7d340c4..dd6c7f548 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -27,8 +27,8 @@ namespace CVC4 {
 class DecisionEngine;
 
 namespace context {
-class Context;
-}
+  class Context;
+}/* CVC4::context namespace */
 
 namespace decision {
 
@@ -47,7 +47,7 @@ public:
   virtual bool needIteSkolemMap() { return false; }
   
   virtual void notifyAssertionsAvailable() { return; }
-};
+};/* class DecisionStrategy */
 
 class ITEDecisionStrategy : public DecisionStrategy {
 public:
@@ -61,7 +61,7 @@ public:
   virtual void addAssertions(const std::vector<Node> &assertions,
                              unsigned assertionsEnd,
                              IteSkolemMap iteSkolemMap) = 0;
-};
+};/* class ITEDecisionStrategy */
 
 class RelevancyStrategy : public ITEDecisionStrategy {
 public:
@@ -71,10 +71,9 @@ public:
 
   virtual bool isRelevant(TNode n) = 0;
   virtual prop::SatValue getPolarity(TNode n) = 0;
-};
+};/* class RelevancyStrategy */
 
-
-}/* decision namespace */
+}/* CVC4::decision namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__DECISION__DECISION_STRATEGY_H */
diff --git a/src/decision/options b/src/decision/options
new file mode 100644
index 000000000..7e457f125
--- /dev/null
+++ b/src/decision/options
@@ -0,0 +1,23 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module DECISION "decision/options.h" Decision heuristics
+
+# When/whether to use any decision strategies
+option decisionMode --decision=MODE decision::DecisionMode :handler CVC4::decision::stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "decision/decision_mode.h" :handler-include "decision/options_handlers.h"
+ choose decision mode, see --decision=help
+
+option decisionRelevancyLeaves bool
+# permille = part per thousand
+option decisionMaxRelTimeAsPermille --decision-budget=N "unsigned short" :read-write :predicate less_equal(1000L) :predicate CVC4::decision::checkDecisionBudget :predicate-include "decision/options_handlers.h"
+ impose a budget for relevancy heuristic which increases linearly with each decision. N between 0 and 1000. (default: 1000, no budget)
+# if false, do justification stuff using relevancy.h
+option decisionComputeRelevancy bool
+# use the must be relevant
+option decisionMustRelevancy bool
+# only use DE to determine when to stop, not to make decisions
+option decisionStopOnly bool
+
+endmodule
diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h
new file mode 100644
index 000000000..e9f227043
--- /dev/null
+++ b/src/decision/options_handlers.h
@@ -0,0 +1,112 @@
+/*********************                                                        */
+/*! \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, 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 Custom handlers and predicates for DecisionEngine options
+ **
+ ** Custom handlers and predicates for DecisionEngine options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__DECISION__OPTIONS_HANDLERS_H
+#define __CVC4__DECISION__OPTIONS_HANDLERS_H
+
+#include "decision/decision_mode.h"
+#include "main/options.h"
+
+namespace CVC4 {
+namespace decision {
+
+static const std::string decisionModeHelp = "\
+Decision modes currently supported by the --decision option:\n\
+\n\
+internal (default)\n\
++ Use the internal decision hueristics of the SAT solver\n\
+\n\
+justification\n\
++ An ATGP-inspired justification heuristic\n\
+\n\
+justification-stoponly\n\
++ Use the justification heuristic only to stop early, not for decisions\n\
+\n\
+relevancy\n\
++ Under development may-relevancy\n\
+\n\
+relevancy-leaves\n\
++ May-relevancy, but decide only on leaves\n\
+\n\
+Developer modes:\n\
+\n\
+justification-rel\n\
++ Use the relevancy code to do the justification stuff\n\
++ (This should do exact same thing as justification)\n\
+\n\
+justification-must\n\
++ Start deciding on literals close to root instead of those\n\
++ near leaves (don't expect it to work well) [Unimplemented]\n\
+";
+
+inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  options::decisionRelevancyLeaves.set(false);
+  options::decisionMaxRelTimeAsPermille.set(1000);
+  options::decisionComputeRelevancy.set(true);
+  options::decisionMustRelevancy.set(false);
+  options::decisionStopOnly.set(false);
+
+  if(optarg == "internal") {
+    return DECISION_STRATEGY_INTERNAL;
+  } else if(optarg == "justification") {
+    return DECISION_STRATEGY_JUSTIFICATION;
+  } else if(optarg == "justification-stoponly") {
+    options::decisionStopOnly.set(true);
+    return DECISION_STRATEGY_JUSTIFICATION;
+  } else if(optarg == "relevancy") {
+    options::decisionRelevancyLeaves.set(false);
+    return DECISION_STRATEGY_RELEVANCY;
+  } else if(optarg == "relevancy-leaves") {
+    options::decisionRelevancyLeaves.set(true);
+    Trace("options") << "version is " << options::version() << std::endl;
+    return DECISION_STRATEGY_RELEVANCY;
+  } else if(optarg == "justification-rel") {
+    // relevancyLeaves : irrelevant
+    // maxRelTimeAsPermille : irrelevant
+    options::decisionComputeRelevancy.set(false);
+    options::decisionMustRelevancy.set(false);
+    return DECISION_STRATEGY_RELEVANCY;
+  } else if(optarg == "justification-must") {
+    // relevancyLeaves : irrelevant
+    // maxRelTimeAsPermille : irrelevant
+    options::decisionComputeRelevancy.set(false);
+    options::decisionMustRelevancy.set(true);
+    return DECISION_STRATEGY_RELEVANCY;
+  } else if(optarg == "help") {
+    puts(decisionModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --decision: `") +
+                          optarg + "'.  Try --decision help.");
+  }
+}
+
+inline void checkDecisionBudget(std::string option, unsigned short budget, SmtEngine* smt) throw(OptionException) {
+  if(budget == 0) {
+    Warning() << "Decision budget is 0. Consider using internal decision heuristic and "
+              << std::endl << " removing this option." << std::endl;
+              
+  }
+}
+
+}/* CVC4::decision namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DECISION__OPTIONS_HANDLERS_H */
diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp
index d0d44f606..fe5bdcc20 100644
--- a/src/decision/relevancy.cpp
+++ b/src/decision/relevancy.cpp
@@ -34,7 +34,7 @@ void Relevancy::setJustified(TNode n)
 {
   Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl;
   d_justified.insert(n);
-  if(d_opt.computeRelevancy) {
+  if(options::decisionComputeRelevancy()) {
     d_relevancy[n] = d_maxRelevancy[n];
     updateRelevancy(n);
   }
@@ -117,7 +117,7 @@ bool Relevancy::findSplitterRec(TNode node,
   if(d_polarityCache.find(node) == d_polarityCache.end()) {
     d_polarityCache[node] = desiredVal;
   } else {
-    Assert(d_multipleBacktrace || d_opt.computeRelevancy);
+    Assert(d_multipleBacktrace || options::decisionComputeRelevancy());
     return true;
   }
 
@@ -289,7 +289,7 @@ bool Relevancy::handleOrFalse(TNode node, SatValue desiredVal) {
   bool ret = false;
   for(int i = 0; i < n; ++i) {
     if (findSplitterRec(node[i], desiredVal)) {
-      if(!d_opt.computeRelevancy) 
+      if(!options::decisionComputeRelevancy()) 
         return true;
       else
         ret = true;
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
index f45ce2e8f..a529b974e 100644
--- a/src/decision/relevancy.h
+++ b/src/decision/relevancy.h
@@ -35,12 +35,12 @@
 
 #include "decision_engine.h"
 #include "decision_strategy.h"
+#include "decision/options.h"
 
 #include "context/cdhashset.h"
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "prop/sat_solver_types.h"
-#include "util/options.h"
 
 namespace CVC4 {
 
@@ -109,9 +109,6 @@ class Relevancy : public RelevancyStrategy {
   bool d_multipleBacktrace;
   //bool d_computeRelevancy;     // are we in a mode where we compute relevancy?
 
-  /** Only leaves can be relevant */
-  Options::DecisionOptions d_opt;        // may be we shouldn't be caching them?
-
   static const double secondsPerDecision = 0.001;
   static const double secondsPerExpense = 1e-7;
   static const double EPS = 1e-9;
@@ -121,7 +118,7 @@ class Relevancy : public RelevancyStrategy {
   /** current decision for the recursive call */
   SatLiteral* d_curDecision;
 public:
-  Relevancy(CVC4::DecisionEngine* de, context::Context *c, const Options::DecisionOptions &decOpt):
+  Relevancy(CVC4::DecisionEngine* de, context::Context *c):
     RelevancyStrategy(de, c),
     d_justified(c),
     d_prvsIndex(c, 0),
@@ -132,10 +129,9 @@ public:
     d_expense("decision::rel::expense", 0),
     d_timestat("decision::rel::time"),
     d_relevancy(c),
-    d_multipleBacktrace(decOpt.computeRelevancy),
+    d_multipleBacktrace(options::decisionComputeRelevancy()),
     //    d_computeRelevancy(decOpt.computeRelevancy),
-    d_opt(decOpt),
-    d_maxTimeAsPercentageOfTotalTime(decOpt.maxRelTimeAsPermille*1.0/10.0),
+    d_maxTimeAsPercentageOfTotalTime(options::decisionMaxRelTimeAsPermille()*1.0/10.0),
     d_curDecision(NULL)
   {
     Warning() << "There are known bugs in this Relevancy code which we know"
@@ -149,11 +145,11 @@ public:
     StatisticsRegistry::registerStat(&d_expense);
     StatisticsRegistry::registerStat(&d_timestat);
     Trace("decision") << "relevancy enabled with" << std::endl;
-    Trace("decision") << "  * computeRelevancy: " << (d_opt.computeRelevancy ? "on" : "off")
+    Trace("decision") << "  * computeRelevancy: " << (options::decisionComputeRelevancy() ? "on" : "off")
                       << std::endl;
-    Trace("decision") << "  * relevancyLeaves: " << (d_opt.relevancyLeaves ? "on" : "off")
+    Trace("decision") << "  * relevancyLeaves: " << (options::decisionRelevancyLeaves() ? "on" : "off")
                       << std::endl;
-    Trace("decision") << "  * mustRelevancy [unimplemented]: " << (d_opt.mustRelevancy ? "on" : "off")
+    Trace("decision") << "  * mustRelevancy [unimplemented]: " << (options::decisionMustRelevancy() ? "on" : "off")
                       << std::endl;
   }
   ~Relevancy() {
@@ -189,13 +185,13 @@ public:
       SatValue desiredVal = SAT_VALUE_TRUE;
       SatLiteral litDecision = findSplitter(d_assertions[i], desiredVal);
 
-      if(!d_opt.computeRelevancy && litDecision != undefSatLiteral) {
+      if(!options::decisionComputeRelevancy() && litDecision != undefSatLiteral) {
         d_prvsIndex = i;
         return litDecision;
       }
     }
 
-    if(d_opt.computeRelevancy) return undefSatLiteral;
+    if(options::decisionComputeRelevancy()) return undefSatLiteral;
 
     Trace("decision") << "jh: Nothing to split on " << std::endl;
 
@@ -244,7 +240,7 @@ public:
     for(unsigned i = 0; i < assertionsEnd; ++i) {
       d_assertions.push_back(assertions[i]);
       d_visited.clear();
-      if(d_opt.computeRelevancy) increaseMaxRelevancy(assertions[i]);
+      if(options::decisionComputeRelevancy()) increaseMaxRelevancy(assertions[i]);
       d_visited.clear();
     }
 
@@ -267,7 +263,7 @@ public:
       return true;
     }
     
-    if(d_opt.relevancyLeaves && !isAtomicFormula(n)) {
+    if(options::decisionRelevancyLeaves() && !isAtomicFormula(n)) {
       Trace("decision") << "no [not a leaf]" << std::endl;
       return false;
     }