Minimization modes for fmf bound.

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 1d7355d9fbdb3d157f220feb8b10304c457f6b60..0dac423626549aafe245267d3f24263c0d7b6a14 100644 (file)
--- 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 e327b9c8ea30b1b830a611c531c8c779427a3ff7..45aea7b79e296a707d40ba05047115914df7ed28 100644 (file)
--- 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 cc6abaa8b8343b7391585798549eef03ff97e7a1..e4c539e096b2a2ccbbd4b793eb9faf7612dbda9a 100644 (file)
--- 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 856de103e754521a52cc028777ff15f31e1249e1..cf8fca2fa64be66b3772bcdfa0f3f2d6c32a01b5 100644 (file)
--- 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 
  

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 09bb2dab3efae78b0eb2fbd6452b913f40501893..c488e8c23b30778f235a3154e782313db8fbd2aa 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -407,8 +407,10 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
               Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() );
               d_bounds[b][f][v] = bound_int_range_term[b][v];
             }
-            Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );
-            d_range[f][v] = Rewriter::rewrite( r );
+            if( options::fmfBoundMinMode()==FMF_BOUND_MIN_ALL || options::fmfBoundMinMode()==FMF_BOUND_MIN_INT_RANGE ){
+              Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );
+              d_range[f][v] = Rewriter::rewrite( r );
+            }
             Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
           }
         }else if( it->second==BOUND_SET_MEMBER ){
@@ -416,7 +418,9 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
           setBoundVar = true;
           d_setm_range[f][v] = bound_lit_map[2][v][1];
           d_setm_range_lit[f][v] = bound_lit_map[2][v];
-          d_range[f][v] = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] );
+          if( options::fmfBoundMinMode()==FMF_BOUND_MIN_ALL || options::fmfBoundMinMode()==FMF_BOUND_MIN_SET_CARD ){
+            d_range[f][v] = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] );
+          }
           Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[2][v] << std::endl;
         }else if( it->second==BOUND_FIXED_SET ){
           setBoundedVar( f, v, BOUND_FIXED_SET );
@@ -509,8 +513,9 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
     d_bound_quants.push_back( f );
     for( unsigned i=0; i<d_set[f].size(); i++) {
       Node v = d_set[f][i];
-      if( d_bound_type[f][v]==BOUND_INT_RANGE || d_bound_type[f][v]==BOUND_SET_MEMBER ){
-        Node r = d_range[f][v];
+      std::map< Node, Node >::iterator itr = d_range[f].find( v );
+      if( itr != d_range[f].end() ){
+        Node r = itr->second;
         Assert( !r.isNull() );
         bool isProxy = false;
         if( r.hasBoundVar() ){