From 4604e6119a0a5e968e47cf23ce93b09c17a726b8 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 15 Feb 2017 11:26:56 -0600 Subject: [PATCH] Minimization modes for fmf bound. --- src/options/options_handler.cpp | 37 +++++++++++++++++++++ src/options/options_handler.h | 2 ++ src/options/quantifiers_modes.h | 11 ++++++ src/options/quantifiers_options | 2 ++ src/theory/quantifiers/bounded_integers.cpp | 15 ++++++--- 5 files changed, 62 insertions(+), 5 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 diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 09bb2dab3..c488e8c23 100644 --- 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::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() ){ -- 2.30.2