diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-15 11:26:56 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-15 11:26:56 -0600 |
| commit | 4604e6119a0a5e968e47cf23ce93b09c17a726b8 (patch) | |
| tree | 037c78de7e1fd6445cf404ccd1026c076054e253 /src/theory/quantifiers/bounded_integers.cpp | |
| parent | 3837f84ab251d1563726f3d13b95f541eaa331a4 (diff) | |
Minimization modes for fmf bound.
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
| -rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 15 |
1 files changed, 10 insertions, 5 deletions
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() ){ |