Properly consider aliases in option handlers (#6683)

This PR makes sure that option handlers have access to both the canonical option name and the option name that was actually used. It also updates the options README and gets rid of the base_handlers.h of which only a fraction was used.

9 files changed, 468 insertions, 369 deletions

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]]