diff options
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/Makefile | 4 | ||||
-rw-r--r-- | src/options/Makefile.am | 134 | ||||
-rw-r--r-- | src/options/base_options | 110 | ||||
-rw-r--r-- | src/options/base_options_handlers.h | 173 | ||||
-rw-r--r-- | src/options/base_options_template.cpp | 35 | ||||
-rw-r--r-- | src/options/base_options_template.h | 55 | ||||
-rwxr-xr-x | src/options/mkoptions | 1260 | ||||
-rw-r--r-- | src/options/options.h | 150 | ||||
-rw-r--r-- | src/options/options.i | 10 | ||||
-rw-r--r-- | src/options/options_holder_template.h | 42 | ||||
-rw-r--r-- | src/options/options_template.cpp | 471 |
11 files changed, 2444 insertions, 0 deletions
diff --git a/src/options/Makefile b/src/options/Makefile new file mode 100644 index 000000000..54a46191d --- /dev/null +++ b/src/options/Makefile @@ -0,0 +1,4 @@ +topdir = ../.. +srcdir = src/options + +include $(topdir)/Makefile.subdir diff --git a/src/options/Makefile.am b/src/options/Makefile.am new file mode 100644 index 000000000..1f4e991a5 --- /dev/null +++ b/src/options/Makefile.am @@ -0,0 +1,134 @@ +OPTIONS_FILES = \ + options/base_options \ + expr/options \ + theory/booleans/options \ + theory/options \ + theory/bv/options \ + theory/datatypes/options \ + theory/builtin/options \ + theory/arith/options \ + theory/uf/options \ + theory/arrays/options \ + theory/quantifiers/options \ + theory/rewriterules/options \ + prop/options \ + proof/options \ + printer/options \ + smt/options \ + decision/options \ + main/options \ + parser/options + +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = liboptions.la + +liboptions_la_SOURCES = \ + options.h \ + base_options_handlers.h + +nodist_liboptions_la_SOURCES = \ + options.cpp \ + options_holder.h \ + $(OPTIONS_FILES:%=../%.cpp) \ + $(OPTIONS_FILES:%=../%.h) +nodist_liboptions_la_OBJECTS = \ + $(patsubst %.cpp,%.lo,$(filter %.cpp,$(nodist_liboptions_la_SOURCES))) + +BUILT_SOURCES = \ + options.cpp \ + options_holder.h \ + base_options.cpp \ + base_options.h \ + ../smt/smt_options.cpp \ + $(OPTIONS_FILES:%=../%.cpp) \ + $(OPTIONS_FILES:%=../%.h) \ + exprs-builts + +DISTCLEANFILES = \ + $(BUILT_SOURCES) \ + options-stamp + +EXTRA_DIST = \ + mkoptions \ + base_options \ + base_options_template.h \ + base_options_template.cpp \ + options_template.cpp \ + options_holder_template.h \ + options.i \ + $(OPTIONS_FILES:%=../%) + +if CVC4_DEBUG +# listing Debug_tags too ensures that make doesn't auto-remove it +# after building (if it does, we don't get the "cached" effect with +# the .tmp files below, and we have to re-compile and re-link each +# time, even when there are no changes). +BUILT_SOURCES += \ + Debug_tags.h \ + Debug_tags +endif +if CVC4_TRACING +# listing Trace_tags too ensures that make doesn't auto-remove it +# after building (if it does, we don't get the "cached" effect with +# the .tmp files below, and we have to re-compile and re-link each +# time, even when there are no changes). +BUILT_SOURCES += \ + Trace_tags.h \ + Trace_tags +endif +%_tags.h: %_tags + $(AM_V_GEN)( \ + echo 'static char const* const $^[] = {'; \ + for tag in `cat $^`; do \ + echo "\"$$tag\","; \ + done; \ + echo 'NULL'; \ + echo '};' \ + ) >"$@" + +# This .tmp business is to keep from having to re-compile options.cpp +# (and then re-link the libraries) if nothing has changed. +%_tags: %_tags.tmp + $(AM_V_GEN)\ + diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true +# .PHONY ensures the .tmp version is always rebuilt (to check for any changes) +.PHONY: Debug_tags.tmp Trace_tags.tmp +# The "sed" invocation below is particularly obnoxious, but it works around +# inconsistencies in REs on different platforms, using only a basic regular +# expression (no |, no \<, ...). +Debug_tags.tmp Trace_tags.tmp: + $(AM_V_GEN)\ + grep '\<$(@:_tags.tmp=) *( *\".*\" *)' \ + `find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \ + sed 's/^$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/' | sort | uniq >"$@" + +MOSTLYCLEANFILES = \ + Debug_tags \ + Trace_tags \ + Debug_tags.tmp \ + Trace_tags.tmp \ + Debug_tags.h \ + Trace_tags.h + +options_holder.h options.cpp ../smt/smt_options.cpp base_options.cpp base_options.h $(OPTIONS_FILES:%=../%.cpp) $(OPTIONS_FILES:%=../%.h): options-stamp +options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILES:%=../%) + $(AM_V_at)chmod +x @srcdir@/mkoptions + $(AM_V_GEN)(@srcdir@/mkoptions \ + @srcdir@/options_holder_template.h @srcdir@/options_holder.h \ + @srcdir@/options_template.cpp @srcdir@/options.cpp \ + @srcdir@/../smt/smt_options_template.cpp @srcdir@/../smt/smt_options.cpp \ + @top_builddir@/doc/cvc4.1_template @top_builddir@/doc/cvc4.1 \ + -t \ + @srcdir@/base_options_template.h @srcdir@/base_options_template.cpp \ + $(foreach o,$(OPTIONS_FILES),"$(srcdir)/../$(o)" "$(dir $(srcdir)/../$(o))") \ + ) + touch "$@" + +base_options $(OPTIONS_FILES:%=../%):; + +.PHONY: exprs-builts +exprs-builts:; $(AM_V_at)[ "$(FROM_EXPR)" != 1 ] && $(MAKE) -C ../expr builts || true diff --git a/src/options/base_options b/src/options/base_options new file mode 100644 index 000000000..10ad564e6 --- /dev/null +++ b/src/options/base_options @@ -0,0 +1,110 @@ +# +# Option specification file for CVC4 +# +# This is essentially a shell script interpreted with special commands. +# +# Lines starting with whitespace are special. They are passed in their entirety (minus +# the first whitespace char) to the "doc" command. Lines starting with a single slash +# are stripped of this initial character and interpreted by the "doc-alt" command. A period +# "." in the first column of a line, followed optionally by whitespace but without any other +# content on the line, is interpreted as an empty string passed to doc. (This allows +# multi-paragraph documentation for options.) Lines may be continued with a backslash (\) +# at the end of a line. +# +# commands are: +# +# module ID "include-file" name +# +# Identifies the module. Must be the first command in the file. ID is a suitable +# identifier for a preprocessor definition, and should be unique; name is a "pretty" +# name used for the benefit of the end CVC4 user in, e.g., option listings. +# +# common-option SPECIFICATION +# option SPECIFICATION +# expert-option SPECIFICATION +# undocumented-option SPECIFICATION +# +# These commands declare (respectively) common options presented first to the user, +# standard options that the user might want to see with "--help" documentation, +# expert options that should be marked as expert-only, and options that should not +# appear in normal option documentation (even if documentation is included here). +# +# SPECIFICATIONs take this form: +# +# SPECIFICATION ::= (internal-name | -) [-short-option/-alternate-short-option] [--long-option/--alternate-long-option] [smt-option-name] C++-type [ATTRIBUTEs...] +# ATTRIBUTE ::= :include include-files.. +# | :default C++-expression +# | :handler custom-option-handlers.. +# | :handler-include include-files.. +# | :read-only +# | :read-write +# | :link linked-options.. +# +# alias smt-option-name = (smt-option-name[=argument])+ +# alias (-short-option | --long-option) = (-option[=argument] | --long-option[=argument])+ +# +# The alias command creates a new SmtEngine option name, or short option, or long option, +# and binds it to act the same way as if the options to the right of "=" were passed. +# For example, if there are options to --disable-warning-1 and --disable-warning-2, etc., +# a useful alias might be: +# +# alias --disable-all-warnings = --disable-warning-1 --disable-warning-2 +# +# Aliases cannot take arguments, and command-line aliases cannot set SmtEngine properties, +# and SmtEngine aliases cannot set command-line properties. For these things, you need a +# custom handler. +# +# warning message +# +# Warn about something during processing (like a FIXME). +# +# endmodule +# +# This file should end with the "endmodule" command, and nothing should follow it. +# + +module BASE "options/base_options.h" Base + +option binary_name std::string + +option in std::istream* :default &std::cin :include <iostream> +option out std::ostream* :default &std::cout :include <iostream> +option err std::ostream* :default &std::cerr :include <iostream> + +common-option inputLanguage -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write + force input language (default is "auto"; see --lang help) +common-option outputLanguage --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write + force input language (default is "auto"; see --lang help) +option languageHelp bool + +option verbosity verbosity int :read-write :default 0 + the verbosity level of CVC4 +common-option - -v --verbose void :handler CVC4::options::increaseVerbosity + increase verbosity (may be repeated) +common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity + decrease verbosity (may be repeated) + +common-option statistics stats --stats bool + give statistics on exit + +common-option parseOnly parse-only --parse-only bool :read-write + exit after parsing input + +common-option preprocessOnly preprocess-only --preprocess-only bool + exit after preprocessing input + +option segvNoSpin --segv-nospin bool + don't spin on segfault waiting for gdb + +option - -t --trace=TAG argument :handler CVC4::options::addTraceTag + trace something (e.g. -t pushpop), can repeat +option - -d --debug=TAG argument :handler CVC4::options::addDebugTag + debug something (e.g. -d arith), can repeat + +option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h" + print the "success" output required of SMT-LIBv2 + +alias --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success + SMT-LIBv2 compliance mode (implies other options) + +endmodule diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h new file mode 100644 index 000000000..5f82280da --- /dev/null +++ b/src/options/base_options_handlers.h @@ -0,0 +1,173 @@ +/********************* */ +/*! \file base_options_handlers.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#ifndef __CVC4__BASE_OPTIONS_HANDLERS_H +#define __CVC4__BASE_OPTIONS_HANDLERS_H + +#include <iostream> +#include <string> +#include <sstream> + +#include "expr/command.h" + +namespace CVC4 { +namespace options { + +inline void increaseVerbosity(std::string option, SmtEngine* smt) { + options::verbosity.set(options::verbosity() + 1); +} + +inline void decreaseVerbosity(std::string option, SmtEngine* smt) { + options::verbosity.set(options::verbosity() - 1); +} + +inline OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "cvc4" || optarg == "pl") { + return language::output::LANG_CVC4; + } else if(optarg == "smtlib" || optarg == "smt") { + return language::output::LANG_SMTLIB; + } else if(optarg == "smtlib2" || optarg == "smt2") { + return language::output::LANG_SMTLIB_V2; + } else if(optarg == "tptp") { + return language::output::LANG_TPTP; + } else if(optarg == "ast") { + return language::output::LANG_AST; + } else if(optarg == "auto") { + return language::output::LANG_AUTO; + } + + if(optarg != "help") { + throw OptionException(std::string("unknown language for --output-lang: `") + + optarg + "'. Try --output-lang help."); + } + + options::languageHelp.set(true); + return language::output::LANG_AUTO; +} + +inline InputLanguage stringToInputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation") { + return language::input::LANG_CVC4; + } else if(optarg == "smtlib" || optarg == "smt") { + return language::input::LANG_SMTLIB; + } else if(optarg == "smtlib2" || optarg == "smt2") { + return language::input::LANG_SMTLIB_V2; + } else if(optarg == "tptp") { + return language::input::LANG_TPTP; + } else if(optarg == "auto") { + return language::input::LANG_AUTO; + } + + if(optarg != "help") { + throw OptionException(std::string("unknown language for --lang: `") + + optarg + "'. Try --lang help."); + } + + options::languageHelp.set(true); + return language::input::LANG_AUTO; +} + +inline void addTraceTag(std::string option, std::string optarg, SmtEngine* smt) { + if(Configuration::isTracingBuild()) { + if(!Configuration::isTraceTag(optarg.c_str())) + throw OptionException(std::string("trace tag ") + optarg + + std::string(" not available")); + } else { + throw OptionException("trace tags not available in non-tracing builds"); + } + Trace.on(optarg); +} + +inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt) { + if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { + if(!Configuration::isDebugTag(optarg.c_str()) && + !Configuration::isTraceTag(optarg.c_str())) { + throw OptionException(std::string("debug tag ") + optarg + + std::string(" not available")); + } + } else if(! Configuration::isDebugBuild()) { + throw OptionException("debug tags not available in non-debug builds"); + } else { + throw OptionException("debug tags not available in non-tracing builds"); + } + Debug.on(optarg); + Trace.on(optarg); +} + +inline void setPrintSuccess(std::string option, bool value, SmtEngine* smt) { + Debug.getStream() << Command::printsuccess(value); + Trace.getStream() << Command::printsuccess(value); + Notice.getStream() << Command::printsuccess(value); + Chat.getStream() << Command::printsuccess(value); + Message.getStream() << Command::printsuccess(value); + Warning.getStream() << Command::printsuccess(value); + *options::out() << Command::printsuccess(value); +} + +template <template <class U> class Cmp> +class comparator { + long d_lbound; + double d_dbound; + bool d_hasLbound; + +public: + comparator(long l) throw() : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {} + comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {} + + template <class T> + void operator()(std::string option, const T& value, SmtEngine* smt) { + 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(long l) throw() : comparator<std::greater>(l) {} + greater(double d) throw() : comparator<std::greater>(d) {} +};/* struct greater */ + +struct greater_equal : public comparator<std::greater_equal> { + greater_equal(long l) throw() : comparator<std::greater_equal>(l) {} + greater_equal(double d) throw() : comparator<std::greater_equal>(d) {} +};/* struct greater_equal */ + +struct less : public comparator<std::less> { + less(long l) throw() : comparator<std::less>(l) {} + less(double d) throw() : comparator<std::less>(d) {} +};/* struct less */ + +struct less_equal : public comparator<std::less_equal> { + less_equal(long l) throw() : comparator<std::less_equal>(l) {} + less_equal(double d) throw() : comparator<std::less_equal>(d) {} +};/* struct less_equal */ + +struct not_equal : public comparator<std::not_equal_to> { + not_equal(long l) throw() : comparator<std::not_equal_to>(l) {} + not_equal(double d) throw() : comparator<std::not_equal_to>(d) {} +};/* struct not_equal_to */ + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__BASE_OPTIONS_HANDLERS_H */ + diff --git a/src/options/base_options_template.cpp b/src/options/base_options_template.cpp new file mode 100644 index 000000000..97d747652 --- /dev/null +++ b/src/options/base_options_template.cpp @@ -0,0 +1,35 @@ +/********************* */ +/*! \file base_options_template.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Contains code for handling command-line options. + ** + ** Contains code for handling command-line options + **/ + +#include "options/options_holder.h" + +namespace CVC4 { + +${module_accessors} + +#line 26 "${template}" + +namespace options { + +${module_global_definitions} + +#line 32 "${template}" + +}/* CVC4::options namespace */ + +}/* CVC4 namespace */ diff --git a/src/options/base_options_template.h b/src/options/base_options_template.h new file mode 100644 index 000000000..211cb866a --- /dev/null +++ b/src/options/base_options_template.h @@ -0,0 +1,55 @@ +/********************* */ +/*! \file base_options_template.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Contains code for handling command-line options. + ** + ** Contains code for handling command-line options + **/ + +#ifndef __CVC4__OPTIONS__${module_id}_H +#define __CVC4__OPTIONS__${module_id}_H + +#include "options/options.h" +${module_includes} + +#line 26 "${template}" + +${module_optionholder_spec} + +#line 30 "${template}" + +namespace CVC4 { + +namespace options { + +${module_decls} + +#line 38 "${template}" + +}/* CVC4::options namespace */ + +${module_specializations} + +#line 44 "${template}" + +namespace options { + +${module_inlines} + +#line 50 "${template}" + +}/* CVC4::options namespace */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__OPTIONS__${module_id}_H */ 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 + diff --git a/src/options/options.h b/src/options/options.h new file mode 100644 index 000000000..a3abdd54b --- /dev/null +++ b/src/options/options.h @@ -0,0 +1,150 @@ +/********************* */ +/*! \file options.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: taking, cconway + ** Minor contributors (to current version): dejan + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Global (command-line, set-option, ...) parameters for SMT. + ** + ** Global (command-line, set-option, ...) parameters for SMT. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__OPTIONS__OPTIONS_H +#define __CVC4__OPTIONS__OPTIONS_H + +#include <iostream> +#include <fstream> +#include <string> + +#include "util/exception.h" +#include "util/language.h" +#include "util/tls.h" + +namespace CVC4 { + +namespace options { + class OptionsHolder; +}/* CVC4::options namespace */ + +class ExprStream; +class NodeManager; +class NodeManagerScope; +class SmtEngine; + +/** Class representing an option-parsing exception. */ +class CVC4_PUBLIC OptionException : public CVC4::Exception { +public: + OptionException(const std::string& s) throw() : + CVC4::Exception("Error in option parsing: " + s) { + } +};/* class OptionException */ + +class CVC4_PUBLIC Options { + /** The struct that holds all option values. */ + options::OptionsHolder* d_holder; + + /** The current Options in effect */ + static CVC4_THREADLOCAL(Options*) s_current; + + /** Low-level assignment function for options */ + template <class T> + void assign(T, std::string option, std::string value, SmtEngine* smt); + /** Low-level assignment function for bool-valued options */ + template <class T> + void assignBool(T, std::string option, bool value, SmtEngine* smt); + + friend class NodeManager; + friend class NodeManagerScope; + friend class SmtEngine; + +public: + + /** Get the current Options in effect */ + static inline Options& current() { + return *s_current; + } + + Options(); + Options(const Options& options); + ~Options(); + + /** + * Set the value of the given option. Use of this default + * implementation causes a compile-time error; write-able + * options specialize this template with a real implementation. + */ + template <class T> + void set(T, const typename T::type&) { + // Flag a compile-time error. Write-able options specialize + // this template to provide an implementation. + T::you_are_trying_to_assign_to_a_read_only_option; + } + + /** Get the value of the given option. Const access only. */ + template <class T> + const typename T::type& operator[](T) const; + + /** + * Returns true iff the value of the given option was set + * by the user via a command-line option or SmtEngine::setOption(). + * (Options::set() is low-level and doesn't count.) Returns false + * otherwise. + */ + template <class T> + bool wasSetByUser(T) const; + + /** + * Get a description of the command-line flags accepted by + * parseOptions. The returned string will be escaped so that it is + * suitable as an argument to printf. */ + std::string getDescription() const; + + /** + * Print overall command-line option usage message, prefixed by + * "msg"---which could be an error message causing the usage + * output in the first place, e.g. "no such option --foo" + */ + static void printUsage(const std::string msg, std::ostream& out); + + /** + * Print command-line option usage message for only the most-commonly + * used options. The message is prefixed by "msg"---which could be + * an error message causing the usage output in the first place, e.g. + * "no such option --foo" + */ + static void printShortUsage(const std::string msg, std::ostream& out); + + /** Print help for the --lang command line option */ + static void printLanguageHelp(std::ostream& out); + + /** + * Initialize the options based on the given command-line arguments. + */ + int parseOptions(int argc, char* argv[]) throw(OptionException); + + /** + * Set the output language based on the given string. + */ + void setOutputLanguage(const char* str) throw(OptionException); + + /** + * Set the input language based on the given string. + */ + void setInputLanguage(const char* str) throw(OptionException); + +};/* class Options */ + +}/* CVC4 namespace */ + +#include "options/base_options.h" + +#endif /* __CVC4__OPTIONS__OPTIONS_H */ diff --git a/src/options/options.i b/src/options/options.i new file mode 100644 index 000000000..25eecaf2d --- /dev/null +++ b/src/options/options.i @@ -0,0 +1,10 @@ +%{ +#include "options/options.h" +%} + +%ignore CVC4::operator<<(std::ostream&, SimplificationMode); +%ignore CVC4::operator<<(std::ostream&, ArithPivotRule); + +%apply char** STRING_ARRAY { char* argv[] } +%include "options/options.h" +%clear char* argv[]; diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h new file mode 100644 index 000000000..5b2c9a35d --- /dev/null +++ b/src/options/options_holder_template.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file options_holder_template.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Global (command-line, set-option, ...) parameters for SMT + ** + ** Global (command-line, set-option, ...) parameters for SMT. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__OPTIONS__OPTIONS_HOLDER_H +#define __CVC4__OPTIONS__OPTIONS_HOLDER_H + +${include_all_option_headers} + +#line 27 "${template}" + +namespace CVC4 { +namespace options { + +struct OptionsHolder { + OptionsHolder(); +${all_modules_contributions} + +#line 36 "${template}" + +};/* struct OptionsHolder */ + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__OPTIONS__OPTIONS_HOLDER_H */ diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp new file mode 100644 index 000000000..2df69b5d3 --- /dev/null +++ b/src/options/options_template.cpp @@ -0,0 +1,471 @@ +/********************* */ +/*! \file options_template.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Contains code for handling command-line options. + ** + ** Contains code for handling command-line options + **/ + +#include <cstdio> +#include <cstdlib> +#include <new> +#include <string> +#include <sstream> +#include <limits> +#include <unistd.h> +#include <string.h> +#include <stdint.h> +#include <time.h> + +#include <getopt.h> + +#include "expr/expr.h" +#include "util/configuration.h" +#include "util/exception.h" +#include "util/language.h" + +${include_all_option_headers} + +#line 40 "${template}" + +#include "util/output.h" +#include "options/options_holder.h" +#include "cvc4autoconfig.h" +#include "options/base_options_handlers.h" + +${option_handler_includes} + +#line 49 "${template}" + +using namespace CVC4; +using namespace CVC4::options; + +namespace CVC4 { + +CVC4_THREADLOCAL(Options*) Options::s_current = NULL; + +/** + * This is a default handler for options of built-in C++ type. This + * template is really just a helper for the handleOption() template, + * below. Variants of this template handle numeric and non-numeric, + * integral and non-integral, signed and unsigned C++ types. + * handleOption() makes sure to instantiate the right one. + * + * This implements default behavior when e.g. an option is + * unsigned but the user specifies a negative argument; etc. + */ +template <class T, bool is_numeric, bool is_integer> +struct OptionHandler { + static T handle(std::string option, std::string optarg); +};/* struct OptionHandler<> */ + +/** Variant for integral C++ types */ +template <class T> +struct OptionHandler<T, true, true> { + static T handle(std::string option, std::string optarg) { + try { + Integer i(optarg, 0); + + if(! std::numeric_limits<T>::is_signed && i < 0) { + // unsigned type but user gave negative argument + throw OptionException(option + " 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(); + 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(); + throw OptionException(ss.str()); + } + + if(std::numeric_limits<T>::is_signed) { + return T(i.getLong()); + } else { + return T(i.getUnsignedLong()); + } + } catch(std::invalid_argument&) { + // user gave something other than an integer + throw OptionException(option + " requires an integer argument"); + } + } +};/* 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 optarg) { + std::stringstream in(optarg); + long double r; + in >> r; + if(! in.eof()) { + // we didn't consume the whole string (junk at end) + throw OptionException(option + " 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"); + } 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(); + 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(); + throw OptionException(ss.str()); + } + + return T(r); + } +};/* 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 optarg) { + 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 + // don't worry about the segfault in the next line, the "return" is only + // there to keep the compiler from giving additional, distracting errors + // and warnings. + return *(T*)0; + } +};/* 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 optarg) { + return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optarg); +} + +/** Handle an option of type std::string in the default way. */ +template <> +std::string handleOption<std::string>(std::string option, std::string optarg) { + return optarg; +} + +/** + * 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 optarg, SmtEngine* smt) { + // 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, optarg); +} + +template <class T> +void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) { + // By default, nothing to do for bool. Users add things with + // :predicate in options files to provide custom checking routines + // that can throw exceptions. +} + +${all_custom_handlers} + +#line 186 "${template}" + +#ifdef CVC4_DEBUG +# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true +#else /* CVC4_DEBUG */ +# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false +#endif /* CVC4_DEBUG */ + +#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE) +# define DO_SEMANTIC_CHECKS_BY_DEFAULT false +#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */ +# define DO_SEMANTIC_CHECKS_BY_DEFAULT true +#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */ + +Options::Options() : + d_holder(new options::OptionsHolder()) { +} + +Options::Options(const Options& options) : + d_holder(new options::OptionsHolder(*options.d_holder)) { +} + +Options::~Options() { + delete d_holder; +} + +options::OptionsHolder::OptionsHolder() : ${all_modules_defaults} +{ +} + +#line 216 "${template}" + +static const std::string mostCommonOptionsDescription = "\ +Most commonly-used CVC4 options:${common_documentation}"; + +#line 221 "${template}" + +static const std::string optionsDescription = mostCommonOptionsDescription + "\n\ +\n\ +Additional CVC4 options:${remaining_documentation}"; + +#line 227 "${template}" + +static const std::string languageDescription = "\ +Languages currently supported as arguments to the -L / --lang option:\n\ + auto attempt to automatically determine the input language\n\ + pl | cvc4 CVC4 presentation language\n\ + smt | smtlib SMT-LIB format 1.2\n\ + smt2 | smtlib2 SMT-LIB format 2.0\n\ + tptp TPTP format (cnf and fof)\n\ +\n\ +Languages currently supported as arguments to the --output-lang option:\n\ + auto match the output language to the input language\n\ + pl | cvc4 CVC4 presentation language\n\ + smt | smtlib SMT-LIB format 1.2\n\ + smt2 | smtlib2 SMT-LIB format 2.0\n\ + tptp TPTP format\n\ + ast internal format (simple syntax-tree language)\n\ +"; + +std::string Options::getDescription() const { + return optionsDescription; +} + +void Options::printUsage(const std::string msg, std::ostream& out) { + out << msg << optionsDescription << std::endl << std::flush; +} + +void Options::printShortUsage(const std::string msg, std::ostream& out) { + out << msg << mostCommonOptionsDescription << std::endl << std::endl + << "For full usage, please use --help." << std::endl << std::flush; +} + +void Options::printLanguageHelp(std::ostream& out) { + out << languageDescription << std::flush; +} + +/** + * This is a table of long options. By policy, each short option + * should have an equivalent long option (but the reverse isn't the + * case), so this table should thus contain all command-line options. + * + * Each option in this array has four elements: + * + * 1. the long option string + * 2. argument behavior for the option: + * no_argument - no argument permitted + * required_argument - an argument is expected + * optional_argument - an argument is permitted but not required + * 3. this is a pointer to an int which is set to the 4th entry of the + * array if the option is present; or NULL, in which case + * getopt_long() returns the 4th entry + * 4. the return value for getopt_long() when this long option (or the + * value to set the 3rd entry to; see #3) + * + * If you add something here, you should add it in src/main/usage.h + * also, to document it. + * + * If you add something that has a short option equivalent, you should + * add it to the getopt_long() call in parseOptions(). + */ +static struct option cmdlineOptions[] = {${all_modules_long_options} + { NULL, no_argument, NULL, '\0' } +};/* cmdlineOptions */ + +#line 291 "${template}" + +static void preemptGetopt(int& argc, char**& argv, const char* opt) { + const size_t maxoptlen = 128; + + Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl; + + AlwaysAssert(opt != NULL && *opt != '\0'); + AlwaysAssert(strlen(opt) <= maxoptlen); + + ++argc; + unsigned i = 1; + while(argv[i] != NULL && argv[i][0] != '\0') { + ++i; + } + + if(argv[i] == NULL) { + argv = (char**) realloc(argv, (i + 6) * sizeof(char*)); + for(unsigned j = i; j < i + 5; ++j) { + argv[j] = (char*) malloc(sizeof(char) * maxoptlen); + argv[j][0] = '\0'; + } + argv[i + 5] = NULL; + } + + strncpy(argv[i], opt, maxoptlen - 1); + argv[i][maxoptlen - 1] = '\0'; // ensure NUL-termination even on overflow +} + +namespace options { + +/** Set a given Options* as "current" just for a particular scope. */ +class OptionsGuard { + Options** d_field; + Options* d_old; +public: + OptionsGuard(Options** field, Options* opts) : + d_field(field), + d_old(*field) { + *field = opts; + } + ~OptionsGuard() { + *d_field = d_old; + } +};/* class OptionsGuard */ + +}/* CVC4::options namespace */ + +/** Parse argc/argv and put the result into a CVC4::Options. */ +int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { + options::OptionsGuard guard(&s_current, this); + + const char *progName = main_argv[0]; + SmtEngine* const smt = NULL; + + // Reset getopt(), in the case of multiple calls to parseOptions(). + // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. + optind = 0; +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this +#endif /* HAVE_DECL_OPTRESET */ + + // find the base name of the program + const char *x = strrchr(progName, '/'); + if(x != NULL) { + progName = x + 1; + } + d_holder->binary_name = std::string(progName); + + int extra_argc = 1; + char **extra_argv = (char**) malloc(2 * sizeof(char*)); + extra_argv[0] = NULL; + extra_argv[1] = NULL; + + int extra_optind = 0, main_optind = 0; + int old_optind; + + char** argv = main_argv; + + for(;;) { + int c = -1; + Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind << ", extra_argc == " << extra_argc << std::endl; + if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) { +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this +#endif /* HAVE_DECL_OPTRESET */ + old_optind = optind = extra_optind; + argv = extra_argv; + Debug("preemptGetopt") << "in preempt code, next arg is " << extra_argv[optind == 0 ? 1 : optind] << std::endl; + c = getopt_long(extra_argc, extra_argv, + ":${all_modules_short_options}", + cmdlineOptions, NULL); + Debug("preemptGetopt") << "in preempt code, c == " << c << " (`" << char(c) << "') optind == " << optind << std::endl; + if(optind >= extra_argc) { + Debug("preemptGetopt") << "-- no more preempt args" << std::endl; + unsigned i = 0; + while(extra_argv[i] != NULL && extra_argv[i][0] != '\0') { + extra_argv[i][0] = '\0'; + ++i; + } + extra_argc = 1; + extra_optind = 0; + } else { + Debug("preemptGetopt") << "-- more preempt args" << std::endl; + extra_optind = optind; + } + } + if(c == -1) { +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this +#endif /* HAVE_DECL_OPTRESET */ + old_optind = optind = main_optind; + argv = main_argv; + c = getopt_long(argc, main_argv, + ":${all_modules_short_options}", + cmdlineOptions, NULL); + main_optind = optind; + if(c == -1) { + break; + } + } + + Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "')" << std::endl; + + switch(c) { +${all_modules_option_handlers} + +#line 418 "${template}" + + case ':': + // This can be a long or short option, and the way to get at the + // name of it is different. + if(optopt == 0 || + ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) { + // was a long option + throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument"); + } else { + // was a short option + throw OptionException(std::string("option `-") + char(optopt) + "' missing its required argument"); + } + + case '?': + default: + if(optopt == 0 && + !strncmp(argv[optind - 1], "--thread", 8) && + strlen(argv[optind - 1]) > 8 && + isdigit(argv[optind - 1][8])) { + std::vector<std::string>& threadArgv = d_holder->threadArgv; + int tnum = atoi(argv[optind - 1] + 8); + threadArgv.resize(tnum + 1); + if(threadArgv[tnum] != "") { + threadArgv[tnum] += " "; + } + const char* p = strchr(argv[optind - 1] + 9, '='); + if(p == NULL) { // e.g., we have --thread0 "foo" + threadArgv[tnum] += argv[optind++]; + } else { // e.g., we have --thread0="foo" + threadArgv[tnum] += p + 1; + } + break; + } + + // This can be a long or short option, and the way to get at the name of it is different. + if(optopt == 0) { // was a long option + throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "'"); + } else { // was a short option + throw OptionException(std::string("can't understand option `-") + char(optopt) + "'"); + } + } + } + + if((*this)[options::incrementalSolving] && (*this)[options::proof]) { + throw OptionException(std::string("The use of --incremental with --proof is not yet supported")); + } + + return optind; +} + +#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT +#undef DO_SEMANTIC_CHECKS_BY_DEFAULT + +}/* CVC4 namespace */ |