summaryrefslogtreecommitdiff
path: root/src/options/mkoptions
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/mkoptions')
-rwxr-xr-xsrc/options/mkoptions1260
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
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback