diff options
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/base_options | 6 | ||||
-rw-r--r-- | src/options/boolean_term_conversion_mode.cpp | 1 | ||||
-rw-r--r-- | src/options/boolean_term_conversion_mode.h | 2 | ||||
-rw-r--r-- | src/options/bv_bitblast_mode.cpp | 2 | ||||
-rw-r--r-- | src/options/bv_bitblast_mode.h | 2 | ||||
-rw-r--r-- | src/options/options_handler_interface.cpp | 126 | ||||
-rw-r--r-- | src/options/simplification_mode.cpp | 2 | ||||
-rw-r--r-- | src/options/simplification_mode.h | 2 |
8 files changed, 73 insertions, 70 deletions
diff --git a/src/options/base_options b/src/options/base_options index 588220817..edbef801d 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -81,9 +81,9 @@ module BASE "options/base_options.h" Base option binary_name std::string -option in std::istream* :default &std::cin :include <iostream> -option out std::ostream* :default &std::cout :include <iostream> -option err std::ostream* :default &std::cerr :include <iostream> +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 force input language (default is "auto"; see --lang help) diff --git a/src/options/boolean_term_conversion_mode.cpp b/src/options/boolean_term_conversion_mode.cpp index efeb3ab16..d1466ae14 100644 --- a/src/options/boolean_term_conversion_mode.cpp +++ b/src/options/boolean_term_conversion_mode.cpp @@ -18,7 +18,6 @@ #include <iostream> - namespace CVC4 { std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) { diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h index 5671dea13..65cc7a8a5 100644 --- a/src/options/boolean_term_conversion_mode.h +++ b/src/options/boolean_term_conversion_mode.h @@ -20,7 +20,7 @@ #ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H #define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H -#include <iostream> +#include <iosfwd> namespace CVC4 { namespace theory { diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp index 9576134f6..99ceb41ee 100644 --- a/src/options/bv_bitblast_mode.cpp +++ b/src/options/bv_bitblast_mode.cpp @@ -16,6 +16,8 @@ #include "options/bv_bitblast_mode.h" +#include <iostream> + namespace CVC4 { std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) { diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h index 89ecdc381..08a6e4077 100644 --- a/src/options/bv_bitblast_mode.h +++ b/src/options/bv_bitblast_mode.h @@ -19,7 +19,7 @@ #ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H #define __CVC4__THEORY__BV__BITBLAST_MODE_H -#include <iostream> +#include <iosfwd> namespace CVC4 { namespace theory { diff --git a/src/options/options_handler_interface.cpp b/src/options/options_handler_interface.cpp index d803fced0..bce3643aa 100644 --- a/src/options/options_handler_interface.cpp +++ b/src/options/options_handler_interface.cpp @@ -44,313 +44,313 @@ static const char* s_third_argument_warning = // 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); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(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); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(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); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(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); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(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); + 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){ - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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){ - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(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); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + PrettyCheckArgument(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); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + 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) { - CheckArgument(handler != NULL, handler, s_third_argument_warning); + PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); return handler->rlimitPerHandler(option, optarg); } diff --git a/src/options/simplification_mode.cpp b/src/options/simplification_mode.cpp index 08f961c15..ab7851ef9 100644 --- a/src/options/simplification_mode.cpp +++ b/src/options/simplification_mode.cpp @@ -17,6 +17,8 @@ #include "options/simplification_mode.h" +#include <iostream> + namespace CVC4 { std::ostream& operator<<(std::ostream& out, SimplificationMode mode) { diff --git a/src/options/simplification_mode.h b/src/options/simplification_mode.h index b0b78d318..dd02ada5c 100644 --- a/src/options/simplification_mode.h +++ b/src/options/simplification_mode.h @@ -20,7 +20,7 @@ #ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H #define __CVC4__SMT__SIMPLIFICATION_MODE_H -#include <iostream> +#include <iosfwd> namespace CVC4 { |