diff options
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r-- | src/options/options_handler.cpp | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 1d7355d9f..0dac42362 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -515,6 +515,24 @@ depth \n\ \n\ "; +const std::string OptionsHandler::s_fmfBoundMinModeModeHelp = "\ +Modes for finite model finding bound minimization, supported by --fmf-bound-min-mode:\n\ +\n\ +none \n\ ++ Do not minimize inferred bounds.\n\ +\n\ +int (default) \n\ ++ Minimize integer ranges only.\n\ +\n\ +setc \n\ ++ Minimize cardinality of set membership ranges only.\n\ +\n\ +all \n\ ++ Minimize all inferred bounds.\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; @@ -831,6 +849,25 @@ theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(std::stri } } + +theory::quantifiers::FmfBoundMinMode OptionsHandler::stringToFmfBoundMinMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none" ) { + return theory::quantifiers::FMF_BOUND_MIN_NONE; + } else if(optarg == "int" || optarg == "default") { + return theory::quantifiers::FMF_BOUND_MIN_INT_RANGE; + } else if(optarg == "setc" || optarg == "default") { + return theory::quantifiers::FMF_BOUND_MIN_SET_CARD; + } else if(optarg == "all") { + return theory::quantifiers::FMF_BOUND_MIN_ALL; + } else if(optarg == "help") { + puts(s_fmfBoundMinModeModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --fmf-bound-min-mode: `") + + optarg + "'. Try --fmf-bound-min-mode help."); + } +} + // theory/bv/options_handlers.h void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) { #ifndef CVC4_USE_ABC |