diff options
| author | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
| commit | 2ba8bb701ce289ba60afec01b653b0930cc59298 (patch) | |
| tree | 46df365b7b41ce662a0f94de5b11c3ed20829851 /src/options | |
| parent | 42b665f2a00643c81b42932fab1441987628c5a5 (diff) | |
Adding listeners to Options.
- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.
- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.
- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.
- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.
- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.
- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.
- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
Diffstat (limited to 'src/options')
37 files changed, 3162 insertions, 1028 deletions
diff --git a/src/options/Makefile.am b/src/options/Makefile.am index cf38708e1..8a465c522 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -162,16 +162,16 @@ CPP_TEMPLATE_FILES = \ base_options_template.cpp \ options_holder_template.h \ options_template.cpp \ - options_handler_get_option_template.cpp \ - options_handler_set_option_template.cpp + options_get_option_template.cpp \ + options_set_option_template.cpp CPP_TEMPLATE_SEDS = \ base_options_template.h.sed \ base_options_template.cpp.sed \ options_holder_template.h.sed \ options_template.cpp.sed \ - options_handler_get_option_template.cpp.sed \ - options_handler_set_option_template.cpp.sed + options_get_option_template.cpp.sed \ + options_set_option_template.cpp.sed DOCUMENTATION_FILES = \ @@ -206,6 +206,8 @@ liboptions_la_SOURCES = \ arith_propagation_mode.h \ arith_unate_lemma_mode.cpp \ arith_unate_lemma_mode.h \ + argument_extender.cpp \ + argument_extender.h \ base_handlers.h \ boolean_term_conversion_mode.cpp \ boolean_term_conversion_mode.h \ @@ -218,11 +220,13 @@ liboptions_la_SOURCES = \ didyoumean.h \ language.cpp \ language.h \ - logic_info_forward.h \ + open_ostream.cpp \ + open_ostream.h \ option_exception.h \ options.h \ - options_handler_interface.cpp \ - options_handler_interface.h \ + options_handler.cpp \ + options_handler.h \ + options_public_functions.cpp \ printer_modes.cpp \ printer_modes.h \ quantifiers_modes.cpp \ @@ -241,8 +245,8 @@ nodist_liboptions_la_SOURCES = \ options_holder.h \ $(OPTIONS_HEADS) \ $(OPTIONS_CPPS) \ - options_handler_get_option.cpp \ - options_handler_set_option.cpp + options_get_option.cpp \ + options_set_option.cpp BUILT_SOURCES = \ @@ -254,20 +258,11 @@ BUILT_SOURCES = \ $(OPTIONS_OPTIONS_FILES) \ $(OPTIONS_SEDS) \ options.cpp \ - options_handler_get_option.cpp \ - options_handler_set_option.cpp \ + options_get_option.cpp \ + options_set_option.cpp \ options_holder.h \ summary.sed -# listing {Debug,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 += \ - Debug_tags.h \ - Debug_tags \ - Trace_tags.h \ - Trace_tags CLEANFILES = \ $(BUILT_SOURCES) \ @@ -283,47 +278,19 @@ EXTRA_DIST = \ base_options_template.h \ language.i \ mkoptions \ - mktagheaders \ - mktags \ option_exception.i \ options.i \ - options_handler_get_option_template.cpp \ - options_handler_interface.i \ - options_handler_set_option_template.cpp \ + options_get_option_template.cpp \ options_holder_template.h \ + options_set_option_template.cpp \ options_template.cpp -%_tags.h: %_tags mktagheaders - $(AM_V_at)chmod +x @srcdir@/mktagheaders - $(AM_V_GEN)( @srcdir@/mktagheaders "$<" "$<" ) >"$@" -# 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: mktags - $(AM_V_at)chmod +x @srcdir@/mktags - $(AM_V_GEN)(@srcdir@/mktags \ - '$(@:_tags.tmp=)' \ - "$$(find @srcdir@/../ -name '*.cpp' -o -name '*.h' -o -name '*.cc' -o -name '*.g')") >"$@" - -MOSTLYCLEANFILES = \ - Debug_tags \ - Trace_tags \ - Debug_tags.tmp \ - Trace_tags.tmp \ - Debug_tags.h \ - Trace_tags.h + # Make sure the implicit rules never mistake a _template.cpp or _template.h file for source file. -options_holder_template.h options_template.cpp options_handler_get_option_template.cpp options_handler_set_option_template.cpp base_options_template.h base_options_template.cpp :; +options_holder_template.h options_template.cpp options_get_option_template.cpp options_set_option_template.cpp base_options_template.h base_options_template.cpp :; # Make sure the implicit rules never mistake X_options for the -o file for a # CPP file. @@ -418,19 +385,19 @@ options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.se # mkoptions apply-sed-to-template sed-file template-file -options_handler_get_option.cpp : options_handler_get_option_template.cpp options_handler_get_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) +options_get_option.cpp : options_get_option_template.cpp options_get_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ - @srcdir@/options_handler_get_option_template.cpp \ - @builddir@/options_handler_get_option_template.cpp.sed \ + @srcdir@/options_get_option_template.cpp \ + @builddir@/options_get_option_template.cpp.sed \ summary.sed \ ) > "$@" -options_handler_set_option.cpp : options_handler_set_option_template.cpp options_handler_set_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) +options_set_option.cpp : options_set_option_template.cpp options_set_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ - @srcdir@/options_handler_set_option_template.cpp \ - @builddir@/options_handler_set_option_template.cpp.sed \ + @srcdir@/options_set_option_template.cpp \ + @builddir@/options_set_option_template.cpp.sed \ summary.sed \ ) > "$@" diff --git a/src/options/argument_extender.cpp b/src/options/argument_extender.cpp new file mode 100644 index 000000000..d55610590 --- /dev/null +++ b/src/options/argument_extender.cpp @@ -0,0 +1,74 @@ +/********************* */ +/*! \file preempt_get_option.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Utility function for parsing commandline options. + ** + ** Utility function for parsing commandline options. + **/ + +#include "options/argument_extender.h" + +#include <cstdlib> +#include <cstring> +#include <vector> + +#include "base/cvc4_assert.h" +#include "base/output.h" + +namespace CVC4 { +namespace options { + +ArgumentExtender::ArgumentExtender(unsigned additional, size_t length) + : d_additional(additional) + , d_length(length) +{ + AlwaysAssert(d_additional >= 1); + AlwaysAssert(d_length >= 1); +} + +ArgumentExtender::~ArgumentExtender(){} + +unsigned ArgumentExtender::getIncrease() const { return d_additional; } +size_t ArgumentExtender::getLength() const { return d_length; } + +void ArgumentExtender::extend(int& argc, char**& argv, const char* opt, + std::vector<char*>& allocated) +{ + + Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl; + + AlwaysAssert(opt != NULL && *opt != '\0'); + AlwaysAssert(strlen(opt) <= getLength()); + + ++argc; + unsigned i = 1; + while(argv[i] != NULL && argv[i][0] != '\0') { + ++i; + } + + if(argv[i] == NULL) { + unsigned newSize = i + getIncrease(); + argv = (char**) realloc(argv, newSize * sizeof(char*)); + for(unsigned j = i; j < newSize-1; ++j) { + char* newString = (char*) malloc(sizeof(char) * getLength()); + newString[0] = '\0'; + argv[j] = newString; + allocated.push_back(newString); + } + argv[newSize - 1] = NULL; + } + + strncpy(argv[i], opt, getLength() - 1); + argv[i][getLength() - 1] = '\0'; // ensure NULL-termination even on overflow +} + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ diff --git a/src/options/argument_extender.h b/src/options/argument_extender.h new file mode 100644 index 000000000..1f7e3c1dd --- /dev/null +++ b/src/options/argument_extender.h @@ -0,0 +1,79 @@ +/********************* */ +/*! \file preempt_get_option.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Utility function for extending commandline options. + ** + ** Utility function for extending commandline options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__OPTIONS__PREMPT_GET_OPTION_H +#define __CVC4__OPTIONS__PREMPT_GET_OPTION_H + +#include <cstddef> +#include <vector> + +namespace CVC4 { +namespace options { + + +class ArgumentExtender { + public: + /** + * Preconditions: + * additional >= 1 + * length >= 1 + */ + ArgumentExtender(unsigned additional, size_t length); + ~ArgumentExtender(); + + /** + * This purpose of this function is to massage argc and argv upon the event + * of parsing during Options::parseOptions of an option with the :link or + * :link-alternative attributes. The purpose of the function is to extend argv + * with another commandline argument. + * + * Preconditions: + * opt is '\0' terminated, non-null and non-empty c-string. + * strlen(opt) <= getLength() + * + * Let P be the first position in argv that is >= 1 and is either NULL or + * empty: + * argv[P] == NULL || argv[P] == '\0' + * + * This has a very specific set of side effects: + * - argc is incremented by one. + * - If argv[P] == NULL, this reallocates argv to have (P+additional) + * elements. + * - The 0 through P-1 elements of argv are the same. + * - The P element of argv is a copy of the first len-1 characters of opt. + * This is a newly allocated '\0' terminated c string of length len. + * - The P+1 through (P+additional-2) elements of argv are newly allocated + * empty '\0' terminated c strings of size len. + * - The last element at (P+additional-1) of argv is NULL. + * - All allocations are pushed back onto allocated. + */ + void extend(int& argc, char**& argv, const char* opt, + std::vector<char*>& allocated); + + unsigned getIncrease() const; + size_t getLength() const; + + private: + unsigned d_additional; + size_t d_length; +}; + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__OPTIONS__PREMPT_GET_OPTION_H */ diff --git a/src/options/arith_options b/src/options/arith_options index 9737d5382..9f4003004 100644 --- a/src/options/arith_options +++ b/src/options/arith_options @@ -5,10 +5,10 @@ module ARITH "options/arith_options.h" Arithmetic theory -option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::options::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "options/options_handler_interface.h" :include "options/arith_unate_lemma_mode.h" +option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :include "options/arith_unate_lemma_mode.h" determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help) -option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler CVC4::options::stringToArithPropagationMode :default BOTH_PROP :handler-include "options/options_handler_interface.h" :include "options/arith_propagation_mode.h" +option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler stringToArithPropagationMode :default BOTH_PROP :include "options/arith_propagation_mode.h" turns on arithmetic propagation (default is 'old', see --arith-prop=help) # The maximum number of difference pivots to do per invocation of simplex. @@ -25,7 +25,7 @@ option arithHeuristicPivots --heuristic-pivots=N int16_t :default 0 :read-write expert-option arithStandardCheckVarOrderPivots --standard-effort-variable-order-pivots=N int16_t :default -1 :read-write limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule -option arithErrorSelectionRule --error-selection-rule=RULE ErrorSelectionRule :handler CVC4::options::stringToErrorSelectionRule :default MINIMUM_AMOUNT :handler-include "options/options_handler_interface.h" :include "options/arith_heuristic_pivot_rule.h" +option arithErrorSelectionRule --error-selection-rule=RULE ErrorSelectionRule :handler stringToErrorSelectionRule :default MINIMUM_AMOUNT :include "options/arith_heuristic_pivot_rule.h" change the pivot rule for the basic variable (default is 'min', see --pivot-rule help) # The number of pivots before simplex rechecks every basic variable for a conflict @@ -42,8 +42,9 @@ option arithPivotThreshold --pivot-threshold=N uint16_t :default 2 :read-write option arithPropagateMaxLength --prop-row-length=N uint16_t :default 16 sets the maximum row length to be used in propagation -option arithDioSolver /--disable-dio-solver bool :default true - turns off Linear Diophantine Equation solver (Griggio, JSAT 2012) +option arithDioSolver --enable-dio-solver/--disable-dio-solver bool :default true + turns on Linear Diophantine Equation solver (Griggio, JSAT 2012) +/turns off Linear Diophantine Equation solver (Griggio, JSAT 2012) # Whether to split (= x y) into (and (<= x y) (>= x y)) in # arithmetic preprocessing. diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h index b37dde5c6..d4137255e 100644 --- a/src/options/base_handlers.h +++ b/src/options/base_handlers.h @@ -24,6 +24,8 @@ #include <string> #include <sstream> +#include "options/option_exception.h" + namespace CVC4 { namespace options { @@ -39,7 +41,7 @@ public: comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {} template <class T> - void operator()(std::string option, const T& value, OptionsHandler* handler) { + void operator()(std::string option, const T& value) { if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) || (!d_hasLbound && !(Cmp<T>()(value, T(d_dbound))))) { std::stringstream ss; diff --git a/src/options/base_options b/src/options/base_options index edbef801d..7346641c7 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -3,31 +3,34 @@ # # 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. +# 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. +# 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). +# 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: # @@ -36,9 +39,13 @@ # | :default C++-expression # | :handler custom-option-handlers.. # | :handler-include include-files.. +# | :predicate custom-option-handlers.. +# | :predicate-include include-files.. +# | :notify custom-option-notifications.. # | :read-only # | :read-write # | :link linked-options.. +# | :link-smt linked-option [value] # # common-alias ALIAS_SPECIFICATION # alias ALIAS_SPECIFICATION @@ -74,7 +81,76 @@ # # endmodule # -# This file should end with the "endmodule" command, and nothing should follow it. +# This file should end with the "endmodule" command, and nothing should +# follow it. +# +# +# The options/ package supports a wide range of operations for responding to +# an option being set. Roughly the three major concepts are: +# - :handler is to parse an option before setting its value. +# - :predicate is to reject bad values for the option. +# - :notify is used for dynamic dispatch after an option is assigned. +# +# More details on each class of custom handlers. +# :handler custom-option-handler +# Handlers provide support for parsing custom types and parsing for options. +# The signature for a handler call is: +# T custom-option-handler(std::string option, std::string optarg, +# OptionsHandler* handler); +# where T is the type of the option. The suggested implementation is to +# implement custom-handler as a dispatch into a function on handler with the +# signature: +# T OptionsHandler::custom-option-handler(std::string option, +# std::string optarg); +# The handlers are run before predicates and notifications. +# Having multiple handlers is considered bad practice and is unsupported. +# Handlers may have arbitrary side effects, but should call no code +# inaccessible to liboptions. For side effects that are not required in order +# to parse the option, using :predicate is recommended. Use :notify to +# achieve dynamic dispatch outside of base/, lib/, and options/. Memory +# management done by a handler needs to either be encapsulated by the type +# and the destructor for the type or should *always* be owned by handler. More +# elaborate memory management schemes are not currently supported. +# +# :predicate custom-predicate +# Predicates provide support for checking whether or not the value of an +# is acceptable. Predicates are run after handlers and before notifications. +# The signature for a predicate call is: +# void custom-predicate(std::string option, T value, +# OptionsHandler* handler); +# where T is the type of the option. The suggested implementation is to +# implement custom-predicate as a dispatch into a function on handler with the +# signature: +# void OptionsHandler::custom-predicate(std::string option, T value); +# The predicates are run after handlers and before notifications. Multiple +# predicates may be defined for the same option, but the order they are run +# is not guaranteed. Predicates may have arbitrary side effects, but should +# call no code inaccessible to liboptions. Use :notify to +# achieve dynamic dispatch outside of base/, lib/, and options/. +# Predicates are expected to reject bad value for the option by throwing an +# OptionsException. +# +# :notify custom-notification +# This allows for the installation of custom post-processing callbacks using +# the Listener infrastructure. custom-option-notification is a C++ function +# that is called after the assignment of the option is updated. +# The normal usage of an notify is to call a Listener that is registered for +# this specific option. This is how dynamic dispatch outside of the +# liboptions package should always be done. +# The signature of custom-option-notification should take an option name as +# well as an OptionsHandler*. +# void custom-notification( +# const std::string& option, CVC4::options::OptionsHandler* handler); +# The name is provided so multiple options can use the same notification +# implementation. +# This is called after all handlers and predicates have been run. +# Formally, this is always placed at the end of either the generated +# Options::assign or Options::assignBool function for the option. +# Because of this :notify cannot be used with void type options. +# Users of this feature should *always* check the code generated in +# builds/src/options/options.cpp for the correctness of the placement of the +# generated code. The Listener notify() function is allowed to throw +# an arbitrary std::exception. # module BASE "options/base_options.h" Base @@ -85,9 +161,9 @@ option in std::istream* :default &std::cin :include <iosfwd> option out std::ostream* :default &std::cout :include <iosfwd> option err std::ostream* :default &std::cerr :include <iosfwd> -common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "options/language.h" :default language::input::LANG_AUTO :read-write +common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler stringToInputLanguage :include "options/language.h" :default language::input::LANG_AUTO :read-write force input language (default is "auto"; see --lang help) -common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "options/language.h" :default language::output::LANG_AUTO :read-write +common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler stringToOutputLanguage :include "options/language.h" :default language::output::LANG_AUTO :read-write force output language (default is "auto"; see --output-lang help) option languageHelp bool @@ -96,18 +172,18 @@ option languageHelp bool undocumented-alias --language=L = --lang=L undocumented-alias --output-language=L = --output-lang=L -option verbosity verbosity int :read-write :default 0 :predicate CVC4::options::setVerbosity :predicate-include "options/base_handlers.h" +option verbosity verbosity int :read-write :default 0 :predicate setVerbosity the verbosity level of CVC4 -common-option - -v --verbose void :handler CVC4::options::increaseVerbosity +common-option - -v --verbose void :handler increaseVerbosity increase verbosity (may be repeated) -common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity +common-option - -q --quiet void :handler decreaseVerbosity decrease verbosity (may be repeated) -common-option statistics statistics --stats bool :predicate CVC4::options::statsEnabledBuild :predicate-include "options/options_handler_interface.h" +common-option statistics statistics --stats bool :predicate statsEnabledBuild give statistics on exit undocumented-alias --statistics = --stats undocumented-alias --no-statistics = --no-stats -option statsEveryQuery --stats-every-query bool :default false :link --stats +option statsEveryQuery --stats-every-query bool :default false :link --stats :link-smt statistics in incremental mode, print stats after every satisfiability or validity query undocumented-alias --statistics-every-query = --stats-every-query undocumented-alias --no-statistics-every-query = --no-stats-every-query @@ -123,12 +199,12 @@ option parseOnly parse-only --parse-only bool :read-write option preprocessOnly preprocess-only --preprocess-only bool exit after preprocessing input -option - trace -t --trace=TAG argument :handler CVC4::options::addTraceTag +option - trace -t --trace=TAG argument :handler addTraceTag trace something (e.g. -t pushpop), can repeat -option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag +option - debug -d --debug=TAG argument :handler addDebugTag debug something (e.g. -d arith), can repeat -option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/options_handler_interface.h" +option printSuccess print-success --print-success bool :notify notifyPrintSuccess print the "success" output required of SMT-LIBv2 alias --smtlib-strict = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values diff --git a/src/options/booleans_options b/src/options/booleans_options index 2e2cbee1f..a150c1d83 100644 --- a/src/options/booleans_options +++ b/src/options/booleans_options @@ -5,7 +5,7 @@ module BOOLEANS "options/booleans_options.h" Boolean theory -option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "options/boolean_term_conversion_mode.h" :handler CVC4::options::stringToBooleanTermConversionMode :handler-include "options/options_handler_interface.h" +option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "options/boolean_term_conversion_mode.h" :handler stringToBooleanTermConversionMode policy for converting Boolean terms endmodule diff --git a/src/options/bv_options b/src/options/bv_options index 245c56b51..c1180dba3 100644 --- a/src/options/bv_options +++ b/src/options/bv_options @@ -7,34 +7,34 @@ module BV "options/bv_options.h" Bitvector theory # Option to set the bit-blasting mode (lazy, eager) -option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler CVC4::options::stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "options/bv_bitblast_mode.h" :handler-include "options/options_handler_interface.h" +option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "options/bv_bitblast_mode.h" choose bitblasting mode, see --bitblast=help # Options for eager bit-blasting -option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::options::abcEnabledBuild CVC4::options::setBitblastAig :predicate-include "options/options_handler_interface.h" :read-write +option bitvectorAig --bitblast-aig bool :default false :predicate abcEnabledBuild setBitblastAig :read-write bitblast by first converting to AIG (implies --bitblast=eager) -expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate CVC4::options::abcEnabledBuild :read-write :link --bitblast-aig :link-smt bitblast-aig +expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate abcEnabledBuild :read-write :link --bitblast-aig :link-smt bitblast-aig abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") # Options for lazy bit-blasting - option bitvectorPropagate --bv-propagate bool :default true :read-write use bit-vector propagation in the bit-blaster -option bitvectorEqualitySolver --bv-eq-solver bool :default true :read-write +option bitvectorEqualitySolver --bv-eq-solver bool :default true :read-write use the equality engine for the bit-vector theory (only if --bitblast=lazy) -option bitvectorEqualitySlicer --bv-eq-slicer=MODE CVC4::theory::bv::BvSlicerMode :handler CVC4::options::stringToBvSlicerMode :default CVC4::theory::bv::BITVECTOR_SLICER_OFF :read-write :include "options/bv_bitblast_mode.h" :handler-include "options/options_handler_interface.h" :read-write :link --bv-eq-solver +option bitvectorEqualitySlicer --bv-eq-slicer=MODE CVC4::theory::bv::BvSlicerMode :handler stringToBvSlicerMode :default CVC4::theory::bv::BITVECTOR_SLICER_OFF :read-write :include "options/bv_bitblast_mode.h" :read-write :link --bv-eq-solver :link-smt bv-eq-solver turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy) + option bitvectorInequalitySolver --bv-inequality-solver bool :default true :read-write turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy) -option bitvectorAlgebraicSolver --bv-algebraic-solver bool :default true :read-write +option bitvectorAlgebraicSolver --bv-algebraic-solver bool :default true :read-write turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy) -expert-option bitvectorAlgebraicBudget --bv-algebraic-budget unsigned :default 1500 :read-write :link --bv-algebraic-solver +expert-option bitvectorAlgebraicBudget --bv-algebraic-budget unsigned :default 1500 :read-write :link --bv-algebraic-solver :link-smt bv-algebraic-solver the budget allowed for the algebraic solver in number of SAT conflicts # General options diff --git a/src/options/decision_options b/src/options/decision_options index 35a1de1e9..2490d2808 100644 --- a/src/options/decision_options +++ b/src/options/decision_options @@ -6,7 +6,7 @@ module DECISION "options/decision_options.h" Decision heuristics # When/whether to use any decision strategies -option decisionMode decision-mode --decision=MODE decision::DecisionMode :handler CVC4::options::stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "options/decision_mode.h" :handler-include "options/options_handler_interface.h" +option decisionMode decision-mode --decision=MODE decision::DecisionMode :handler stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "options/decision_mode.h" choose decision mode, see --decision=help # only use DE to determine when to stop, not to make decisions @@ -21,7 +21,7 @@ expert-option decisionUseWeight --decision-use-weight bool :default false expert-option decisionRandomWeight --decision-random-weight=N int :default 0 assign random weights to nodes between 0 and N-1 (0: disable) -expert-option decisionWeightInternal --decision-weight-internal=HOW decision::DecisionWeightInternal :handler CVC4::options::stringToDecisionWeightInternal :default decision::DECISION_WEIGHT_INTERNAL_OFF :handler-include "options/options_handler_interface.h" +expert-option decisionWeightInternal --decision-weight-internal=HOW decision::DecisionWeightInternal :handler stringToDecisionWeightInternal :default decision::DECISION_WEIGHT_INTERNAL_OFF computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) endmodule diff --git a/src/options/expr_options b/src/options/expr_options index fc92c75a6..75354a010 100644 --- a/src/options/expr_options +++ b/src/options/expr_options @@ -5,16 +5,16 @@ module EXPR "options/expr_options.h" Expression package -option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::options::setDefaultExprDepth :predicate-include "options/options_handler_interface.h" +option defaultExprDepth --default-expr-depth=N int :default 0 :predicate setDefaultExprDepthPredicate :notify notifySetDefaultExprDepth print exprs to depth N (0 == default, -1 == no limit) undocumented-alias --expr-depth=N = --default-expr-depth=N -option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::options::setDefaultDagThresh :predicate-include "options/options_handler_interface.h" +option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate setDefaultDagThreshPredicate :notify notifySetDefaultDagThresh dagify common subexprs appearing > N times (1 == default, 0 == don't dagify) undocumented-alias --dag-thresh=N = --default-dag-thresh=N undocumented-alias --dag-threshold=N = --default-dag-thresh=N -option - --print-expr-types void :handler CVC4::options::setPrintExprTypes :handler-include "options/options_handler_interface.h" +option printExprTypes --print-expr-types bool :default false :notify notifySetPrintExprTypes print types with variables when printing exprs option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :default USE_EARLY_TYPE_CHECKING_BY_DEFAULT @@ -23,7 +23,7 @@ option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :defaul # --no-type-checking will override any --early-type-checking or --lazy-type-checking option # --lazy-type-checking is linked because earlyTypeChecking should be set false too -option typeChecking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking +option typeChecking type-checking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking never type check expressions option biasedITERemoval --biased-ites bool :default false diff --git a/src/options/logic_info_forward.h b/src/options/logic_info_forward.h deleted file mode 100644 index b60e56034..000000000 --- a/src/options/logic_info_forward.h +++ /dev/null @@ -1,26 +0,0 @@ -/*! \file logic_info_forward.h - ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief A temporary forward delcaration file for LogicInfo. - ** - ** A temporary forward delcaration file for LogicInfo. - **/ - - -#include "cvc4_public.h" - -#ifndef __CVC4__OPTIONS_LOGIC_INFO_FORWARD_H -#define __CVC4__OPTIONS_LOGIC_INFO_FORWARD_H - -namespace CVC4 { -class LogicInfo; -}/* CVC4 namespace */ - -#endif /* __CVC4__OPTIONS_LOGIC_INFO_FORWARD_H */ diff --git a/src/options/main_options b/src/options/main_options index 8b161e5df..7ec4fedb3 100644 --- a/src/options/main_options +++ b/src/options/main_options @@ -12,21 +12,21 @@ undocumented-alias --license = --version common-option help -h --help/ bool full command line reference -common-option - --show-config void :handler CVC4::options::showConfiguration :handler-include "options/options_handler_interface.h" +common-option - --show-config void :handler showConfiguration show CVC4 static configuration -option - --show-debug-tags void :handler CVC4::options::showDebugTags :handler-include "options/options_handler_interface.h" +option - --show-debug-tags void :handler showDebugTags show all available tags for debugging -option - --show-trace-tags void :handler CVC4::options::showTraceTags :handler-include "options/options_handler_interface.h" +option - --show-trace-tags void :handler showTraceTags show all available tags for tracing expert-option earlyExit --early-exit bool :default true do not run destructors at exit; default on except in debug builds # portfolio options -option threads --threads=N unsigned :default 2 :predicate options::greater(0) +option threads --threads=N unsigned :default 2 :predicate unsignedGreater0 Total number of threads for portfolio -option - --threadN=string void :handler CVC4::options::threadN :handler-include "options/options_handler_interface.h" +option - --threadN=string void :handler threadN configures portfolio thread N (0..#threads-1) option threadStackSize --thread-stack=N unsigned :default 0 stack size for worker threads in MB (0 means use Boost/thread lib default) @@ -38,16 +38,16 @@ option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write don't share (among portfolio threads) lemmas strictly longer than N option fallbackSequential --fallback-sequential bool :default false Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode -option incrementalParallel --incremental-parallel bool :default false :link --incremental +option incrementalParallel --incremental-parallel bool :default false :link --incremental :link-smt incremental Use parallel solver even in incremental mode (may print 'unknown's at times) option interactive : --interactive bool :read-write force interactive/non-interactive mode -undocumented-option interactivePrompt /--no-interactive-prompt bool :default true - turn off interactive prompting while in interactive mode +undocumented-option interactivePrompt --interactive-prompt bool :default true + interactive prompting while in interactive mode # error behaviors (--immediate-exit is default in cases we support, thus no options) -option continuedExecution --continued-execution/ bool :default false :link "--interactive --no-interactive-prompt"/ +option continuedExecution --continued-execution/ bool :default false :link "--interactive --no-interactive-prompt"/ :link-smt interactive :link-smt interactivePrompt \"false\" continue executing commands, even on error option segvSpin --segv-spin bool :default false diff --git a/src/options/mkoptions b/src/options/mkoptions index 05280baa8..ad8d7033f 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -115,6 +115,7 @@ long_option_alternate= long_option_alternate_set= type= predicates= +notifications= # just for duplicates-checking all_declared_internal_options= @@ -247,6 +248,7 @@ function handle_option { default_value= handlers= predicates= + notifications= links= links_alternate= smt_links= @@ -425,6 +427,12 @@ function handle_option { predicates="${predicates} ${args[$i]}" done ;; + :notify) + while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do + let ++i + notifications="${notifications} ${args[$i]}" + done + ;; :link) while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do let ++i @@ -535,11 +543,11 @@ 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, options::OptionsHandler* handler);" +template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value);" elif [ "$internal" != - ]; then module_specializations="${module_specializations} #line $lineno \"$kf\" -template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, options::OptionsHandler* handler);" +template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value);" fi module_accessors="${module_accessors} @@ -585,6 +593,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r run_links= run_links_alternate= run_smt_links= + run_notifications= if [ -n "$links" -a -z "$smt_links" -a -n "$smtname" ]; then WARN "$smtname has no :link-smt, but equivalent command-line has :link" elif [ -n "$smt_links" -a -z "$links" ] && [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o "$long_option_alternate" ]; then @@ -595,7 +604,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r for link in $links; do run_links="$run_links #line $lineno \"$kf\" - preemptGetopt(extra_argc, extra_argv, \"$link\");" + argumentExtender.extend(extra_argc, extra_argv, \"$link\", allocated);" done fi if [ -n "$smt_links" ]; then @@ -605,7 +614,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r while [ $i -lt ${#smt_links[@]} ]; do run_smt_links="$run_smt_links #line $lineno \"$kf\" - handler->setOption(std::string(\"${smt_links[$i]}\"), (${smt_links[$(($i+1))]}));" + setOption(std::string(\"${smt_links[$i]}\"), (${smt_links[$(($i+1))]}));" i=$((i+2)) done fi @@ -614,7 +623,14 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r for link in $links_alternate; do run_links_alternate="$run_links_alternate #line $lineno \"$kf\" - preemptGetopt(extra_argc, extra_argv, \"$link\");" + argumentExtender.extend(extra_argc, extra_argv, \"$link\", allocated);" + done + fi + if [ -n "$notifications" ]; then + for notification in $notifications; do + run_notifications="$run_notifications +#line $lineno \"$kf\" + d_handler->$notification(option);" done fi if [ "$type" = bool ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then @@ -626,7 +642,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r for predicate in $predicates; do run_handlers="$run_handlers #line $lineno \"$kf\" - $predicate(option, b, handler);" + handler->$predicate(option, b);" done fi if [ -n "$run_handlers" ]; then @@ -641,7 +657,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o if [ "$type" = bool ]; then all_modules_option_handlers="${all_modules_option_handlers}${cases} #line $lineno \"$kf\" - assignBool(options::$internal, option, true, handler);$run_links + assignBool(options::$internal, option, true);$run_links break; " elif [ -n "$expect_arg" -a "$internal" != - ]; then @@ -650,7 +666,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(option, optionarg, handler);" + handler->$handler(option, optionarg);" done else run_handlers=" @@ -661,7 +677,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o for predicate in $predicates; do run_handlers="$run_handlers #line $lineno \"$kf\" - $predicate(option, retval, handler);" + handler->$predicate(option, retval);" done fi all_custom_handlers="${all_custom_handlers} @@ -674,7 +690,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options }" all_modules_option_handlers="${all_modules_option_handlers}${cases} #line $lineno \"$kf\" - assign(options::$internal, option, optionarg, handler);$run_links + assign(options::$internal, option, optionarg);$run_links break; " elif [ -n "$expect_arg" ]; then @@ -686,7 +702,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(option, optionarg, handler);" + handler->$handler(option, optionarg);" done fi all_modules_option_handlers="${all_modules_option_handlers}${cases} @@ -703,7 +719,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(option, handler);" + handler->$handler(option);" done fi all_modules_option_handlers="${all_modules_option_handlers}${cases} @@ -712,12 +728,12 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options break; " fi - fi + fi # ends if [ -n "$cases" ]; 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, option, false, handler);$run_links_alternate + assignBool(options::$internal, option, false);$run_links_alternate break; " else @@ -770,7 +786,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - Options::current()->assignBool(options::$internal, \"$smtname\", optionarg == \"true\", handler);$run_smt_links + Options::current()->assignBool(options::$internal, \"$smtname\", optionarg == \"true\");$run_smt_links return; }" elif [ -n "$expect_arg" -a "$internal" != - ]; then @@ -779,7 +795,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(\"$smtname\", optionarg, handler); + handler->$handler(\"$smtname\", optionarg); " done fi @@ -787,7 +803,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - Options::current()->assign(options::$internal, \"$smtname\", optionarg, handler);$run_smt_links + Options::current()->assign(options::$internal, \"$smtname\", optionarg);$run_smt_links return; }" elif [ -n "$expect_arg" ]; then @@ -795,7 +811,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(\"$smtname\", optionarg, handler); + handler->$handler(\"$smtname\", optionarg); " done smt_setoption_handlers="${smt_setoption_handlers} @@ -810,7 +826,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(\"$smtname\", handler); + handler->$handler(\"$smtname\"); " done smt_setoption_handlers="${smt_setoption_handlers} @@ -849,26 +865,26 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options # 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, options::OptionsHandler* handler) { +template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value) { #line $lineno \"$kf\" - runBoolPredicates(options::$internal, option, value, handler); + runBoolPredicates(options::$internal, option, value, d_handler); #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; + Trace(\"options\") << \"user assigned option $internal\" << std::endl;$run_notifications }" elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$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, options::OptionsHandler* handler) { +template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value) { #line $lineno \"$kf\" - d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, handler); + d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, d_handler); #line $lineno \"$kf\" d_holder->${internal}__setByUser__ = true; #line $lineno \"$kf\" - Trace(\"options\") << \"user assigned option $internal\" << std::endl; + Trace(\"options\") << \"user assigned option $internal\" << std::endl;$run_notifications }" fi } @@ -912,8 +928,6 @@ function handle_alias { readOnly=true required_argument=false default_value= - handlers= - predicates= links= links_alternate= @@ -999,12 +1013,12 @@ function handle_alias { fi links="$links #line $lineno \"$kf\" - preemptGetopt(extra_argc, extra_argv, \"$linkopt\");" + argumentExtender.extend(extra_argc, extra_argv, \"$linkopt\", allocated);" if [ "$linkarg" ]; then # include also the arg links="$links #line $lineno \"$kf\" - preemptGetopt(extra_argc, extra_argv, optionarg.c_str());" + argumentExtender.extend(extra_argc, extra_argv, optionarg.c_str(), allocated);" fi shift done diff --git a/src/options/mktagheaders b/src/options/mktagheaders deleted file mode 100755 index af44cee8d..000000000 --- a/src/options/mktagheaders +++ /dev/null @@ -1,24 +0,0 @@ -#!/bin/bash -# -# mktagheaders -# -# The purpose of this script is to generate the *_tag.h header file from the -# *_tags file. -# -# Invocation: -# -# mktagheaders <tag-name> <tag-file> -# -# <tag-name> will be the name of the generated array. -# <tag-file> each line of this file is turned into a string in the generated -# array. - -TAG_NAME=$1 -TAG_FILE=$2 - -echo 'static char const* const '$TAG_NAME'[] = {'; -for tag in `cat $TAG_FILE`; do - echo "\"$tag\","; -done; -echo 'NULL'; -echo '};' diff --git a/src/options/mktags b/src/options/mktags deleted file mode 100755 index 090e57014..000000000 --- a/src/options/mktags +++ /dev/null @@ -1,35 +0,0 @@ -#!/bin/bash -# -# mktags -# -# The purpose of this script is to create Debug_tags and Trace_tags files. -# Note that in the Makefile workflow these are first stored in a *_tags.tmp -# file. This file contains a list of all of the strings that occur in things -# like Debug("foo") or Debug.isOn("bar") in a given directory. The list is -# seperated by newlines. The expected Debug_tags file for the previous two -# tags would be: -# bar -# foo -# -# Invocation: -# -# mktags {Debug,Trace} <input-files> -# -# <input-files> is expected to be passed a single space separated list of files. -# One can use quotes to achieve this. This is one reason to use "$(...)" -# instead of back ticks `...`. - -DebugOrTrace=$1 -InputFiles=$2 - -grep -h '\<'$DebugOrTrace'\(\.isOn\)* *( *\".*\" *)' \ - $InputFiles | \ - sed 's/\/\/.*//;s/^'$DebugOrTrace'\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]'$DebugOrTrace'\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | \ - LC_ALL=C sort | \ - uniq - - -# Reference copy of what this is replacing. -# grep -h '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \ -# `find @srcdir@/../ -name "*.cpp" -o -name "*.h" -o -name "*.cc" -o -name "*.g"` | \ -# sed 's/\/\/.*//;s/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp new file mode 100644 index 000000000..4c92d056b --- /dev/null +++ b/src/options/open_ostream.cpp @@ -0,0 +1,102 @@ +/********************* */ +/*! \file open_ostream.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** 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 + **/ + +#include "options/open_ostream.h" + + +#include <cerrno> +#include <iostream> +#include <ostream> +#include <sstream> +#include <string> +#include <utility> + +#include "lib/strtok_r.h" +#include "options/parser_options.h" + +namespace CVC4 { + +OstreamOpener::OstreamOpener(const char* channelName) + : d_channelName(channelName) + , d_specialCases() +{} + +void OstreamOpener::addSpecialCase(const std::string& name, std::ostream* out){ + d_specialCases[name] = out; +} + + + +std::pair< bool, std::ostream* > OstreamOpener::open(const std::string& optarg) const + throw(OptionException) +{ + if(optarg == "") { + std::stringstream ss; + ss << "Bad file name setting for " << d_channelName; + throw OptionException(ss.str()); + } + if(d_specialCases.find(optarg) != d_specialCases.end()){ + return std::make_pair(false, (*d_specialCases.find(optarg)).second); + } else if(!options::filesystemAccess()) { + throw OptionException(std::string("Filesystem access not permitted")); + } else { + errno = 0; + std::ostream* outStream; + outStream = new std::ofstream(optarg.c_str(), + std::ofstream::out | std::ofstream::trunc); + if(outStream == NULL || !*outStream) { + std::stringstream ss; + ss << "Cannot open " << d_channelName << " file: `" + << optarg << "': " << cvc4_errno_failreason(); + throw OptionException(ss.str()); + } + return make_pair(true, outStream); + } +} + +std::string cvc4_errno_failreason() { +#if HAVE_STRERROR_R +#if STRERROR_R_CHAR_P + if(errno != 0) { + // GNU version of strerror_r: *might* use the given buffer, + // or might not. It returns a pointer to buf, or not. + char buf[80]; + return std::string(strerror_r(errno, buf, sizeof buf)); + } else { + return "unknown reason"; + } +#else /* STRERROR_R_CHAR_P */ + if(errno != 0) { + // XSI version of strerror_r: always uses the given buffer. + // Returns an error code. + char buf[80]; + if(strerror_r(errno, buf, sizeof buf) == 0) { + return std::string(buf); + } else { + // some error occurred while getting the error string + return "unknown reason"; + } + } else { + return "unknown reason"; + } +#endif /* STRERROR_R_CHAR_P */ +#else /* HAVE_STRERROR_R */ + return "unknown reason"; +#endif /* HAVE_STRERROR_R */ +} + +}/* CVC4 namespace */ diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h new file mode 100644 index 000000000..ab83427a9 --- /dev/null +++ b/src/options/open_ostream.h @@ -0,0 +1,63 @@ +/********************* */ +/*! \file open_stream.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 New York University and The University of Iowa + ** 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 + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__OPEN_OSTREAM_H +#define __CVC4__OPEN_OSTREAM_H + +#include <map> +#include <ostream> +#include <string> +#include <utility> + +#include "options/option_exception.h" + +namespace CVC4 { + +class OstreamOpener { + public: + OstreamOpener(const char* channelName); + + void addSpecialCase(const std::string& name, std::ostream* out); + + /** + * If name == "", this throws OptionException with the message, messageIfEmpty. + * If name is a special case, this return <false, out> where out is the + * special case that was added. + * If name == "std::cerr", this return <false, &cerr>. + * If none of the previous conditions hold and !options::filesystemAccess(), + * this throws an OptionException. + * Otherwise, this attempts to open a ofstream using the filename, name. + * If this fails, this throws and OptionException. If this succeeds, this + * returns <true, stream> where stream is a ostream allocated by new. + * The caller is in this case the owner of the allocated memory. + */ + std::pair<bool, std::ostream*> open(const std::string& name) const + throw(OptionException); + + private: + const char* d_channelName; + std::map< std::string, std::ostream* > d_specialCases; + +}; /* class OstreamOpener */ + +std::string cvc4_errno_failreason(); + +}/* CVC4 namespace */ + +#endif /* __CVC4__OPEN_OSTREAM_H */ diff --git a/src/options/options.h b/src/options/options.h index 8e1ca2b65..8fb52146f 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -19,12 +19,16 @@ #ifndef __CVC4__OPTIONS__OPTIONS_H #define __CVC4__OPTIONS__OPTIONS_H -#include <iostream> #include <fstream> +#include <ostream> #include <string> #include <vector> +#include "base/listener.h" +#include "base/modal_exception.h" #include "base/tls.h" +#include "options/language.h" +#include "options/printer_modes.h" #include "options/option_exception.h" namespace CVC4 { @@ -38,18 +42,90 @@ class CVC4_PUBLIC Options { /** The struct that holds all option values. */ options::OptionsHolder* d_holder; + /** The handler for the options of the theory. */ + options::OptionsHandler* d_handler; + /** The current Options in effect */ static CVC4_THREADLOCAL(Options*) s_current; + /** Listeners for options::forceLogicString being set. */ + ListenerCollection d_forceLogicListeners; + + /** Listeners for notifyBeforeSearch. */ + ListenerCollection d_beforeSearchListeners; + + /** Listeners for options::tlimit. */ + ListenerCollection d_tlimitListeners; + + /** Listeners for options::tlimit-per. */ + ListenerCollection d_tlimitPerListeners; + + /** Listeners for options::rlimit. */ + ListenerCollection d_rlimitListeners; + + /** Listeners for options::tlimit-per. */ + ListenerCollection d_rlimitPerListeners; + + /** Listeners for options::useTheoryList. */ + ListenerCollection d_useTheoryListListeners; + + /** Listeners for options::defaultExprDepth. */ + ListenerCollection d_setDefaultExprDepthListeners; + + /** Listeners for options::defaultDagThresh. */ + ListenerCollection d_setDefaultDagThreshListeners; + + /** Listeners for options::printExprTypes. */ + ListenerCollection d_setPrintExprTypesListeners; + + /** Listeners for options::dumpModeString. */ + ListenerCollection d_setDumpModeListeners; + + /** Listeners for options::printSuccess. */ + ListenerCollection d_setPrintSuccessListeners; + + /** Listeners for options::dumpToFileName. */ + ListenerCollection d_dumpToFileListeners; + + /** Listeners for options::regularChannelName. */ + ListenerCollection d_setRegularChannelListeners; + + /** Listeners for options::diagnosticChannelName. */ + ListenerCollection d_setDiagnosticChannelListeners; + + /** Listeners for options::replayFilename. */ + ListenerCollection d_setReplayFilenameListeners; + + + static ListenerCollection::Registration* registerAndNotify( + ListenerCollection& collection, Listener* listener, bool notify); + /** Low-level assignment function for options */ template <class T> - void assign(T, std::string option, std::string value, options::OptionsHandler* handler); + void assign(T, std::string option, std::string value); /** Low-level assignment function for bool-valued options */ template <class T> - void assignBool(T, std::string option, bool value, options::OptionsHandler* handler); + void assignBool(T, std::string option, bool value); friend class options::OptionsHandler; + /** + * Options cannot be copied as they are given an explicit list of + * Listeners to respond to. + */ + Options(const Options& options) CVC4_UNDEFINED; + + /** + * Options cannot be assigned as they are given an explicit list of + * Listeners to respond to. + */ + Options& operator=(const Options& options) CVC4_UNDEFINED; + + static std::string formatThreadOptionException(const std::string& option); + + static const size_t s_maxoptlen = 128; + static const unsigned s_preemptAdditional = 6; + public: class CVC4_PUBLIC OptionsScope { private: @@ -76,10 +152,14 @@ public: } Options(); - Options(const Options& options); ~Options(); - Options& operator=(const Options& options); + /** + * Copies the value of the options stored in OptionsHolder into the current + * Options object. + * This does not copy the listeners in the Options object. + */ + void copyValues(const Options& options); /** * Set the value of the given option. Use of this default @@ -93,11 +173,99 @@ public: T::you_are_trying_to_assign_to_a_read_only_option; } + /** + * Set the value of the given option by key. + */ + void setOption(const std::string& key, const std::string& optionarg) + throw(OptionException, ModalException); + + /** Get the value of the given option. Const access only. */ template <class T> const typename T::type& operator[](T) const; /** + * Gets the value of the given option by key and returns value as a string. + */ + std::string getOption(const std::string& key) const + throw(OptionException); + + // Get accessor functions. + InputLanguage getInputLanguage() const; + InstFormatMode getInstFormatMode() const; + OutputLanguage getOutputLanguage() const; + bool getCheckProofs() const; + bool getContinuedExecution() const; + bool getDumpInstantiations() const; + bool getDumpModels() const; + bool getDumpProofs() const; + bool getDumpSynth() const; + bool getDumpUnsatCores() const; + bool getEarlyExit() const; + bool getFallbackSequential() const; + bool getFilesystemAccess() const; + bool getForceNoLimitCpuWhileDump() const; + bool getHelp() const; + bool getIncrementalParallel() const; + bool getIncrementalSolving() const; + bool getInteractive() const; + bool getInteractivePrompt() const; + bool getLanguageHelp() const; + bool getMemoryMap() const; + bool getParseOnly() const; + bool getProduceModels() const; + bool getProof() const; + bool getSegvSpin() const; + bool getSemanticChecks() const; + bool getStatistics() const; + bool getStatsEveryQuery() const; + bool getStatsHideZeros() const; + bool getStrictParsing() const; + bool getTearDownIncremental() const; + bool getVersion() const; + bool getWaitToJoin() const; + const std::string& getForceLogicString() const; + const std::vector<std::string>& getThreadArgv() const; + int getSharingFilterByLength() const; + int getThreadId() const; + int getVerbosity() const; + std::istream* getIn() const; + std::ostream* getErr(); + std::ostream* getOut(); + std::ostream* getOutConst() const; // TODO: Remove this. + std::string getBinaryName() const; + std::string getReplayInputFilename() const; + unsigned getParseStep() const; + unsigned getThreadStackSize() const; + unsigned getThreads() const; + + + // TODO: Document these. + void setCeGuidedInst(bool); + void setDumpSynth(bool); + void setInputLanguage(InputLanguage); + void setInteractive(bool); + void setOut(std::ostream*); + void setOutputLanguage(OutputLanguage); + void setSharingFilterByLength(int length); + void setThreadId(int); + + bool wasSetByUserCeGuidedInst() const; + bool wasSetByUserDumpSynth() const; + bool wasSetByUserEarlyExit() const; + bool wasSetByUserForceLogicString() const; + bool wasSetByUserIncrementalSolving() const; + bool wasSetByUserInteractive() const; + bool wasSetByUserThreadStackSize() const; + bool wasSetByUserThreads() const; + + // Static accessor functions. + // TODO: Document these. + static int currentGetSharingFilterByLength(); + static int currentGetThreadId(); + static std::ostream* currentGetOut(); + + /** * 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 @@ -150,13 +318,216 @@ public: * The return value is what's left of the command line (that is, the * non-option arguments). */ - std::vector<std::string> parseOptions(int argc, char* argv[], options::OptionsHandler* handler) throw(OptionException); + std::vector<std::string> parseOptions(int argc, char* argv[]) + throw(OptionException); /** * Get the setting for all options. */ std::vector< std::vector<std::string> > getOptions() const throw(); + + /** + * Registers a listener for the notification, notifyBeforeSearch. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + * + * This has multiple usages so having a notifyIfSet flag does not add + * clarity. Users should check the relevant flags before registering this. + */ + ListenerCollection::Registration* registerBeforeSearchListener( + Listener* listener); + + + /** + * Registers a listener for options::forceLogic being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerForceLogicListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::tlimit being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerTlimitListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::tlimit-per being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerTlimitPerListener( + Listener* listener, bool notifyIfSet); + + + /** + * Registers a listener for options::rlimit being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerRlimitListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::rlimit-per being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerRlimitPerListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::useTheoryList being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerUseTheoryListListener( + Listener* listener, bool notifyIfSet); + + + /** + * Registers a listener for options::defaultExprDepth being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerSetDefaultExprDepthListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::defaultDagThresh being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerSetDefaultExprDagListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::printExprTypes being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerSetPrintExprTypesListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::dumpModeString being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerSetDumpModeListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::printSuccess being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerSetPrintSuccessListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::dumpToFileName being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerDumpToFileNameListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::regularChannelName being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerSetRegularOutputChannelListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::diagnosticChannelName being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerSetDiagnosticOutputChannelListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::replayLogFilename being set. + * + * If notifyIfSet is true, this calls notify on the listener + * if the option was set by the user. + * + * The memory for the Registration is controlled by the user and must + * be destroyed before the Options object is. + */ + ListenerCollection::Registration* registerSetReplayLogFilename( + Listener* listener, bool notifyIfSet); + + /** Sends a std::flush to getErr(). */ + void flushErr(); + + /** Sends a std::flush to getOut(). */ + void flushOut(); + };/* class Options */ }/* CVC4 namespace */ diff --git a/src/options/options_handler_get_option_template.cpp b/src/options/options_get_option_template.cpp index b5da8c68d..b7e5433ee 100644 --- a/src/options/options_handler_get_option_template.cpp +++ b/src/options/options_get_option_template.cpp @@ -26,29 +26,28 @@ #include "base/output.h" #include "base/modal_exception.h" #include "options/option_exception.h" -#include "options/options_handler_interface.h" +#include "options/options.h" +#include "options/options_handler.h" ${include_all_option_headers} ${option_handler_includes} -#line 31 "${template}" +#line 37 "${template}" using namespace std; namespace CVC4 { -namespace options { -std::string OptionsHandler::getOption(const std::string& key) const +std::string Options::getOption(const std::string& key) const throw(OptionException) { Trace("options") << "SMT getOption(" << key << ")" << endl; ${smt_getoption_handlers} -#line 57 "${template}" +#line 49 "${template}" throw UnrecognizedOptionException(key); } -}/* options namespace */ }/* CVC4 namespace */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp new file mode 100644 index 000000000..1c48f4bb1 --- /dev/null +++ b/src/options/options_handler.cpp @@ -0,0 +1,1380 @@ +/********************* */ +/*! \file options_handler.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Interface for custom handlers and predicates options. + ** + ** Interface for custom handlers and predicates options. + **/ + +#include "options/options_handler.h" + +#include <ostream> +#include <string> +#include <cerrno> + +#include "cvc4autoconfig.h" + +#include "base/configuration.h" +#include "base/cvc4_assert.h" +#include "base/exception.h" +#include "base/modal_exception.h" +#include "base/output.h" +#include "lib/strtok_r.h" +#include "options/arith_heuristic_pivot_rule.h" +#include "options/arith_propagation_mode.h" +#include "options/arith_unate_lemma_mode.h" +#include "options/base_options.h" +#include "options/boolean_term_conversion_mode.h" +#include "options/bv_bitblast_mode.h" +#include "options/bv_options.h" +#include "options/decision_mode.h" +#include "options/decision_options.h" +#include "options/didyoumean.h" +#include "options/language.h" +#include "options/option_exception.h" +#include "options/printer_modes.h" +#include "options/quantifiers_modes.h" +#include "options/simplification_mode.h" +#include "options/smt_options.h" +#include "options/theory_options.h" +#include "options/theoryof_mode.h" +#include "options/ufss_mode.h" + +namespace CVC4 { +namespace options { + +OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } + +void OptionsHandler::notifyForceLogic(const std::string& option){ + d_options->d_forceLogicListeners.notify(); +} + +void OptionsHandler::notifyBeforeSearch(const std::string& option) + throw(ModalException) +{ + try{ + d_options->d_beforeSearchListeners.notify(); + } catch (ModalException&){ + std::stringstream ss; + ss << "cannot change option `" << option + << "' after final initialization (i.e., after logic has been set)"; + throw ModalException(ss.str()); + } +} + + +void OptionsHandler::notifyTlimit(const std::string& option) { + d_options->d_tlimitListeners.notify(); +} + +void OptionsHandler::notifyTlimitPer(const std::string& option) { + d_options->d_tlimitPerListeners.notify(); +} + +void OptionsHandler::notifyRlimit(const std::string& option) { + d_options->d_rlimitListeners.notify(); +} + +void OptionsHandler::notifyRlimitPer(const std::string& option) { + d_options->d_rlimitPerListeners.notify(); +} + + +unsigned long OptionsHandler::tlimitHandler(std::string option, std::string optarg) throw(OptionException) { + unsigned long ms; + std::istringstream convert(optarg); + if (!(convert >> ms)) { + throw OptionException("option `"+option+"` requires a number as an argument"); + } + return ms; +} + +unsigned long OptionsHandler::tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) { + unsigned long ms; + + std::istringstream convert(optarg); + if (!(convert >> ms)) { + throw OptionException("option `"+option+"` requires a number as an argument"); + } + return ms; +} + +unsigned long OptionsHandler::rlimitHandler(std::string option, std::string optarg) throw(OptionException) { + unsigned long ms; + + std::istringstream convert(optarg); + if (!(convert >> ms)) { + throw OptionException("option `"+option+"` requires a number as an argument"); + } + return ms; +} + + +unsigned long OptionsHandler::rlimitPerHandler(std::string option, std::string optarg) throw(OptionException) { + unsigned long ms; + + std::istringstream convert(optarg); + if (!(convert >> ms)) { + throw OptionException("option `"+option+"` requires a number as an argument"); + } + + return ms; +} + + +/* options/base_options_handlers.h */ +void OptionsHandler::notifyPrintSuccess(std::string option) { + d_options->d_setPrintSuccessListeners.notify(); +} + +// theory/arith/options_handlers.h +const std::string OptionsHandler::s_arithUnateLemmasHelp = "\ +Unate lemmas are generated before SAT search begins using the relationship\n\ +of constant terms and polynomials.\n\ +Modes currently supported by the --unate-lemmas option:\n\ ++ none \n\ ++ ineqs \n\ + Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\ ++ eqs \n\ + Outputs lemmas of the general forms\n\ + (= p c) implies (<= p d) for c < d, or\n\ + (= p c) implies (not (= p d)) for c != d.\n\ ++ all \n\ + A combination of inequalities and equalities.\n\ +"; + +const std::string OptionsHandler::s_arithPropagationModeHelp = "\ +This decides on kind of propagation arithmetic attempts to do during the search.\n\ ++ none\n\ ++ unate\n\ + use constraints to do unate propagation\n\ ++ bi (Bounds Inference)\n\ + infers bounds on basic variables using the upper and lower bounds of the\n\ + non-basic variables in the tableau.\n\ ++both\n\ +"; + +const std::string OptionsHandler::s_errorSelectionRulesHelp = "\ +This decides on the rule used by simplex during heuristic rounds\n\ +for deciding the next basic variable to select.\n\ +Heuristic pivot rules available:\n\ ++min\n\ + The minimum abs() value of the variable's violation of its bound. (default)\n\ ++max\n\ + The maximum violation the bound\n\ ++varord\n\ + The variable order\n\ +"; + +ArithUnateLemmaMode OptionsHandler::stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "all") { + return ALL_PRESOLVE_LEMMAS; + } else if(optarg == "none") { + return NO_PRESOLVE_LEMMAS; + } else if(optarg == "ineqs") { + return INEQUALITY_PRESOLVE_LEMMAS; + } else if(optarg == "eqs") { + return EQUALITY_PRESOLVE_LEMMAS; + } else if(optarg == "help") { + puts(s_arithUnateLemmasHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --unate-lemmas: `") + + optarg + "'. Try --unate-lemmas help."); + } +} + +ArithPropagationMode OptionsHandler::stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none") { + return NO_PROP; + } else if(optarg == "unate") { + return UNATE_PROP; + } else if(optarg == "bi") { + return BOUND_INFERENCE_PROP; + } else if(optarg == "both") { + return BOTH_PROP; + } else if(optarg == "help") { + puts(s_arithPropagationModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --arith-prop: `") + + optarg + "'. Try --arith-prop help."); + } +} + +ErrorSelectionRule OptionsHandler::stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "min") { + return MINIMUM_AMOUNT; + } else if(optarg == "varord") { + return VAR_ORDER; + } else if(optarg == "max") { + return MAXIMUM_AMOUNT; + } else if(optarg == "help") { + puts(s_errorSelectionRulesHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") + + optarg + "'. Try --heuristic-pivot-rule help."); + } +} +// theory/quantifiers/options_handlers.h + +const std::string OptionsHandler::s_instWhenHelp = "\ +Modes currently supported by the --inst-when option:\n\ +\n\ +full-last-call (default)\n\ ++ Alternate running instantiation rounds at full effort and last\n\ + call. In other words, interleave instantiation and theory combination.\n\ +\n\ +full\n\ ++ Run instantiation round at full effort, before theory combination.\n\ +\n\ +full-delay \n\ ++ Run instantiation round at full effort, before theory combination, after\n\ + all other theories have finished.\n\ +\n\ +full-delay-last-call \n\ ++ Alternate running instantiation rounds at full effort after all other\n\ + theories have finished, and last call. \n\ +\n\ +last-call\n\ ++ Run instantiation at last call effort, after theory combination and\n\ + and theories report sat.\n\ +\n\ +"; + +const std::string OptionsHandler::s_literalMatchHelp = "\ +Literal match modes currently supported by the --literal-match option:\n\ +\n\ +none (default)\n\ ++ Do not use literal matching.\n\ +\n\ +predicate\n\ ++ Consider the phase requirements of predicate literals when applying heuristic\n\ + quantifier instantiation. For example, the trigger P( x ) in the quantified \n\ + formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\ + terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\ + Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\ +\n\ +"; + +const std::string OptionsHandler::s_mbqiModeHelp = "\ +Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ +\n\ +default \n\ ++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ + Modulo Theories.\n\ +\n\ +none \n\ ++ Disable model-based quantifier instantiation.\n\ +\n\ +gen-ev \n\ ++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ + model finding paper based on generalizing evaluations.\n\ +\n\ +fmc-interval \n\ ++ Same as default, but with intervals for models of integer functions.\n\ +\n\ +abs \n\ ++ Use abstract MBQI algorithm (uses disjoint sets). \n\ +\n\ +"; + +const std::string OptionsHandler::s_qcfWhenModeHelp = "\ +Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\ +\n\ +default \n\ ++ Default, apply conflict finding at full effort.\n\ +\n\ +last-call \n\ ++ Apply conflict finding at last call, after theory combination and \n\ + and all theories report sat. \n\ +\n\ +std \n\ ++ Apply conflict finding at standard effort.\n\ +\n\ +std-h \n\ ++ Apply conflict finding at standard effort when heuristic says to. \n\ +\n\ +"; + +const std::string OptionsHandler::s_qcfModeHelp = "\ +Quantifier conflict find modes currently supported by the --quant-cf option:\n\ +\n\ +prop-eq \n\ ++ Default, apply QCF algorithm to propagate equalities as well as conflicts. \n\ +\n\ +conflict \n\ ++ Apply QCF algorithm to find conflicts only.\n\ +\n\ +partial \n\ ++ Apply QCF algorithm to instantiate heuristically as well. \n\ +\n\ +mc \n\ ++ Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ +\n\ +"; + +const std::string OptionsHandler::s_userPatModeHelp = "\ +User pattern modes currently supported by the --user-pat option:\n\ +\n\ +trust \n\ ++ When provided, use only user-provided patterns for a quantified formula.\n\ +\n\ +use \n\ ++ Use both user-provided and auto-generated patterns when patterns\n\ + are provided for a quantified formula.\n\ +\n\ +resort \n\ ++ Use user-provided patterns only after auto-generated patterns saturate.\n\ +\n\ +ignore \n\ ++ Ignore user-provided patterns. \n\ +\n\ +interleave \n\ ++ Alternate between use/resort. \n\ +\n\ +"; + +const std::string OptionsHandler::s_triggerSelModeHelp = "\ +Trigger selection modes currently supported by the --trigger-sel option:\n\ +\n\ +default \n\ ++ Default, consider all subterms of quantified formulas for trigger selection.\n\ +\n\ +min \n\ ++ Consider only minimal subterms that meet criteria for triggers.\n\ +\n\ +max \n\ ++ Consider only maximal subterms that meet criteria for triggers. \n\ +\n\ +"; +const std::string OptionsHandler::s_prenexQuantModeHelp = "\ +Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ +\n\ +default \n\ ++ Default, prenex all nested quantifiers except those with user patterns.\n\ +\n\ +all \n\ ++ Prenex all nested quantifiers.\n\ +\n\ +none \n\ ++ Do no prenex nested quantifiers. \n\ +\n\ +"; + +const std::string OptionsHandler::s_cegqiFairModeHelp = "\ +Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\ +\n\ +uf-dt-size \n\ ++ Enforce fairness using an uninterpreted function for datatypes size.\n\ +\n\ +default | dt-size \n\ ++ Default, enforce fairness using size theory operator.\n\ +\n\ +dt-height-bound \n\ ++ Enforce fairness by height bound predicate.\n\ +\n\ +none \n\ ++ Do not enforce fairness. \n\ +\n\ +"; + +const std::string OptionsHandler::s_termDbModeHelp = "\ +Modes for term database, supported by --term-db-mode:\n\ +\n\ +all \n\ ++ Quantifiers module considers all ground terms.\n\ +\n\ +relevant \n\ ++ Quantifiers module considers only ground terms connected to current assertions. \n\ +\n\ +"; + +const std::string OptionsHandler::s_iteLiftQuantHelp = "\ +Modes for term database, supported by --ite-lift-quant:\n\ +\n\ +none \n\ ++ Do not lift if-then-else in quantified formulas.\n\ +\n\ +simple \n\ ++ Lift if-then-else in quantified formulas if results in smaller term size.\n\ +\n\ +all \n\ ++ Lift if-then-else in quantified formulas. \n\ +\n\ +"; + +const std::string OptionsHandler::s_sygusInvTemplHelp = "\ +Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ +\n\ +none \n\ ++ Synthesize invariant directly.\n\ +\n\ +pre \n\ ++ Synthesize invariant based on weakening of precondition .\n\ +\n\ +post \n\ ++ Synthesize invariant based on strengthening of postcondition. \n\ +\n\ +"; + +const std::string OptionsHandler::s_macrosQuantHelp = "\ +Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ +\n\ +all \n\ ++ Infer definitions for functions, including those containing quantified formulas.\n\ +\n\ +ground (default) \n\ ++ Only infer ground definitions for functions.\n\ +\n\ +ground-uf \n\ ++ Only infer ground definitions for functions that result in triggers for all free variables.\n\ +\n\ +"; + +theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "pre-full") { + return theory::quantifiers::INST_WHEN_PRE_FULL; + } else if(optarg == "full") { + return theory::quantifiers::INST_WHEN_FULL; + } else if(optarg == "full-delay") { + return theory::quantifiers::INST_WHEN_FULL_DELAY; + } else if(optarg == "full-last-call") { + return theory::quantifiers::INST_WHEN_FULL_LAST_CALL; + } else if(optarg == "full-delay-last-call") { + return theory::quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL; + } else if(optarg == "last-call") { + return theory::quantifiers::INST_WHEN_LAST_CALL; + } else if(optarg == "help") { + puts(s_instWhenHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --inst-when: `") + + optarg + "'. Try --inst-when help."); + } +} + +void OptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException) { + if(mode == theory::quantifiers::INST_WHEN_PRE_FULL) { + throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release."); + } +} + +theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none") { + return theory::quantifiers::LITERAL_MATCH_NONE; + } else if(optarg == "predicate") { + return theory::quantifiers::LITERAL_MATCH_PREDICATE; + } else if(optarg == "equality") { + return theory::quantifiers::LITERAL_MATCH_EQUALITY; + } else if(optarg == "help") { + puts(s_literalMatchHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --literal-matching: `") + + optarg + "'. Try --literal-matching help."); + } +} + +void OptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) { + if(mode == theory::quantifiers::LITERAL_MATCH_EQUALITY) { + throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release."); + } +} + +theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "gen-ev") { + return theory::quantifiers::MBQI_GEN_EVAL; + } else if(optarg == "none") { + return theory::quantifiers::MBQI_NONE; + } else if(optarg == "default" || optarg == "fmc") { + return theory::quantifiers::MBQI_FMC; + } else if(optarg == "fmc-interval") { + return theory::quantifiers::MBQI_FMC_INTERVAL; + } else if(optarg == "abs") { + return theory::quantifiers::MBQI_ABS; + } else if(optarg == "trust") { + return theory::quantifiers::MBQI_TRUST; + } else if(optarg == "help") { + puts(s_mbqiModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --mbqi: `") + + optarg + "'. Try --mbqi help."); + } +} + + +void OptionsHandler::checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException) {} + + +theory::quantifiers::QcfWhenMode OptionsHandler::stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default") { + return theory::quantifiers::QCF_WHEN_MODE_DEFAULT; + } else if(optarg == "last-call") { + return theory::quantifiers::QCF_WHEN_MODE_LAST_CALL; + } else if(optarg == "std") { + return theory::quantifiers::QCF_WHEN_MODE_STD; + } else if(optarg == "std-h") { + return theory::quantifiers::QCF_WHEN_MODE_STD_H; + } else if(optarg == "help") { + puts(s_qcfWhenModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --quant-cf-when: `") + + optarg + "'. Try --quant-cf-when help."); + } +} + +theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "conflict") { + return theory::quantifiers::QCF_CONFLICT_ONLY; + } else if(optarg == "default" || optarg == "prop-eq") { + return theory::quantifiers::QCF_PROP_EQ; + } else if(optarg == "partial") { + return theory::quantifiers::QCF_PARTIAL; + } else if(optarg == "mc" ) { + return theory::quantifiers::QCF_MC; + } else if(optarg == "help") { + puts(s_qcfModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --quant-cf-mode: `") + + optarg + "'. Try --quant-cf-mode help."); + } +} + +theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "use") { + return theory::quantifiers::USER_PAT_MODE_USE; + } else if(optarg == "default" || optarg == "trust") { + return theory::quantifiers::USER_PAT_MODE_TRUST; + } else if(optarg == "resort") { + return theory::quantifiers::USER_PAT_MODE_RESORT; + } else if(optarg == "ignore") { + return theory::quantifiers::USER_PAT_MODE_IGNORE; + } else if(optarg == "interleave") { + return theory::quantifiers::USER_PAT_MODE_INTERLEAVE; + } else if(optarg == "help") { + puts(s_userPatModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --user-pat: `") + + optarg + "'. Try --user-pat help."); + } +} + +theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default" || optarg == "all" ) { + return theory::quantifiers::TRIGGER_SEL_DEFAULT; + } else if(optarg == "min") { + return theory::quantifiers::TRIGGER_SEL_MIN; + } else if(optarg == "max") { + return theory::quantifiers::TRIGGER_SEL_MAX; + } else if(optarg == "help") { + puts(s_triggerSelModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --trigger-sel: `") + + optarg + "'. Try --trigger-sel help."); + } +} + + +theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default" ) { + return theory::quantifiers::PRENEX_NO_USER_PAT; + } else if(optarg == "all") { + return theory::quantifiers::PRENEX_ALL; + } else if(optarg == "none") { + return theory::quantifiers::PRENEX_NONE; + } else if(optarg == "help") { + puts(s_prenexQuantModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --prenex-quant: `") + + optarg + "'. Try --prenex-quant help."); + } +} + +theory::quantifiers::CegqiFairMode OptionsHandler::stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "uf-dt-size" ) { + return theory::quantifiers::CEGQI_FAIR_UF_DT_SIZE; + } else if(optarg == "default" || optarg == "dt-size") { + return theory::quantifiers::CEGQI_FAIR_DT_SIZE; + } else if(optarg == "dt-height-bound" ){ + return theory::quantifiers::CEGQI_FAIR_DT_HEIGHT_PRED; + } else if(optarg == "none") { + return theory::quantifiers::CEGQI_FAIR_NONE; + } else if(optarg == "help") { + puts(s_cegqiFairModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --cegqi-fair: `") + + optarg + "'. Try --cegqi-fair help."); + } +} + +theory::quantifiers::TermDbMode OptionsHandler::stringToTermDbMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "all" ) { + return theory::quantifiers::TERM_DB_ALL; + } else if(optarg == "relevant") { + return theory::quantifiers::TERM_DB_RELEVANT; + } else if(optarg == "help") { + puts(s_termDbModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --term-db-mode: `") + + optarg + "'. Try --term-db-mode help."); + } +} + +theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "all" ) { + return theory::quantifiers::ITE_LIFT_QUANT_MODE_ALL; + } else if(optarg == "simple") { + return theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE; + } else if(optarg == "none") { + return theory::quantifiers::ITE_LIFT_QUANT_MODE_NONE; + } else if(optarg == "help") { + puts(s_iteLiftQuantHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --ite-lift-quant: `") + + optarg + "'. Try --ite-lift-quant help."); + } +} + +theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none" ) { + return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE; + } else if(optarg == "pre") { + return theory::quantifiers::SYGUS_INV_TEMPL_MODE_PRE; + } else if(optarg == "post") { + return theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST; + } else if(optarg == "help") { + puts(s_sygusInvTemplHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --sygus-inv-templ: `") + + optarg + "'. Try --sygus-inv-templ help."); + } +} + +theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "all" ) { + return theory::quantifiers::MACROS_QUANT_MODE_ALL; + } else if(optarg == "ground") { + return theory::quantifiers::MACROS_QUANT_MODE_GROUND; + } else if(optarg == "ground-uf") { + return theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF; + } else if(optarg == "help") { + puts(s_macrosQuantHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --macros-quant-mode: `") + + optarg + "'. Try --macros-quant-mode help."); + } +} + + +// theory/bv/options_handlers.h +void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) { +#ifndef CVC4_USE_ABC + if(value) { + std::stringstream ss; + ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_USE_ABC */ +} + +void OptionsHandler::abcEnabledBuild(std::string option, std::string value) throw(OptionException) { +#ifndef CVC4_USE_ABC + if(!value.empty()) { + std::stringstream ss; + ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_USE_ABC */ +} + +const std::string OptionsHandler::s_bitblastingModeHelp = "\ +Bit-blasting modes currently supported by the --bitblast option:\n\ +\n\ +lazy (default)\n\ ++ Separate boolean structure and term reasoning betwen the core\n\ + SAT solver and the bv SAT solver\n\ +\n\ +eager\n\ ++ Bitblast eagerly to bv SAT solver\n\ +"; + +theory::bv::BitblastMode OptionsHandler::stringToBitblastMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "lazy") { + if (!options::bitvectorPropagate.wasSetByUser()) { + options::bitvectorPropagate.set(true); + } + if (!options::bitvectorEqualitySolver.wasSetByUser()) { + options::bitvectorEqualitySolver.set(true); + } + if (!options::bitvectorEqualitySlicer.wasSetByUser()) { + if (options::incrementalSolving() || + options::produceModels()) { + options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_OFF); + } else { + options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_AUTO); + } + } + + if (!options::bitvectorInequalitySolver.wasSetByUser()) { + options::bitvectorInequalitySolver.set(true); + } + if (!options::bitvectorAlgebraicSolver.wasSetByUser()) { + options::bitvectorAlgebraicSolver.set(true); + } + return theory::bv::BITBLAST_MODE_LAZY; + } else if(optarg == "eager") { + + if (options::incrementalSolving() && + options::incrementalSolving.wasSetByUser()) { + throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\ + Try --bitblast=lazy")); + } + if (!options::bitvectorToBool.wasSetByUser()) { + options::bitvectorToBool.set(true); + } + + if (!options::bvAbstraction.wasSetByUser() && + !options::skolemizeArguments.wasSetByUser()) { + options::bvAbstraction.set(true); + options::skolemizeArguments.set(true); + } + return theory::bv::BITBLAST_MODE_EAGER; + } else if(optarg == "help") { + puts(s_bitblastingModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --bitblast: `") + + optarg + "'. Try --bitblast=help."); + } +} + +const std::string OptionsHandler::s_bvSlicerModeHelp = "\ +Bit-vector equality slicer modes supported by the --bv-eq-slicer option:\n\ +\n\ +auto (default)\n\ ++ Turn slicer on if input has only equalities over core symbols\n\ +\n\ +on\n\ ++ Turn slicer on\n\ +\n\ +off\n\ ++ Turn slicer off\n\ +"; + +theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "auto") { + return theory::bv::BITVECTOR_SLICER_AUTO; + } else if(optarg == "on") { + return theory::bv::BITVECTOR_SLICER_ON; + } else if(optarg == "off") { + return theory::bv::BITVECTOR_SLICER_OFF; + } else if(optarg == "help") { + puts(s_bitblastingModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --bv-eq-slicer: `") + + optarg + "'. Try --bv-eq-slicer=help."); + } +} + +void OptionsHandler::setBitblastAig(std::string option, bool arg) throw(OptionException) { + if(arg) { + if(options::bitblastMode.wasSetByUser()) { + if(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) { + throw OptionException("bitblast-aig must be used with eager bitblaster"); + } + } else { + theory::bv::BitblastMode mode = stringToBitblastMode("", "eager"); + options::bitblastMode.set(mode); + } + if(!options::bitvectorAigSimplifications.wasSetByUser()) { + options::bitvectorAigSimplifications.set("balance;drw"); + } + } +} + + +// theory/booleans/options_handlers.h +const std::string OptionsHandler::s_booleanTermConversionModeHelp = "\ +Boolean term conversion modes currently supported by the\n\ +--boolean-term-conversion-mode option:\n\ +\n\ +bitvectors [default]\n\ ++ Boolean terms are converted to bitvectors of size 1.\n\ +\n\ +datatypes\n\ ++ Boolean terms are converted to enumerations in the Datatype theory.\n\ +\n\ +native\n\ ++ Boolean terms are converted in a \"natural\" way depending on where they\n\ + are used. If in a datatype context, they are converted to an enumeration.\n\ + Elsewhere, they are converted to a bitvector of size 1.\n\ +"; + +theory::booleans::BooleanTermConversionMode OptionsHandler::stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException){ + if(optarg == "bitvectors") { + return theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS; + } else if(optarg == "datatypes") { + return theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES; + } else if(optarg == "native") { + return theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE; + } else if(optarg == "help") { + puts(s_booleanTermConversionModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") + + optarg + "'. Try --boolean-term-conversion-mode help."); + } +} + + +// theory/uf/options_handlers.h +const std::string OptionsHandler::s_ufssModeHelp = "\ +UF strong solver options currently supported by the --uf-ss option:\n\ +\n\ +full \n\ ++ Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\ +\n\ +no-minimal \n\ ++ Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\ +\n\ +none \n\ ++ Do not use uf strong solver to shrink model sizes. \n\ +\n\ +"; + +theory::uf::UfssMode OptionsHandler::stringToUfssMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default" || optarg == "full" ) { + return theory::uf::UF_SS_FULL; + } else if(optarg == "no-minimal") { + return theory::uf::UF_SS_NO_MINIMAL; + } else if(optarg == "none") { + return theory::uf::UF_SS_NONE; + } else if(optarg == "help") { + puts(s_ufssModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --uf-ss: `") + + optarg + "'. Try --uf-ss help."); + } +} + + + +// theory/options_handlers.h +const std::string OptionsHandler::s_theoryOfModeHelp = "\ +TheoryOf modes currently supported by the --theoryof-mode option:\n\ +\n\ +type (default) \n\ ++ type variables, constants and equalities by type\n\ +\n\ +term \n\ ++ type variables as uninterpreted, equalities by the parametric theory\n\ +"; + +theory::TheoryOfMode OptionsHandler::stringToTheoryOfMode(std::string option, std::string optarg) { + if(optarg == "type") { + return theory::THEORY_OF_TYPE_BASED; + } else if(optarg == "term") { + return theory::THEORY_OF_TERM_BASED; + } else if(optarg == "help") { + puts(s_theoryOfModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --theoryof-mode: `") + + optarg + "'. Try --theoryof-mode help."); + } +} + +// theory/options_handlers.h +std::string OptionsHandler::handleUseTheoryList(std::string option, std::string optarg) { + std::string currentList = options::useTheoryList(); + if(currentList.empty()){ + return optarg; + } else { + return currentList +','+ optarg; + } +} + +void OptionsHandler::notifyUseTheoryList(std::string option) { + d_options->d_useTheoryListListeners.notify(); +} + + + +// printer/options_handlers.h +const std::string OptionsHandler::s_modelFormatHelp = "\ +Model format modes currently supported by the --model-format option:\n\ +\n\ +default \n\ ++ Print model as expressions in the output language format.\n\ +\n\ +table\n\ ++ Print functional expressions over finite domains in a table format.\n\ +"; + +const std::string OptionsHandler::s_instFormatHelp = "\ +Inst format modes currently supported by the --model-format option:\n\ +\n\ +default \n\ ++ Print instantiations as a list in the output language format.\n\ +\n\ +szs\n\ ++ Print instantiations as SZS compliant proof.\n\ +"; + +ModelFormatMode OptionsHandler::stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default") { + return MODEL_FORMAT_MODE_DEFAULT; + } else if(optarg == "table") { + return MODEL_FORMAT_MODE_TABLE; + } else if(optarg == "help") { + puts(s_modelFormatHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --model-format: `") + + optarg + "'. Try --model-format help."); + } +} + +InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default") { + return INST_FORMAT_MODE_DEFAULT; + } else if(optarg == "szs") { + return INST_FORMAT_MODE_SZS; + } else if(optarg == "help") { + puts(s_instFormatHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --inst-format: `") + + optarg + "'. Try --inst-format help."); + } +} + + +// decision/options_handlers.h +const std::string OptionsHandler::s_decisionModeHelp = "\ +Decision modes currently supported by the --decision option:\n\ +\n\ +internal (default)\n\ ++ Use the internal decision heuristics of the SAT solver\n\ +\n\ +justification\n\ ++ An ATGP-inspired justification heuristic\n\ +\n\ +justification-stoponly\n\ ++ Use the justification heuristic only to stop early, not for decisions\n\ +"; + +decision::DecisionMode OptionsHandler::stringToDecisionMode(std::string option, std::string optarg) throw(OptionException) { + options::decisionStopOnly.set(false); + + if(optarg == "internal") { + return decision::DECISION_STRATEGY_INTERNAL; + } else if(optarg == "justification") { + return decision::DECISION_STRATEGY_JUSTIFICATION; + } else if(optarg == "justification-stoponly") { + options::decisionStopOnly.set(true); + return decision::DECISION_STRATEGY_JUSTIFICATION; + } else if(optarg == "help") { + puts(s_decisionModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --decision: `") + + optarg + "'. Try --decision help."); + } +} + +decision::DecisionWeightInternal OptionsHandler::stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "off") + return decision::DECISION_WEIGHT_INTERNAL_OFF; + else if(optarg == "max") + return decision::DECISION_WEIGHT_INTERNAL_MAX; + else if(optarg == "sum") + return decision::DECISION_WEIGHT_INTERNAL_SUM; + else if(optarg == "usr1") + return decision::DECISION_WEIGHT_INTERNAL_USR1; + else + throw OptionException(std::string("--decision-weight-internal must be off, max or sum.")); +} + + +// smt/options_handlers.h +const std::string OptionsHandler::s_simplificationHelp = "\ +Simplification modes currently supported by the --simplification option:\n\ +\n\ +batch (default) \n\ ++ save up all ASSERTions; run nonclausal simplification and clausal\n\ + (MiniSat) propagation for all of them only after reaching a querying command\n\ + (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\ +\n\ +none\n\ ++ do not perform nonclausal simplification\n\ +"; + + + +SimplificationMode OptionsHandler::stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "batch") { + return SIMPLIFICATION_MODE_BATCH; + } else if(optarg == "none") { + return SIMPLIFICATION_MODE_NONE; + } else if(optarg == "help") { + puts(s_simplificationHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --simplification: `") + + optarg + "'. Try --simplification help."); + } +} + + +void OptionsHandler::setProduceAssertions(std::string option, bool value) throw() { + options::produceAssertions.set(value); + options::interactiveMode.set(value); +} + + +void OptionsHandler::proofEnabledBuild(std::string option, bool value) throw(OptionException) { +#ifndef CVC4_PROOF + if(value) { + std::stringstream ss; + ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_PROOF */ +} + +void OptionsHandler::notifyDumpToFile(std::string option) { + d_options->d_dumpToFileListeners.notify(); +} + + +void OptionsHandler::notifySetRegularOutputChannel(std::string option) { + d_options->d_setRegularChannelListeners.notify(); +} + +void OptionsHandler::notifySetDiagnosticOutputChannel(std::string option) { + d_options->d_setDiagnosticChannelListeners.notify(); +} + + +std::string OptionsHandler::checkReplayFilename(std::string option, std::string optarg) { +#ifdef CVC4_REPLAY + if(optarg == "") { + throw OptionException (std::string("Bad file name for --replay")); + } else { + return optarg; + } +#else /* CVC4_REPLAY */ + throw OptionException("The replay feature was disabled in this build of CVC4."); +#endif /* CVC4_REPLAY */ +} + +void OptionsHandler::notifySetReplayLogFilename(std::string option) { + d_options->d_setReplayFilenameListeners.notify(); +} + +void OptionsHandler::statsEnabledBuild(std::string option, bool value) throw(OptionException) { +#ifndef CVC4_STATISTICS_ON + if(value) { + std::stringstream ss; + ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_STATISTICS_ON */ +} + +void OptionsHandler::threadN(std::string option) { + throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); +} + +void OptionsHandler::notifyDumpMode(std::string option) throw(OptionException) { + d_options->d_setDumpModeListeners.notify(); +} + + +// expr/options_handlers.h +void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) { + if(depth < -1) { + throw OptionException("--default-expr-depth requires a positive argument, or -1."); + } +} + +void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) { + if(dag < 0) { + throw OptionException("--default-dag-thresh requires a nonnegative argument."); + } +} + +void OptionsHandler::notifySetDefaultExprDepth(std::string option) { + d_options->d_setDefaultExprDepthListeners.notify(); +} + +void OptionsHandler::notifySetDefaultDagThresh(std::string option) { + d_options->d_setDefaultDagThreshListeners.notify(); +} + +void OptionsHandler::notifySetPrintExprTypes(std::string option) { + d_options->d_setPrintExprTypesListeners.notify(); +} + + +// main/options_handlers.h +void OptionsHandler::showConfiguration(std::string option) { + fputs(Configuration::about().c_str(), stdout); + printf("\n"); + printf("version : %s\n", Configuration::getVersionString().c_str()); + if(Configuration::isGitBuild()) { + const char* branchName = Configuration::getGitBranchName(); + if(*branchName == '\0') { + branchName = "-"; + } + printf("scm : git [%s %s%s]\n", + branchName, + std::string(Configuration::getGitCommit()).substr(0, 8).c_str(), + Configuration::hasGitModifications() ? + " (with modifications)" : ""); + } else if(Configuration::isSubversionBuild()) { + printf("scm : svn [%s r%u%s]\n", + Configuration::getSubversionBranchName(), + Configuration::getSubversionRevision(), + Configuration::hasSubversionModifications() ? + " (with modifications)" : ""); + } else { + printf("scm : no\n"); + } + printf("\n"); + printf("library : %u.%u.%u\n", + Configuration::getVersionMajor(), + Configuration::getVersionMinor(), + Configuration::getVersionRelease()); + printf("\n"); + printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no"); + printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no"); + printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no"); + printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); + printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no"); + printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); + printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); + printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no"); + printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); + printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); + printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); + printf("\n"); + printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no"); + printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); + printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); + printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); + printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); + printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no"); + printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); + exit(0); +} + +void OptionsHandler::showDebugTags(std::string option) { + if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { + printf("available tags:"); + unsigned ntags = Configuration::getNumDebugTags(); + char const* const* tags = Configuration::getDebugTags(); + for(unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + } 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"); + } + exit(0); +} + +void OptionsHandler::showTraceTags(std::string option) { + if(Configuration::isTracingBuild()) { + printf("available tags:"); + unsigned ntags = Configuration::getNumTraceTags(); + char const* const* tags = Configuration::getTraceTags(); + for (unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + } else { + throw OptionException("trace tags not available in non-tracing build"); + } + exit(0); +} + + +OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "help") { + options::languageHelp.set(true); + return language::output::LANG_AUTO; + } + + try { + return language::toOutputLanguage(optarg); + } catch(OptionException& oe) { + throw OptionException("Error in " + option + ": " + oe.getMessage() + + "\nTry --output-language help"); + } + + Unreachable(); +} + +InputLanguage OptionsHandler::stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "help") { + options::languageHelp.set(true); + return language::input::LANG_AUTO; + } + + try { + return language::toInputLanguage(optarg); + } catch(OptionException& oe) { + throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --language help"); + } + + Unreachable(); +} + +/* options/base_options_handlers.h */ +void OptionsHandler::setVerbosity(std::string option, int value) throw(OptionException) { + if(Configuration::isMuzzledBuild()) { + DebugChannel.setStream(&CVC4::null_os); + TraceChannel.setStream(&CVC4::null_os); + NoticeChannel.setStream(&CVC4::null_os); + ChatChannel.setStream(&CVC4::null_os); + MessageChannel.setStream(&CVC4::null_os); + WarningChannel.setStream(&CVC4::null_os); + } else { + if(value < 2) { + ChatChannel.setStream(&CVC4::null_os); + } else { + ChatChannel.setStream(&std::cout); + } + if(value < 1) { + NoticeChannel.setStream(&CVC4::null_os); + } else { + NoticeChannel.setStream(&std::cout); + } + if(value < 0) { + MessageChannel.setStream(&CVC4::null_os); + WarningChannel.setStream(&CVC4::null_os); + } else { + MessageChannel.setStream(&std::cout); + WarningChannel.setStream(&std::cerr); + } + } +} + +void OptionsHandler::increaseVerbosity(std::string option) { + options::verbosity.set(options::verbosity() + 1); + setVerbosity(option, options::verbosity()); +} + +void OptionsHandler::decreaseVerbosity(std::string option) { + options::verbosity.set(options::verbosity() - 1); + setVerbosity(option, options::verbosity()); +} + + +void OptionsHandler::addTraceTag(std::string option, std::string optarg) { + if(Configuration::isTracingBuild()) { + if(!Configuration::isTraceTag(optarg.c_str())) { + + if(optarg == "help") { + printf("available tags:"); + unsigned ntags = Configuration::getNumTraceTags(); + char const* const* tags = Configuration::getTraceTags(); + for(unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + exit(0); + } + + throw OptionException(std::string("trace tag ") + optarg + + std::string(" not available.") + + suggestTags(Configuration::getTraceTags(), optarg) ); + } + } else { + throw OptionException("trace tags not available in non-tracing builds"); + } + Trace.on(optarg); +} + +void OptionsHandler::addDebugTag(std::string option, std::string optarg) { + if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { + if(!Configuration::isDebugTag(optarg.c_str()) && + !Configuration::isTraceTag(optarg.c_str())) { + + if(optarg == "help") { + printf("available tags:"); + unsigned ntags = Configuration::getNumDebugTags(); + char const* const* tags = Configuration::getDebugTags(); + for(unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + exit(0); + } + + throw OptionException(std::string("debug tag ") + optarg + + std::string(" not available.") + + suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) ); + } + } 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); +} + + + + +std::string OptionsHandler::suggestTags(char const* const* validTags, std::string inputTag, + char const* const* additionalTags) +{ + DidYouMean didYouMean; + + const char* opt; + for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) { + didYouMean.addWord(validTags[i]); + } + if(additionalTags != NULL) { + for(size_t i = 0; (opt = additionalTags[i]) != NULL; ++i) { + didYouMean.addWord(additionalTags[i]); + } + } + + return didYouMean.getMatchAsString(inputTag); +} + + + + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ diff --git a/src/options/options_handler.h b/src/options/options_handler.h new file mode 100644 index 000000000..9aa037004 --- /dev/null +++ b/src/options/options_handler.h @@ -0,0 +1,224 @@ +/********************* */ +/*! \file options_handler.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Interface for custom handlers and predicates options. + ** + ** Interface for custom handlers and predicates options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__OPTIONS__OPTIONS_HANDLER_H +#define __CVC4__OPTIONS__OPTIONS_HANDLER_H + +#include <ostream> +#include <string> + +#include "base/modal_exception.h" +#include "options/arith_heuristic_pivot_rule.h" +#include "options/arith_propagation_mode.h" +#include "options/arith_unate_lemma_mode.h" +#include "options/base_handlers.h" +#include "options/boolean_term_conversion_mode.h" +#include "options/bv_bitblast_mode.h" +#include "options/decision_mode.h" +#include "options/language.h" +#include "options/option_exception.h" +#include "options/options.h" +#include "options/printer_modes.h" +#include "options/quantifiers_modes.h" +#include "options/simplification_mode.h" +#include "options/theoryof_mode.h" +#include "options/ufss_mode.h" + +namespace CVC4 { +namespace options { + +class OptionsHandler { +public: + OptionsHandler(Options* options); + virtual ~OptionsHandler() {} + + void unsignedGreater0(const std::string& option, unsigned value) { + options::greater(0)(option, value); + } + + void unsignedLessEqual2(const std::string& option, unsigned value) { + options::less_equal(2)(option, value); + } + + void doubleGreaterOrEqual0(const std::string& option, double value) { + options::greater_equal(0.0)(option, value); + } + + void doubleLessOrEqual1(const std::string& option, double value) { + options::less_equal(1.0)(option, value); + } + + // DONE + // decision/options_handlers.h + // expr/options_handlers.h + // main/options_handlers.h + // options/base_options_handlers.h + // printer/options_handlers.h + // smt/options_handlers.h + // theory/options_handlers.h + // theory/booleans/options_handlers.h + // theory/uf/options_handlers.h + // theory/bv/options_handlers.h + // theory/quantifiers/options_handlers.h + // theory/arith/options_handlers.h + + + // theory/arith/options_handlers.h + ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException); + ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException); + ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException); + + // theory/quantifiers/options_handlers.h + theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException); + void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException); + theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException); + void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException); + theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg) throw(OptionException); + void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException); + theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException); + + // theory/bv/options_handlers.h + void abcEnabledBuild(std::string option, bool value) throw(OptionException); + void abcEnabledBuild(std::string option, std::string value) throw(OptionException); + theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException); + theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException); + void setBitblastAig(std::string option, bool arg) throw(OptionException); + + + // theory/booleans/options_handlers.h + theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException); + + // theory/uf/options_handlers.h + theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException); + + // theory/options_handlers.h + theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg); + void notifyUseTheoryList(std::string option); + std::string handleUseTheoryList(std::string option, std::string optarg); + + + // printer/options_handlers.h + ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException); + InstFormatMode stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException); + + // decision/options_handlers.h + decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg) throw(OptionException); + decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException); + + + /* smt/options_handlers.h */ + void notifyForceLogic(const std::string& option); + void notifyBeforeSearch(const std::string& option) throw(ModalException); + void notifyDumpMode(std::string option) throw(OptionException); + SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException); + void setProduceAssertions(std::string option, bool value) throw(); + void proofEnabledBuild(std::string option, bool value) throw(OptionException); + void notifyDumpToFile(std::string option); + void notifySetRegularOutputChannel(std::string option); + void notifySetDiagnosticOutputChannel(std::string option); + std::string checkReplayFilename(std::string option, std::string optarg); + void notifySetReplayLogFilename(std::string option); + + void statsEnabledBuild(std::string option, bool value) throw(OptionException); + + unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException); + unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException); + unsigned long rlimitHandler(std::string option, std::string optarg) throw(OptionException); + unsigned long rlimitPerHandler(std::string option, std::string optarg) throw(OptionException); + + void notifyTlimit(const std::string& option); + void notifyTlimitPer(const std::string& option); + void notifyRlimit(const std::string& option); + void notifyRlimitPer(const std::string& option); + + + /* expr/options_handlers.h */ + void setDefaultExprDepthPredicate(std::string option, int depth); + void setDefaultDagThreshPredicate(std::string option, int dag); + void notifySetDefaultExprDepth(std::string option); + void notifySetDefaultDagThresh(std::string option); + void notifySetPrintExprTypes(std::string option); + + /* main/options_handlers.h */ + void showConfiguration(std::string option); + void showDebugTags(std::string option); + void showTraceTags(std::string option); + void threadN(std::string option); + + /* options/base_options_handlers.h */ + void setVerbosity(std::string option, int value) throw(OptionException); + void increaseVerbosity(std::string option); + void decreaseVerbosity(std::string option); + OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException); + InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException); + void addTraceTag(std::string option, std::string optarg); + void addDebugTag(std::string option, std::string optarg); + void notifyPrintSuccess(std::string option); + + private: + + /* Helper utilities */ + static std::string suggestTags(char const* const* validTags, std::string inputTag, + char const* const* additionalTags = NULL); + + /** Pointer to the containing Options object.*/ + Options* d_options; + + /* Help strings */ + static const std::string s_bitblastingModeHelp; + static const std::string s_booleanTermConversionModeHelp; + static const std::string s_bvSlicerModeHelp; + static const std::string s_cegqiFairModeHelp; + static const std::string s_decisionModeHelp; + static const std::string s_instFormatHelp ; + static const std::string s_instWhenHelp; + static const std::string s_iteLiftQuantHelp; + static const std::string s_literalMatchHelp; + static const std::string s_macrosQuantHelp; + static const std::string s_mbqiModeHelp; + static const std::string s_modelFormatHelp; + static const std::string s_prenexQuantModeHelp; + static const std::string s_qcfModeHelp; + static const std::string s_qcfWhenModeHelp; + static const std::string s_simplificationHelp; + static const std::string s_sygusInvTemplHelp; + static const std::string s_termDbModeHelp; + static const std::string s_theoryOfModeHelp; + static const std::string s_triggerSelModeHelp; + static const std::string s_ufssModeHelp; + static const std::string s_userPatModeHelp; + static const std::string s_errorSelectionRulesHelp; + static const std::string s_arithPropagationModeHelp; + static const std::string s_arithUnateLemmasHelp; + +}; /* class OptionHandler */ + + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__OPTIONS__OPTIONS_HANDLER_H */ diff --git a/src/options/options_handler_interface.cpp b/src/options/options_handler_interface.cpp deleted file mode 100644 index 2cf19a611..000000000 --- a/src/options/options_handler_interface.cpp +++ /dev/null @@ -1,358 +0,0 @@ -/********************* */ -/*! \file options_handler_interface.cpp - ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Interface for custom handlers and predicates options. - ** - ** Interface for custom handlers and predicates options. - **/ - -#include "options/options_handler_interface.h" - -#include <ostream> -#include <string> - -#include "base/cvc4_assert.h" -#include "base/exception.h" -#include "base/modal_exception.h" -#include "options/arith_heuristic_pivot_rule.h" -#include "options/arith_propagation_mode.h" -#include "options/arith_unate_lemma_mode.h" -#include "options/boolean_term_conversion_mode.h" -#include "options/bv_bitblast_mode.h" -#include "options/decision_mode.h" -#include "options/language.h" -#include "options/option_exception.h" -#include "options/printer_modes.h" -#include "options/quantifiers_modes.h" -#include "options/simplification_mode.h" -#include "options/theoryof_mode.h" -#include "options/ufss_mode.h" - -namespace CVC4 { -namespace options { - -static const char* s_third_argument_warning = - "We no longer support passing the third argument to the setting an option as NULL."; - -// theory/arith/options_handlers.h -ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToArithUnateLemmaMode(option, optarg); -} -ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToArithPropagationMode(option, optarg); -} -ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToErrorSelectionRule(option, optarg); -} - -// theory/quantifiers/options_handlers.h -theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToInstWhenMode(option, optarg); -} -void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->checkInstWhenMode(option, mode); -} -theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToLiteralMatchMode(option, optarg); -} -void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->checkLiteralMatchMode(option, mode); -} -theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToMbqiMode(option, optarg); -} -void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->checkMbqiMode(option, mode); -} -theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToQcfWhenMode(option, optarg); -} -theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToQcfMode(option, optarg); -} -theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToUserPatMode(option, optarg); -} -theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToTriggerSelMode(option, optarg); -} -theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToPrenexQuantMode(option, optarg); -} -theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToCegqiFairMode(option, optarg); -} -theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler-> stringToTermDbMode(option, optarg); -} -theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToIteLiftQuantMode(option, optarg); -} -theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToSygusInvTemplMode(option, optarg); -} -theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToMacrosQuantMode(option, optarg); -} - - -// theory/bv/options_handlers.h -void abcEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->abcEnabledBuild(option, value); -} -void abcEnabledBuild(std::string option, std::string value, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->abcEnabledBuild(option, value); -} -theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToBitblastMode(option, optarg); -} -theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToBvSlicerMode(option, optarg); -} -void setBitblastAig(std::string option, bool arg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->setBitblastAig(option, arg); -} - - -// theory/booleans/options_handlers.h -theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToBooleanTermConversionMode( option, optarg); -} - -// theory/uf/options_handlers.h -theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToUfssMode(option, optarg); -} - -// theory/options_handlers.h -theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToTheoryOfMode(option, optarg); -} -void useTheory(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->useTheory(option, optarg); -} - -// printer/options_handlers.h -ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToModelFormatMode(option, optarg); -} - -InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToInstFormatMode(option, optarg); -} - - -// decision/options_handlers.h -decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToDecisionMode(option, optarg); -} - -decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToDecisionWeightInternal(option, optarg); -} - - -/* options/base_options_handlers.h */ -void setVerbosity(std::string option, int value, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->setVerbosity(option, value); -} -void increaseVerbosity(std::string option, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->increaseVerbosity(option); -} -void decreaseVerbosity(std::string option, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->decreaseVerbosity(option); -} - -OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToOutputLanguage(option, optarg); -} - -InputLanguage stringToInputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToInputLanguage(option, optarg); -} - -void addTraceTag(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->addTraceTag(option, optarg); -} - -void addDebugTag(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->addDebugTag(option, optarg); -} - -void setPrintSuccess(std::string option, bool value, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->setPrintSuccess(option, value); -} - - -/* main/options_handlers.h */ -void showConfiguration(std::string option, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->showConfiguration(option); -} - -void showDebugTags(std::string option, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->showDebugTags(option); -} - -void showTraceTags(std::string option, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->showTraceTags(option); -} - -void threadN(std::string option, OptionsHandler* handler){ - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->threadN(option); -} - -/* expr/options_handlers.h */ -void setDefaultExprDepth(std::string option, int depth, OptionsHandler* handler){ - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->setDefaultExprDepth(option, depth); -} - -void setDefaultDagThresh(std::string option, int dag, OptionsHandler* handler){ - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->setDefaultDagThresh(option, dag); -} - -void setPrintExprTypes(std::string option, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->setPrintExprTypes(option); -} - - -/* smt/options_handlers.h */ -void dumpMode(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->dumpMode(option, optarg); -} - -LogicInfo* stringToLogicInfo(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){ - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToLogicInfo(option, optarg); -} - -SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){ - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->stringToSimplificationMode(option, optarg); -} - -// ensure we haven't started search yet -void beforeSearch(std::string option, bool value, OptionsHandler* handler) throw(ModalException){ - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->beforeSearch(option, value); -} - -void setProduceAssertions(std::string option, bool value, OptionsHandler* handler) throw() { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->setProduceAssertions(option, value); -} - -// ensure we are a proof-enabled build of CVC4 -void proofEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->proofEnabledBuild(option, value); -} - -void dumpToFile(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->dumpToFile(option, optarg); -} - -void setRegularOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->setRegularOutputChannel(option, optarg); -} - -void setDiagnosticOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - handler->setDiagnosticOutputChannel(option, optarg); -} - -std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->checkReplayFilename(option, optarg); -} - - -// ensure we are a stats-enabled build of CVC4 -void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->statsEnabledBuild(option, value); -} - -unsigned long tlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->tlimitHandler(option, optarg); -} - -unsigned long tlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler-> tlimitPerHandler(option, optarg); -} - -unsigned long rlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->rlimitHandler(option, optarg); -} - -unsigned long rlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->rlimitPerHandler(option, optarg); -} - - - -OptionsHandler::OptionsHandler() { } - -}/* CVC4::options namespace */ -}/* CVC4 namespace */ diff --git a/src/options/options_handler_interface.h b/src/options/options_handler_interface.h deleted file mode 100644 index e9e91ef0b..000000000 --- a/src/options/options_handler_interface.h +++ /dev/null @@ -1,272 +0,0 @@ -/********************* */ -/*! \file options_handler_interface.h - ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Interface for custom handlers and predicates options. - ** - ** Interface for custom handlers and predicates options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__OPTIONS__OPTIONS_HANDLER_INTERFACE_H -#define __CVC4__OPTIONS__OPTIONS_HANDLER_INTERFACE_H - -#include <ostream> -#include <string> - -#include "base/modal_exception.h" -#include "options/arith_heuristic_pivot_rule.h" -#include "options/arith_propagation_mode.h" -#include "options/arith_unate_lemma_mode.h" -#include "options/boolean_term_conversion_mode.h" -#include "options/bv_bitblast_mode.h" -#include "options/decision_mode.h" -#include "options/language.h" -#include "options/option_exception.h" -#include "options/printer_modes.h" -#include "options/quantifiers_modes.h" -#include "options/simplification_mode.h" -#include "options/theoryof_mode.h" -#include "options/ufss_mode.h" - -namespace CVC4 { -class LogicInfo; -}/* CVC4 namespace */ - -namespace CVC4 { -namespace options { - -class OptionsHandler { -public: - OptionsHandler(); - virtual ~OptionsHandler() {} - - void setOption(const std::string& key, const std::string& optionarg) throw(OptionException, ModalException); - - std::string getOption(const std::string& key) const throw(OptionException); - - // DONE - // decision/options_handlers.h - // expr/options_handlers.h - // main/options_handlers.h - // options/base_options_handlers.h - // printer/options_handlers.h - // smt/options_handlers.h - // theory/options_handlers.h - // theory/booleans/options_handlers.h - // theory/uf/options_handlers.h - // theory/bv/options_handlers.h - // theory/quantifiers/options_handlers.h - // theory/arith/options_handlers.h - - - // theory/arith/options_handlers.h - virtual ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException) = 0; - - // theory/quantifiers/options_handlers.h - virtual theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException) = 0; - virtual theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) = 0; - virtual theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException) = 0; - virtual theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException) = 0; - - // theory/bv/options_handlers.h - virtual void abcEnabledBuild(std::string option, bool value) throw(OptionException) = 0; - virtual void abcEnabledBuild(std::string option, std::string value) throw(OptionException) = 0; - virtual theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual void setBitblastAig(std::string option, bool arg) throw(OptionException) = 0; - - - // theory/booleans/options_handlers.h - virtual theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException) = 0; - - // theory/uf/options_handlers.h - virtual theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException) = 0; - - // theory/options_handlers.h - virtual theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg) = 0; - virtual void useTheory(std::string option, std::string optarg) = 0; - - - // printer/options_handlers.h - virtual ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual InstFormatMode stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException) = 0; - - // decision/options_handlers.h - virtual decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg) throw(OptionException) = 0; - virtual decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException) = 0; - - - /* smt/options_handlers.h */ - virtual void dumpMode(std::string option, std::string optarg) = 0; - virtual LogicInfo* stringToLogicInfo(std::string option, std::string optarg) throw(OptionException) = 0; - virtual SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException) = 0; - - virtual void beforeSearch(std::string option, bool value) throw(ModalException) = 0; - virtual void setProduceAssertions(std::string option, bool value) throw() = 0; - virtual void proofEnabledBuild(std::string option, bool value) throw(OptionException) = 0; - virtual void dumpToFile(std::string option, std::string optarg) = 0; - virtual void setRegularOutputChannel(std::string option, std::string optarg) = 0; - virtual void setDiagnosticOutputChannel(std::string option, std::string optarg) = 0; - virtual std::string checkReplayFilename(std::string option, std::string optarg) = 0; - virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException) = 0; - virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException) = 0; - virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) = 0; - virtual unsigned long rlimitHandler(std::string option, std::string optarg) throw(OptionException) = 0; - virtual unsigned long rlimitPerHandler(std::string option, std::string optarg) throw(OptionException) = 0; - - /* expr/options_handlers.h */ - virtual void setDefaultExprDepth(std::string option, int depth) = 0; - virtual void setDefaultDagThresh(std::string option, int dag) = 0; - virtual void setPrintExprTypes(std::string option) = 0; - - /* main/options_handlers.h */ - virtual void showConfiguration(std::string option) = 0; - virtual void showDebugTags(std::string option) = 0; - virtual void showTraceTags(std::string option) = 0; - virtual void threadN(std::string option) = 0; - - /* options/base_options_handlers.h */ - virtual void setVerbosity(std::string option, int value) throw(OptionException) = 0; - virtual void increaseVerbosity(std::string option) = 0; - virtual void decreaseVerbosity(std::string option) = 0; - virtual OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException) = 0; - virtual InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) = 0; - virtual void addTraceTag(std::string option, std::string optarg) = 0; - virtual void addDebugTag(std::string option, std::string optarg) = 0; - virtual void setPrintSuccess(std::string option, bool value) = 0; -}; /* class OptionHandler */ - -// theory/arith/options_handlers.h -ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - -// theory/quantifiers/options_handlers.h -theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - - -// theory/bv/options_handlers.h -void abcEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException); -void abcEnabledBuild(std::string option, std::string value, OptionsHandler* handler) throw(OptionException); -theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -void setBitblastAig(std::string option, bool arg, OptionsHandler* handler) throw(OptionException); - -// theory/booleans/options_handlers.h -theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - -// theory/uf/options_handlers.h -theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - - -// theory/options_handlers.h -theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, OptionsHandler* handler); -void useTheory(std::string option, std::string optarg, OptionsHandler* handler); - -// printer/options_handlers.h -ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - -// decision/options_handlers.h -decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - - -/* options/base_options_handlers.h */ -void setVerbosity(std::string option, int value, OptionsHandler* handler) throw(OptionException); -void increaseVerbosity(std::string option, OptionsHandler* handler); -void decreaseVerbosity(std::string option, OptionsHandler* handler); -OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -InputLanguage stringToInputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); -void addTraceTag(std::string option, std::string optarg, OptionsHandler* handler); -void addDebugTag(std::string option, std::string optarg, OptionsHandler* handler); -void setPrintSuccess(std::string option, bool value, OptionsHandler* handler); - -/* main/options_handlers.h */ -void showConfiguration(std::string option, OptionsHandler* handler); -void showDebugTags(std::string option, OptionsHandler* handler); -void showTraceTags(std::string option, OptionsHandler* handler); -void threadN(std::string option, OptionsHandler* handler); - -/* expr/options_handlers.h */ -void setDefaultExprDepth(std::string option, int depth, OptionsHandler* handler); -void setDefaultDagThresh(std::string option, int dag, OptionsHandler* handler); -void setPrintExprTypes(std::string option, OptionsHandler* handler); - -/* smt/options_handlers.h */ -void dumpMode(std::string option, std::string optarg, OptionsHandler* handler); - -LogicInfo* stringToLogicInfo(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - -SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - -// ensure we haven't started search yet -void beforeSearch(std::string option, bool value, OptionsHandler* handler) throw(ModalException); - -void setProduceAssertions(std::string option, bool value, OptionsHandler* handler) throw(); - -// ensure we are a proof-enabled build of CVC4 -void proofEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException); - -void dumpToFile(std::string option, std::string optarg, OptionsHandler* handler); - -void setRegularOutputChannel(std::string option, std::string optarg, OptionsHandler* handler); - -void setDiagnosticOutputChannel(std::string option, std::string optarg, OptionsHandler* handler); - -std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler); - -// ensure we are a stats-enabled build of CVC4 -void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException); - -unsigned long tlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - -unsigned long tlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - -unsigned long rlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - -unsigned long rlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); - - -}/* CVC4::options namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__OPTIONS__OPTIONS_HANDLER_INTERFACE_H */ diff --git a/src/options/options_handler_interface.i b/src/options/options_handler_interface.i deleted file mode 100644 index b7076a0b8..000000000 --- a/src/options/options_handler_interface.i +++ /dev/null @@ -1,5 +0,0 @@ -%{ -#include "options/options_handler_interface.h" -%} - -%include "options/options_handler_interface.h" diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp new file mode 100644 index 000000000..2e86c732e --- /dev/null +++ b/src/options/options_public_functions.cpp @@ -0,0 +1,322 @@ +/********************* */ +/*! \file options_public_functions.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Kshitij Bansal + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Definitions of public facing interface functions for Options. + ** + ** Definitions of public facing interface functions for Options. These are + ** all 1 line wrappers for Options::get<T>, Options::set<T>, and + ** Options::wasSetByUser<T> for different option types T. + **/ + +#include "options.h" + +#include <fstream> +#include <ostream> +#include <string> +#include <vector> + +#include "base/listener.h" +#include "base/modal_exception.h" +#include "base/tls.h" +#include "options/base_options.h" +#include "options/language.h" +#include "options/main_options.h" +#include "options/parser_options.h" +#include "options/printer_modes.h" +#include "options/printer_options.h" +#include "options/option_exception.h" +#include "options/smt_options.h" +#include "options/quantifiers_options.h" + +namespace CVC4 { + +// Get accessor functions. +InputLanguage Options::getInputLanguage() const { + return (*this)[options::inputLanguage]; +} + +InstFormatMode Options::getInstFormatMode() const { + return (*this)[options::instFormatMode]; +} + +OutputLanguage Options::getOutputLanguage() const { + return (*this)[options::outputLanguage]; +} + +bool Options::getCheckProofs() const{ + return (*this)[options::checkProofs]; +} + +bool Options::getContinuedExecution() const{ + return (*this)[options::continuedExecution]; +} + +bool Options::getDumpInstantiations() const{ + return (*this)[options::dumpInstantiations]; +} + +bool Options::getDumpModels() const{ + return (*this)[options::dumpModels]; +} + +bool Options::getDumpProofs() const{ + return (*this)[options::dumpProofs]; +} + +bool Options::getDumpSynth() const{ + return (*this)[options::dumpSynth]; +} + +bool Options::getDumpUnsatCores() const{ + return (*this)[options::dumpUnsatCores]; +} + +bool Options::getEarlyExit() const{ + return (*this)[options::earlyExit]; +} + +bool Options::getFallbackSequential() const{ + return (*this)[options::fallbackSequential]; +} + +bool Options::getFilesystemAccess() const{ + return (*this)[options::filesystemAccess]; +} + +bool Options::getForceNoLimitCpuWhileDump() const{ + return (*this)[options::forceNoLimitCpuWhileDump]; +} + +bool Options::getHelp() const{ + return (*this)[options::help]; +} + +bool Options::getIncrementalParallel() const{ + return (*this)[options::incrementalParallel]; +} + +bool Options::getIncrementalSolving() const{ + return (*this)[options::incrementalSolving]; +} + +bool Options::getInteractive() const{ + return (*this)[options::interactive]; +} + +bool Options::getInteractivePrompt() const{ + return (*this)[options::interactivePrompt]; +} + +bool Options::getLanguageHelp() const{ + return (*this)[options::languageHelp]; +} + +bool Options::getMemoryMap() const{ + return (*this)[options::memoryMap]; +} + +bool Options::getParseOnly() const{ + return (*this)[options::parseOnly]; +} + +bool Options::getProduceModels() const{ + return (*this)[options::produceModels]; +} + +bool Options::getProof() const{ + return (*this)[options::proof]; +} + +bool Options::getSegvSpin() const{ + return (*this)[options::segvSpin]; +} + +bool Options::getSemanticChecks() const{ + return (*this)[options::semanticChecks]; +} + +bool Options::getStatistics() const{ + return (*this)[options::statistics]; +} + +bool Options::getStatsEveryQuery() const{ + return (*this)[options::statsEveryQuery]; +} + +bool Options::getStatsHideZeros() const{ + return (*this)[options::statsHideZeros]; +} + +bool Options::getStrictParsing() const{ + return (*this)[options::strictParsing]; +} + +bool Options::getTearDownIncremental() const{ + return (*this)[options::tearDownIncremental]; +} + +bool Options::getVersion() const{ + return (*this)[options::version]; +} + +bool Options::getWaitToJoin() const{ + return (*this)[options::waitToJoin]; +} + +const std::string& Options::getForceLogicString() const{ + return (*this)[options::forceLogicString]; +} + +const std::vector<std::string>& Options::getThreadArgv() const{ + return (*this)[options::threadArgv]; +} + +int Options::getSharingFilterByLength() const{ + return (*this)[options::sharingFilterByLength]; +} + +int Options::getThreadId() const{ + return (*this)[options::thread_id]; +} + +int Options::getVerbosity() const{ + return (*this)[options::verbosity]; +} + +std::istream* Options::getIn() const{ + return (*this)[options::in]; +} + +std::ostream* Options::getErr(){ + return (*this)[options::err]; +} + +std::ostream* Options::getOut(){ + return (*this)[options::out]; +} + +std::ostream* Options::getOutConst() const{ +#warning "Remove Options::getOutConst" + return (*this)[options::out]; +} + +std::string Options::getBinaryName() const{ + return (*this)[options::binary_name]; +} + +std::string Options::getReplayInputFilename() const{ + return (*this)[options::replayInputFilename]; +} + +unsigned Options::getParseStep() const{ + return (*this)[options::parseStep]; +} + +unsigned Options::getThreadStackSize() const{ + return (*this)[options::threadStackSize]; +} + +unsigned Options::getThreads() const{ + return (*this)[options::threads]; +} + +int Options::currentGetSharingFilterByLength() { + return current()->getSharingFilterByLength(); +} + +int Options::currentGetThreadId() { + return current()->getThreadId(); +} + +std::ostream* Options::currentGetOut() { + return current()->getOut(); +} + + +// TODO: Document these. +void Options::setCeGuidedInst(bool value) { + set(options::ceGuidedInst, value); +} + +void Options::setDumpSynth(bool value) { + set(options::dumpSynth, value); +} + +void Options::setInputLanguage(InputLanguage value) { + set(options::inputLanguage, value); +} + +void Options::setInteractive(bool value) { + set(options::interactive, value); +} + +void Options::setOut(std::ostream* value) { + set(options::out, value); +} + +void Options::setOutputLanguage(OutputLanguage value) { + set(options::outputLanguage, value); +} + +void Options::setSharingFilterByLength(int length) { + set(options::sharingFilterByLength, length); +} + +void Options::setThreadId(int value) { + set(options::thread_id, value); +} + +bool Options::wasSetByUserCeGuidedInst() const { + return wasSetByUser(options::ceGuidedInst); +} + +bool Options::wasSetByUserDumpSynth() const { + return wasSetByUser(options::dumpSynth); +} + +bool Options::wasSetByUserEarlyExit() const { + return wasSetByUser(options::earlyExit); +} + +bool Options::wasSetByUserForceLogicString() const { + return wasSetByUser(options::forceLogicString); +} + +bool Options::wasSetByUserIncrementalSolving() const { + return wasSetByUser(options::incrementalSolving); +} + +bool Options::wasSetByUserInteractive() const { + return wasSetByUser(options::interactive); +} + +bool Options::wasSetByUserThreadStackSize() const { + return wasSetByUser(options::threadStackSize); +} + +bool Options::wasSetByUserThreads() const { + return wasSetByUser(options::threads); +} + + +void Options::flushErr() { + if(getErr() != NULL) { + *(getErr()) << std::flush; + } +} + +void Options::flushOut() { + if(getOut() != NULL) { + *(getOut()) << std::flush; + } +} + +}/* CVC4 namespace */ diff --git a/src/options/options_handler_set_option_template.cpp b/src/options/options_set_option_template.cpp index 86821bc0a..04f3800f7 100644 --- a/src/options/options_handler_set_option_template.cpp +++ b/src/options/options_set_option_template.cpp @@ -18,36 +18,35 @@ ** first generate options/summary.sed. **/ + #include <string> #include <sstream> -#include "base/output.h" #include "base/modal_exception.h" +#include "base/output.h" #include "options/option_exception.h" -#include "options/options_handler_interface.h" - +#include "options/options.h" +#include "options/options_handler.h" ${include_all_option_headers} ${option_handler_includes} -#line 31 "${template}" +#line 35 "${template}" using namespace std; namespace CVC4 { -namespace options { -void OptionsHandler::setOption(const std::string& key, const std::string& optionarg) +void Options::setOption(const std::string& key, const std::string& optionarg) throw(OptionException, ModalException) { - options::OptionsHandler* const handler = this; + options::OptionsHandler* handler = d_handler; Trace("options") << "SMT setOption(" << key << ", " << optionarg << ")" << endl; ${smt_setoption_handlers} -#line 44 "${template}" +#line 48 "${template}" throw UnrecognizedOptionException(key); } -}/* options namespace */ }/* CVC4 namespace */ diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 231e5de90..51b2bea5e 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -52,13 +52,14 @@ extern int optreset; #include "base/exception.h" #include "base/output.h" #include "base/tls.h" +#include "options/argument_extender.h" #include "options/didyoumean.h" #include "options/language.h" -#include "options/options_handler_interface.h" +#include "options/options_handler.h" ${include_all_option_headers} -#line 58 "${template}" +#line 63 "${template}" #include "options/options_holder.h" #include "cvc4autoconfig.h" @@ -66,7 +67,7 @@ ${include_all_option_headers} ${option_handler_includes} -#line 67 "${template}" +#line 71 "${template}" using namespace CVC4; using namespace CVC4::options; @@ -75,6 +76,8 @@ 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, @@ -110,7 +113,8 @@ struct OptionHandler<T, true, true> { bool success = stringToInt(i, optionarg); if(!success){ - throw OptionException(option + ": failed to parse "+ optionarg +" as an integer of the appropraite type."); + throw OptionException(option + ": failed to parse "+ optionarg + + " as an integer of the appropraite type."); } // Depending in the platform unsigned numbers with '-' signs may parse. @@ -121,12 +125,14 @@ struct OptionHandler<T, true, true> { } else if(i < std::numeric_limits<T>::min()) { // negative overflow for type std::stringstream ss; - ss << option << " requires an argument >= " << std::numeric_limits<T>::min(); + ss << 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(); + ss << option << " requires an argument <= " + << std::numeric_limits<T>::max(); throw OptionException(ss.str()); } @@ -162,12 +168,14 @@ struct OptionHandler<T, true, false> { } else if(r < -std::numeric_limits<T>::max()) { // negative overflow for type std::stringstream ss; - ss << option << " requires an argument >= " << -std::numeric_limits<T>::max(); + ss << 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(); + ss << option << " requires an argument <= " + << std::numeric_limits<T>::max(); throw OptionException(ss.str()); } @@ -221,9 +229,167 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h // that can throw exceptions. } + +Options::Options() + : d_holder(new options::OptionsHolder()) + , d_handler(new options::OptionsHandler(this)) + , d_forceLogicListeners() + , d_beforeSearchListeners() + , d_tlimitListeners() + , d_tlimitPerListeners() + , d_rlimitListeners() + , d_rlimitPerListeners() +{} + +Options::~Options() { + delete d_handler; + delete d_holder; +} + +void Options::copyValues(const Options& options){ + if(this != &options) { + delete d_holder; + d_holder = new options::OptionsHolder(*options.d_holder); + } +} + +std::string Options::formatThreadOptionException(const std::string& option) { + std::stringstream ss; + ss << "can't understand option `" << option + << "': expected something like --threadN=\"--option1 --option2\"," + << " where N is a nonnegative integer"; + return ss.str(); +} + +ListenerCollection::Registration* Options::registerAndNotify( + ListenerCollection& collection, Listener* listener, bool notify) +{ + ListenerCollection::Registration* registration = + collection.registerListener(listener); + if(notify) { + listener->notify(); + } + return registration; +} + +ListenerCollection::Registration* Options::registerForceLogicListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::forceLogicString); + return registerAndNotify(d_forceLogicListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerBeforeSearchListener( + Listener* listener) +{ + return d_beforeSearchListeners.registerListener(listener); +} + +ListenerCollection::Registration* Options::registerTlimitListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && + wasSetByUser(options::cumulativeMillisecondLimit); + return registerAndNotify(d_tlimitListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerTlimitPerListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::perCallMillisecondLimit); + return registerAndNotify(d_tlimitPerListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerRlimitListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::cumulativeResourceLimit); + return registerAndNotify(d_rlimitListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerRlimitPerListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::perCallResourceLimit); + return registerAndNotify(d_rlimitPerListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerUseTheoryListListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::useTheoryList); + return registerAndNotify(d_useTheoryListListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::defaultExprDepth); + return registerAndNotify(d_setDefaultExprDepthListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerSetDefaultExprDagListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::defaultDagThresh); + return registerAndNotify(d_setDefaultDagThreshListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerSetPrintExprTypesListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::printExprTypes); + return registerAndNotify(d_setPrintExprTypesListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerSetDumpModeListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::dumpModeString); + return registerAndNotify(d_setDumpModeListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerSetPrintSuccessListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::printSuccess); + return registerAndNotify(d_setPrintSuccessListeners, listener, notify); +} + +ListenerCollection::Registration* Options::registerDumpToFileNameListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::dumpToFileName); + return registerAndNotify(d_dumpToFileListeners, listener, notify); +} + +ListenerCollection::Registration* +Options::registerSetRegularOutputChannelListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::regularChannelName); + return registerAndNotify(d_setRegularChannelListeners, listener, notify); +} + +ListenerCollection::Registration* +Options::registerSetDiagnosticOutputChannelListener( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::diagnosticChannelName); + return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify); +} + +ListenerCollection::Registration* +Options::registerSetReplayLogFilename( + Listener* listener, bool notifyIfSet) +{ + bool notify = notifyIfSet && wasSetByUser(options::replayLogFilename); + return registerAndNotify(d_setReplayFilenameListeners, listener, notify); +} + ${all_custom_handlers} -#line 204 "${template}" +#line 393 "${template}" #ifdef CVC4_DEBUG # define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true @@ -237,42 +403,22 @@ ${all_custom_handlers} # 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& Options::operator=(const Options& options) { - if(this != &options) { - delete d_holder; - d_holder = new options::OptionsHolder(*options.d_holder); - } - return *this; -} - options::OptionsHolder::OptionsHolder() : ${all_modules_defaults} { } -#line 242 "${template}" +#line 411 "${template}" static const std::string mostCommonOptionsDescription = "\ Most commonly-used CVC4 options:${common_documentation}"; -#line 247 "${template}" +#line 416 "${template}" static const std::string optionsDescription = mostCommonOptionsDescription + "\n\ \n\ Additional CVC4 options:${remaining_documentation}"; -#line 253 "${template}" +#line 422 "${template}" static const std::string optionsFootnote = "\n\ [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ @@ -315,7 +461,8 @@ void Options::printUsage(const std::string msg, std::ostream& out) { void Options::printShortUsage(const std::string msg, std::ostream& out) { out << msg << mostCommonOptionsDescription << std::endl << optionsFootnote << std::endl - << "For full usage, please use --help." << std::endl << std::endl << std::flush; + << "For full usage, please use --help." + << std::endl << std::endl << std::flush; } void Options::printLanguageHelp(std::ostream& out) { @@ -350,34 +497,33 @@ static struct option cmdlineOptions[] = {${all_modules_long_options} { NULL, no_argument, NULL, '\0' } };/* cmdlineOptions */ -#line 330 "${template}" +#line 501 "${template}" -static void preemptGetopt(int& argc, char**& argv, const char* opt) { - const size_t maxoptlen = 128; +// static void preemptGetopt(int& argc, char**& argv, const char* opt) { - Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl; +// Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl; - AlwaysAssert(opt != NULL && *opt != '\0'); - AlwaysAssert(strlen(opt) <= maxoptlen); +// AlwaysAssert(opt != NULL && *opt != '\0'); +// AlwaysAssert(strlen(opt) <= maxoptlen); - ++argc; - unsigned i = 1; - while(argv[i] != NULL && argv[i][0] != '\0') { - ++i; - } +// ++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; - } +// 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 -} +// strncpy(argv[i], opt, maxoptlen - 1); +// argv[i][maxoptlen - 1] = '\0'; // ensure NUL-termination even on overflow +// } namespace options { @@ -403,11 +549,17 @@ public: * The return value is what's left of the command line (that is, the * non-option arguments). */ -std::vector<std::string> Options::parseOptions(int argc, char* main_argv[], options::OptionsHandler* const handler) throw(OptionException) { +std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { options::OptionsGuard guard(&s_current, this); + // Having this synonym simplifies the generation code in mkoptions. + options::OptionsHandler* handler = d_handler; + const char *progName = main_argv[0]; + ArgumentExtender argumentExtender(s_preemptAdditional, s_maxoptlen); + std::vector<char*> allocated; + Debug("options") << "main_argv == " << main_argv << std::endl; // Reset getopt(), in the case of multiple calls to parseOptions(). @@ -441,7 +593,8 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[], opti int c = -1; optopt = 0; std::string option, optionarg; - Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind << ", extra_argc == " << extra_argc << std::endl; + 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 if(optind_ref != &extra_optind) { @@ -451,14 +604,20 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[], opti old_optind = optind = extra_optind; optind_ref = &extra_optind; argv = extra_argv; - Debug("preemptGetopt") << "in preempt code, next arg is " << extra_argv[optind == 0 ? 1 : optind] << std::endl; + Debug("preemptGetopt") << "in preempt code, next arg is " + << extra_argv[optind == 0 ? 1 : optind] + << std::endl; if(extra_argv[extra_optind == 0 ? 1 : extra_optind][0] != '-') { - InternalError("preempted args cannot give non-options command-line args (found `%s')", extra_argv[extra_optind == 0 ? 1 : extra_optind]); + InternalError( + "preempted args cannot give non-options command-line args (found `%s')", + extra_argv[extra_optind == 0 ? 1 : extra_optind]); } 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; + Debug("preemptGetopt") << "in preempt code" + << ", c == " << c << " (`" << char(c) << "')" + << " optind == " << optind << std::endl; if(optopt == 0 || ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) { // long option @@ -522,13 +681,16 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[], opti Debug("options") << "I restored optind to " << optind << std::endl;*/ } #endif /* __MINGW32__ || __MINGW64__ */ - Debug("options") << "[ argc == " << argc << ", main_argv == " << main_argv << " ]" << std::endl; + Debug("options") << "[ argc == " << argc + << ", main_argv == " << main_argv << " ]" << std::endl; c = getopt_long(argc, main_argv, "+:${all_modules_short_options}", cmdlineOptions, NULL); main_optind = optind; - Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" << std::endl; - Debug("options") << "[ next option will be at pos: " << optind << " ]" << std::endl; + Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" + << std::endl; + Debug("options") << "[ next option will be at pos: " << optind << " ]" + << std::endl; if(c == -1) { Debug("options") << "done with option parsing" << std::endl; break; @@ -537,12 +699,13 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[], opti optionarg = (optarg == NULL) ? "" : optarg; } - Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "'), " << option << std::endl; + Debug("preemptGetopt") << "processing option " << c + << " (`" << char(c) << "'), " << option << std::endl; switch(c) { ${all_modules_option_handlers} -#line 523 "${template}" +#line 709 "${template}" case ':': // This can be a long or short option, and the way to get at the @@ -555,13 +718,13 @@ ${all_modules_option_handlers} !strncmp(argv[optind - 1], "--thread", 8) && strlen(argv[optind - 1]) > 8 ) { if(! isdigit(argv[optind - 1][8])) { - throw OptionException(std::string("can't understand option `") + option + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer"); + throw OptionException(formatThreadOptionException(option)); } std::vector<std::string>& threadArgv = d_holder->threadArgv; char *end; long tnum = strtol(argv[optind - 1] + 8, &end, 10); if(tnum < 0 || (*end != '\0' && *end != '=')) { - throw OptionException(std::string("can't understand option `") + option + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer"); + throw OptionException(formatThreadOptionException(option)); } if(threadArgv.size() <= size_t(tnum)) { threadArgv.resize(tnum + 1); @@ -571,29 +734,42 @@ ${all_modules_option_handlers} } if(*end == '\0') { // e.g., we have --thread0 "foo" if(argc <= optind) { - throw OptionException(std::string("option `") + option + "' missing its required argument"); + throw OptionException(std::string("option `") + option + + "' missing its required argument"); } - Debug("options") << "thread " << tnum << " gets option " << argv[optind] << std::endl; + Debug("options") << "thread " << tnum << " gets option " + << argv[optind] << std::endl; threadArgv[tnum] += argv[(*optind_ref)++]; } else { // e.g., we have --thread0="foo" if(end[1] == '\0') { - throw OptionException(std::string("option `") + option + "' missing its required argument"); + throw OptionException(std::string("option `") + option + + "' missing its required argument"); } - Debug("options") << "thread " << tnum << " gets option " << (end + 1) << std::endl; + Debug("options") << "thread " << tnum << " gets option " << (end + 1) + << std::endl; threadArgv[tnum] += end + 1; } - Debug("options") << "thread " << tnum << " now has " << threadArgv[tnum] << std::endl; + Debug("options") << "thread " << tnum << " now has " << threadArgv[tnum] + << std::endl; break; } - throw OptionException(std::string("can't understand option `") + option + "'" - + suggestCommandLineOptions(option)); + throw OptionException(std::string("can't understand option `") + option + + "'" + suggestCommandLineOptions(option)); } } Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl; free(extra_argv); + for(std::vector<char*>::iterator i = allocated.begin(), iend = allocated.end(); + i != iend; ++i) + { + char* current = *i; + #warning "TODO: Unit tests fail if garbage collection is done here." + //free(current); + } + allocated.clear(); return nonOptions; } @@ -611,7 +787,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th static const char* smtOptions[] = { ${all_modules_smt_options}, -#line 592 "${template}" +#line 790 "${template}" NULL };/* smtOptions[] */ @@ -633,11 +809,12 @@ std::vector< std::vector<std::string> > Options::getOptions() const throw() { ${all_modules_get_options} -#line 614 "${template}" +#line 813 "${template}" return opts; } + #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT #undef DO_SEMANTIC_CHECKS_BY_DEFAULT diff --git a/src/options/parser_options b/src/options/parser_options index e91c735fe..d1e9aa142 100644 --- a/src/options/parser_options +++ b/src/options/parser_options @@ -11,24 +11,25 @@ common-option strictParsing --strict-parsing bool option memoryMap --mmap bool memory map file input -option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking +option semanticChecks semantic-checks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking disable ALL semantic checks, including type checks option globalDeclarations global-declarations bool :default false force all declarations and definitions to be global -# this is to support security in the online version, and in other similar contexts -# (--no-include-file disables filesystem access in TPTP and SMT2 parsers) -# the name --no-include-file is legacy: it also now limits any filesystem access -# (read or write) for example by using --dump-to (or the equivalent set-option) or -# set-option :regular-output-channel/:diagnostic-output-channel. However, the main -# driver is still permitted to read the input file given on the command-line if any. -# creation/use of temp files are still permitted (but the paths aren't given by the -# user). Also note this is only safe for the version invoked through the main driver, -# there are ways via the API to get the CVC4 library to open a file for reading or -# writing and thus leak information from an existing file, or overwrite an existing -# file with malicious content. -undocumented-option filesystemAccess /--no-filesystem-access bool :default true +# this is to support security in the online version, and in other similar +# contexts (--no-include-file disables filesystem access in TPTP and SMT2 +# parsers) the name --no-include-file is legacy: it also now limits any +# filesystem access (read or write) for example by using --dump-to (or the +# equivalent set-option) or set-option +# :regular-output-channel/:diagnostic-output-channel. However, the main driver +# is still permitted to read the input file given on the command-line if any. +# creation/use of temp files are still permitted (but the paths aren't given by +# the user). Also note this is only safe for the version invoked through the +# main driver, there are ways via the API to get the CVC4 library to open a file +# for reading or writing and thus leak information from an existing file, or +# overwrite an existing file with malicious content. +undocumented-option filesystemAccess filesystem-access /--no-filesystem-access bool :default true undocumented-alias --no-include-file = --no-filesystem-access endmodule diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h index f18799aaa..8ccceb13f 100644 --- a/src/options/printer_modes.h +++ b/src/options/printer_modes.h @@ -25,20 +25,20 @@ namespace CVC4 { /** Enumeration of model_format modes (how to print models from get-model command). */ -typedef enum { +enum CVC4_PUBLIC ModelFormatMode { /** default mode (print expressions in the output language format) */ MODEL_FORMAT_MODE_DEFAULT, /** print functional values in a table format */ MODEL_FORMAT_MODE_TABLE, -} ModelFormatMode; +}; /** Enumeration of inst_format modes (how to print models from get-model command). */ -typedef enum { +enum CVC4_PUBLIC InstFormatMode { /** default mode (print expressions in the output language format) */ INST_FORMAT_MODE_DEFAULT, /** print as SZS proof */ INST_FORMAT_MODE_SZS, -} InstFormatMode; +}; std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, InstFormatMode mode) CVC4_PUBLIC; diff --git a/src/options/printer_options b/src/options/printer_options index 7491570c6..c276c0dd5 100644 --- a/src/options/printer_options +++ b/src/options/printer_options @@ -5,10 +5,10 @@ module PRINTER "options/printer_options.h" Printing -option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::options::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "options/printer_modes.h" :handler-include "options/options_handler_interface.h" +option modelFormatMode --model-format=MODE ModelFormatMode :handler stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "options/printer_modes.h" print format mode for models, see --model-format=help -option instFormatMode --inst-format=MODE InstFormatMode :handler CVC4::options::stringToInstFormatMode :default INST_FORMAT_MODE_DEFAULT :read-write :include "options/printer_modes.h" :handler-include "options/options_handler_interface.h" +option instFormatMode --inst-format=MODE InstFormatMode :handler stringToInstFormatMode :default INST_FORMAT_MODE_DEFAULT :read-write :include "options/printer_modes.h" print format mode for instantiations, see --inst-format=help endmodule diff --git a/src/options/prop_options b/src/options/prop_options index 3c3198147..87112197c 100644 --- a/src/options/prop_options +++ b/src/options/prop_options @@ -5,18 +5,18 @@ module PROP "options/prop_options.h" SAT layer -option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate options::greater_equal(0.0) options::less_equal(1.0) +option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate doubleGreaterOrEqual0 doubleLessOrEqual1 sets the frequency of random decisions in the sat solver (P=0.0 by default) option satRandomSeed random-seed --random-seed=S uint32_t :default 0 :read-write sets the random seed for the sat solver -option satVarDecay double :default 0.95 :predicate options::less_equal(1.0) options::greater_equal(0.0) +option satVarDecay double :default 0.95 :predicate doubleGreaterOrEqual0 doubleLessOrEqual1 variable activity decay factor for Minisat -option satClauseDecay double :default 0.999 :predicate options::less_equal(1.0) options::greater_equal(0.0) +option satClauseDecay double :default 0.999 :predicate doubleGreaterOrEqual0 doubleLessOrEqual1 clause activity decay factor for Minisat option satRestartFirst --restart-int-base=N unsigned :default 25 sets the base restart interval for the sat solver (N=25 by default) -option satRestartInc --restart-int-inc=F double :default 3.0 :predicate options::greater_equal(0.0) +option satRestartInc --restart-int-inc=F double :default 3.0 :predicate doubleGreaterOrEqual0 sets the restart interval increase factor for the sat solver (F=3.0 by default) option sat_refine_conflicts --refine-conflicts bool :default false diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 5bc20f9a8..f5a6ee843 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -19,7 +19,7 @@ option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write miniscope quantifiers for ground subformulas option quantSplit --quant-split bool :default true apply splitting to quantified formulas based on variable disjoint disjuncts -option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "options/quantifiers_modes.h" :read-write :handler CVC4::options::stringToPrenexQuantMode :handler-include "options/options_handler_interface.h" +option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode prenex mode for quantified formulas # Whether to variable-eliminate quantifiers. # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to @@ -29,7 +29,7 @@ option varElimQuant --var-elim-quant bool :default true option dtVarExpandQuant --dt-var-exp-quant bool :default true expand datatype variables bound to one constructor in quantifiers #ite lift mode for quantified formulas -option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "options/quantifiers_modes.h" :read-write :handler CVC4::options::stringToIteLiftQuantMode :handler-include "options/options_handler_interface.h" +option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "options/quantifiers_modes.h" :read-write :handler stringToIteLiftQuantMode ite lifting mode for quantified formulas option condVarSplitQuant --cond-var-split-quant bool :default true split quantified formulas that lead to variable eliminations @@ -63,7 +63,7 @@ option purifyQuant --purify-quant bool :default false option eMatching --e-matching bool :read-write :default true whether to do heuristic E-matching -option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "options/quantifiers_modes.h" :handler CVC4::options::stringToTermDbMode :handler-include "options/options_handler_interface.h" +option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "options/quantifiers_modes.h" :handler stringToTermDbMode which ground terms to consider for instantiation option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching @@ -86,14 +86,14 @@ option multiTriggerWhenSingle --multi-trigger-when-single bool :default false select multi triggers when single triggers exist option multiTriggerPriority --multi-trigger-priority bool :default false only try multi triggers if single triggers give no instantiations -option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "options/quantifiers_modes.h" :handler CVC4::options::stringToTriggerSelMode :handler-include "options/options_handler_interface.h" +option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerSelMode selection mode for triggers -option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "options/quantifiers_modes.h" :handler CVC4::options::stringToUserPatMode :handler-include "options/options_handler_interface.h" +option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "options/quantifiers_modes.h" :handler stringToUserPatMode policy for handling user-provided patterns for quantifier instantiation option incrementTriggers --increment-triggers bool :default true generate additional triggers as needed during search -option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "options/quantifiers_modes.h" :handler CVC4::options::stringToInstWhenMode :handler-include "options/options_handler_interface.h" :predicate CVC4::options::checkInstWhenMode :predicate-include "options/options_handler_interface.h" +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "options/quantifiers_modes.h" :handler stringToInstWhenMode :predicate checkInstWhenMode when to apply instantiation option instMaxLevel --inst-max-level=N int :read-write :default -1 @@ -113,7 +113,7 @@ option fullSaturateQuantRd --full-saturate-quant-rd bool :default true option fullSaturateInst --fs-inst bool :default false interleave full saturate instantiation with other techniques -option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "options/quantifiers_modes.h" :handler CVC4::options::stringToLiteralMatchMode :handler-include "options/options_handler_interface.h" :predicate CVC4::options::checkLiteralMatchMode :predicate-include "options/options_handler_interface.h" +option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode choose literal matching mode ### finite model finding options @@ -130,7 +130,7 @@ option fmfFunWellDefinedRelevant --fmf-fun-rlv bool :default false option fmfEmptySorts --fmf-empty-sorts bool :default false allow finite model finding to assume sorts that do not occur in ground assertions are empty -option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "options/quantifiers_modes.h" :handler CVC4::options::stringToMbqiMode :handler-include "options/options_handler_interface.h" :predicate CVC4::options::checkMbqiMode :predicate-include "options/options_handler_interface.h" +option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "options/quantifiers_modes.h" :handler stringToMbqiMode :predicate checkMbqiMode choose mode for model-based quantifier instantiation option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false only add one instantiation per quantifier per round for mbqi @@ -156,9 +156,9 @@ option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write option quantConflictFind --quant-cf bool :read-write :default true enable conflict find mechanism for quantifiers -option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "options/quantifiers_modes.h" :handler CVC4::options::stringToQcfMode :handler-include "options/options_handler_interface.h" +option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "options/quantifiers_modes.h" :handler stringToQcfMode what effort to apply conflict find mechanism -option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler CVC4::options::stringToQcfWhenMode :handler-include "options/options_handler_interface.h" +option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler stringToQcfWhenMode when to invoke conflict find mechanism for quantifiers option qcfTConstraint --qcf-tconstraint bool :read-write :default false enable entailment checks for t-constraints in qcf algorithm @@ -205,7 +205,7 @@ option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false option ceGuidedInst --cegqi bool :default false :read-write counterexample-guided quantifier instantiation -option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "options/quantifiers_modes.h" :handler CVC4::options::stringToCegqiFairMode :handler-include "options/options_handler_interface.h" +option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "options/quantifiers_modes.h" :handler stringToCegqiFairMode if and how to apply fairness for cegqi option cegqiSingleInv --cegqi-si bool :default false :read-write process single invocation synthesis conjectures @@ -233,7 +233,7 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true generalize based on content in global search space narrowing -option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler CVC4::options::stringToSygusInvTemplMode :handler-include "options/options_handler_interface.h" +option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode template mode for sygus invariant synthesis # approach applied to general quantified formulas @@ -281,7 +281,7 @@ option quantAlphaEquiv --quant-alpha-equiv bool :default true infer alpha equivalence between quantified formulas option macrosQuant --macros-quant bool :read-write :default false perform quantifiers macro expansion -option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "options/quantifiers_modes.h" :handler CVC4::options::stringToMacrosQuantMode :handler-include "options/options_handler_interface.h" +option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "options/quantifiers_modes.h" :handler stringToMacrosQuantMode mode for quantifiers macro expansion ### recursive function options diff --git a/src/options/smt_options b/src/options/smt_options index b99a8a83b..bc2586fe0 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -5,15 +5,15 @@ module SMT "options/smt_options.h" SMT layer -common-option - dump --dump=MODE argument :handler CVC4::options::dumpMode :handler-include "options/options_handler_interface.h" +common-option dumpModeString dump --dump=MODE std::string :default "" :notify notifyDumpMode dump preprocessed assertions, etc., see --dump=help -common-option - dump-to --dump-to=FILE argument :handler CVC4::options::dumpToFile :handler-include "options/options_handler_interface.h" +common-option dumpToFileName dump-to --dump-to=FILE std::string :notify notifyDumpToFile all dumping goes to FILE (instead of stdout) -expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo* :include "options/logic_info_forward.h" :handler CVC4::options::stringToLogicInfo :handler-include "options/options_handler_interface.h" :default NULL +expert-option forceLogicString force-logic --force-logic=LOGIC std::string :default "" :notify notifyForceLogic set the logic, and override all further user attempts to change it -option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::options::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "options/simplification_mode.h" :handler-include "options/options_handler_interface.h" +option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "options/simplification_mode.h" choose simplification mode, see --simplification=help alias --no-simplification = --simplification=none turn off all simplification (same as --simplification=none) @@ -23,35 +23,35 @@ option doStaticLearning static-learning --static-learning bool :default true option expandDefinitions expand-definitions bool :default false always expand symbol definitions in output -common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" +common-option produceModels produce-models -m --produce-models bool :default false :notify notifyBeforeSearch support the get-value and get-model commands -option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" +option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :notify notifyBeforeSearch after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions -option dumpModels --dump-models bool :default false :link --produce-models +option dumpModels --dump-models bool :default false :link --produce-models :link-smt produce-models output models after every SAT/INVALID/UNKNOWN response -option proof produce-proofs --proof bool :default false :predicate CVC4::options::proofEnabledBuild CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" +option proof produce-proofs --proof bool :default false :predicate proofEnabledBuild :notify notifyBeforeSearch turn on proof generation -option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" :read-write +option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :notify notifyBeforeSearch :read-write after UNSAT/VALID, machine-check the generated proof -option dumpProofs --dump-proofs bool :default false :link --proof +option dumpProofs --dump-proofs bool :default false :link --proof :link-smt produce-proofs output proofs after every UNSAT/VALID response option dumpInstantiations --dump-instantiations bool :default false output instantiations of quantified formulas after every UNSAT/VALID response option dumpSynth --dump-synth bool :read-write :default false output solution for synthesis conjectures after every UNSAT/VALID response -option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::options::proofEnabledBuild CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" +option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch turn on unsat core generation option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produce-unsat-cores :link-smt produce-unsat-cores :read-write after UNSAT/VALID, produce and check an unsat core (expensive) -option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" +option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :notify notifyBeforeSearch output unsat cores after every UNSAT/VALID response -option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" +option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch support the get-assignment command -undocumented-option interactiveMode interactive-mode bool :predicate CVC4::options::beforeSearch CVC4::options::setProduceAssertions :predicate-include "options/options_handler_interface.h" :read-write +undocumented-option interactiveMode interactive-mode bool :predicate setProduceAssertions :read-write :notify notifyBeforeSearch deprecated name for produce-assertions -common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::options::beforeSearch CVC4::options::setProduceAssertions :predicate-include "options/options_handler_interface.h" :read-write +common-option produceAssertions produce-assertions --produce-assertions bool :predicate setProduceAssertions :read-write :notify notifyBeforeSearch keep an assertions list (enables get-assertions command) option doITESimp --ite-simp bool :read-write @@ -86,18 +86,18 @@ option abstractValues abstract-values --abstract-values bool :default false option modelUninterpDtEnum --model-u-dt-enum bool :default false in models, output uninterpreted sorts as datatype enumerations -option - regular-output-channel argument :handler CVC4::options::setRegularOutputChannel :handler-include "options/options_handler_interface.h" +option regularChannelName regular-output-channel std::string :notify notifySetRegularOutputChannel set the regular output channel of the solver -option - diagnostic-output-channel argument :handler CVC4::options::setDiagnosticOutputChannel :handler-include "options/options_handler_interface.h" +option diagnosticChannelName diagnostic-output-channel std::string :notify notifySetDiagnosticOutputChannel set the diagnostic output channel of the solver -common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler CVC4::options::tlimitHandler :handler-include "options/options_handler_interface.h" +common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler tlimitHandler :notify notifyTlimit enable time limiting (give milliseconds) -common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" :handler CVC4::options::tlimitPerHandler :handler-include "options/options_handler_interface.h" +common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" :handler tlimitPerHandler :notify notifyTlimitPer enable time limiting per query (give milliseconds) -common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler CVC4::options::rlimitHandler :handler-include "options/options_handler_interface.h" +common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler rlimitHandler :notify notifyRlimit enable resource limiting (currently, roughly the number of SAT conflicts) -common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler CVC4::options::rlimitPerHandler :handler-include "options/options_handler_interface.h" +common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler rlimitPerHandler :notify notifyRlimitPer enable resource limiting per query common-option hardLimit hard-limit --hard-limit bool :default false the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out) @@ -145,14 +145,19 @@ expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsi expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 + # --replay is currently broken; don't document it for 1.0 -undocumented-option replayFilename --replay=FILE std::string :handler CVC4::options::checkReplayFilename :handler-include "options/options_handler_interface.h" +undocumented-option replayInputFilename --replay=FILE std::string :handler checkReplayFilename replay decisions from file +# --replay is currently broken; don't document it for 1.0 +undocumented-option replayLogFilename --replay-log=FILE std::string :handler checkReplayFilename :notify notifySetReplayLogFilename :notify notifyBeforeSearch + replay decisions from file option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false Force no CPU limit when dumping models and proofs -option solveIntAsBV --solve-int-as-bv uint32_t :default 0 +undocumented-option solveIntAsBV --solve-int-as-bv uint32_t :default 0 + attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental) endmodule diff --git a/src/options/strings_options b/src/options/strings_options index 6247ad3a1..65c293dbc 100644 --- a/src/options/strings_options +++ b/src/options/strings_options @@ -9,11 +9,11 @@ option stringExp strings-exp --strings-exp bool :default false :read-write experimental features in the theory of strings # :predicate-include "smt/smt_engine.h" -option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate options::less_equal(2) :predicate-include "options/base_handlers.h" +option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate unsignedLessEqual2 the strategy of LB rule application: 0-lazy, 1-eager, 2-no # :predicate-include "smt/smt_engine.h" -option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate options::less_equal(2) :predicate-include "options/base_handlers.h" +option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate unsignedLessEqual2 the alphabet contains only characters from the standard ASCII or the extended one option stringFMF strings-fmf --strings-fmf bool :default false :read-write diff --git a/src/options/theory_options b/src/options/theory_options index f6d6d0f84..131b5fb80 100644 --- a/src/options/theory_options +++ b/src/options/theory_options @@ -5,11 +5,10 @@ module THEORY "options/theory_options.h" Theory layer -expert-option theoryOfMode theoryof-mode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::options::stringToTheoryOfMode :handler-include "options/options_handler_interface.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "options/theoryof_mode.h" :read-write +expert-option theoryOfMode theoryof-mode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler stringToTheoryOfMode :default CVC4::theory::THEORY_OF_TYPE_BASED :include "options/theoryof_mode.h" :read-write mode for Theory::theoryof() -option - use-theory --use-theory=NAME argument :handler CVC4::options::useTheory :handler-include "options/options_handler_interface.h" - use alternate theory implementation NAME (--use-theory=help for a list) -option theoryAlternates ::std::map<std::string,bool> :include <map> :read-write +option useTheoryList use-theory --use-theory=NAME std::string :handler handleUseTheoryList :notify notifyUseTheoryList + use alternate theory implementation NAME (--use-theory=help for a list). This option may be repeated or a comma separated list. endmodule diff --git a/src/options/uf_options b/src/options/uf_options index e7df9a2db..cbac04b18 100644 --- a/src/options/uf_options +++ b/src/options/uf_options @@ -11,7 +11,7 @@ option ufSymmetryBreaker uf-symmetry-breaker --symmetry-breaker bool :read-write option condenseFunctionValues condense-function-values --condense-function-values bool :default true condense models for functions rather than explicitly representing them -option ufssRegions /--disable-uf-ss-regions bool :default true +option ufssRegions --uf-ss-regions bool :default true disable region-based method for discovering cliques and splits in uf strong solver option ufssEagerSplits --uf-ss-eager-split bool :default false add splits eagerly for uf strong solver @@ -29,7 +29,7 @@ option ufssSimpleCliques --uf-ss-simple-cliques bool :default true always use simple clique lemmas for uf strong solver option ufssDiseqPropagation --uf-ss-deq-prop bool :default false eagerly propagate disequalities for uf strong solver -option ufssMode --uf-ss=MODE CVC4::theory::uf::UfssMode :default CVC4::theory::uf::UF_SS_FULL :include "options/options_handler_interface.h" :handler CVC4::options::stringToUfssMode :handler-include "options/options_handler_interface.h" +option ufssMode --uf-ss=MODE CVC4::theory::uf::UfssMode :default CVC4::theory::uf::UF_SS_FULL :include "options/ufss_mode.h" :handler stringToUfssMode mode of operation for uf strong solver. option ufssCliqueSplits --uf-ss-clique-splits bool :default false use cliques instead of splitting on demand to shrink model diff --git a/src/options/ufss_mode.h b/src/options/ufss_mode.h index 25eb1d2d7..6ce05d46a 100644 --- a/src/options/ufss_mode.h +++ b/src/options/ufss_mode.h @@ -22,7 +22,7 @@ namespace CVC4 { namespace theory { namespace uf { - + enum UfssMode{ /** default, use uf strong solver to find minimal models for uninterpreted sorts */ UF_SS_FULL, @@ -37,4 +37,3 @@ enum UfssMode{ }/* CVC4 namespace */ #endif /* __CVC4__BASE__UFSS_MODE_H */ - |