Options merge. This commit:

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

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

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

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

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

Benefits of the new options system include:

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

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

1 files changed, 1260 insertions, 0 deletions

diff --git a/src/options/mkoptions b/src/options/mkoptions
new file mode 100755
index 000000000..2bfd6a2d9
--- /dev/null
+++ b/src/options/mkoptions
@@ -0,0 +1,1260 @@
+#!/bin/bash
+#
+# mkoptions
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2011  The CVC4 Project
+#
+# The purpose of this script is to create options.{h,cpp}
+# from template files and a list of options.
+#
+# Invocation:
+#
+#   mkoptions (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+
+#
+
+copyright=2011
+
+me=$(basename "$0")
+
+function usage {
+  echo "usage: $me (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+" >&2
+}
+
+declare -a templates
+declare -a outputs
+
+while [ "$1" != -t ]; do
+  if [ "$#" -lt 2 ]; then
+    echo "$me: error: expected -t on command line" >&2
+    usage
+    exit 1
+  fi
+  templates[${#templates[@]}]="$1"; shift
+  if [ "$1" = -t ]; then
+    echo "$me: error: mismatched number of templates and output files (before -t)" >&2
+    usage
+    exit 1
+  fi
+  outputs[${#outputs[@]}]="$1"; shift
+done
+
+shift
+if [ "$#" -lt 3 ]; then
+  echo "$me: error: not enough arguments" >&2
+  usage
+  exit 1
+fi
+
+options_h_template="$1"; shift
+options_cpp_template="$1"; shift
+
+all_modules_defaults=
+all_modules_short_options=
+all_modules_long_options=
+all_modules_option_handlers=
+smt_getoption_handlers=
+smt_setoption_handlers=
+include_all_option_headers=
+all_modules_contributions=
+option_handler_includes=
+all_custom_handlers=
+common_documentation=
+remaining_documentation=
+common_manpage_documentation=
+remaining_manpage_documentation=
+
+seen_module=false
+seen_endmodule=false
+expect_doc=false
+expect_doc_alternate=false
+n_long=256
+
+internal=
+smtname=
+short_option=
+short_option_alternate=
+long_option=
+long_option_alternate=
+long_option_alternate_set=
+type=
+predicates=
+
+# just for duplicates-checking
+all_declared_internal_options=
+all_declared_long_options=
+all_declared_short_options=
+all_declared_smt_options=
+
+long_option_value_begin=$n_long
+
+function module {
+  # module id name
+
+  module_id=
+  module_name=
+  module_includes=
+  module_optionholder_spec=
+  module_decls=
+  module_specializations=
+  module_inlines=
+  module_accessors=
+  module_global_definitions=
+
+  seen_module=true
+  if [ $# -lt 3 -o -z "$1" -o -z "$2" -o -z "$3" ]; then
+    echo "$kf:$lineno: error: \"module\" directive requires exactly three arguments" >&2
+    exit 1
+  fi
+
+  module_id="$1"; shift
+  include="$1"; shift
+  module_name="$@"
+  include_all_option_headers="${include_all_option_headers}
+#line $lineno \"$kf\"
+#include $(check_include "$include")"
+  all_modules_contributions="${all_modules_contributions}
+  CVC4_OPTIONS__${module_id}__FOR_OPTION_HOLDER"
+  module_optionholder_spec="#define CVC4_OPTIONS__${module_id}__FOR_OPTION_HOLDER"
+
+  remaining_documentation="${remaining_documentation}\\n\\n\"
+#line $lineno \"$kf\"
+\"$module_name options:"
+  remaining_manpage_documentation="${remaining_manpage_documentation}
+.SH `echo "$module_name" | tr a-z A-Z` OPTIONS
+"
+}
+
+function endmodule {
+  # endmodule
+  check_module_seen
+  check_doc
+  seen_endmodule=true
+  if [ $# -ne 0 ]; then
+    echo "$kf:$lineno: error: endmodule takes no arguments" >&2
+    exit 1
+  fi
+}
+
+function common-option {
+  # common-option option-args...
+  handle_option COMMON "$@"
+}
+
+function option {
+  # option option-args...
+  handle_option STANDARD "$@"
+}
+
+function expert-option {
+  # expert-option option-args...
+  handle_option EXPERT "$@"
+}
+
+function undocumented-option {
+  # undocumented-option option-args...
+  handle_option UNDOCUMENTED "$@"
+}
+
+function handle_option {
+  check_module_seen
+  check_doc
+
+  args=("$@")
+
+  category="${args[0]}"
+  internal="${args[1]}"
+  smtname=
+  short_option=
+  short_option_alternate=
+  long_option=
+  long_option_alternate=
+  long_option_alternate_set=
+  type=
+  readOnly=true
+  required_argument=false
+  default_value=
+  handlers=
+  predicates=
+  links=
+  links_alternate=
+
+  options_already_documented=false
+  alternate_options_already_documented=false
+
+  if [ "$category" = UNDOCUMENTED ]; then
+    expect_doc=false
+  else
+    expect_doc=true
+  fi
+  expect_doc_alternate=false
+
+  # scan ahead to see where the type is
+  type_pos=2
+  while [ $(($type_pos+1)) -lt ${#args[@]} ] && ! expr "${args[$(($type_pos+1))]}" : ":" &>/dev/null; do
+    let ++type_pos
+  done
+
+  type="${args[$type_pos]}"
+
+  if [ "$type" = argument ]; then
+    type=void
+    required_argument=true
+  fi
+
+  if [ $type_pos -eq 2 ]; then
+    expect_doc=false
+    readOnly=false
+  else
+    i=2
+    while [ $i -lt $type_pos ]; do
+      if expr "${args[$i]}" : '--' &>/dev/null || expr "${args[$i]}" : '/--' &>/dev/null; then
+        if [ -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
+          exit 1
+        fi
+        long_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
+        if [ -n "$long_option" ]; then
+          if ! expr "$long_option" : '--.' &>/dev/null; then
+            echo "$kf:$option: bad long option \`$long_option': expected something like \`--foo'" >&2
+            exit 1
+          fi
+          long_option="$(echo "$long_option" | sed 's,^--,,')"
+        fi
+        if expr "${args[$i]}" : '.*/' &>/dev/null; then
+          long_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
+          long_option_alternate_set=set
+          if [ -n "$long_option_alternate" ]; then
+            if ! expr "$long_option_alternate" : '--.' &>/dev/null; then
+              echo "$kf:$option: bad alternate long option \`$long_option_alternate': expected something like \`--foo'" >&2
+              exit 1
+            fi
+            long_option_alternate="$(echo "$long_option_alternate" | sed 's,^--,,')"
+          fi
+        fi
+      elif expr "${args[$i]}" : '-' &>/dev/null || expr "${args[$i]}" : '/-' &>/dev/null; then
+        if [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
+          exit 1
+        fi
+        short_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
+        if [ -n "$short_option" ]; then
+          if ! expr "$short_option" : '-.$' &>/dev/null; then
+            echo "$kf:$option: bad short option \`$short_option': expected something like \`-x'" >&2
+            exit 1
+          fi
+          short_option="$(echo "$short_option" | sed 's,^-,,')"
+        fi
+        if expr "${args[$i]}" : '.*/' &>/dev/null; then
+          short_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
+          if expr "$short_option_alternate" : - &>/dev/null; then
+            if ! expr "$short_option_alternate" : '-.$' &>/dev/null; then
+              echo "$kf:$option: bad alternate short option \`$short_option_alternate': expected something like \`-x'" >&2
+              exit 1
+            fi
+            short_option_alternate="$(echo "$short_option_alternate" | sed 's,^-,,')"
+          fi
+        fi
+      else
+        if [ -n "$smtname" -o -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
+          exit 1
+        fi
+        smtname="${args[$i]}"
+      fi
+      let ++i
+    done
+  fi
+
+  if [ "$type" = void -a "$internal" != - ]; then
+    echo "$kf:$lineno: error: $internal cannot be void-typed; use \`-' as the name if its to be void" >&2
+    exit 1
+  elif [ "$type" != void -a "$internal" = - ]; then
+    echo "$kf:$lineno: error: cannot use an unnamed option if its type is not void" >&2
+    exit 1
+  fi
+
+  if [ "$type" = bool -a -n "$long_option$short_option" -a "$category" != UNDOCUMENTED ]; then
+    if [ -n "$short_option_alternate" -o -n "$long_option_alternate" ]; then
+      expect_doc_alternate=true
+    fi
+  fi
+  if [ "$type" = bool -a -n "$long_option" -a -z "$long_option_alternate" -a -z "$long_option_alternate_set" ]; then
+    long_option_alternate="no-$(echo "$long_option" | sed 's,^--,,')"
+  fi
+  if [ "$type" != bool -a -n "$short_option_alternate" ]; then
+    echo "$kf:$lineno: error: cannot use alternate short option -$short_option_alternate for \`$internal' because it's not of bool type" >&2
+    exit 1
+  elif [ "$type" != bool -a -n "$long_option_alternate" ]; then
+    echo "$kf:$lineno: error: cannot use alternate long option --$long_option_alternate for \`$internal' because it's not of bool type" >&2
+    exit 1
+  fi
+
+  # check for duplicates
+  if [ "$internal" != - ]; then
+    if echo " $all_declared_internal_options " | grep -q " $internal "; then
+      echo "$kf:$lineno: error: internal option name \`$internal' previously declared" >&2
+      exit 1
+    fi
+    all_declared_internal_options="$all_declared_internal_options $internal"
+  fi
+  if [ -n "$long_option" ]; then
+    if echo " $all_declared_long_options " | grep -q " $long_option "; then
+      echo "$kf:$lineno: error: long option name \`--$long_option' previously declared" >&2
+      exit 1
+    fi
+    all_declared_long_options="$all_declared_long_options $long_option"
+  fi
+  if [ -n "$long_option_alternate" ]; then
+    if echo " $all_declared_long_options " | grep -q " $long_option_alternate "; then
+      echo "$kf:$lineno: error: long option name \`--$long_option_alternate' previously declared" >&2
+      exit 1
+    fi
+    all_declared_long_options="$all_declared_long_options $long_option_alternate"
+  fi
+  if [ -n "$short_option" ]; then
+    if echo " $all_declared_short_options " | grep -q " $short_option "; then
+      echo "$kf:$lineno: error: short option name \`-$short_option' previously declared" >&2
+      exit 1
+    fi
+    all_declared_short_options="$all_declared_short_options $short_option"
+  fi
+  if [ -n "$short_option_alternate" ]; then
+    if echo " $all_declared_short_options " | grep -q " $short_option_alternate "; then
+      echo "$kf:$lineno: error: short option name \`-$short_option_alternate' previously declared" >&2
+      exit 1
+    fi
+    all_declared_short_options="$all_declared_short_options $short_option_alternate"
+  fi
+  if [ -n "$smtname" ]; then
+    if echo " $all_declared_smt_options " | grep -q " $smtname "; then
+      echo "$kf:$lineno: error: SMT option name \`$smtname' previously declared" >&2
+      exit 1
+    fi
+    all_declared_smt_options="$all_declared_smt_options $smtname"
+  fi
+
+  # parse attributes
+  i=$(($type_pos+1))
+  while [ $i -lt ${#args[@]} ]; do
+    attribute="${args[$i]}"
+    case "$attribute" in
+    :default)
+       let ++i
+       default_value="${args[$i]}"
+       ;;
+    :handler)
+       let ++i
+       if [ -n "$handlers" ]; then
+         echo "$kf:$lineno: error: cannot specify more than one handler; maybe you want a :handler and a :predicate" >&2
+         exit 1
+       fi
+       handlers="${args[$i]}"
+       ;;
+    :predicate)
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+         let ++i
+         predicates="${predicates} ${args[$i]}"
+       done
+       ;;
+    :link)
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+         let ++i
+         link="${args[$i]}"
+         if expr "${args[$i]}" : '.*/' &>/dev/null; then
+           links="${links} $(echo "${args[$i]}" | sed 's,/.*,,')"
+           links_alternate="${links_alternate} $(echo "${args[$i]}" | sed 's,[^/]*/,,')"
+         else
+           links="${links} ${args[$i]}"
+           links_alternate="${links_alternate} ${args[$i]}"
+         fi
+       done
+       ;;
+    :include)
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+         let ++i
+         module_includes="${module_includes}
+#line $lineno \"$kf\"
+#include $(check_include "${args[$i]}")"
+       done
+       ;;
+    :handler-include|:predicate-include)
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+         let ++i
+         option_handler_includes="${option_handler_includes}
+#line $lineno \"$kf\"
+#include $(check_include "${args[$i]}")"
+       done
+       ;;
+    :read-write)
+       readOnly=false
+       ;;
+    :read-only)
+       readOnly=true
+       ;;
+    *)
+       echo "$kf:$lineno: error in option \`$internal': bad attribute \`$attribute'" >&2
+       exit 1
+    esac
+    let ++i
+  done
+
+  # set up structures
+  if [ "$internal" != - ]; then
+    # set up a field in the options_holder
+    module_optionholder_spec="${module_optionholder_spec} \\
+  ${internal}__option_t::type $internal; \\
+  bool ${internal}__setByUser__;"
+    all_modules_defaults="${all_modules_defaults:+${all_modules_defaults},}
+#line $lineno \"$kf\"
+  $internal($default_value),
+#line $lineno \"$kf\"
+  ${internal}__setByUser__(false)"
+    if $readOnly; then
+      module_decls="${module_decls}
+#line $lineno \"$kf\"
+extern struct CVC4_PUBLIC ${internal}__option_t { typedef $type type; type operator()() const; bool wasSetByUser() const; } $internal CVC4_PUBLIC;"
+      module_inlines="${module_inlines}
+#line $lineno \"$kf\"
+inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return Options::current()[*this]; }
+#line $lineno \"$kf\"
+inline bool ${internal}__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
+"
+    else
+      module_decls="${module_decls}
+#line $lineno \"$kf\"
+extern struct CVC4_PUBLIC ${internal}__option_t { typedef $type type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } $internal CVC4_PUBLIC;"
+      module_inlines="${module_inlines}
+#line $lineno \"$kf\"
+inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return Options::current()[*this]; }
+#line $lineno \"$kf\"
+inline bool ${internal}__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
+#line $lineno \"$kf\"
+inline void ${internal}__option_t::set(const ${internal}__option_t::type& v) { Options::current().set(*this, v); }
+"
+      module_specializations="${module_specializations}
+#line $lineno \"$kf\"
+template <> void Options::set(options::${internal}__option_t, const options::${internal}__option_t::type& x);"
+      module_accessors="${module_accessors}
+#line $lineno \"$kf\"
+template <> void Options::set(options::${internal}__option_t, const options::${internal}__option_t::type& x) { d_holder->$internal = x; }"
+    fi
+    module_global_definitions="${module_global_definitions}
+#line $lineno \"$kf\"
+struct ${internal}__option_t $internal;"
+    module_specializations="${module_specializations}
+#line $lineno \"$kf\"
+template <> const options::${internal}__option_t::type& Options::operator[](options::${internal}__option_t) const;
+#line $lineno \"$kf\"
+template <> bool Options::wasSetByUser(options::${internal}__option_t) const;"
+    if [ "$type" = bool ]; then
+      module_specializations="${module_specializations}
+#line $lineno \"$kf\"
+template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, SmtEngine* smt);"
+    elif [ "$internal" != - ]; then
+      module_specializations="${module_specializations}
+#line $lineno \"$kf\"
+template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt);"
+    fi
+
+    module_accessors="${module_accessors}
+#line $lineno \"$kf\"
+template <> const options::${internal}__option_t::type& Options::operator[](options::${internal}__option_t) const { return d_holder->$internal; }
+#line $lineno \"$kf\"
+template <> bool Options::wasSetByUser(options::${internal}__option_t) const { return d_holder->${internal}__setByUser__; }"
+  fi
+
+  if $required_argument || [ "$type" != bool -a "$type" != void ]; then
+    expect_arg=:
+    expect_arg_long=required_argument
+  else
+    expect_arg=
+    expect_arg_long=no_argument
+  fi
+  cases=
+  cases_alternate=
+  if [ -n "$short_option" ]; then
+    all_modules_short_options="${all_modules_short_options}$short_option$expect_arg"
+    cases="${cases}
+    case '$short_option':"
+  fi
+  if [ -n "$short_option_alternate" ]; then
+    all_modules_short_options="${all_modules_short_options}$short_option_alternate$expect_arg"
+    cases_alternate="${cases_alternate}
+    case '$short_option_alternate':"
+  fi
+  if [ -n "$long_option" ]; then
+    all_modules_long_options="${all_modules_long_options}
+  { \"$(echo "$long_option" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long },"
+    cases="${cases}
+    case $n_long:// --$long_option"
+    let ++n_long
+  fi
+  if [ -n "$long_option_alternate" ]; then
+    all_modules_long_options="${all_modules_long_options}
+  { \"$(echo "$long_option_alternate" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long },"
+    cases_alternate="${cases_alternate}
+    case $n_long:// --$long_option_alternate"
+    let ++n_long
+  fi
+  run_links=
+  run_links_alternate=
+  if [ -n "$links" ]; then
+    for link in $links; do
+      run_links="$run_links
+#line $lineno \"$kf\"
+      preemptGetopt(extra_argc, extra_argv, \"$link\");"
+    done
+  fi
+  if [ -n "$links_alternate" ]; then
+    for link in $links_alternate; do
+      run_links_alternate="$run_links_alternate
+#line $lineno \"$kf\"
+      preemptGetopt(extra_argc, extra_argv, \"$link\");"
+    done
+  fi
+  if [ "$type" = bool -a -n "$cases" -o -n "$cases_alternate" ]; then
+    run_handlers=
+    if [ -n "$handlers" ]; then
+      echo "$kf:$lineno: error: bool-valued options cannot have handlers" >&2
+      exit 1
+    fi
+    if [ -n "$predicates" ]; then
+      for predicate in $predicates; do
+        run_handlers="$run_handlers
+#line $lineno \"$kf\"
+  $predicate(option, b, smt);"
+      done
+    fi
+    if [ -n "$run_handlers" ]; then
+      all_custom_handlers="${all_custom_handlers}
+#line $lineno \"$kf\"
+template <> void runBoolPredicates(options::${internal}__option_t, std::string option, bool b, SmtEngine* smt) {
+  $run_handlers
+}"
+    fi
+  fi
+  if [ -n "$cases" ]; then
+    if [ "$type" = bool ]; then
+      all_modules_option_handlers="${all_modules_option_handlers}${cases}
+#line $lineno \"$kf\"
+      assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], true, NULL);$run_links
+      break;
+"
+    elif [ -n "$expect_arg" -a "$internal" != - ]; then
+      run_handlers=
+      if [ -n "$handlers" ]; then
+        for handler in $handlers; do
+          run_handlers="$run_handlers
+#line $lineno \"$kf\"
+  $handler(option, optarg, smt);"
+        done
+      else
+        run_handlers="
+#line $lineno \"$kf\"
+  handleOption<$type>(option, optarg);"
+      fi
+      if [ -n "$predicates" ]; then
+        for predicate in $predicates; do
+          run_handlers="$run_handlers
+#line $lineno \"$kf\"
+  $predicate(option, retval, smt);"
+        done
+      fi
+      all_custom_handlers="${all_custom_handlers}
+#line $lineno \"$kf\"
+template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optarg, SmtEngine* smt) {
+#line $lineno \"$kf\"
+  options::${internal}__option_t::type retval = $run_handlers
+#line $lineno \"$kf\"
+  return retval;
+}"
+      all_modules_option_handlers="${all_modules_option_handlers}${cases}
+#line $lineno \"$kf\"
+      assign(options::$internal, argv[old_optind == 0 ? 1 : old_optind], optarg, NULL);$run_links
+      break;
+"
+    elif [ -n "$expect_arg" ]; then
+      run_handlers=
+      if [ -n "$predicates" ]; then
+        echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
+        exit 1
+      fi
+      if [ -n "$handlers" ]; then
+        for handler in $handlers; do
+          run_handlers="$run_handlers
+#line $lineno \"$kf\"
+      $handler(argv[old_optind == 0 ? 1 : old_optind], optarg, smt);"
+        done
+      fi
+      all_modules_option_handlers="${all_modules_option_handlers}${cases}
+#line $lineno \"$kf\"
+      $run_handlers$run_links
+      break;
+"
+    else
+      run_handlers=
+      if [ -n "$predicates" ]; then
+        echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
+        exit 1
+      fi
+      if [ -n "$handlers" ]; then
+        for handler in $handlers; do
+          run_handlers="$run_handlers
+#line $lineno \"$kf\"
+      $handler(argv[old_optind == 0 ? 1 : old_optind], smt);"
+        done
+      fi
+      all_modules_option_handlers="${all_modules_option_handlers}${cases}
+#line $lineno \"$kf\"
+      $run_handlers$run_links
+      break;
+"
+    fi
+  fi
+  if [ -n "$cases_alternate" ]; then
+    if [ "$type" = bool ]; then
+      all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate}
+#line $lineno \"$kf\"
+      assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], false, NULL);$run_links_alternate
+      break;
+"
+    else
+      echo "$kf:$lineno: internal error: expected BOOL-typed option in alternate handler" >&2
+      exit 1
+    fi
+  fi
+
+  if [ -n "$smtname" ]; then
+    if [ "$internal" != - ]; then
+      smt_getoption_handlers="${smt_getoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    stringstream ss; ss << options::$internal();
+    return SExpr(ss.str());
+  }"
+    fi
+
+    if [ "$type" = bool ]; then
+      smt_setoption_handlers="${smt_setoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    Options::current().assignBool(options::$internal, \"$smtname\", optarg == \"true\", smt);$run_links
+    return;
+  }"
+    elif [ -n "$expect_arg" -a "$internal" != - ]; then
+      run_handlers=
+      if [ -n "$handlers" ]; then
+        for handler in $handlers; do
+          run_handlers="$run_handlers
+#line $lineno \"$kf\"
+    $handler(\"$smtname\", value, smt);
+"
+        done
+      fi
+      smt_setoption_handlers="${smt_setoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    Options::current().assign(options::$internal, \"$smtname\", optarg, smt);$run_links
+    return;
+  }"
+    elif [ -n "$expect_arg" ]; then
+      run_handlers=
+      for handler in $handlers; do
+        run_handlers="$run_handlers
+#line $lineno \"$kf\"
+    $handler(\"$smtname\", value, smt);
+"
+      done
+      smt_setoption_handlers="${smt_setoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    $run_handlers$run_links
+    return;
+  }"
+    else
+      run_handlers=
+      for handler in $handlers; do
+        run_handlers="$run_handlers
+#line $lineno \"$kf\"
+    $handler(\"$smtname\", smt);
+"
+      done
+      smt_setoption_handlers="${smt_setoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    $run_handlers$run_links
+    return;
+  }"
+    fi
+  fi
+
+  if [ "$type" = bool ]; then
+    # emit assignBool/assign
+    all_custom_handlers="${all_custom_handlers}
+#line $lineno \"$kf\"
+template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, SmtEngine* smt) {
+#line $lineno \"$kf\"
+  runBoolPredicates(options::$internal, option, value, smt);
+#line $lineno \"$kf\"
+  d_holder->$internal = value;
+#line $lineno \"$kf\"
+  d_holder->${internal}__setByUser__ = true;
+#line $lineno \"$kf\"
+  Trace(\"options\") << \"user assigned option $internal\" << std::endl;
+}"
+  elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o "$cases_alternate" -o "$smtname" ]; then
+    all_custom_handlers="${all_custom_handlers}
+#line $lineno \"$kf\"
+template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt) {
+#line $lineno \"$kf\"
+  d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, smt);
+#line $lineno \"$kf\"
+  d_holder->${internal}__setByUser__ = true;
+#line $lineno \"$kf\"
+  Trace(\"options\") << \"user assigned option $internal\" << std::endl;
+}"
+  fi
+}
+
+function alias {
+  # alias (smtname | -option) = (smtname [arg] | -option [arg])+
+  check_module_seen
+  check_doc
+
+  category=STANDARD
+  internal=-
+  smtname=
+  short_option=
+  short_option_alternate=
+  long_option=
+  long_option_alternate=
+  long_option_alternate_set=
+  type=void
+  readOnly=true
+  required_argument=false
+  default_value=
+  handlers=
+  predicates=
+  links=
+  links_alternate=
+
+  options_already_documented=false
+  alternate_options_already_documented=false
+
+  if [ $# -lt 3 ]; then
+    echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
+    exit 1
+  fi
+  options=
+  while [ $# -gt 0 -a "$1" != = ]; do
+    options="$options $1"
+    shift
+  done
+  if [ $# -eq 0 ]; then
+    echo "$kf:$lineno: error: malformed \"alias\" command; expected \`='" >&2
+    exit 1
+  fi
+  shift
+  if [ $# -eq 0 ]; then
+    echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
+    exit 1
+  fi
+  cases=
+  for option in $options; do
+    if ! expr "$option" : - &>/dev/null; then
+      echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2
+      exit 1
+    fi
+    if expr "$option" : -- &>/dev/null; then
+      option="$(echo "$option" | sed 's,--,,')"
+      all_modules_long_options="${all_modules_long_options}
+  { \"$(echo "$option" | sed 's,=.*,,')\", no_argument, NULL, $n_long },"
+      cases="${cases}
+    case $n_long:// --$option"
+      let ++n_long
+      long_option="${long_option:+$long_option | --}$option"
+    else
+      if ! expr "$option" : '-.$' &>/dev/null; then
+        echo "$kf:$lineno: error: expected short option specification, got \`$option'" >&2
+        exit 1
+      fi
+      option="$(echo "$option" | sed 's,-,,')"
+      all_modules_short_options="${all_modules_short_options}$option"
+      cases="${cases}
+    case '$option':"
+      short_option="${short_option:+$short_option | -}$option"
+    fi
+  done
+  while [ $# -gt 0 ]; do
+    links="$links
+#line $lineno \"$kf\"
+      preemptGetopt(extra_argc, extra_argv, \"$1\");"
+    shift
+  done
+  all_modules_option_handlers="$all_modules_option_handlers$cases$links
+      break;
+"
+  expect_doc=true
+  expect_doc_alternate=false
+}
+
+function warning {
+  # warning message
+  check_module_seen
+  check_doc
+
+  echo "$kf:$lineno: warning: $@" >&2
+}
+
+function doc {
+  # doc text...
+  check_module_seen
+  expect_doc=false
+
+  if [ -z "$short_option" -a -z "$long_option" ]; then
+    if [ -n "$short_option_alternate" -o -n "$long_option_alternate" ]; then
+      if [ -n "$smtname" ]; then
+        expect_doc_alternate=true
+      else
+        doc-alternate "$@"
+        return
+      fi
+    fi
+  fi
+
+  if [ "$category" = UNDOCUMENTED ]; then
+    return
+  fi
+
+  if ! $options_already_documented; then
+    options_already_documented=true
+    the_opt=
+    if [ "$long_option" ]; then
+      the_opt="--$long_option"
+      if [ "$short_option" ]; then
+        shortoptarg=
+        if expr "$the_opt" : '.*=' &>/dev/null; then
+          shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')"
+        fi
+        the_opt="$the_opt | -$short_option$shortoptarg"
+      fi
+    elif [ "$short_option" ]; then
+      the_opt="-$short_option"
+    fi
+    if [ -z "$the_opt" ]; then
+      # nothing to document
+      return
+    fi
+
+    the_doc="$@"
+    if [ "$category" = EXPERT ]; then
+      the_doc="$the_doc (EXPERTS only)"
+    fi
+
+    doc_line=
+    while [ -n "$the_doc" ]; do
+      remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')"
+      the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')"
+      if [ -z "$doc_line" ]; then
+        if expr "$the_opt" : '.\{23\}' &>/dev/null; then
+          # break into two lines
+          doc_line="$(printf '  %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")"
+        else
+          doc_line="$(printf '  %-22s %s' "$the_opt" "$the_doc")"
+        fi
+      else
+        doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")"
+      fi
+      the_doc="$(expr "$remaining_doc" : '\(.*\) ')"
+    done
+
+    if [ "$category" = COMMON ]; then
+      common_documentation="${common_documentation}\\n\"
+#line $lineno \"$kf\"
+\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
+      common_manpage_documentation="${common_manpage_documentation}
+.IP \"$the_opt\"
+$@"
+    else
+      remaining_documentation="${remaining_documentation}\\n\"
+#line $lineno \"$kf\"
+\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
+      remaining_manpage_documentation="${remaining_manpage_documentation}
+.IP \"$the_opt\"
+$@"
+    fi
+  else
+    if [ "$category" = COMMON ]; then
+      common_manpage_documentation="${common_manpage_documentation}
+$@"
+    else
+      remaining_manpage_documentation="${remaining_manpage_documentation}
+$@"
+    fi
+  fi
+}
+
+function doc-alternate {
+  # doc-alternate text...
+  check_module_seen
+  expect_doc_alternate=false
+
+  if $expect_doc; then
+    echo "$kf:$lineno: error: must provide documentation before alternate documentation" >&2
+    exit 1
+  fi
+
+  if [ -z "$short_option_alternate" -a -z "$long_option_alternate" ]; then
+    echo "$kf:$lineno: cannot document an alternative for option \`$internal'; one does not exist" >&2
+    exit 1
+  fi
+
+  if [ "$category" = UNDOCUMENTED ]; then
+    return
+  fi
+
+  if ! $alternate_options_already_documented; then
+    alternate_options_already_documented=true
+    the_opt=
+    if [ "$long_option_alternate" ]; then
+      the_opt="--$long_option_alternate"
+      shortoptarg=
+      if expr "$the_opt" : '.*=' &>/dev/null; then
+        shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')"
+      fi
+      if [ "$short_option_alternate" ]; then
+        the_opt="$the_opt | -$short_option_alternate$shortoptarg"
+      fi
+    elif [ "$short_option_alternate" ]; then
+      the_opt="-$short_option_alternate"
+    fi
+    if [ -z "$the_opt" ]; then
+      # nothing to document
+      return
+    fi
+
+    the_doc="$@"
+    if [ "$category" = EXPERT ]; then
+      the_doc="$the_doc (EXPERTS only)"
+    fi
+
+    doc_line=
+    while [ -n "$the_doc" ]; do
+      remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')"
+      the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')"
+      if [ -z "$doc_line" ]; then
+        if expr "$the_opt" : '.\{23\}' &>/dev/null; then
+          # break into two lines
+          doc_line="$(printf '  %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")"
+        else
+          doc_line="$(printf '  %-22s %s' "$the_opt" "$the_doc")"
+        fi
+      else
+        doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")"
+      fi
+      the_doc="$(expr "$remaining_doc" : '\(.*\) ')"
+    done
+
+    if [ "$category" = COMMON ]; then
+      common_documentation="${common_documentation}\\n\"
+#line $lineno \"$kf\"
+\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
+      common_manpage_documentation="${common_manpage_documentation}
+.IP \"$the_opt\"
+$@"
+    else
+      remaining_documentation="${remaining_documentation}\\n\"
+#line $lineno \"$kf\"
+\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
+      remaining_manpage_documentation="${remaining_manpage_documentation}
+.IP \"$the_opt\"
+$@"
+    fi
+  else
+    if [ "$category" = COMMON ]; then
+      common_manpage_documentation="${common_manpage_documentation}
+$@"
+    else
+      remaining_manpage_documentation="${remaining_manpage_documentation}
+$@"
+    fi
+  fi
+}
+
+function check_doc {
+  if $expect_doc; then
+    if [ "$internal" != - ]; then
+      echo "$kf:$lineno: warning: $internal is lacking documentation" >&2
+    elif [ -n "$long_option" ]; then
+      echo "$kf:$lineno: warning: option --$long_option is lacking documentation" >&2
+    elif [ -n "$short_option" ]; then
+      echo "$kf:$lineno: warning: option -$short_option is lacking documentation" >&2
+    elif [ -n "$smtname" ]; then
+      echo "$kf:$lineno: warning: SMT option $smtname is lacking documentation" >&2
+    fi
+    expect_doc=false
+  fi
+
+  if $expect_doc_alternate; then
+    echo "$kf:$lineno: warning: $internal is lacking documentation for the alternative option(s): $short_option_alternate $long_option_alternate" >&2
+    expect_doc_alternate=false
+  fi
+}
+
+function check_module_seen {
+  if $seen_endmodule; then
+    echo "$kf:$lineno: error: command after \"endmodule\" declaration (endmodule has to be last)" >&2
+    exit 1
+  fi
+  if ! $seen_module; then
+    echo "$kf:$lineno: error: no \"module\" declaration found (it has to be first)" >&2
+    exit 1
+  fi
+}
+
+function check_include {
+  if ! expr "$1" : '".*"$' &>/dev/null && ! expr "$1" : '<.*>$' &>/dev/null; then
+    echo "\"$1\""
+  else
+    echo "$1"
+  fi
+}
+
+function output_module {
+  template="$1"
+  output="$2"
+
+  filename="$(basename "$output")"
+
+  #echo "generating module $output from $template"
+
+  # generate warnings about incorrect #line annotations in templates
+  nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
+    awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
+
+  text=$(cat "$template")
+  for var in \
+      module_id \
+      module_name \
+      module_includes \
+      module_optionholder_spec \
+      module_decls \
+      module_specializations \
+      module_inlines \
+      module_accessors \
+      module_global_definitions \
+      template \
+      ; do
+    eval text="\${text//\\\$\\{$var\\}/\${$var}}"
+  done
+  error="$(echo "$text" | grep '.*\${[^}]*}.*' | head -n 1)"
+  if [ -n "$error" ]; then
+    error="$(echo "$error" | sed 's,.*\${\([^}]*\)}.*,\1,')"
+    echo "$template:0: error: undefined replacement \${$error}" >&2
+    exit 1
+  fi
+
+  (
+
+  # Output header (if this is a .cpp or .c or .h file) and then the
+  # processed text
+
+  if expr "$output" : '.*\.cpp$' &>/dev/null || expr "$output" : '.*\.[ch]$' &>/dev/null; then
+
+  cat <<EOF
+/*********************                                                        */
+/** $filename
+ **
+ ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ **
+ ** This file automatically generated by:
+ **
+ **     $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* Edit the template file instead:                     */
+/* $1 */
+
+EOF
+  fi
+
+  echo "$text"
+
+  ) >"$output.tmp"
+
+  diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && echo "regenerated $output")
+  rm -f "$output.tmp"
+}
+
+while [ $# -gt 0 ]; do
+  kf="$1"; shift
+  if [ $# -eq 0 ]; then
+    echo "$me: error: mismatched number of templates and output files (before -t)" >&2
+    usage
+    exit 1
+  fi
+  outdir="$1"; shift
+
+  #echo "scanning $kf"
+
+  seen_module=false
+  seen_endmodule=false
+  b=$(basename $(dirname "$kf"))
+  lineno=0
+  # IFS= forces read to read an entire line
+  while IFS= read -r line; do
+    let ++lineno
+    # read any continuations of the line
+    while expr "$line" : '.*\\$' &>/dev/null; do
+      IFS= read -r line2
+      line="$(echo "$line" | sed 's,\\$,,')$line2"
+      let ++lineno
+    done
+    if expr "$line" : '[ 	].*' &>/dev/null; then
+      doc "$(echo "$line" | sed 's,^[ 	],,')"
+    elif expr "$line" : '\.[ 	]*$' &>/dev/null; then
+      doc ""
+    elif expr "$line" : '\.' &>/dev/null; then
+      echo "$kf:$lineno: error: malformed line during processing of option \`$internal': continuation lines should not have content" >&2
+      exit 1
+    elif expr "$line" : '/.*' &>/dev/null; then
+      doc-alternate "$(echo "$line" | sed 's,^/,,')"
+    else
+      line="$(echo "$line" | sed 's,\([<>&()!?*]\),\\\1,g')"
+      if ! eval "$line"; then
+        echo "$kf:$lineno: error was due to evaluation of this line" >&2
+        exit 1
+      fi
+    fi
+  done < "$kf"
+  if ! $seen_module; then
+    echo "$kf: error: no module content found in file!" >&2
+    exit 1
+  fi
+  if ! $seen_endmodule; then
+    echo "$kf:$lineno: error: no \"endmodule\" declaration found (it is required at the end)" >&2
+    exit 1
+  fi
+
+  output_module "$options_h_template" "$outdir/$(basename "$kf").h"
+  output_module "$options_cpp_template" "$outdir/$(basename "$kf").cpp"
+done
+
+## final outputs
+
+i=0; while [ $i -lt ${#templates[@]} ]; do
+
+template="${templates[$i]}"
+output="${outputs[$i]}"
+
+let ++i
+
+filename="$(basename "$output")"
+
+#echo "generating $output from $template"
+
+# generate warnings about incorrect #line annotations in templates
+nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
+  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
+
+long_option_value_end=$n_long
+
+text=$(cat "$template")
+for var in \
+    all_modules_defaults \
+    all_modules_short_options \
+    all_modules_long_options \
+    all_modules_option_handlers \
+    include_all_option_headers \
+    all_modules_contributions \
+    option_handler_includes \
+    all_custom_handlers \
+    common_documentation \
+    remaining_documentation \
+    common_manpage_documentation \
+    remaining_manpage_documentation \
+    smt_getoption_handlers \
+    smt_setoption_handlers \
+    long_option_value_begin \
+    long_option_value_end \
+    template \
+    ; do
+  eval text="\${text//\\\$\\{$var\\}/\${$var}}"
+done
+error="$(echo "$text" | grep '.*\${[^}]*}.*' | head -n 1)"
+if [ -n "$error" ]; then
+  error="$(echo "$error" | sed 's,.*\${\([^}]*\)}.*,\1,')"
+  echo "$template:0: error: undefined replacement \${$error}" >&2
+  exit 1
+fi
+
+(
+
+# Output header (if this is a .cpp or .c or .h file) and then the
+# processed text
+
+if expr "$output" : '.*\.cpp$' &>/dev/null || expr "$output" : '.*\.[ch]$' &>/dev/null; then
+
+cat <<EOF
+/*********************                                                        */
+/** $filename
+ **
+ ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ **
+ ** This file automatically generated by:
+ **
+ **     $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* Edit the template file instead:                     */
+/* $1 */
+
+EOF
+fi
+
+echo "$text"
+
+) >"$output.tmp"
+
+diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && echo "regenerated $output")
+rm -f "$output.tmp"
+
+done
+