summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
Diffstat (limited to 'src/options')
-rw-r--r--src/options/Makefile4
-rw-r--r--src/options/Makefile.am134
-rw-r--r--src/options/base_options110
-rw-r--r--src/options/base_options_handlers.h173
-rw-r--r--src/options/base_options_template.cpp35
-rw-r--r--src/options/base_options_template.h55
-rwxr-xr-xsrc/options/mkoptions1260
-rw-r--r--src/options/options.h150
-rw-r--r--src/options/options.i10
-rw-r--r--src/options/options_holder_template.h42
-rw-r--r--src/options/options_template.cpp471
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback