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/options_handler.cpp | |
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/options_handler.cpp')
-rw-r--r-- | src/options/options_handler.cpp | 1380 |
1 files changed, 1380 insertions, 0 deletions
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 */ |