Minimization modes for fmf bound.

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