summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/options_handler.cpp37
-rw-r--r--src/options/options_handler.h2
-rw-r--r--src/options/quantifiers_modes.h11
-rw-r--r--src/options/quantifiers_options2
-rw-r--r--src/theory/quantifiers/bounded_integers.cpp15
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<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() ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback