Improvements to sets + cardinality + quantifiers (#2200)

1 files changed, 0 insertions, 37 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 6f9d31024..b48647116 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -582,23 +582,6 @@ 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)
 {
@@ -1038,26 +1021,6 @@ theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(
   }
 }
 
-theory::quantifiers::FmfBoundMinMode OptionsHandler::stringToFmfBoundMinMode(
-    std::string option, std::string optarg)
-{
-  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)
 {