TERM_IT t_it = d_terms_cache.begin();
while( t_it != d_terms_cache.end() ) {
- if( d_rReps_memberReps_cache.find(t_it->first) == d_rReps_memberReps_cache.end() ) {
- Trace("rels-debug") << "[sets-rels] A term does not have membership constraints: " << t_it->first << std::endl;
- KIND_TERM_IT k_t_it = t_it->second.begin();
-
- while( k_t_it != t_it->second.end() ) {
- if( k_t_it->first == kind::JOIN || k_t_it->first == kind::PRODUCT ) {
- std::vector<Node>::iterator term_it = k_t_it->second.begin();
- while(term_it != k_t_it->second.end()) {
- computeMembersForBinOpRel( *term_it );
- ++term_it;
- }
- } else if( k_t_it->first == kind::TRANSPOSE ) {
- std::vector<Node>::iterator term_it = k_t_it->second.begin();
- while( term_it != k_t_it->second.end() ) {
- computeMembersForUnaryOpRel( *term_it );
- ++term_it;
- }
- } else if ( k_t_it->first == kind::TCLOSURE ) {
- std::vector<Node>::iterator term_it = k_t_it->second.begin();
- while( term_it != k_t_it->second.end() ) {
- buildTCGraphForRel( *term_it );
- ++term_it;
- }
- } else if( k_t_it->first == kind::JOIN_IMAGE ) {
- std::vector<Node>::iterator term_it = k_t_it->second.begin();
- while( term_it != k_t_it->second.end() ) {
- computeMembersForJoinImageTerm( *term_it );
- ++term_it;
- }
- } else if( k_t_it->first == kind::IDEN ) {
- std::vector<Node>::iterator term_it = k_t_it->second.begin();
- while( term_it != k_t_it->second.end() ) {
- computeMembersForIdenTerm( *term_it );
- ++term_it;
- }
+ // check the terms in this equivalence class for e.g. upwards closure
+ // (computeMembersForBinOpRel / computeMembersForUnaryOpRel). This is
+ // done regardless of whether we have initialized
+ // d_rReps_memberReps_cache for this equivalence class.
+ Trace("rels-debug")
+ << "[sets-rels] Check equivalence class: "
+ << t_it->first << std::endl;
+ KIND_TERM_IT k_t_it = t_it->second.begin();
+
+ while (k_t_it != t_it->second.end())
+ {
+ Trace("rels-debug") << "[sets-rels] Check " << k_t_it->second.size()
+ << " terms of kind " << k_t_it->first << std::endl;
+ std::vector<Node>::iterator term_it = k_t_it->second.begin();
+ if (k_t_it->first == kind::JOIN || k_t_it->first == kind::PRODUCT)
+ {
+ while (term_it != k_t_it->second.end())
+ {
+ computeMembersForBinOpRel(*term_it);
+ ++term_it;
+ }
+ }
+ else if (k_t_it->first == kind::TRANSPOSE)
+ {
+ while (term_it != k_t_it->second.end())
+ {
+ computeMembersForUnaryOpRel(*term_it);
+ ++term_it;
+ }
+ }
+ else if (k_t_it->first == kind::TCLOSURE)
+ {
+ while (term_it != k_t_it->second.end())
+ {
+ buildTCGraphForRel(*term_it);
+ ++term_it;
}
- ++k_t_it;
}
+ else if (k_t_it->first == kind::JOIN_IMAGE)
+ {
+ while (term_it != k_t_it->second.end())
+ {
+ computeMembersForJoinImageTerm(*term_it);
+ ++term_it;
+ }
+ }
+ else if (k_t_it->first == kind::IDEN)
+ {
+ while (term_it != k_t_it->second.end())
+ {
+ computeMembersForIdenTerm(*term_it);
+ ++term_it;
+ }
+ }
+ ++k_t_it;
}
++t_it;
}
if( eqc_node.getKind() == kind::TRANSPOSE || eqc_node.getKind() == kind::JOIN ||
eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE ||
eqc_node.getKind() == kind::JOIN_IMAGE || eqc_node.getKind() == kind::IDEN ) {
- std::vector<Node> terms;
- std::map< kind::Kind_t, std::vector<Node> > rel_terms;
- TERM_IT terms_it = d_terms_cache.find(eqc_rep);
-
- if( terms_it == d_terms_cache.end() ) {
- terms.push_back(eqc_node);
- rel_terms[eqc_node.getKind()] = terms;
- d_terms_cache[eqc_rep] = rel_terms;
- } else {
- KIND_TERM_IT kind_term_it = terms_it->second.find(eqc_node.getKind());
-
- if( kind_term_it == terms_it->second.end() ) {
- terms.push_back(eqc_node);
- d_terms_cache[eqc_rep][eqc_node.getKind()] = terms;
- } else {
- kind_term_it->second.push_back(eqc_node);
- }
- }
+ d_terms_cache[eqc_rep][eqc_node.getKind()].push_back(eqc_node);
}
// need to add all tuple elements as shared terms
}
Node rel_rep = getRepresentative( tc_rel[0] );
Node tc_rel_rep = getRepresentative( tc_rel );
- std::vector< Node > members = d_rReps_memberReps_cache[rel_rep];
- std::vector< Node > exps = d_rReps_memberReps_exp_cache[rel_rep];
+ const std::vector<Node>& members = d_rReps_memberReps_cache[rel_rep];
+ const std::vector<Node>& exps = d_rReps_memberReps_exp_cache[rel_rep];
- for( unsigned int i = 0; i < members.size(); i++ ) {
+ for (size_t i = 0, msize = members.size(); i < msize; i++)
+ {
Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 ));
Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 ));
Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep );
default:
break;
}
- if(d_rReps_memberReps_cache.find(getRepresentative(rel[0])) == d_rReps_memberReps_cache.end() ||
- d_rReps_memberReps_cache.find(getRepresentative(rel[1])) == d_rReps_memberReps_cache.end()) {
- return;
- }
composeMembersForRels(rel);
}
}
NodeManager* nm = NodeManager::currentNM();
- std::vector<Node> members = d_rReps_memberReps_cache[rel0_rep];
- std::vector<Node> exps = d_rReps_memberReps_exp_cache[rel0_rep];
+ const std::vector<Node>& members = d_rReps_memberReps_cache[rel0_rep];
+ const std::vector<Node>& exps = d_rReps_memberReps_exp_cache[rel0_rep];
Assert(members.size() == exps.size());
- for(unsigned int i = 0; i < members.size(); i++) {
- Node reason = exps[i];
- if( rel.getKind() == kind::TRANSPOSE) {
+ if (rel.getKind() == kind::TRANSPOSE)
+ {
+ for (size_t i = 0, msize = members.size(); i < msize; i++)
+ {
+ Node reason = exps[i];
if( rel[0] != exps[i][1] ) {
- reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, rel[0], exps[i][1]));
+ reason = nm->mkNode(
+ kind::AND, reason, nm->mkNode(kind::EQUAL, rel[0], exps[i][1]));
}
sendInfer(nm->mkNode(MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel),
InferenceId::SETS_RELS_TRANSPOSE_REV,
* consider the case that (a, b) in r1, (c, d) in r2.
*
* For JOIN, we have three cases:
- * b = c, we infer (a, d) in (join r1 r2)
- * b != c, do nothing
- * else, if neither holds, we add the splitting lemma (b=c or b!=c)
+ * if b = c, we infer (a, d) in (join r1 r2)
+ * else, we mark b and c as shared terms; their equality will be split in
+ * theory combination if necessary.
*
* For PRODUCT, we infer (a, b, c, d) in (product r1 r2).
*/
Node r1_rmost =
RelsUtils::nthElementOfTuple(r1_rep_exps[i][0], r1_tuple_len - 1);
Node r2_lmost = RelsUtils::nthElementOfTuple(r2_rep_exps[j][0], 0);
+ // Since we require notification r1_rmost and r2_lmost are equal,
+ // they must be shared terms of theory of sets. Hence, we make the
+ // following calls to makeSharedTerm to ensure this is the case.
+ makeSharedTerm(r1_rmost, r1_rmost.getType());
+ makeSharedTerm(r2_lmost, r2_lmost.getType());
Trace("rels-debug") << "[Theory::Rels] r1_rmost: " << r1_rmost
<< " of type " << r1_rmost.getType() << std::endl;
<< " of type " << r2_lmost.getType() << std::endl;
if (!areEqual(r1_rmost, r2_lmost))
{
- if (!d_state.areDisequal(r1_rmost, r2_lmost))
- {
- // If we have (a,b) in R1, (c,d) in R2, and we are considering
- // join(R1, R2) must split on b=c if they are neither equal nor
- // disequal.
- Node eq = r1_rmost.eqNode(r2_lmost);
- Node lem = nm->mkNode(kind::OR, eq, eq.negate());
- d_im.addPendingLemma(lem, InferenceId::SETS_RELS_JOIN_ELEM_SPLIT);
- }
+
continue;
}
else if (r1_rmost != r2_lmost)
{
+ Trace("rels-debug") << "...equal" << std::endl;
reasons.push_back(nm->mkNode(kind::EQUAL, r1_rmost, r2_lmost));
}
}
return true;
} else if( hasTerm( a ) && hasTerm( b ) ){
return d_state.areEqual(a, b);
- } else if(a.getType().isTuple()) {
- bool equal = true;
- for(unsigned int i = 0; i < a.getType().getTupleLength(); i++) {
- equal = equal && areEqual(RelsUtils::nthElementOfTuple(a, i), RelsUtils::nthElementOfTuple(b, i));
+ }
+ TypeNode atn = a.getType();
+ if (atn.isTuple())
+ {
+ size_t tlen = atn.getTupleLength();
+ for (size_t i = 0; i < tlen; i++)
+ {
+ if (!areEqual(RelsUtils::nthElementOfTuple(a, i),
+ RelsUtils::nthElementOfTuple(b, i)))
+ {
+ return false;
+ }
}
- return equal;
- } else if(!a.getType().isBoolean()){
+ return true;
+ }
+ else if (!atn.isBoolean())
+ {
// TODO(project##230): Find a safe type for the singleton operator
- makeSharedTerm(a, a.getType());
+ makeSharedTerm(a, atn);
makeSharedTerm(b, b.getType());
}
return false;
projects / cvc5.git / commitdiff