{
//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{
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;
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();
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 ) {
d_bop_index.clear();
d_op_list.clear();
d_card_enabled = false;
+ d_t_card_enabled.clear();
d_rels_enabled = false;
d_eqc_to_card_term.clear();
}else if( n.getKind()==kind::CARD ){
d_card_enabled = true;
TypeNode tnc = n[0].getType().getSetElementType();
+ d_t_card_enabled[tnc] = true;
if( tnc.isInterpretedFinite() ){
std::stringstream ss;
- ss << "ERROR: cannot use cardinality on sets with finite element type." << std::endl;
+ ss << "ERROR: cannot use cardinality on sets with finite element "
+ "type (term is "
+ << n << ")." << std::endl;
throw LogicException(ss.str());
//TODO: extend approach for this case
}
+ // if we do not handle the kind, set incomplete
+ Kind nk = n[0].getKind();
+ if (nk == kind::UNIVERSE_SET || d_rels->isRelationKind(nk))
+ {
+ d_full_check_incomplete = true;
+ Trace("sets-incomplete")
+ << "Sets : incomplete because of " << n << "." << std::endl;
+ }
Node r = d_equalityEngine.getRepresentative( n[0] );
if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){
d_eqc_to_card_term[ r ] = n;
}
void TheorySetsPrivate::registerCardinalityTerm( Node n, std::vector< Node >& lemmas ){
+ TypeNode tnc = n.getType().getSetElementType();
+ if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end())
+ {
+ // if no cardinality constraints for sets of this type, we can ignore
+ return;
+ }
if( d_card_processed.find( n )==d_card_processed.end() ){
d_card_processed.insert( n );
Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
fullEffortCheck();
if( !d_conflict && !d_sentLemma ){
//invoke relations solver
- d_rels->check(level);
- if( d_card_enabled && ( d_rels_enabled || options::setsExt() ) ){
- //if cardinality constraints are enabled,
- // then model construction may fail in there are relational operators, or universe set.
- // TODO: should internally check model, return unknown if fail
- d_full_check_incomplete = true;
- Trace("sets-incomplete") << "Sets : incomplete because of extended operators." << std::endl;
- }
+ d_rels->check(level);
}
- if( d_full_check_incomplete ){
+ if (!d_conflict && !d_sentLemma && d_full_check_incomplete)
+ {
d_external.d_out->setIncomplete();
}
}
projects / cvc5.git / commitdiff