diff options
Diffstat (limited to 'src/theory/quantifiers/fmf')
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 165 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h | 8 |
2 files changed, 99 insertions, 74 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index ae1e3df32..7094ad541 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -388,6 +388,7 @@ void BoundedIntegers::checkOwnership(Node f) { //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister Trace("bound-int") << "check ownership quantifier " << f << std::endl; + NodeManager* nm = NodeManager::currentNM(); bool success; do{ @@ -413,21 +414,26 @@ void BoundedIntegers::checkOwnership(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]; } - 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 ); - } + Node r = nm->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 ){ - setBoundedVar( f, v, BOUND_SET_MEMBER ); - setBoundVar = true; - d_setm_range[f][v] = bound_lit_map[2][v][1]; - d_setm_range_lit[f][v] = bound_lit_map[2][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] ); + // only handles infinite element types currently (cardinality is not + // supported for finite element types #1123). Regardless, this is + // typically not a limitation since this variable can be bound in a + // standard way below since its type is finite. + if (!v.getType().isInterpretedFinite()) + { + setBoundedVar(f, v, BOUND_SET_MEMBER); + 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] = nm->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; } - 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; @@ -644,10 +650,14 @@ bool BoundedIntegers::isGroundRange( Node q, Node v ) { Node BoundedIntegers::getSetRange( Node q, Node v, RepSetIterator * rsi ) { Node sr = d_setm_range[q][v]; if( d_nground_range[q].find(v)!=d_nground_range[q].end() ){ + Trace("bound-int-rsi-debug") + << sr << " is non-ground, apply substitution..." << std::endl; //get the substitution std::vector< Node > vars; std::vector< Node > subs; if( getRsiSubsitution( q, v, vars, subs, rsi ) ){ + Trace("bound-int-rsi-debug") + << " apply " << vars << " -> " << subs << std::endl; sr = sr.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); }else{ sr = Node::null(); @@ -658,73 +668,80 @@ Node BoundedIntegers::getSetRange( Node q, Node v, RepSetIterator * rsi ) { Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { Node sr = getSetRange( q, v, rsi ); - if( !sr.isNull() ){ - Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl; - sr = d_quantEngine->getModel()->getValue( sr ); - //if non-constant, then sr does not occur in the model, we fail - if( !sr.isConst() ){ - return Node::null(); - } - Trace("bound-int-rsi") << "Value is " << sr << std::endl; - //as heuristic, map to term model - if( sr.getKind()!=EMPTYSET ){ - std::map< Node, Node > val_to_term; - while( sr.getKind()==UNION ){ - Assert( sr[1].getKind()==kind::SINGLETON ); - val_to_term[ sr[1][0] ] = sr[1][0]; - sr = sr[0]; - } - Assert( sr.getKind()==kind::SINGLETON ); - val_to_term[ sr[0] ] = sr[0]; - //must look back at assertions, not term database (theory of sets introduces extraneous terms internally) - Theory* theory = d_quantEngine->getTheoryEngine()->theoryOf( THEORY_SETS ); - if( theory ){ - context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for( unsigned i = 0; it != it_end; ++ it, ++i ){ - Node lit = (*it).assertion; - if( lit.getKind()==kind::MEMBER ){ - Node vr = d_quantEngine->getModel()->getValue( lit[0] ); - Trace("bound-int-rsi-debug") << "....membership for " << lit << " ==> " << vr << std::endl; - Trace("bound-int-rsi-debug") << " " << (val_to_term.find( vr )!=val_to_term.end()) << " " << d_quantEngine->getEqualityQuery()->areEqual( d_setm_range_lit[q][v][1], lit[1] ) << std::endl; - if( val_to_term.find( vr )!=val_to_term.end() ){ - if( d_quantEngine->getEqualityQuery()->areEqual( d_setm_range_lit[q][v][1], lit[1] ) ){ - Trace("bound-int-rsi") << " Map value to term : " << vr << " -> " << lit[0] << std::endl; - val_to_term[ vr ] = lit[0]; - } - } - } - } - } - //rebuild value - Node nsr; - for( std::map< Node, Node >::iterator it = val_to_term.begin(); it != val_to_term.end(); ++it ){ - Node nv = NodeManager::currentNM()->mkNode( kind::SINGLETON, it->second ); - if( nsr.isNull() ){ - nsr = nv; - }else{ - nsr = NodeManager::currentNM()->mkNode( kind::UNION, nsr, nv ); - } - } - Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl; - return nsr; - - /* - Node lit = d_setm_range_lit[q][v]; - Trace("bound-int-rsi-debug") << "Bounded from lit " << lit << std::endl; - Node f = d_quantEngine->getTermDatabase()->getMatchOperator( lit ); - TermArgTrie * ta = d_quantEngine->getTermDatabase()->getTermArgTrie( f ); - if( ta ){ - Trace("bound-int-rsi-debug") << "Got term index for " << f << std::endl; - for( std::map< TNode, TermArgTrie >::iterator it = ta->d_data.begin(); it != ta->d_data.end(); ++it ){ - - } + if (sr.isNull()) + { + return sr; + } + Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl; + Assert(!sr.hasFreeVar()); + Node sro = sr; + sr = d_quantEngine->getModel()->getValue(sr); + // if non-constant, then sr does not occur in the model, we fail + if (!sr.isConst()) + { + return Node::null(); + } + Trace("bound-int-rsi") << "Value is " << sr << std::endl; + if (sr.getKind() == EMPTYSET) + { + return sr; + } + NodeManager* nm = NodeManager::currentNM(); + Node nsr; + TypeNode tne = sr.getType().getSetElementType(); + // we can use choice functions for canonical symbolic instantiations + unsigned srCard = 0; + while (sr.getKind() == UNION) + { + srCard++; + sr = sr[0]; + } + Assert(sr.getKind() == SINGLETON); + srCard++; + // choices[i] stores the canonical symbolic representation of the (i+1)^th + // element of sro + std::vector<Node> choices; + Node srCardN = nm->mkNode(CARD, sro); + Node choice_i; + for (unsigned i = 0; i < srCard; i++) + { + if (i == d_setm_choice[sro].size()) + { + choice_i = nm->mkBoundVar(tne); + choices.push_back(choice_i); + Node cBody = nm->mkNode(MEMBER, choice_i, sro); + if (choices.size() > 1) + { + cBody = nm->mkNode(AND, cBody, nm->mkNode(DISTINCT, choices)); } - */ + choices.pop_back(); + Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i); + Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConst(Rational(i))); + choice_i = nm->mkNode(CHOICE, bvl, nm->mkNode(OR, cMinCard, cBody)); + d_setm_choice[sro].push_back(choice_i); + } + Assert(i < d_setm_choice[sro].size()); + choice_i = d_setm_choice[sro][i]; + choices.push_back(choice_i); + Node sChoiceI = nm->mkNode(SINGLETON, choice_i); + if (nsr.isNull()) + { + nsr = sChoiceI; + } + else + { + nsr = nm->mkNode(UNION, nsr, sChoiceI); } - } - return sr; + // turns the concrete model value of sro into a canonical representation + // e.g. + // singleton(0) union singleton(1) + // becomes + // C1 union ( choice y. card(S)<=1 OR ( y in S AND distinct( y, C1 ) ) ) + // where C1 = ( choice x. card(S)<=0 OR x in S ). + Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl; + return nsr; } bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ) { diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index c6293f1fe..90928c0bc 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -62,6 +62,14 @@ private: //set membership range std::map< Node, std::map< Node, Node > > d_setm_range; std::map< Node, std::map< Node, Node > > d_setm_range_lit; + /** set membership element choice functions + * + * For each set S and integer n, d_setm_choice[S][n] is the canonical + * representation for the (n+1)^th member of set S. It is of the form: + * choice x. (|S| <= n OR ( x in S AND + * distinct( x, d_setm_choice[S][0], ..., d_setm_choice[S][n-1] ) ) ) + */ + std::map<Node, std::vector<Node> > d_setm_choice; //fixed finite set range std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_gr_range; std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_ngr_range; |