Minimization modes for fmf bound.

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