diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:15 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:31 -0600 |
commit | e8c09abb9165278b13491c83bdcbe17ae535126e (patch) | |
tree | 1101d3e878bcfd9e12cd64aaad3017aa320c896b /src/theory/quantifiers/bounded_integers.cpp | |
parent | 0e956da9b32ce8a8fcf20ec65e5a2820b4e31324 (diff) |
Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 298 |
1 files changed, 235 insertions, 63 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index dc0019383..1112c2ef2 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -171,31 +171,110 @@ bool BoundedIntegers::isBound( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); } -bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) { - if( b.getKind()==BOUND_VARIABLE ){ - if( !isBound( f, b ) ){ - return true; - } - }else{ - for( unsigned i=0; i<b.getNumChildren(); i++ ){ - if( hasNonBoundVar( f, b[i] ) ){ +bool BoundedIntegers::hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ) { + if( visited.find( b )==visited.end() ){ + visited[b] = true; + if( b.getKind()==BOUND_VARIABLE ){ + if( !isBound( f, b ) ){ return true; } + }else{ + for( unsigned i=0; i<b.getNumChildren(); i++ ){ + if( hasNonBoundVar( f, b[i], visited ) ){ + return true; + } + } } } return false; } +bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) { + std::map< Node, bool > visited; + return hasNonBoundVar( f, b, visited ); +} -void BoundedIntegers::processLiteral( Node q, Node lit, bool pol, - std::map< Node, unsigned >& bound_lit_type_map, - std::map< int, std::map< Node, Node > >& bound_lit_map, - std::map< int, std::map< Node, bool > >& bound_lit_pol_map, - std::map< int, std::map< Node, Node > >& bound_int_range_term ) { - if( lit.getKind()==GEQ ){ - if( lit[0].getType().isInteger() ){ +bool BoundedIntegers::processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases ) { + if( n.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + Node t = n[i]; + if( !hasNonBoundVar( q, n[1-i] ) ){ + if( t==v ){ + v_cases.push_back( n[1-i] ); + return true; + }else if( v.isNull() && t.getKind()==BOUND_VARIABLE ){ + v = t; + v_cases.push_back( n[1-i] ); + return true; + } + } + } + } + return false; +} + +void BoundedIntegers::process( Node q, Node n, bool pol, + std::map< Node, unsigned >& bound_lit_type_map, + std::map< int, std::map< Node, Node > >& bound_lit_map, + std::map< int, std::map< Node, bool > >& bound_lit_pol_map, + std::map< int, std::map< Node, Node > >& bound_int_range_term, + std::map< Node, std::vector< Node > >& bound_fixed_set ){ + if( n.getKind()==OR || n.getKind()==AND ){ + if( (n.getKind()==OR)==pol ){ + for( unsigned i=0; i<n.getNumChildren(); i++) { + process( q, n[i], pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set ); + } + }else{ + //if we are ( x != t1 ^ ...^ x != tn ), then x can be bound to { t1...tn } + Node conj = n; + if( !pol ){ + conj = TermDb::simpleNegate( conj ); + } + Trace("bound-int-debug") << "Process possible finite disequality conjunction : " << conj << std::endl; + Assert( conj.getKind()==AND ); + Node v; + std::vector< Node > v_cases; + bool success = true; + for( unsigned i=0; i<conj.getNumChildren(); i++ ){ + if( conj[i].getKind()==NOT && processEqDisjunct( q, conj[i][0], v, v_cases ) ){ + //continue + }else{ + Trace("bound-int-debug") << "...failed due to " << conj[i] << std::endl; + success = false; + break; + } + } + 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_fixed_set[v].clear(); + bound_fixed_set[v].insert( bound_fixed_set[v].end(), v_cases.begin(), v_cases.end() ); + } + } + }else if( n.getKind()==EQUAL ){ + if( !pol ){ + // non-applied DER on x != t, x can be bound to { t } + Node v; + std::vector< Node > v_cases; + 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; + Assert( v_cases.size()==1 ); + bound_fixed_set[v].clear(); + bound_fixed_set[v].push_back( v_cases[0] ); + } + } + } + }else if( n.getKind()==NOT ){ + process( q, n[0], !pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set ); + }else if( n.getKind()==GEQ ){ + if( n[0].getType().isInteger() ){ std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( lit, msum ) ){ - Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl; + if( QuantArith::getMonomialSumLit( n, msum ) ){ + Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is monomial sum : " << std::endl; 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 ) ){ @@ -221,7 +300,7 @@ void BoundedIntegers::processLiteral( Node q, Node lit, bool pol, 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] = lit; + 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; @@ -231,32 +310,15 @@ void BoundedIntegers::processLiteral( Node q, Node lit, bool pol, } } } - }else if( lit.getKind()==MEMBER ){ - //TODO: enable this when sets models are fixed - if( !pol && lit[0].getKind()==BOUND_VARIABLE && !isBound( q, lit[0] ) && !lit[1].hasBoundVar() ){ - Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is membership." << std::endl; - bound_lit_type_map[lit[0]] = BOUND_SET_MEMBER; - bound_lit_map[0][lit[0]] = lit; - bound_lit_pol_map[0][lit[0]] = pol; + }else if( n.getKind()==MEMBER ){ + 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; } - }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) { - Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl; - } -} - -void BoundedIntegers::process( Node q, Node n, bool pol, - std::map< Node, unsigned >& bound_lit_type_map, - std::map< int, std::map< Node, Node > >& bound_lit_map, - std::map< int, std::map< Node, bool > >& bound_lit_pol_map, - std::map< int, std::map< Node, Node > >& bound_int_range_term ){ - if( (n.getKind()==OR && pol) || (n.getKind()==AND && !pol) ){ - for( unsigned i=0; i<n.getNumChildren(); i++) { - process( q, n[i], pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term ); - } - }else if( n.getKind()==NOT ){ - process( q, n[0], !pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term ); - }else { - processLiteral( q, n, pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term ); + }else{ + Assert( n.getKind()!=LEQ && n.getKind()!=LT && n.getKind()!=GT ); } } @@ -294,8 +356,9 @@ void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) { Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl; } -void BoundedIntegers::registerQuantifier( Node f ) { - Trace("bound-int") << "Register quantifier " << f << std::endl; +void BoundedIntegers::preRegisterQuantifier( Node f ) { + //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister + Trace("bound-int") << "preRegister quantifier " << f << std::endl; bool success; do{ @@ -303,8 +366,9 @@ void BoundedIntegers::registerQuantifier( Node f ) { std::map< int, std::map< Node, Node > > bound_lit_map; std::map< int, std::map< Node, bool > > bound_lit_pol_map; std::map< int, std::map< Node, Node > > bound_int_range_term; + std::map< Node, std::vector< Node > > bound_fixed_set; success = false; - process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term ); + process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set ); //for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){ for( std::map< Node, unsigned >::iterator it = bound_lit_type_map.begin(); it != bound_lit_type_map.end(); ++it ){ Node v = it->first; @@ -315,7 +379,6 @@ void BoundedIntegers::registerQuantifier( Node f ) { if( bound_lit_map[0].find( v )!=bound_lit_map[0].end() && bound_lit_map[1].find( v )!=bound_lit_map[1].end() ){ setBoundedVar( f, v, BOUND_INT_RANGE ); setBoundVar = true; - success = true; for( unsigned b=0; b<2; b++ ){ //set the bounds Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() ); @@ -330,9 +393,23 @@ void BoundedIntegers::registerQuantifier( Node f ) { 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_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; + }else if( it->second==BOUND_FIXED_SET ){ + setBoundedVar( f, v, BOUND_FIXED_SET ); + setBoundVar = true; + for( unsigned i=0; i<bound_fixed_set[v].size(); i++ ){ + Node t = bound_fixed_set[v][i]; + if( t.hasBoundVar() ){ + d_fixed_set_ngr_range[f][v].push_back( t ); + }else{ + 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; } if( setBoundVar ){ + success = true; //set Attributes on literals for( unsigned b=0; b<2; b++ ){ if( bound_lit_map[b].find( v )!=bound_lit_map[b].end() ){ @@ -346,6 +423,19 @@ void BoundedIntegers::registerQuantifier( Node f ) { } } } + if( !success ){ + //resort to setting a finite bound on a variable + for( unsigned i=0; i<f[0].getNumChildren(); i++) { + if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){ + TypeNode tn = f[0][i].getType(); + if( tn.isSort() || getTermDatabase()->mayComplete( tn ) ){ + success = true; + setBoundedVar( f, f[0][i], BOUND_FINITE ); + break; + } + } + } + } }while( success ); Trace("bound-int") << "Bounds are : " << std::endl; @@ -361,12 +451,9 @@ void BoundedIntegers::registerQuantifier( Node f ) { bool bound_success = true; for( unsigned i=0; i<f[0].getNumChildren(); i++) { if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){ - TypeNode tn = f[0][i].getType(); - if( !tn.isSort() && !getTermDatabase()->mayComplete( tn ) ){ - Trace("bound-int-warn") << "Warning : Bounded Integers : Due to quantification on " << f[0][i] << ", could not find bounds for " << f << std::endl; - bound_success = false; - break; - } + Trace("bound-int-warn") << "Warning : Bounded Integers : Due to quantification on " << f[0][i] << ", could not find bounds for " << f << std::endl; + bound_success = false; + break; } } @@ -375,17 +462,13 @@ void BoundedIntegers::registerQuantifier( Node 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; - if( d_bound_type[f][v]==BOUND_INT_RANGE ){ - r = d_range[f][v]; - }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){ - r = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] ); - } + Node r = d_range[f][v]; + Assert( !r.isNull() ); bool isProxy = false; if( r.hasBoundVar() ){ //introduce a new bound Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" ); - d_nground_range[f][v] = d_range[f][v]; + d_nground_range[f][v] = r; d_range[f][v] = new_range; r = new_range; isProxy = true; @@ -403,6 +486,10 @@ void BoundedIntegers::registerQuantifier( Node f ) { } } +void BoundedIntegers::registerQuantifier( Node q ) { + +} + void BoundedIntegers::assertNode( Node n ) { Trace("bound-int-assert") << "Assert " << n << std::endl; Node nlit = n.getKind()==NOT ? n[0] : n; @@ -490,6 +577,8 @@ bool BoundedIntegers::isGroundRange( Node q, Node v ) { return !getLowerBound(q,v).hasBoundVar() && !getUpperBound(q,v).hasBoundVar(); }else if( d_bound_type[q][v]==BOUND_SET_MEMBER ){ return !d_setm_range[q][v].hasBoundVar(); + }else if( d_bound_type[q][v]==BOUND_FIXED_SET ){ + return !d_fixed_set_ngr_range[q][v].empty(); } } return false; @@ -592,21 +681,23 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va Assert( q[0][v]==d_set[q][i] ); Node t = rsi->getCurrentTerm( v ); Trace("bound-int-rsi") << "term : " << t << std::endl; + if( rsi->d_rep_set->d_values_to_terms.find( t )!=rsi->d_rep_set->d_values_to_terms.end() ){ + t = rsi->d_rep_set->d_values_to_terms[t]; + Trace("bound-int-rsi") << "term (post-rep) : " << t << std::endl; + } vars.push_back( d_set[q][i] ); subs.push_back( t ); } //check if it has been instantiated if( !vars.empty() && !d_bnd_it[q][v].hasInstantiated(subs) ){ - if( d_bound_type[q][v]==BOUND_INT_RANGE ){ + if( d_bound_type[q][v]==BOUND_INT_RANGE || d_bound_type[q][v]==BOUND_SET_MEMBER ){ //must add the lemma Node nn = d_nground_range[q][v]; nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] ); Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl; d_quantEngine->getOutputChannel().lemma(lem, false, true); - }else{ - //TODO : sets } return false; }else{ @@ -614,3 +705,84 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va } } +bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) { + if( initial || !isGroundRange( q, v ) ){ + elements.clear(); + unsigned bvt = getBoundVarType( q, v ); + if( bvt==BOUND_INT_RANGE ){ + Node l, u; + getBoundValues( q, v, rsi, l, u ); + if( l.isNull() || u.isNull() ){ + //failed, abort the iterator + return false; + }else{ + Trace("bound-int-rsi") << "Can limit bounds of " << v << " to " << l << "..." << u << std::endl; + Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) ); + Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) ); + Node tl = l; + Node tu = u; + getBounds( q, v, rsi, tl, tu ); + Assert( !tl.isNull() && !tu.isNull() ); + if( ra==d_quantEngine->getTermDatabase()->d_true ){ + long rr = range.getConst<Rational>().getNumerator().getLong()+1; + Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; + for( unsigned k=0; k<rr; k++ ){ + Node t = NodeManager::currentNM()->mkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) ); + t = Rewriter::rewrite( t ); + elements.push_back( t ); + } + return true; + }else{ + Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << v << "." << std::endl; + return false; + } + } + }else if( bvt==BOUND_SET_MEMBER ){ + Node srv = getSetRangeValue( q, v, rsi ); + if( srv.isNull() ){ + return false; + }else{ + Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl; + if( srv.getKind()!=EMPTYSET ){ + while( srv.getKind()==UNION ){ + Assert( srv[1].getKind()==kind::SINGLETON ); + elements.push_back( srv[1][0] ); + srv = srv[0]; + } + Assert( srv.getKind()==kind::SINGLETON ); + elements.push_back( srv[0] ); + } + return true; + } + }else if( bvt==BOUND_FIXED_SET ){ + std::map< Node, std::vector< Node > >::iterator it = d_fixed_set_gr_range[q].find( v ); + if( it!=d_fixed_set_gr_range[q].end() ){ + for( unsigned i=0; i<it->second.size(); i++ ){ + elements.push_back( it->second[i] ); + } + } + it = d_fixed_set_ngr_range[q].find( v ); + if( it!=d_fixed_set_ngr_range[q].end() ){ + std::vector< Node > vars; + std::vector< Node > subs; + if( getRsiSubsitution( q, v, vars, subs, rsi ) ){ + for( unsigned i=0; i<it->second.size(); i++ ){ + Node t = it->second[i].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + elements.push_back( t ); + } + return true; + }else{ + return false; + } + }else{ + return true; + } + }else{ + return false; + } + }else{ + //no change required + return true; + } +} + |