diff options
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/options_handler.cpp | 37 | ||||
-rw-r--r-- | src/options/options_handler.h | 2 | ||||
-rw-r--r-- | src/options/quantifiers_modes.h | 11 | ||||
-rw-r--r-- | src/options/quantifiers_options | 2 |
4 files changed, 52 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 diff --git a/src/options/options_handler.h b/src/options/options_handler.h index e327b9c8e..45aea7b79 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -104,6 +104,7 @@ public: theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::FmfBoundMinMode stringToFmfBoundMinMode(std::string option, std::string optarg) throw(OptionException); // theory/bv/options_handlers.h void abcEnabledBuild(std::string option, bool value) throw(OptionException); @@ -225,6 +226,7 @@ public: static const std::string s_triggerActiveSelModeHelp; static const std::string s_ufssModeHelp; static const std::string s_userPatModeHelp; + static const std::string s_fmfBoundMinModeModeHelp; static const std::string s_errorSelectionRulesHelp; static const std::string s_arithPropagationModeHelp; static const std::string s_arithUnateLemmasHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index cc6abaa8b..e4c539e09 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -209,6 +209,17 @@ enum QuantRepMode { QUANT_REP_MODE_DEPTH, }; +enum FmfBoundMinMode { + /** do not minimize bounds */ + FMF_BOUND_MIN_NONE, + /** default, minimize integer ranges */ + FMF_BOUND_MIN_INT_RANGE, + /** minimize set cardinality ranges */ + FMF_BOUND_MIN_SET_CARD, + /** minimize all bounds */ + FMF_BOUND_MIN_ALL, +}; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 856de103e..cf8fca2fa 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -165,6 +165,8 @@ option fmfBound fmf-bound --fmf-bound bool :default false :read-write finite model finding on bounded quantification option fmfBoundLazy --fmf-bound-lazy bool :default false :read-write enforce bounds for bounded quantification lazily via use of proxy variables +option fmfBoundMinMode --fmf-bound-min-mode=MODE CVC4::theory::quantifiers::FmfBoundMinMode :default CVC4::theory::quantifiers::FMF_BOUND_MIN_INT_RANGE :include "options/quantifiers_modes.h" :handler stringToFmfBoundMinMode + mode for which types of bounds to minimize via first decision heuristics ### conflict-based instantiation options |