summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/bounded_integers.cpp106
1 files changed, 65 insertions, 41 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index e9ac9b484..1e8449dbf 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -246,8 +246,8 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
if( success && !isBound( q, v ) ){
Trace("bound-int-debug") << "Success with variable " << v << std::endl;
bound_lit_type_map[v] = BOUND_FIXED_SET;
- bound_lit_map[0][v] = n;
- bound_lit_pol_map[0][v] = pol;
+ bound_lit_map[3][v] = n;
+ bound_lit_pol_map[3][v] = pol;
bound_fixed_set[v].clear();
bound_fixed_set[v].insert( bound_fixed_set[v].end(), v_cases.begin(), v_cases.end() );
}
@@ -260,8 +260,8 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
if( processEqDisjunct( q, n, v, v_cases ) ){
if( !isBound( q, v ) ){
bound_lit_type_map[v] = BOUND_FIXED_SET;
- bound_lit_map[0][v] = n;
- bound_lit_pol_map[0][v] = pol;
+ bound_lit_map[3][v] = n;
+ bound_lit_pol_map[3][v] = pol;
Assert( v_cases.size()==1 );
bound_fixed_set[v].clear();
bound_fixed_set[v].push_back( v_cases[0] );
@@ -278,32 +278,35 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" );
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( q, it->first ) ){
- Node veq;
- if( QuantArith::isolate( it->first, msum, veq, GEQ )!=0 ){
- Node n1 = veq[0];
- Node n2 = veq[1];
- if(pol){
- //flip
- n1 = veq[1];
- n2 = veq[0];
- if( n1.getKind()==BOUND_VARIABLE ){
- n2 = QuantArith::offset( n2, 1 );
+ //if not bound in another way
+ if( bound_lit_type_map.find( it->first )==bound_lit_type_map.end() || bound_lit_type_map[it->first] == BOUND_INT_RANGE ){
+ Node veq;
+ if( QuantArith::isolate( it->first, msum, veq, GEQ )!=0 ){
+ Node n1 = veq[0];
+ Node n2 = veq[1];
+ if(pol){
+ //flip
+ n1 = veq[1];
+ n2 = veq[0];
+ if( n1.getKind()==BOUND_VARIABLE ){
+ n2 = QuantArith::offset( n2, 1 );
+ }else{
+ n1 = QuantArith::offset( n1, -1 );
+ }
+ veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
+ }
+ Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
+ Node t = n1==it->first ? n2 : n1;
+ if( !hasNonBoundVar( q, t ) ) {
+ Trace("bound-int-debug") << "The bound is relevant." << std::endl;
+ int loru = n1==it->first ? 0 : 1;
+ bound_lit_type_map[it->first] = BOUND_INT_RANGE;
+ bound_int_range_term[loru][it->first] = t;
+ bound_lit_map[loru][it->first] = n;
+ bound_lit_pol_map[loru][it->first] = pol;
}else{
- n1 = QuantArith::offset( n1, -1 );
+ Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
}
- veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
- }
- Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
- Node t = n1==it->first ? n2 : n1;
- if( !hasNonBoundVar( q, t ) ) {
- Trace("bound-int-debug") << "The bound is relevant." << std::endl;
- int loru = n1==it->first ? 0 : 1;
- bound_lit_type_map[it->first] = BOUND_INT_RANGE;
- bound_int_range_term[loru][it->first] = t;
- bound_lit_map[loru][it->first] = n;
- bound_lit_pol_map[loru][it->first] = pol;
- }else{
- Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
}
}
}
@@ -314,8 +317,8 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
if( !pol && n[0].getKind()==BOUND_VARIABLE && !isBound( q, n[0] ) && !hasNonBoundVar( q, n[1] ) ){
Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is membership." << std::endl;
bound_lit_type_map[n[0]] = BOUND_SET_MEMBER;
- bound_lit_map[0][n[0]] = n;
- bound_lit_pol_map[0][n[0]] = pol;
+ bound_lit_map[2][n[0]] = n;
+ bound_lit_pol_map[2][n[0]] = pol;
}
}else{
Assert( n.getKind()!=LEQ && n.getKind()!=LT && n.getKind()!=GT );
@@ -391,10 +394,10 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
}else if( it->second==BOUND_SET_MEMBER ){
setBoundedVar( f, v, BOUND_SET_MEMBER );
setBoundVar = true;
- d_setm_range[f][v] = bound_lit_map[0][v][1];
- d_setm_range_lit[f][v] = bound_lit_map[0][v];
+ 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] );
- Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[0][v] << std::endl;
+ 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 );
setBoundVar = true;
@@ -406,7 +409,7 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
d_fixed_set_gr_range[f][v].push_back( t );
}
}
- Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[0][v] << std::endl;
+ Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[3][v] << std::endl;
}
if( setBoundVar ){
success = true;
@@ -438,13 +441,34 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
}
}while( success );
- Trace("bound-int") << "Bounds are : " << std::endl;
- 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 ){
- Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
- }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
- Trace("bound-int") << " " << v << " in " << d_setm_range[f][v] << std::endl;
+ if( Trace.isOn("bound-int") ){
+ Trace("bound-int") << "Bounds are : " << std::endl;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++) {
+ Node v = f[0][i];
+ if( std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end() ){
+ Assert( d_bound_type[f].find( v )!=d_bound_type[f].end() );
+ if( d_bound_type[f][v]==BOUND_INT_RANGE ){
+ Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
+ }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
+ Trace("bound-int") << " " << v << " in " << d_setm_range[f][v] << std::endl;
+ }else if( d_bound_type[f][v]==BOUND_FIXED_SET ){
+ Trace("bound-int") << " " << v << " in { ";
+ for( unsigned i=0; i<d_fixed_set_ngr_range[f][v].size(); i++ ){
+ Trace("bound-int") << d_fixed_set_ngr_range[f][v][i] << " ";
+ }
+ for( unsigned i=0; i<d_fixed_set_gr_range[f][v].size(); i++ ){
+ Trace("bound-int") << d_fixed_set_gr_range[f][v][i] << " ";
+ }
+ Trace("bound-int") << "}" << std::endl;
+ }else if( d_bound_type[f][v]==BOUND_FINITE ){
+ Trace("bound-int") << " " << v << " has small finite type." << std::endl;
+ }else{
+ Trace("bound-int") << " " << v << " has unknown bound." << std::endl;
+ Assert( false );
+ }
+ }else{
+ Trace("bound-int") << " " << "*** " << v << " is unbounded." << std::endl;
+ }
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback