diff options
Diffstat (limited to 'src/options/options_handler_interface.cpp')
-rw-r--r-- | src/options/options_handler_interface.cpp | 362 |
1 files changed, 362 insertions, 0 deletions
diff --git a/src/options/options_handler_interface.cpp b/src/options/options_handler_interface.cpp new file mode 100644 index 000000000..d803fced0 --- /dev/null +++ b/src/options/options_handler_interface.cpp @@ -0,0 +1,362 @@ +/********************* */ +/*! \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) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToArithUnateLemmaMode(option, optarg); +} +ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToArithPropagationMode(option, optarg); +} +ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->abcEnabledBuild(option, value); +} +void abcEnabledBuild(std::string option, std::string value, OptionsHandler* handler) throw(OptionException) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToBvSlicerMode(option, optarg); +} +void setBitblastAig(std::string option, bool arg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToTheoryOfMode(option, optarg); +} +void useTheory(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(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) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToModelFormatMode(option, optarg); +} + +InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setVerbosity(option, value); +} +void increaseVerbosity(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->increaseVerbosity(option); +} +void decreaseVerbosity(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->decreaseVerbosity(option); +} + +OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToOutputLanguage(option, optarg); +} + +InputLanguage stringToInputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToInputLanguage(option, optarg); +} + +void addTraceTag(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->addTraceTag(option, optarg); +} + +void addDebugTag(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->addDebugTag(option, optarg); +} + +void setPrintSuccess(std::string option, bool value, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setPrintSuccess(option, value); +} + + +/* main/options_handlers.h */ +void showConfiguration(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->showConfiguration(option); +} + +void showDebugTags(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->showDebugTags(option); +} + +void showTraceTags(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->showTraceTags(option); +} + +void threadN(std::string option, OptionsHandler* handler){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->threadN(option); +} + +/* expr/options_handlers.h */ +void setDefaultExprDepth(std::string option, int depth, OptionsHandler* handler){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setDefaultExprDepth(option, depth); +} + +void setDefaultDagThresh(std::string option, int dag, OptionsHandler* handler){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setDefaultDagThresh(option, dag); +} + +void setPrintExprTypes(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setPrintExprTypes(option); +} + + +/* smt/options_handlers.h */ +void dumpMode(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->dumpMode(option, optarg); +} + +LogicInfo* stringToLogicInfo(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToLogicInfo(option, optarg); +} + +SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){ + CheckArgument(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){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->beforeSearch(option, value); +} + +void setProduceAssertions(std::string option, bool value, OptionsHandler* handler) throw() { + CheckArgument(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) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->proofEnabledBuild(option, value); +} + +void dumpToFile(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->dumpToFile(option, optarg); +} + +void setRegularOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setRegularOutputChannel(option, optarg); +} + +void setDiagnosticOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setDiagnosticOutputChannel(option, optarg); +} + +std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->checkReplayFilename(option, optarg); +} + +std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->checkReplayLogFilename(option, optarg); +} + +// ensure we are a stats-enabled build of CVC4 +void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(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) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->rlimitPerHandler(option, optarg); +} + + + +OptionsHandler::OptionsHandler() { } + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ |