Merge branch 'master' into archiveRunScriptsarchiveRunScripts

22 files changed, 783 insertions, 593 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index bec3a8345..2419e1e41 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -441,6 +441,7 @@ libcvc5_add_sources(
   theory/arith/nl/nonlinear_extension.h
   theory/arith/nl/poly_conversion.cpp
   theory/arith/nl/poly_conversion.h
+  theory/arith/nl/pow2_solver.cpp
   theory/arith/nl/pow2_solver.h
   theory/arith/nl/stats.cpp
   theory/arith/nl/stats.h
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 2ec190360..2c5d2873e 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -412,6 +412,22 @@ enum CVC5_EXPORT Kind : int32_t
    *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
    */
   IAND,
+  /**
+   * Operator for raising 2 to a non-negative integer  power
+   *
+   * Create with:
+   *   - `Solver::mkOp(Kind kind) const`
+   *
+
+   * Parameters:
+   *   - 1: Op of kind IAND
+   *   - 2: Integer term
+   *
+   * Create with:
+   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
+   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   */
+  POW2,
 #if 0
   /* Synonym for MULT.  */
   NONLINEAR_MULT,
diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp
index bce6c9b6d..01cb6da42 100644
--- a/src/omt/bitvector_optimizer.cpp
+++ b/src/omt/bitvector_optimizer.cpp
@@ -53,15 +53,13 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker,
   Result intermediateSatResult = optChecker->checkSat();
   // Model-value of objective (used in optimization loop)
   Node value;
-  if (intermediateSatResult.isUnknown())
+  if (intermediateSatResult.isUnknown()
+      || intermediateSatResult.isSat() == Result::UNSAT)
   {
-    return OptimizationResult(OptimizationResult::UNKNOWN, value);
+    return OptimizationResult(intermediateSatResult, value);
   }
-  if (intermediateSatResult.isSat() == Result::UNSAT)
-  {
-    return OptimizationResult(OptimizationResult::UNSAT, value);
-  }
-
+  // the last result that is SAT
+  Result lastSatResult = intermediateSatResult;
   // value equals to upperBound
   value = optChecker->getValue(target);
 
@@ -104,39 +102,35 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker,
                      nm->mkNode(LTOperator, target, nm->mkConst(pivot))));
     }
     intermediateSatResult = optChecker->checkSat();
-    if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
-    {
-      optChecker->pop();
-      return OptimizationResult(OptimizationResult::UNKNOWN, value);
-    }
-    if (intermediateSatResult.isSat() == Result::SAT)
+    switch (intermediateSatResult.isSat())
     {
-      value = optChecker->getValue(target);
-      upperBound = value.getConst<BitVector>();
-    }
-    else if (intermediateSatResult.isSat() == Result::UNSAT)
-    {
-      if (lowerBound == pivot)
-      {
-        // lowerBound == pivot ==> upperbound = lowerbound + 1
-        // and lowerbound <= target < upperbound is UNSAT
-        // return the upperbound
+      case Result::SAT_UNKNOWN:
         optChecker->pop();
-        return OptimizationResult(OptimizationResult::OPTIMAL, value);
-      }
-      else
-      {
-        lowerBound = pivot;
-      }
-    }
-    else
-    {
-      optChecker->pop();
-      return OptimizationResult(OptimizationResult::UNKNOWN, value);
+        return OptimizationResult(intermediateSatResult, value);
+      case Result::SAT:
+        lastSatResult = intermediateSatResult;
+        value = optChecker->getValue(target);
+        upperBound = value.getConst<BitVector>();
+        break;
+      case Result::UNSAT:
+        if (lowerBound == pivot)
+        {
+          // lowerBound == pivot ==> upperbound = lowerbound + 1
+          // and lowerbound <= target < upperbound is UNSAT
+          // return the upperbound
+          optChecker->pop();
+          return OptimizationResult(lastSatResult, value);
+        }
+        else
+        {
+          lowerBound = pivot;
+        }
+        break;
+      default: Unreachable();
     }
     optChecker->pop();
   }
-  return OptimizationResult(OptimizationResult::OPTIMAL, value);
+  return OptimizationResult(lastSatResult, value);
 }
 
 OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
@@ -148,15 +142,13 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
   Result intermediateSatResult = optChecker->checkSat();
   // Model-value of objective (used in optimization loop)
   Node value;
-  if (intermediateSatResult.isUnknown())
+  if (intermediateSatResult.isUnknown()
+      || intermediateSatResult.isSat() == Result::UNSAT)
   {
-    return OptimizationResult(OptimizationResult::UNKNOWN, value);
+    return OptimizationResult(intermediateSatResult, value);
   }
-  if (intermediateSatResult.isSat() == Result::UNSAT)
-  {
-    return OptimizationResult(OptimizationResult::UNSAT, value);
-  }
-
+  // the last result that is SAT
+  Result lastSatResult = intermediateSatResult;
   // value equals to upperBound
   value = optChecker->getValue(target);
 
@@ -196,39 +188,35 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
                    nm->mkNode(GTOperator, target, nm->mkConst(pivot)),
                    nm->mkNode(LEOperator, target, nm->mkConst(upperBound))));
     intermediateSatResult = optChecker->checkSat();
-    if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
-    {
-      optChecker->pop();
-      return OptimizationResult(OptimizationResult::UNKNOWN, value);
-    }
-    if (intermediateSatResult.isSat() == Result::SAT)
+    switch (intermediateSatResult.isSat())
     {
-      value = optChecker->getValue(target);
-      lowerBound = value.getConst<BitVector>();
-    }
-    else if (intermediateSatResult.isSat() == Result::UNSAT)
-    {
-      if (lowerBound == pivot)
-      {
-        // upperbound = lowerbound + 1
-        // and lowerbound < target <= upperbound is UNSAT
-        // return the lowerbound
+      case Result::SAT_UNKNOWN:
         optChecker->pop();
-        return OptimizationResult(OptimizationResult::OPTIMAL, value);
-      }
-      else
-      {
-        upperBound = pivot;
-      }
-    }
-    else
-    {
-      optChecker->pop();
-      return OptimizationResult(OptimizationResult::UNKNOWN, value);
+        return OptimizationResult(intermediateSatResult, value);
+      case Result::SAT:
+        lastSatResult = intermediateSatResult;
+        value = optChecker->getValue(target);
+        lowerBound = value.getConst<BitVector>();
+        break;
+      case Result::UNSAT:
+        if (lowerBound == pivot)
+        {
+          // upperbound = lowerbound + 1
+          // and lowerbound < target <= upperbound is UNSAT
+          // return the lowerbound
+          optChecker->pop();
+          return OptimizationResult(lastSatResult, value);
+        }
+        else
+        {
+          upperBound = pivot;
+        }
+        break;
+      default: Unreachable();
     }
     optChecker->pop();
   }
-  return OptimizationResult(OptimizationResult::OPTIMAL, value);
+  return OptimizationResult(lastSatResult, value);
 }
 
 }  // namespace cvc5::omt
diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp
index 045268337..379b0cd43 100644
--- a/src/omt/integer_optimizer.cpp
+++ b/src/omt/integer_optimizer.cpp
@@ -33,13 +33,10 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
   Result intermediateSatResult = optChecker->checkSat();
   // Model-value of objective (used in optimization loop)
   Node value;
-  if (intermediateSatResult.isUnknown())
+  if (intermediateSatResult.isUnknown()
+      || intermediateSatResult.isSat() == Result::UNSAT)
   {
-    return OptimizationResult(OptimizationResult::UNKNOWN, value);
-  }
-  if (intermediateSatResult.isSat() == Result::UNSAT)
-  {
-    return OptimizationResult(OptimizationResult::UNSAT, value);
+    return OptimizationResult(intermediateSatResult, value);
   }
   // node storing target > old_value (used in optimization loop)
   Node increment;
@@ -56,12 +53,14 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
     // then assert optimization_target > current_model_value
     incrementalOperator = kind::GT;
   }
+  Result lastSatResult = intermediateSatResult;
   // Workhorse of linear search:
   // This loop will keep incrmenting/decrementing the objective until unsat
   // When unsat is hit,
   // the optimized value is the model value just before the unsat call
   while (intermediateSatResult.isSat() == Result::SAT)
   {
+    lastSatResult = intermediateSatResult;
     value = optChecker->getValue(target);
     Assert(!value.isNull());
     increment = nm->mkNode(incrementalOperator, target, value);
@@ -69,7 +68,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
     intermediateSatResult = optChecker->checkSat();
   }
   optChecker->pop();
-  return OptimizationResult(OptimizationResult::OPTIMAL, value);
+  return OptimizationResult(lastSatResult, value);
 }
 
 OptimizationResult OMTOptimizerInteger::minimize(SmtEngine* optChecker,
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 26ced1a24..cc7b621a8 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -17,7 +17,6 @@
 check_python_module("toml")
 
 libcvc5_add_sources(
-  base_handlers.h
   decision_weight.h
   didyoumean.cpp
   didyoumean.h
diff --git a/src/options/README b/src/options/README
deleted file mode 100644
index 868690b85..000000000
--- a/src/options/README
+++ /dev/null
@@ -1,127 +0,0 @@
-Modules
-=======
-
-  Each options module starts with the following required attributes:
-
-    id     ... (string) ID of the module (e.g., "ARITH")
-    name   ... (string) name of the module (e.g., "Arithmetic Theory")
-    header ... (string) name of the options header to generated (e.g., "options/arith_options.h")
-
-  A module defines 0 or more options.
-
-  In general, each attribute/value pair is required to be in one line.
-  Comments start with # and are not allowed in attribute/value lines.
-
-
-Options
-=======
-
-  Options can be defined with the [[option]] tag, the required attributes for
-  an option are:
-
-    category ... (string) common | expert | regular | undocumented
-    type     ... (string) C++ type of the option value
-
-  Optional attributes are:
-
-    name       ... (string) option name that is used to access via
-                            options::<name>()
-    smt_name   ... (string) alternative name to access option via
-                            set-option/get-option commands
-    short      ... (string) short option name consisting of one character
-                            (no '-' prefix required)
-    long       ... (string) long option name (required if short is specified,
-                            no '--' prefix required).
-                            long option names may have a suffix '=XXX' where
-                            'XXX' can be used to indicate the type of the
-                            option value, e.g., '=MODE', '=LANG', '=N', ...
-    default    ... (string) default value of type 'type'
-    handler    ... (string) handler for parsing option values before setting
-                            option
-    predicates ... (list)   functions that check whether given option value is
-                            valid
-    includes   ... (list)   header files required by handler/predicates
-    alternate  ... (bool)   true (default): add --no-<long> alternative option
-                            false: omit --no-<long> alternative option
-    help       ... (string) documentation (required if category is not
-                            undocumented)
-
-  Note that if an option defines a long option name with type 'bool',
-  mkoptions.py automatically generates a --no-<long> option to set the option
-  to false.
-  This behaviour can be explicitely disabled for options with attribute
-  alternate = false.
-  More information on how to use handler and predicates can be found
-  at the end of the README.
-
-
-  Example:
-
-    [[option]]
-      name       = "outputLanguage"
-      smt_name   = "output-language"
-      category   = "common"
-      short      = ""
-      long       = "output-lang=LANG"
-      type       = "OutputLanguage"
-      default    = "language::output::LANG_AUTO"
-      handler    = "stringToOutputLanguage"
-      predicates = []
-      includes   = ["options/language.h"]
-      help       = "force output language (default is \"auto\"; see --output-lang help)"
-
-
-Further information (the old option package)
-============================================
-
-  The options/ package supports a wide range of operations for responding to
-  an option being set. Roughly the three major concepts are:
-
-   - handler to parse an option before setting its value.
-   - predicates to reject bad values for the option.
-
-  More details on each class of custom handlers.
-
-   - handler = ""
-
-    Handlers provide support for parsing custom option types.
-    The signature for a handler call is:
-
-       T custom-option-handler(std::string option, std::string optarg,
-                               OptionsHandler* handler);
-
-    where T is the type of the option. The suggested implementation is to
-    implement custom-handler as a dispatch into a function on handler with the
-    signature:
-
-       T OptionsHandler::custom-option-handler(std::string option,
-                                               std::string optarg);
-
-    The handlers are run before predicates.
-    Having multiple handlers is considered bad practice and is unsupported.
-    Handlers may have arbitrary side effects, but should call no code
-    inaccessible to liboptions. For side effects that are not required in order
-    to parse the option, using :predicate is recommended. Memory
-    management done by a handler needs to either be encapsulated by the type
-    and the destructor for the type or should *always* be owned by handler.
-    More elaborate memory management schemes are not currently supported.
-
-   - predicates = [...]
-
-    Predicates provide support for checking whether or not the value of an
-    option is acceptable. Predicates are run after handlers.
-    The signature for a predicate call is:
-
-      void custom-predicate(std::string option, T value,
-                            OptionsHandler* handler);
-
-    where T is the type of the option. The suggested implementation is to
-    implement custom-predicate as a dispatch into a function on handler with
-    the signature:
-
-      void OptionsHandler::custom-predicate(std::string option, T value);
-
-    The predicates are run after handlers. Multiple
-    predicates may be defined for the same option, but the order they are run
-    is not guaranteed. Predicates may have arbitrary side effects, but should
-    call no code inaccessible to liboptions.
diff --git a/src/options/README.md b/src/options/README.md
new file mode 100644
index 000000000..df5686abc
--- /dev/null
+++ b/src/options/README.md
@@ -0,0 +1,211 @@
+Specifying Modules
+==================
+
+Every options module, that is a group of options that belong together in some
+way, is declared in its own file in `options/{module name}_options.toml`. Each
+options module starts with the following required attributes:
+
+* `id` (string): ID of the module (e.g., `"arith"`)
+* `name` (string): name of the module (e.g., `"Arithmetic Theory"`)
+
+Additional, a module can optionally be defined to be public. A public module
+includes `cvc5_public.h` instead of `cvc5_private.h` can thus be included from
+"external" code like the parser or the main driver.
+
+* `public` (bool): make option module public
+
+A module defines 0 or more options.
+
+In general, each attribute/value pair is required to be in one line. Comments
+start with # and are not allowed in attribute/value lines.
+
+After parsing, a module is extended to have the following attributes:
+
+* `id`: lower-case version of the parsed `id`
+* `id_cap`: upper-case version of `id` (used for the `Holder{id_cap}` class)
+* `filename`: base filename for generated files (`"{id}_options"`)
+* `header`: generated header name (`"options/{filename}.h"`)
+
+
+Specifying Options
+==================
+
+Options can be defined within a module file with the `[[option]]` tag, the
+required attributes for an option are:
+
+* `category` (string): one of `common`, `expert`, `regular`, or `undocumented`
+* `type` (string): the C++ type of the option value
+
+Optional attributes are:
+
+* `name` (string): the option name used to access the option internally
+  (`d_option.{module.id}.{name}`)
+* `long` (string): long option name (without `--` prefix). Long option names may
+  have a suffix `=XXX` where `XXX` can be used to indicate the type of the
+  option value, e.g., `=MODE`, `=LANG`, `=N`, ...
+* `short` (string): short option name consisting of one character (no `-` prefix
+  required), can be given if `long` is specified
+* `alias` (list): alternative names that can be used instead of `long`
+* `default` (string): default value, needs to be a valid C++ expression of type
+  `type`
+* `alternate` (bool, default `true`): if `true`, adds `--no-{long}` alternative
+  option
+* `mode` (list): used to define options whose type shall be an auto-generated
+  enum, more details below
+* `handler` (string): alternate parsing routine for option types not covered by
+  the default parsers, more details below
+* `predicates` (list): custom validation function to check whether an option
+  value is valid, more details below
+* `includes` (list): additional header files required by handler or predicate
+  functions
+* `help` (string): documentation string (required, unless the `category` is
+  `undocumented`)
+* `help_mode` (string): documentation for the mode enum (required if `mode` is
+  given)
+
+
+Handler functions
+-----------------
+
+Custom handler functions are used to turn the option value from a `std::string`
+into the type specified by `type`. Standard handler functions are provided for
+basic types (`std::string`, `bool`, integer types and floating point types) as
+well as enums specified by `mode`. A custom handler function needs to be member
+function of `options::OptionsHandler` with signature `{type} {handler}(const
+std::string& option, const std::string& flag, const std::string& optionvalue)`,
+or alternatively `void {handler}(const std::string& option, const std::string&
+flag)` if the `type` is `void`. The two parameters `option` and `flag` hold the
+canonical and the actually used option names, respectively, and they may differ
+if an alternative name (from `alias`) was used. While `option` should be used to
+identify an option (e.g. by comparing against `*__name`), `flag` should be
+usually used in user messages.
+
+
+Predicate functions
+-------------------
+
+Predicate functions are used to check whether an option value is valid after it
+has been parsed by a (standard or custom) handler function. Like a handler
+function, a predicate function needs to be a member function of
+`options::OptionsHandler` with signature `void {predicate}(const std::string&
+option, const std::string& flag, {type} value)`. If the check fails, the
+predicate should raise an `OptionException`.
+
+
+Mode options
+------------
+
+An option can be defined to hold one of a given set of values we call modes.
+Doing so automatically defines an `enum class` for the set of modes and makes
+the option accept one of the values from the enum. The enum class will be called
+`{type}` and methods `operator<<` and `stringTo{enum}` are automatically
+generated. A mode is defined by specifying `[[option.mode.{NAME}]]` after the
+main `[[option]]` section with the following attributes:
+
+* `name` (string): the string value that corresponds to the enum value
+* `help` (string): documentation about this mode
+
+Example:
+
+    [[option]]
+        name       = "bitblastMode"
+        category   = "regular"
+        long       = "bitblast=MODE"
+        type       = "BitblastMode"
+        default    = "LAZY"
+        help       = "choose bitblasting mode, see --bitblast=help"
+        help_mode  = "Bit-blasting modes."
+    [[option.mode.LAZY]]
+        name = "lazy"
+        help = "Separate boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver."
+    [[option.mode.EAGER]]
+        name = "eager"
+        help = "Bitblast eagerly to bit-vector SAT solver."
+
+The option can now be set with `--bitblast=lazy`, `(set-option :bitblast
+eager)`, or `options::set("bitblast", "eager")`.
+
+
+Generated code
+==============
+
+The entire options setup heavily relies on generating a lot of code from the
+information retrieved from the `*_options.toml` files. After code generation,
+files related to options live either in `src/options/` (if not changed) or in
+`build/src/options/` (if automatically generated). After all code has been
+generated, the entire options setup consists of the following components:
+
+* `options.h`: core `Options` class
+* `options_api.h`: utility methods used by the API (`parse()`, `set()`, `get()`,
+  ...)
+* `options_public.h`: utility methods used to access options from outside of
+  libcvc5
+* `{module}_options.h`: specifics for one single options module
+
+
+`Options` class
+---------------
+
+The `Options` class is the central entry point for regular usage of options. It
+holds a `std::unique_ptr` to an "option holder" for every option module, that
+can be accessed using references `{module}` (either as `const&` or `&`). These
+holders hold the actual option data for the specific module.
+
+The holder types are forward declared and can thus only be accessed if one also
+includes the appropriate `{module}_options.h`, which contains the proper
+declaration for the holder class.
+
+
+Option modules
+--------------
+
+Every option module declares an "option holder" class, which is a simple struct
+that has two members for every option (that is not declared as `type = void`):
+the actual option value as `{option.type} {option.name}` and a Boolean flag
+`bool {option.name}__setByUser` that indicates whether the option value was
+explicitly set by the user. If any of the options of a module is a mode option,
+the option module also defines an enum class that corresponds to the mode,
+including `operator<<()` and `stringTo{mode type}`.
+
+For convenience, the option modules also provide methods `void
+{module.id}::setDefault{option.name}(Options& opts, {option.type} value)`. Each
+such method sets the option value to the given value, if the option was not yet
+set by the user, i.e., the `__setByUser` flag is false. Additionally, every
+option module exports the `long` option name as `static constexpr const char*
+{module.id}::{option.name}__name`.
+
+
+Full Example
+============
+
+    [[option]]
+      category   = "regular"
+      name       = "decisionMode"
+      long       = "decision=MODE"
+      alias      = ["decision-mode"]
+      type       = "DecisionMode"
+      default    = "INTERNAL"
+      predicates = ["setDecisionModeStopOnly"]
+      help       = "choose decision mode, see --decision=help"
+      help_mode  = "Decision modes."
+    [[option.mode.INTERNAL]]
+      name = "internal"
+      help = "Use the internal decision heuristics of the SAT solver."
+    [[option.mode.JUSTIFICATION]]
+      name = "justification"
+      help = "An ATGP-inspired justification heuristic."
+    [[option.mode.RELEVANCY]]
+      name = "justification-stoponly"
+      help = "Use the justification heuristic only to stop early, not for decisions."
+
+This defines a new option that is accessible via
+`d_options.{module.id}.decisionMode` and stores an automatically generated mode
+`DecisionMode`, an enum class with the values `INTERNAL`, `JUSTIFICATION` and
+`RELEVANCY`. From the outside, it can be set by `--decision=internal`, but also
+with `--decision-mode=justification`, and similarly from an SMT-LIB input with
+`(set-option :decision internal)` and `(set-option :decision-mode
+justification)`. The command-line help for this option looks as follows:
+
+    --output-lang=LANG | --output-language=LANG
+                           force output language (default is "auto"; see
+                           --output-lang help)
diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h
deleted file mode 100644
index 86112a907..000000000
--- a/src/options/base_handlers.h
+++ /dev/null
@@ -1,87 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Morgan Deters, Tim King, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__BASE_HANDLERS_H
-#define CVC5__BASE_HANDLERS_H
-
-#include <iostream>
-#include <string>
-#include <sstream>
-
-#include "options/option_exception.h"
-
-namespace cvc5 {
-namespace options {
-
-template <template <class U> class Cmp>
-class comparator {
-  long d_lbound;
-  double d_dbound;
-  bool d_hasLbound;
-
- public:
-  comparator(int i) : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {}
-  comparator(long l) : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {}
-  comparator(double d) : d_lbound(0), d_dbound(d), d_hasLbound(false) {}
-  template <class T>
-  void operator()(std::string option, const T& value) {
-    if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) ||
-       (!d_hasLbound && !(Cmp<T>()(value, T(d_dbound))))) {
-      std::stringstream ss;
-      ss << option << ": " << value << " is not a legal setting";
-      throw OptionException(ss.str());
-    }
-  }
-};/* class comparator */
-
-struct greater : public comparator<std::greater> {
-  greater(int i) : comparator<std::greater>(i) {}
-  greater(long l) : comparator<std::greater>(l) {}
-  greater(double d) : comparator<std::greater>(d) {}
-};/* struct greater */
-
-struct greater_equal : public comparator<std::greater_equal> {
-  greater_equal(int i) : comparator<std::greater_equal>(i) {}
-  greater_equal(long l) : comparator<std::greater_equal>(l) {}
-  greater_equal(double d) : comparator<std::greater_equal>(d) {}
-};/* struct greater_equal */
-
-struct less : public comparator<std::less> {
-  less(int i) : comparator<std::less>(i) {}
-  less(long l) : comparator<std::less>(l) {}
-  less(double d) : comparator<std::less>(d) {}
-};/* struct less */
-
-struct less_equal : public comparator<std::less_equal> {
-  less_equal(int i) : comparator<std::less_equal>(i) {}
-  less_equal(long l) : comparator<std::less_equal>(l) {}
-  less_equal(double d) : comparator<std::less_equal>(d) {}
-};/* struct less_equal */
-
-struct not_equal : public comparator<std::not_equal_to> {
-  not_equal(int i) : comparator<std::not_equal_to>(i) {}
-  not_equal(long l) : comparator<std::not_equal_to>(l) {}
-  not_equal(double d) : comparator<std::not_equal_to>(d) {}
-};/* struct not_equal_to */
-
-}  // namespace options
-}  // namespace cvc5
-
-#endif /* CVC5__BASE_HANDLERS_H */
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 7e1cf68e4..e2fbd4cf1 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -210,6 +210,30 @@ def get_holder_ref_decls(modules):
     return concat_format('  options::Holder{id_cap}& {id};', modules)
 
 
+def get_handler(option):
+    """Render handler call for assignment functions"""
+    optname = option.long_name if option.long else ""
+    if option.handler:
+        if option.type == 'void':
+            return 'opts.handler().{}("{}", option)'.format(option.handler, optname)
+        else:
+            return 'opts.handler().{}("{}", option, optionarg)'.format(option.handler, optname)
+    elif option.mode:
+        return 'stringTo{}(optionarg)'.format(option.type)
+    elif option.type != 'bool':
+        return 'handleOption<{}>("{}", option, optionarg)'.format(option.type, optname)
+    return None
+
+
+def get_predicates(option):
+    """Render predicate calls for assignment functions"""
+    if not option.predicates:
+        return []
+    optname = option.long_name if option.long else ""
+    assert option.type != 'void'
+    return ['opts.handler().{}("{}", option, value);'.format(x, optname)
+            for x in option.predicates]
+
 class Module(object):
     """Options module.
 
@@ -713,31 +737,10 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
             sphinxgen.add(module, option)
 
             # Generate handler call
-            handler = None
-            if option.handler:
-                if option.type == 'void':
-                    handler = 'opts.handler().{}(option)'.format(option.handler)
-                else:
-                    handler = \
-                        'opts.handler().{}(option, optionarg)'.format(option.handler)
-            elif option.mode:
-                handler = 'stringTo{}(optionarg)'.format(option.type)
-            elif option.type != 'bool':
-                handler = \
-                    'handleOption<{}>(option, optionarg)'.format(option.type)
+            handler = get_handler(option)
 
             # Generate predicate calls
-            predicates = []
-            if option.predicates:
-                if option.type == 'bool':
-                    predicates = \
-                        ['opts.handler().{}(option, value);'.format(x) \
-                            for x in option.predicates]
-                else:
-                    assert option.type != 'void'
-                    predicates = \
-                        ['opts.handler().{}(option, value);'.format(x) \
-                            for x in option.predicates]
+            predicates = get_predicates(option)
 
             # Generate options_handler and getopt_long
             cases = []
@@ -813,7 +816,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
                             name=option.name,
                             option='key'))
                 elif option.handler:
-                    h = 'handler->{handler}("{smtname}"'
+                    h = 'handler->{handler}("{smtname}", key'
                     if argument_req:
                         h += ', optionarg'
                     h += ');'
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 1ac5ec56d..e109ab44c 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -67,10 +67,11 @@ void throwLazyBBUnsupported(options::SatSolverMode m)
 
 OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
 
-unsigned long OptionsHandler::limitHandler(std::string option,
-                                           std::string optarg)
+uint64_t OptionsHandler::limitHandler(const std::string& option,
+                                      const std::string& flag,
+                                      const std::string& optarg)
 {
-  unsigned long ms;
+  uint64_t ms;
   std::istringstream convert(optarg);
   if (!(convert >> ms))
   {
@@ -80,14 +81,18 @@ unsigned long OptionsHandler::limitHandler(std::string option,
   return ms;
 }
 
-void OptionsHandler::setResourceWeight(std::string option, std::string optarg)
+void OptionsHandler::setResourceWeight(const std::string& option,
+                                       const std::string& flag,
+                                       const std::string& optarg)
 {
   d_options->base.resourceWeightHolder.emplace_back(optarg);
 }
 
 // theory/quantifiers/options_handlers.h
 
-void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
+void OptionsHandler::checkInstWhenMode(const std::string& option,
+                                       const std::string& flag,
+                                       InstWhenMode mode)
 {
   if (mode == InstWhenMode::PRE_FULL)
   {
@@ -97,7 +102,9 @@ void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
 }
 
 // theory/bv/options_handlers.h
-void OptionsHandler::abcEnabledBuild(std::string option, bool value)
+void OptionsHandler::abcEnabledBuild(const std::string& option,
+                                     const std::string& flag,
+                                     bool value)
 {
 #ifndef CVC5_USE_ABC
   if(value) {
@@ -110,7 +117,9 @@ void OptionsHandler::abcEnabledBuild(std::string option, bool value)
 #endif /* CVC5_USE_ABC */
 }
 
-void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
+void OptionsHandler::abcEnabledBuild(const std::string& option,
+                                     const std::string& flag,
+                                     const std::string& value)
 {
 #ifndef CVC5_USE_ABC
   if(!value.empty()) {
@@ -123,7 +132,9 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
 #endif /* CVC5_USE_ABC */
 }
 
-void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
+void OptionsHandler::checkBvSatSolver(const std::string& option,
+                                      const std::string& flag,
+                                      SatSolverMode m)
 {
   if (m == SatSolverMode::CRYPTOMINISAT
       && !Configuration::isBuiltWithCryptominisat())
@@ -166,7 +177,9 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
   }
 }
 
-void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
+void OptionsHandler::checkBitblastMode(const std::string& option,
+                                       const std::string& flag,
+                                       BitblastMode m)
 {
   if (m == options::BitblastMode::LAZY)
   {
@@ -185,7 +198,9 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
   }
 }
 
-void OptionsHandler::setBitblastAig(std::string option, bool arg)
+void OptionsHandler::setBitblastAig(const std::string& option,
+                                    const std::string& flag,
+                                    bool arg)
 {
   if(arg) {
     if (d_options->bv.bitblastModeWasSetByUser) {
@@ -211,8 +226,9 @@ szs\n\
 + Print instantiations as SZS compliant proof.\n\
 ";
 
-InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
-                                                      std::string optarg)
+InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option,
+                                                      const std::string& flag,
+                                                      const std::string& optarg)
 {
   if(optarg == "default") {
     return InstFormatMode::DEFAULT;
@@ -228,24 +244,30 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
 }
 
 // decision/options_handlers.h
-void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m)
+void OptionsHandler::setDecisionModeStopOnly(const std::string& option,
+                                             const std::string& flag,
+                                             DecisionMode m)
 {
   d_options->decision.decisionStopOnly = (m == DecisionMode::RELEVANCY);
 }
 
-void OptionsHandler::setProduceAssertions(std::string option, bool value)
+void OptionsHandler::setProduceAssertions(const std::string& option,
+                                          const std::string& flag,
+                                          bool value)
 {
   d_options->smt.produceAssertions = value;
   d_options->smt.interactiveMode = value;
 }
 
-void OptionsHandler::setStats(const std::string& option, bool value)
+void OptionsHandler::setStats(const std::string& option,
+                              const std::string& flag,
+                              bool value)
 {
 #ifndef CVC5_STATISTICS_ON
   if (value)
   {
     std::stringstream ss;
-    ss << "option `" << option
+    ss << "option `" << flag
        << "' requires a statistics-enabled build of cvc5; this binary was not "
           "built with statistics support";
     throw OptionException(ss.str());
@@ -282,18 +304,25 @@ void OptionsHandler::setStats(const std::string& option, bool value)
   }
 }
 
-void OptionsHandler::threadN(std::string option) {
-  throw OptionException(option + " is not a real option by itself.  Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
+void OptionsHandler::threadN(const std::string& option, const std::string& flag)
+{
+  throw OptionException(flag + " is not a real option by itself.  Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
 }
 
 // expr/options_handlers.h
-void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
+void OptionsHandler::setDefaultExprDepthPredicate(const std::string& option,
+                                                  const std::string& flag,
+                                                  int depth)
+{
   if(depth < -1) {
     throw OptionException("--expr-depth requires a positive argument, or -1.");
   }
 }
 
-void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
+void OptionsHandler::setDefaultDagThreshPredicate(const std::string& option,
+                                                  const std::string& flag,
+                                                  int dag)
+{
   if(dag < 0) {
     throw OptionException("--dag-thresh requires a nonnegative argument.");
   }
@@ -312,12 +341,16 @@ static void print_config_cond (const char * str, bool cond = false) {
   print_config(str, cond ? "yes" : "no");
 }
 
-void OptionsHandler::copyright(std::string option) {
+void OptionsHandler::copyright(const std::string& option,
+                               const std::string& flag)
+{
   std::cout << Configuration::copyright() << std::endl;
   exit(0);
 }
 
-void OptionsHandler::showConfiguration(std::string option) {
+void OptionsHandler::showConfiguration(const std::string& option,
+                                       const std::string& flag)
+{
   std::cout << Configuration::about() << std::endl;
 
   print_config ("version", Configuration::getVersionString());
@@ -385,7 +418,8 @@ static void printTags(unsigned ntags, char const* const* tags)
   std::cout << std::endl;
 }
 
-void OptionsHandler::showDebugTags(std::string option)
+void OptionsHandler::showDebugTags(const std::string& option,
+                                   const std::string& flag)
 {
   if (!Configuration::isDebugBuild())
   {
@@ -399,7 +433,8 @@ void OptionsHandler::showDebugTags(std::string option)
   exit(0);
 }
 
-void OptionsHandler::showTraceTags(std::string option)
+void OptionsHandler::showTraceTags(const std::string& option,
+                                   const std::string& flag)
 {
   if (!Configuration::isTracingBuild())
   {
@@ -431,7 +466,9 @@ static std::string suggestTags(char const* const* validTags,
   return didYouMean.getMatchAsString(inputTag);
 }
 
-void OptionsHandler::enableTraceTag(std::string option, std::string optarg)
+void OptionsHandler::enableTraceTag(const std::string& option,
+                                    const std::string& flag,
+                                    const std::string& optarg)
 {
   if(!Configuration::isTracingBuild())
   {
@@ -453,7 +490,9 @@ void OptionsHandler::enableTraceTag(std::string option, std::string optarg)
   Trace.on(optarg);
 }
 
-void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
+void OptionsHandler::enableDebugTag(const std::string& option,
+                                    const std::string& flag,
+                                    const std::string& optarg)
 {
   if (!Configuration::isDebugBuild())
   {
@@ -484,8 +523,9 @@ void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
   Trace.on(optarg);
 }
 
-OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
-                                                      std::string optarg)
+OutputLanguage OptionsHandler::stringToOutputLanguage(const std::string& option,
+                                                      const std::string& flag,
+                                                      const std::string& optarg)
 {
   if(optarg == "help") {
     d_options->base.languageHelp = true;
@@ -502,8 +542,9 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
   Unreachable();
 }
 
-InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
-                                                    std::string optarg)
+InputLanguage OptionsHandler::stringToInputLanguage(const std::string& option,
+                                                    const std::string& flag,
+                                                    const std::string& optarg)
 {
   if(optarg == "help") {
     d_options->base.languageHelp = true;
@@ -520,7 +561,9 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
 }
 
 /* options/base_options_handlers.h */
-void OptionsHandler::setVerbosity(std::string option, int value)
+void OptionsHandler::setVerbosity(const std::string& option,
+                                  const std::string& flag,
+                                  int value)
 {
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(&cvc5::null_os);
@@ -550,14 +593,18 @@ void OptionsHandler::setVerbosity(std::string option, int value)
   }
 }
 
-void OptionsHandler::increaseVerbosity(std::string option) {
+void OptionsHandler::increaseVerbosity(const std::string& option,
+                                       const std::string& flag)
+{
   d_options->base.verbosity += 1;
-  setVerbosity(option, options::verbosity());
+  setVerbosity(option, flag, d_options->base.verbosity);
 }
 
-void OptionsHandler::decreaseVerbosity(std::string option) {
+void OptionsHandler::decreaseVerbosity(const std::string& option,
+                                       const std::string& flag)
+{
   d_options->base.verbosity -= 1;
-  setVerbosity(option, options::verbosity());
+  setVerbosity(option, flag, d_options->base.verbosity);
 }
 
 }  // namespace options
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 4b9b1c0ae..9aee1df22 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -19,9 +19,9 @@
 #define CVC5__OPTIONS__OPTIONS_HANDLER_H
 
 #include <ostream>
+#include <sstream>
 #include <string>
 
-#include "options/base_handlers.h"
 #include "options/bv_options.h"
 #include "options/decision_options.h"
 #include "options/language.h"
@@ -44,72 +44,122 @@ class OptionsHandler {
 public:
   OptionsHandler(Options* options);
 
-  void unsignedGreater0(const std::string& option, unsigned value) {
-    options::greater(0)(option, value);
+  template <typename T>
+  void geqZero(const std::string& option,
+               const std::string& flag,
+               T value) const
+  {
+    if (value < 0)
+    {
+      std::stringstream ss;
+      ss << flag << ": " << value << " is not a legal setting, should be "
+         << value << " >= 0.";
+      throw OptionException(ss.str());
+    }
   }
-
-  void unsignedLessEqual2(const std::string& option, unsigned value) {
-    options::less_equal(2)(option, value);
-  }
-
-  void doubleGreaterOrEqual0(const std::string& option, double value) {
-    options::greater_equal(0.0)(option, value);
-  }
-
-  void doubleLessOrEqual1(const std::string& option, double value) {
-    options::less_equal(1.0)(option, value);
+  template <typename T>
+  void betweenZeroAndOne(const std::string& option,
+                         const std::string& flag,
+                         T value) const
+  {
+    if (value < 0 || value > 1)
+    {
+      std::stringstream ss;
+      ss << flag << ": " << value
+         << " is not a legal setting, should be 0 <= " << flag << " <= 1.";
+      throw OptionException(ss.str());
+    }
   }
 
   // theory/quantifiers/options_handlers.h
-  void checkInstWhenMode(std::string option, InstWhenMode mode);
+  void checkInstWhenMode(const std::string& option,
+                         const std::string& flag,
+                         InstWhenMode mode);
 
   // theory/bv/options_handlers.h
-  void abcEnabledBuild(std::string option, bool value);
-  void abcEnabledBuild(std::string option, std::string value);
-
-  template<class T> void checkSatSolverEnabled(std::string option, T m);
-
-  void checkBvSatSolver(std::string option, SatSolverMode m);
-  void checkBitblastMode(std::string option, BitblastMode m);
-
-  void setBitblastAig(std::string option, bool arg);
+  void abcEnabledBuild(const std::string& option,
+                       const std::string& flag,
+                       bool value);
+  void abcEnabledBuild(const std::string& option,
+                       const std::string& flag,
+                       const std::string& value);
+
+  template <class T>
+  void checkSatSolverEnabled(const std::string& option,
+                             const std::string& flag,
+                             T m);
+
+  void checkBvSatSolver(const std::string& option,
+                        const std::string& flag,
+                        SatSolverMode m);
+  void checkBitblastMode(const std::string& option,
+                         const std::string& flag,
+                         BitblastMode m);
+
+  void setBitblastAig(const std::string& option,
+                      const std::string& flag,
+                      bool arg);
 
   // printer/options_handlers.h
-  InstFormatMode stringToInstFormatMode(std::string option, std::string optarg);
+  InstFormatMode stringToInstFormatMode(const std::string& option,
+                                        const std::string& flag,
+                                        const std::string& optarg);
 
   // decision/options_handlers.h
-  void setDecisionModeStopOnly(std::string option, DecisionMode m);
+  void setDecisionModeStopOnly(const std::string& option,
+                               const std::string& flag,
+                               DecisionMode m);
 
   /**
    * Throws a ModalException if this option is being set after final
    * initialization.
    */
-  void setProduceAssertions(std::string option, bool value);
+  void setProduceAssertions(const std::string& option,
+                            const std::string& flag,
+                            bool value);
 
-  void setStats(const std::string& option, bool value);
+  void setStats(const std::string& option, const std::string& flag, bool value);
 
-  unsigned long limitHandler(std::string option, std::string optarg);
-  void setResourceWeight(std::string option, std::string optarg);
+  uint64_t limitHandler(const std::string& option,
+                        const std::string& flag,
+                        const std::string& optarg);
+  void setResourceWeight(const std::string& option,
+                         const std::string& flag,
+                         const std::string& optarg);
 
   /* expr/options_handlers.h */
-  void setDefaultExprDepthPredicate(std::string option, int depth);
-  void setDefaultDagThreshPredicate(std::string option, int dag);
+  void setDefaultExprDepthPredicate(const std::string& option,
+                                    const std::string& flag,
+                                    int depth);
+  void setDefaultDagThreshPredicate(const std::string& option,
+                                    const std::string& flag,
+                                    int dag);
 
   /* main/options_handlers.h */
-  void copyright(std::string option);
-  void showConfiguration(std::string option);
-  void showDebugTags(std::string option);
-  void showTraceTags(std::string option);
-  void threadN(std::string option);
+  void copyright(const std::string& option, const std::string& flag);
+  void showConfiguration(const std::string& option, const std::string& flag);
+  void showDebugTags(const std::string& option, const std::string& flag);
+  void showTraceTags(const std::string& option, const std::string& flag);
+  void threadN(const std::string& option, const std::string& flag);
 
   /* options/base_options_handlers.h */
-  void setVerbosity(std::string option, int value);
-  void increaseVerbosity(std::string option);
-  void decreaseVerbosity(std::string option);
-  OutputLanguage stringToOutputLanguage(std::string option, std::string optarg);
-  InputLanguage stringToInputLanguage(std::string option, std::string optarg);
-  void enableTraceTag(std::string option, std::string optarg);
-  void enableDebugTag(std::string option, std::string optarg);
+  void setVerbosity(const std::string& option,
+                    const std::string& flag,
+                    int value);
+  void increaseVerbosity(const std::string& option, const std::string& flag);
+  void decreaseVerbosity(const std::string& option, const std::string& flag);
+  OutputLanguage stringToOutputLanguage(const std::string& option,
+                                        const std::string& flag,
+                                        const std::string& optarg);
+  InputLanguage stringToInputLanguage(const std::string& option,
+                                      const std::string& flag,
+                                      const std::string& optarg);
+  void enableTraceTag(const std::string& option,
+                      const std::string& flag,
+                      const std::string& optarg);
+  void enableDebugTag(const std::string& option,
+                      const std::string& flag,
+                      const std::string& optarg);
 
  private:
 
@@ -121,8 +171,10 @@ public:
 
 }; /* class OptionHandler */
 
-template<class T>
-void OptionsHandler::checkSatSolverEnabled(std::string option, T m)
+template <class T>
+void OptionsHandler::checkSatSolverEnabled(const std::string& option,
+                                           const std::string& flag,
+                                           T m)
 {
 #if !defined(CVC5_USE_CRYPTOMINISAT) && !defined(CVC5_USE_CADICAL) \
     && !defined(CVC5_USE_KISSAT)
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index e909a5f0a..2c22065c2 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -58,7 +58,6 @@ extern int optreset;
 ${headers_module}$
 
 #include "base/cvc5config.h"
-#include "options/base_handlers.h"
 
 ${headers_handler}$
 
@@ -82,7 +81,9 @@ thread_local Options* Options::s_current = NULL;
  */
 template <class T, bool is_numeric, bool is_integer>
 struct OptionHandler {
-  static T handle(std::string option, std::string optionarg);
+  static T handle(const std::string& option,
+                  const std::string& flag,
+                  const std::string& optionarg);
 };/* struct OptionHandler<> */
 
 /** Variant for integral C++ types */
@@ -99,32 +100,35 @@ struct OptionHandler<T, true, true> {
     return str.find('-') != std::string::npos;
   }
 
-  static T handle(const std::string& option, const std::string& optionarg) {
+  static T handle(const std::string& option,
+                  const std::string& flag,
+                  const std::string& optionarg)
+  {
     try {
       T i;
       bool success = stringToInt(i, optionarg);
 
       if(!success){
-        throw OptionException(option + ": failed to parse "+ optionarg +
-                              " as an integer of the appropriate type.");
+        throw OptionException(flag + ": failed to parse " + optionarg
+                              + " as an integer of the appropriate type.");
       }
 
       // Depending in the platform unsigned numbers with '-' signs may parse.
       // Reject these by looking for any minus if it is not signed.
       if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) {
         // unsigned type but user gave negative argument
-        throw OptionException(option + " requires a nonnegative argument");
+        throw OptionException(flag + " requires a nonnegative argument");
       } else if(i < std::numeric_limits<T>::min()) {
         // negative overflow for type
         std::stringstream ss;
-        ss << option << " requires an argument >= "
-           << std::numeric_limits<T>::min();
+        ss << flag
+           << " requires an argument >= " << std::numeric_limits<T>::min();
         throw OptionException(ss.str());
       } else if(i > std::numeric_limits<T>::max()) {
         // positive overflow for type
         std::stringstream ss;
-        ss << option << " requires an argument <= "
-           << std::numeric_limits<T>::max();
+        ss << flag
+           << " requires an argument <= " << std::numeric_limits<T>::max();
         throw OptionException(ss.str());
       }
 
@@ -137,7 +141,7 @@ struct OptionHandler<T, true, true> {
       // }
     } catch(std::invalid_argument&) {
       // user gave something other than an integer
-      throw OptionException(option + " requires an integer argument");
+      throw OptionException(flag + " requires an integer argument");
     }
   }
 };/* struct OptionHandler<T, true, true> */
@@ -145,29 +149,33 @@ struct OptionHandler<T, true, true> {
 /** Variant for numeric but non-integral C++ types */
 template <class T>
 struct OptionHandler<T, true, false> {
-  static T handle(std::string option, std::string optionarg) {
-    std::stringstream in(optionarg);
+  static T handle(const std::string& option,
+                  const std::string& flag,
+                  const std::string& optionarg)
+  {
+    std::stringstream inss(optionarg);
     long double r;
-    in >> r;
-    if(! in.eof()) {
+    inss >> r;
+    if (!inss.eof())
+    {
       // we didn't consume the whole string (junk at end)
-      throw OptionException(option + " requires a numeric argument");
+      throw OptionException(flag + " requires a numeric argument");
     }
 
     if(! std::numeric_limits<T>::is_signed && r < 0.0) {
       // unsigned type but user gave negative value
-      throw OptionException(option + " requires a nonnegative argument");
+      throw OptionException(flag + " requires a nonnegative argument");
     } else if(r < -std::numeric_limits<T>::max()) {
       // negative overflow for type
       std::stringstream ss;
-      ss << option << " requires an argument >= "
-         << -std::numeric_limits<T>::max();
+      ss << flag
+         << " requires an argument >= " << -std::numeric_limits<T>::max();
       throw OptionException(ss.str());
     } else if(r > std::numeric_limits<T>::max()) {
       // positive overflow for type
       std::stringstream ss;
-      ss << option << " requires an argument <= "
-         << std::numeric_limits<T>::max();
+      ss << flag
+         << " requires an argument <= " << std::numeric_limits<T>::max();
       throw OptionException(ss.str());
     }
 
@@ -178,7 +186,10 @@ struct OptionHandler<T, true, false> {
 /** Variant for non-numeric C++ types */
 template <class T>
 struct OptionHandler<T, false, false> {
-  static T handle(std::string option, std::string optionarg) {
+  static T handle(const std::string& option,
+                  const std::string& flag,
+                  const std::string& optionarg)
+  {
     T::unsupported_handleOption_call___please_write_me;
     // The above line causes a compiler error if this version of the template
     // is ever instantiated (meaning that a specialization is missing).  So
@@ -191,36 +202,26 @@ struct OptionHandler<T, false, false> {
 
 /** Handle an option of type T in the default way. */
 template <class T>
-T handleOption(std::string option, std::string optionarg) {
-  return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optionarg);
+T handleOption(const std::string& option,
+               const std::string& flag,
+               const std::string& optionarg)
+{
+  return OptionHandler<T,
+                       std::numeric_limits<T>::is_specialized,
+                       std::numeric_limits<T>::is_integer>::handle(option,
+                                                                   flag,
+                                                                   optionarg);
 }
 
 /** Handle an option of type std::string in the default way. */
 template <>
-std::string handleOption<std::string>(std::string option, std::string optionarg) {
+std::string handleOption<std::string>(const std::string& option,
+                                      const std::string& flag,
+                                      const std::string& optionarg)
+{
   return optionarg;
 }
 
-/**
- * Run handler, and any user-given predicates, for option T.
- * If a user specifies a :handler or :predicates, it overrides this.
- */
-template <class T>
-typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, options::OptionsHandler* handler) {
-  // By default, parse the option argument in a way appropriate for its type.
-  // E.g., for "unsigned int" options, ensure that the provided argument is
-  // a nonnegative integer that fits in the unsigned int type.
-
-  return handleOption<typename T::type>(option, optionarg);
-}
-
-template <class T>
-void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* handler) {
-  // By default, nothing to do for bool.  Users add things with
-  // :predicate in options files to provide custom checking routines
-  // that can throw exceptions.
-}
-
 Options::Options(OptionsListener* ol)
     : d_handler(new options::OptionsHandler(this)),
 // clang-format off
diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml
index 26d7a451b..eda5ea963 100644
--- a/src/options/prop_options.toml
+++ b/src/options/prop_options.toml
@@ -8,7 +8,7 @@ name   = "SAT Layer"
   long       = "random-freq=P"
   type       = "double"
   default    = "0.0"
-  predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
+  predicates = ["betweenZeroAndOne"]
   help       = "sets the frequency of random decisions in the sat solver (P=0.0 by default)"
 
 [[option]]
@@ -24,7 +24,7 @@ name   = "SAT Layer"
   category   = "regular"
   type       = "double"
   default    = "0.95"
-  predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
+  predicates = ["betweenZeroAndOne"]
   help       = "variable activity decay factor for Minisat"
 
 [[option]]
@@ -32,7 +32,7 @@ name   = "SAT Layer"
   category   = "regular"
   type       = "double"
   default    = "0.999"
-  predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
+  predicates = ["betweenZeroAndOne"]
   help       = "clause activity decay factor for Minisat"
 
 [[option]]
@@ -49,7 +49,7 @@ name   = "SAT Layer"
   long       = "restart-int-inc=F"
   type       = "double"
   default    = "3.0"
-  predicates = ["doubleGreaterOrEqual0"]
+  predicates = ["geqZero"]
   help       = "sets the restart interval increase factor for the sat solver (F=3.0 by default)"
 
 [[option]]
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index e85ea82ef..a46452004 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -32,12 +32,11 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent)
     : d_parent(parent),
       d_optChecker(),
       d_objectives(parent->getUserContext()),
-      d_results(),
-      d_objectiveCombination(LEXICOGRAPHIC)
+      d_results()
 {
 }
 
-OptimizationResult::ResultType OptimizationSolver::checkOpt()
+Result OptimizationSolver::checkOpt(ObjectiveCombination combination)
 {
   // if the results of the previous call have different size than the
   // objectives, then we should clear the pareto optimization context
@@ -48,7 +47,7 @@ OptimizationResult::ResultType OptimizationSolver::checkOpt()
   {
     d_results.emplace_back();
   }
-  switch (d_objectiveCombination)
+  switch (combination)
   {
     case BOX: return optimizeBox(); break;
     case LEXICOGRAPHIC: return optimizeLexicographicIterative(); break;
@@ -76,16 +75,9 @@ void OptimizationSolver::addObjective(TNode target,
 
 std::vector<OptimizationResult> OptimizationSolver::getValues()
 {
-  Assert(d_objectives.size() == d_results.size());
   return d_results;
 }
 
-void OptimizationSolver::setObjectiveCombination(
-    ObjectiveCombination combination)
-{
-  d_objectiveCombination = combination;
-}
-
 std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
     SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout)
 {
@@ -106,13 +98,12 @@ std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
   return optChecker;
 }
 
-OptimizationResult::ResultType OptimizationSolver::optimizeBox()
+Result OptimizationSolver::optimizeBox()
 {
   // resets the optChecker
   d_optChecker = createOptCheckerWithTimeout(d_parent);
   OptimizationResult partialResult;
-  OptimizationResult::ResultType aggregatedResultType =
-      OptimizationResult::OPTIMAL;
+  Result aggregatedResult(Result::Sat::SAT);
   std::unique_ptr<OMTOptimizer> optimizer;
   for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
   {
@@ -134,18 +125,19 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox()
     }
     // match the optimization result type, and aggregate the results of
     // subproblems
-    switch (partialResult.getType())
+    switch (partialResult.getResult().isSat())
     {
-      case OptimizationResult::OPTIMAL: break;
-      case OptimizationResult::UNBOUNDED: break;
-      case OptimizationResult::UNSAT:
-        if (aggregatedResultType == OptimizationResult::OPTIMAL)
+      case Result::SAT: break;
+      case Result::UNSAT:
+        // the assertions are unsatisfiable
+        for (size_t j = 0; j < numObj; ++j)
         {
-          aggregatedResultType = OptimizationResult::UNSAT;
+          d_results[j] = partialResult;
         }
-        break;
-      case OptimizationResult::UNKNOWN:
-        aggregatedResultType = OptimizationResult::UNKNOWN;
+        d_optChecker.reset();
+        return partialResult.getResult();
+      case Result::SAT_UNKNOWN:
+        aggregatedResult = partialResult.getResult();
         break;
       default: Unreachable();
     }
@@ -154,15 +146,20 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox()
   }
   // kill optChecker after optimization ends
   d_optChecker.reset();
-  return aggregatedResultType;
+  return aggregatedResult;
 }
 
-OptimizationResult::ResultType
-OptimizationSolver::optimizeLexicographicIterative()
+Result OptimizationSolver::optimizeLexicographicIterative()
 {
   // resets the optChecker
   d_optChecker = createOptCheckerWithTimeout(d_parent);
-  OptimizationResult partialResult;
+  // partialResult defaults to SAT if no objective is present
+  // NOTE: the parenthesis around Result(Result::SAT) is required,
+  // otherwise the compiler will report "parameter declarator cannot be
+  // qualified". For more details:
+  // https://stackoverflow.com/questions/44045257/c-compiler-error-c2751-what-exactly-causes-it
+  // https://en.wikipedia.org/wiki/Most_vexing_parse
+  OptimizationResult partialResult((Result(Result::SAT)), TNode());
   std::unique_ptr<OMTOptimizer> optimizer;
   for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
   {
@@ -186,26 +183,33 @@ OptimizationSolver::optimizeLexicographicIterative()
     d_results[i] = partialResult;
 
     // checks the optimization result of the current objective
-    switch (partialResult.getType())
+    switch (partialResult.getResult().isSat())
     {
-      case OptimizationResult::OPTIMAL:
+      case Result::SAT:
         // assert target[i] == value[i] and proceed
         d_optChecker->assertFormula(d_optChecker->getNodeManager()->mkNode(
             kind::EQUAL, d_objectives[i].getTarget(), d_results[i].getValue()));
         break;
-      case OptimizationResult::UNBOUNDED: return OptimizationResult::UNBOUNDED;
-      case OptimizationResult::UNSAT: return OptimizationResult::UNSAT;
-      case OptimizationResult::UNKNOWN: return OptimizationResult::UNKNOWN;
+      case Result::UNSAT:
+        d_optChecker.reset();
+        return partialResult.getResult();
+      case Result::SAT_UNKNOWN:
+        d_optChecker.reset();
+        return partialResult.getResult();
       default: Unreachable();
     }
+
+    // if the result for the current objective is unbounded
+    // then just stop
+    if (partialResult.isUnbounded()) break;
   }
   // kill optChecker in case pareto misuses it
   d_optChecker.reset();
-  // now all objectives are OPTIMAL, just return OPTIMAL as overall result
-  return OptimizationResult::OPTIMAL;
+  // now all objectives are optimal, just return SAT as the overall result
+  return partialResult.getResult();
 }
 
-OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
+Result OptimizationSolver::optimizeParetoNaiveGIA()
 {
   // initial call to Pareto optimizer, create the checker
   if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent);
@@ -216,8 +220,8 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
 
   switch (satResult.isSat())
   {
-    case Result::Sat::UNSAT: return OptimizationResult::UNSAT;
-    case Result::Sat::SAT_UNKNOWN: return OptimizationResult::UNKNOWN;
+    case Result::Sat::UNSAT: return satResult;
+    case Result::Sat::SAT_UNKNOWN: return satResult;
     case Result::Sat::SAT:
     {
       // if satisfied, use d_results to store the initial results
@@ -226,14 +230,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
       for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
       {
         d_results[i] = OptimizationResult(
-            OptimizationResult::OPTIMAL,
-            d_optChecker->getValue(d_objectives[i].getTarget()));
+            satResult, d_optChecker->getValue(d_objectives[i].getTarget()));
       }
       break;
     }
     default: Unreachable();
   }
 
+  Result lastSatResult = satResult;
+
   // a vector storing assertions saying that no objective is worse
   std::vector<Node> noWorseObj;
   // a vector storing assertions saying that there is at least one objective
@@ -278,15 +283,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
       case Result::Sat::SAT_UNKNOWN:
         // if result is UNKNOWN, abort the current session and return UNKNOWN
         d_optChecker.reset();
-        return OptimizationResult::UNKNOWN;
+        return satResult;
       case Result::Sat::SAT:
       {
+        lastSatResult = satResult;
         // if result is SAT, update d_results to the more optimal values
         for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
         {
           d_results[i] = OptimizationResult(
-              OptimizationResult::OPTIMAL,
-              d_optChecker->getValue(d_objectives[i].getTarget()));
+              satResult, d_optChecker->getValue(d_objectives[i].getTarget()));
         }
         break;
       }
@@ -302,7 +307,7 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
   // for the next run.
   d_optChecker->assertFormula(nm->mkOr(someObjBetter));
 
-  return OptimizationResult::OPTIMAL;
+  return lastSatResult;
 }
 
 }  // namespace smt
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 6d138deb2..d13168780 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -33,63 +33,75 @@ namespace smt {
 /**
  * The optimization result of an optimization objective
  * containing:
- * - whether it's optimal or not
- * - if so, the optimal value, otherwise the value might be empty node or
- *   something suboptimal
+ * - the optimization result: SAT/UNSAT/UNKNOWN
+ * - the optimal value if SAT and bounded
+ *     (optimal value reached and it's not infinity),
+ *   or an empty node if SAT and unbounded
+ *     (optimal value is +inf for maximum or -inf for minimum),
+ *   otherwise the value might be empty node
+ *   or something suboptimal
+ * - whether the objective is unbounded
  */
 class OptimizationResult
 {
  public:
   /**
-   * Enum indicating whether the checkOpt result
-   * is optimal or not.
-   **/
-  enum ResultType
-  {
-    // whether the value is optimal is UNKNOWN
-    UNKNOWN,
-    // the original set of assertions has result UNSAT
-    UNSAT,
-    // the value is optimal
-    OPTIMAL,
-    // the goal is unbounded,
-    // if objective is maximize, it's +infinity
-    // if objective is minimize, it's -infinity
-    UNBOUNDED,
-  };
-
-  /**
    * Constructor
    * @param type the optimization outcome
    * @param value the optimized value
+   * @param unbounded whether the objective is unbounded
    **/
-  OptimizationResult(ResultType type, TNode value)
-      : d_type(type), d_value(value)
+  OptimizationResult(Result result, TNode value, bool unbounded = false)
+      : d_result(result), d_value(value), d_unbounded(unbounded)
+  {
+  }
+  OptimizationResult()
+      : d_result(Result::Sat::SAT_UNKNOWN,
+                 Result::UnknownExplanation::NO_STATUS),
+        d_value(),
+        d_unbounded(false)
   {
   }
-  OptimizationResult() : d_type(UNKNOWN), d_value() {}
   ~OptimizationResult() = default;
 
   /**
    * Returns an enum indicating whether
-   * the result is optimal or not.
-   * @return an enum showing whether the result is optimal, unbounded,
-   *   unsat or unknown.
+   * the result is SAT or not.
+   * @return whether the result is SAT, UNSAT or SAT_UNKNOWN
    **/
-  ResultType getType() const { return d_type; }
+  Result getResult() const { return d_result; }
+
   /**
    * Returns the optimal value.
    * @return Node containing the optimal value,
-   *   if getType() is not OPTIMAL, it might return an empty node or a node
-   *   containing non-optimal value
+   *   if result is unbounded, this will be an empty node,
+   *   if getResult() is UNSAT, it will return an empty node,
+   *   if getResult() is SAT_UNKNOWN, it will return something suboptimal
+   *   or an empty node, depending on how the solver runs.
    **/
   Node getValue() const { return d_value; }
 
+  /**
+   * Checks whether the objective is unbouned
+   * @return whether the objective is unbounded
+   *   if the objective is unbounded (this function returns true), 
+   *   then the optimal value is:
+   *   +inf, if it's maximize;
+   *   -inf, if it's minimize
+   **/
+  bool isUnbounded() const { return d_unbounded; }
+
  private:
-  /** the indicating whether the result is optimal or something else **/
-  ResultType d_type;
-  /** if the result is optimal, this is storing the optimal value **/
+  /** indicating whether the result is SAT, UNSAT or UNKNOWN **/
+  Result d_result;
+  /** if the result is bounded, this is storing the value **/
   Node d_value;
+  /** whether the objective is unbounded
+   * If this is true, then:
+   * if objective is maximize, it's +infinity;
+   * if objective is minimize, it's -infinity
+   **/
+  bool d_unbounded;
 };
 
 /**
@@ -199,10 +211,10 @@ class OptimizationSolver
   /**
    * Run the optimization loop for the added objective
    * For multiple objective combination, it defaults to lexicographic,
-   * and combination could be set by calling
-   *   setObjectiveCombination(BOX/LEXICOGRAPHIC/PARETO)
+   * possible combinations: BOX, LEXICOGRAPHIC, PARETO
+   * @param combination BOX / LEXICOGRAPHIC / PARETO
    */
-  OptimizationResult::ResultType checkOpt();
+  Result checkOpt(ObjectiveCombination combination = LEXICOGRAPHIC);
 
   /**
    * Add an optimization objective.
@@ -223,11 +235,6 @@ class OptimizationSolver
    **/
   std::vector<OptimizationResult> getValues();
 
-  /**
-   * Sets the objective combination
-   **/
-  void setObjectiveCombination(ObjectiveCombination combination);
-
  private:
   /**
    * Initialize an SMT subsolver for offline optimization purpose
@@ -244,26 +251,26 @@ class OptimizationSolver
 
   /**
    * Optimize multiple goals in Box order
-   * @return OPTIMAL if all of the objectives are either OPTIMAL or UNBOUNDED;
-   *   UNSAT if at least one objective is UNSAT and no objective is UNKNOWN;
-   *   UNKNOWN if any of the objective is UNKNOWN.
+   * @return SAT if all of the objectives are optimal or unbounded;
+   *   UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN;
+   *   SAT_UNKNOWN if any of the objective is SAT_UNKNOWN.
    **/
-  OptimizationResult::ResultType optimizeBox();
+  Result optimizeBox();
 
   /**
    * Optimize multiple goals in Lexicographic order,
    * using iterative implementation
-   * @return OPTIMAL if all objectives are OPTIMAL and bounded;
-   *   UNBOUNDED if one of the objectives is UNBOUNDED
+   * @return SAT if the objectives are optimal,
+   *     if one of the objectives is unbounded,
+   *     the optimization will stop at that objective;
+   *   UNSAT if any of the objectives is UNSAT
    *     and optimization will stop at that objective;
-   *   UNSAT if one of the objectives is UNSAT
-   *     and optimization will stop at that objective;
-   *   UNKNOWN if one of the objectives is UNKNOWN
+   *   SAT_UNKNOWN if any of the objectives is UNKNOWN
    *     and optimization will stop at that objective;
    *   If the optimization is stopped at an objective,
-   *     all objectives following that objective will be UNKNOWN.
+   *     all objectives following that objective will be SAT_UNKNOWN.
    **/
-  OptimizationResult::ResultType optimizeLexicographicIterative();
+  Result optimizeLexicographicIterative();
 
   /**
    * Optimize multiple goals in Pareto order
@@ -277,11 +284,12 @@ class OptimizationSolver
    * D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm.
    *  Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009.
    *
-   * @return if it finds a new Pareto optimal result it will return OPTIMAL;
+   * @return if it finds a new Pareto optimal result it will return SAT;
    *   if it exhausts the results in the Pareto front it will return UNSAT;
-   *   if the underlying SMT solver returns UNKNOWN, it will return UNKNOWN.
+   *   if the underlying SMT solver returns SAT_UNKNOWN,
+   *   it will return SAT_UNKNOWN.
    **/
-  OptimizationResult::ResultType optimizeParetoNaiveGIA();
+  Result optimizeParetoNaiveGIA();
 
   /** A pointer to the parent SMT engine **/
   SmtEngine* d_parent;
@@ -294,9 +302,6 @@ class OptimizationSolver
 
   /** The results of the optimizations from the last checkOpt call **/
   std::vector<OptimizationResult> d_results;
-
-  /** The current objective combination method **/
-  ObjectiveCombination d_objectiveCombination;
 };
 
 }  // namespace smt
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 396befb35..0c93db90f 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -26,6 +26,7 @@ operator INTS_MODULUS_TOTAL 2 "integer modulus with interpreted division by 0 (i
 operator ABS 1 "absolute value"
 parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term"
 operator POW 2 "arithmetic power"
+operator POW2 1 "arithmetic power of 2"
 
 operator EXPONENTIAL 1 "exponential"
 operator SINE 1 "sine"
@@ -148,6 +149,7 @@ typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>"
 typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>"
 typerule ARCSECANT "SimpleTypeRule<RReal, AReal>"
 typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>"
+typerule POW2 "SimpleTypeRule<RInteger, AInteger>"
 
 typerule SQRT "SimpleTypeRule<RReal, AReal>"
 
diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp
new file mode 100644
index 000000000..534895c7f
--- /dev/null
+++ b/src/theory/arith/nl/pow2_solver.cpp
@@ -0,0 +1,73 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Makai Mann, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of pow2 solver.
+ */
+
+#include "theory/arith/nl/pow2_solver.h"
+
+#include "theory/arith/arith_msum.h"
+#include "theory/arith/arith_state.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+Pow2Solver::Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model)
+    : d_im(im), d_model(model), d_initRefine(state.getUserContext())
+{
+  NodeManager* nm = NodeManager::currentNM();
+  d_false = nm->mkConst(false);
+  d_true = nm->mkConst(true);
+  d_zero = nm->mkConst(Rational(0));
+  d_one = nm->mkConst(Rational(1));
+  d_two = nm->mkConst(Rational(2));
+}
+
+Pow2Solver::~Pow2Solver() {}
+
+void Pow2Solver::initLastCall(const std::vector<Node>& assertions,
+                              const std::vector<Node>& false_asserts,
+                              const std::vector<Node>& xts)
+{
+  d_pow2s.clear();
+  Trace("pow2-mv") << "POW2 terms : " << std::endl;
+  for (const Node& a : xts)
+  {
+    Kind ak = a.getKind();
+    if (ak != POW2)
+    {
+      // don't care about other terms
+      continue;
+    }
+    d_pow2s.push_back(a);
+  }
+  Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl;
+}
+
+void Pow2Solver::checkInitialRefine() {}
+
+void Pow2Solver::checkFullRefine() {}
+
+Node Pow2Solver::valueBasedLemma(Node i) { return Node(); }
+
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index fe4ed4c22..778c842a6 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -75,6 +75,10 @@ const char* toString(InferenceId i)
       return "ARITH_NL_IAND_SUM_REFINE";
     case InferenceId::ARITH_NL_IAND_BITWISE_REFINE:
       return "ARITH_NL_IAND_BITWISE_REFINE";
+    case InferenceId::ARITH_NL_POW2_INIT_REFINE:
+      return "ARITH_NL_POW2_INIT_REFINE";
+    case InferenceId::ARITH_NL_POW2_VALUE_REFINE:
+      return "ARITH_NL_POW2_VALUE_REFINE";
     case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT";
     case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL:
       return "ARITH_NL_CAD_EXCLUDED_INTERVAL";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 169992f41..6a87776d6 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -126,6 +126,11 @@ enum class InferenceId
   ARITH_NL_IAND_SUM_REFINE,
   // bitwise refinements (IAndSolver::checkFullRefine)
   ARITH_NL_IAND_BITWISE_REFINE,
+  //-------------------- nonlinear pow2 solver
+  // initial refinements (Pow2Solver::checkInitialRefine)
+  ARITH_NL_POW2_INIT_REFINE,
+  // value refinements (Pow2Solver::checkFullRefine)
+  ARITH_NL_POW2_VALUE_REFINE,
   //-------------------- nonlinear cad solver
   // conflict / infeasible subset obtained from cad
   ARITH_NL_CAD_CONFLICT,
diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index c23ce79dd..5cd29878e 100644
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -57,9 +57,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min)
 
   d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, (uint32_t)0x3FFFFFA1));
@@ -78,9 +78,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min)
 
   d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>();
   std::cout << "opt value is: " << val << std::endl;
@@ -105,9 +105,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
 
   d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>();
   std::cout << "opt value is: " << val << std::endl;
@@ -130,9 +130,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max)
 
   d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   // expect the maxmum x =
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
@@ -154,9 +154,9 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary)
 
   d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   // expect the maximum x = 18
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index cf0434ddc..583f908e7 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -62,9 +62,9 @@ TEST_F(TestTheoryWhiteIntOpt, max)
   // We activate our objective so the subsolver knows to optimize it
   d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   // We expect max_cost == 99
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
@@ -93,9 +93,9 @@ TEST_F(TestTheoryWhiteIntOpt, min)
   // We activate our objective so the subsolver knows to optimize it
   d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   // We expect max_cost == 99
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
@@ -125,10 +125,10 @@ TEST_F(TestTheoryWhiteIntOpt, result)
   d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
 
   // This should return OPT_UNSAT since 0 > x > 100 is impossible.
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
   // We expect our check to have returned UNSAT
-  ASSERT_EQ(r, OptimizationResult::UNSAT);
+  ASSERT_EQ(r.isSat(), Result::UNSAT);
   d_smtEngine->resetAssertions();
 }
 
@@ -157,9 +157,9 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval)
 
   d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp
index 73c6d9e7e..9a091fb3b 100644
--- a/test/unit/theory/theory_opt_multigoal_white.cpp
+++ b/test/unit/theory/theory_opt_multigoal_white.cpp
@@ -54,11 +54,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, box)
   // y <= x
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
 
-  // Box optimization
   OptimizationSolver optSolver(d_smtEngine.get());
 
-  optSolver.setObjectiveCombination(OptimizationSolver::BOX);
-
   // minimize x
   optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
   // maximize y with `signed` comparison over bit-vectors.
@@ -66,9 +63,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, box)
   // maximize z
   optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
 
-  OptimizationResult::ResultType r = optSolver.checkOpt();
+  // Box optimization
+  Result r = optSolver.checkOpt(OptimizationSolver::BOX);
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   std::vector<OptimizationResult> results = optSolver.getValues();
 
@@ -100,8 +98,6 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex)
 
   OptimizationSolver optSolver(d_smtEngine.get());
 
-  optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
-
   // minimize x
   optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
   // maximize y with `signed` comparison over bit-vectors.
@@ -109,9 +105,9 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex)
   // maximize z
   optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
 
-  OptimizationResult::ResultType r = optSolver.checkOpt();
+  Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   std::vector<OptimizationResult> results = optSolver.getValues();
 
@@ -180,18 +176,17 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
     (maximize b)
    */
   OptimizationSolver optSolver(d_smtEngine.get());
-  optSolver.setObjectiveCombination(OptimizationSolver::PARETO);
   optSolver.addObjective(a, OptimizationObjective::MAXIMIZE);
   optSolver.addObjective(b, OptimizationObjective::MAXIMIZE);
 
-  OptimizationResult::ResultType r;
+  Result r;
 
   // all possible result pairs <a, b>
   std::set<std::pair<uint32_t, uint32_t>> possibleResults = {
       {1, 3}, {2, 2}, {3, 1}};
 
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  r = optSolver.checkOpt(OptimizationSolver::PARETO);
+  ASSERT_EQ(r.isSat(), Result::SAT);
   std::vector<OptimizationResult> results = optSolver.getValues();
   std::pair<uint32_t, uint32_t> res = {
       results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
@@ -205,8 +200,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
   ASSERT_EQ(possibleResults.count(res), 1);
   possibleResults.erase(res);
 
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  r = optSolver.checkOpt(OptimizationSolver::PARETO);
+  ASSERT_EQ(r.isSat(), Result::SAT);
   results = optSolver.getValues();
   res = {
       results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
@@ -220,8 +215,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
   ASSERT_EQ(possibleResults.count(res), 1);
   possibleResults.erase(res);
 
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  r = optSolver.checkOpt(OptimizationSolver::PARETO);
+  ASSERT_EQ(r.isSat(), Result::SAT);
   results = optSolver.getValues();
   res = {
       results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
@@ -235,8 +230,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
   ASSERT_EQ(possibleResults.count(res), 1);
   possibleResults.erase(res);
 
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::UNSAT);
+  r = optSolver.checkOpt(OptimizationSolver::PARETO);
+  ASSERT_EQ(r.isSat(), Result::UNSAT);
   ASSERT_EQ(possibleResults.size(), 0);
 }
 
@@ -254,11 +249,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
   // y <= x
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
 
-  // Lexico optimization
   OptimizationSolver optSolver(d_smtEngine.get());
 
-  optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
-
   // minimize x
   optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
 
@@ -270,9 +262,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
   // maximize z
   optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
 
-  OptimizationResult::ResultType r = optSolver.checkOpt();
+  // Lexico optimization
+  Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   std::vector<OptimizationResult> results = optSolver.getValues();
 
@@ -290,16 +283,16 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
   d_smtEngine->pop();
 
   // now we only have one objective: (minimize x)
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
+  ASSERT_EQ(r.isSat(), Result::SAT);
   results = optSolver.getValues();
   ASSERT_EQ(results.size(), 1);
   ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
 
   // resetting the assertions also resets the optimization objectives
   d_smtEngine->resetAssertions();
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
+  ASSERT_EQ(r.isSat(), Result::SAT);
   results = optSolver.getValues();
   ASSERT_EQ(results.size(), 0);
 }