diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-15 11:26:56 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-15 11:26:56 -0600 |
commit | 4604e6119a0a5e968e47cf23ce93b09c17a726b8 (patch) | |
tree | 037c78de7e1fd6445cf404ccd1026c076054e253 /src/options/options_handler.cpp | |
parent | 3837f84ab251d1563726f3d13b95f541eaa331a4 (diff) |
Minimization modes for fmf bound.
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 |