diff options
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 71 |
1 files changed, 48 insertions, 23 deletions
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index f6ea88b75..a4028d8fb 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -1039,9 +1039,15 @@ void TheorySetsRels::check(Theory::Effort level) } /* - * Explicitly compose the join or product relations of r1 and r2 - * e.g. If (a, b) in X and (b, c) in Y, (a, c) in (X JOIN Y) + * Explicitly compose the join or product relations of r1 and r2. For example, + * 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) + * + * For PRODUCT, we infer (a, b, c, d) in (product r1 r2). */ void TheorySetsRels::composeMembersForRels( Node rel ) { Trace("rels-debug") << "[Theory::Rels] Start composing members for relation = " << rel << std::endl; @@ -1058,26 +1064,48 @@ void TheorySetsRels::check(Theory::Effort level) std::vector<Node> r1_rep_exps = d_rReps_memberReps_exp_cache[r1_rep]; std::vector<Node> r2_rep_exps = d_rReps_memberReps_exp_cache[r2_rep]; - unsigned int r1_tuple_len = r1.getType().getSetElementType().getTupleLength(); - unsigned int r2_tuple_len = r2.getType().getSetElementType().getTupleLength(); + size_t r1_tuple_len = r1.getType().getSetElementType().getTupleLength(); + size_t r2_tuple_len = r2.getType().getSetElementType().getTupleLength(); + Kind rk = rel.getKind(); + TypeNode tn = rel.getType().getSetElementType(); for( unsigned int i = 0; i < r1_rep_exps.size(); i++ ) { for( unsigned int j = 0; j < r2_rep_exps.size(); j++ ) { std::vector<Node> tuple_elements; - TypeNode tn = rel.getType().getSetElementType(); - 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 ); tuple_elements.push_back(tn.getDType()[0].getConstructor()); + std::vector<Node> reasons; + if (rk == kind::JOIN) + { + 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); + + Trace("rels-debug") << "[Theory::Rels] r1_rmost: " << r1_rmost + << " of type " << r1_rmost.getType() << std::endl; + Trace("rels-debug") << "[Theory::Rels] r2_lmost: " << r2_lmost + << " 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) + { + reasons.push_back(nm->mkNode(kind::EQUAL, r1_rmost, r2_lmost)); + } + } - Trace("rels-debug") << "[Theory::Rels] r1_rmost: " << r1_rmost - << " of type " << r1_rmost.getType() << std::endl; - Trace("rels-debug") << "[Theory::Rels] r2_lmost: " << r2_lmost - << " of type " << r2_lmost.getType() << std::endl; - - if (rel.getKind() == kind::PRODUCT - || (rel.getKind() == kind::JOIN && areEqual(r1_rmost, r2_lmost))) + if (rk == kind::PRODUCT || rk == kind::JOIN) { - bool isProduct = rel.getKind() == kind::PRODUCT; + bool isProduct = rk == kind::PRODUCT; unsigned int k = 0; unsigned int l = 1; @@ -1092,25 +1120,22 @@ void TheorySetsRels::check(Theory::Effort level) tuple_elements.push_back( RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], l ) ); } - Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); - Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, composed_tuple, rel); - std::vector<Node> reasons; + Node composed_tuple = + nm->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); + Node fact = nm->mkNode(kind::MEMBER, composed_tuple, rel); reasons.push_back( r1_rep_exps[i] ); reasons.push_back( r2_rep_exps[j] ); if( r1 != r1_rep_exps[i][1] ) { - reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1, r1_rep_exps[i][1]) ); + reasons.push_back(nm->mkNode(kind::EQUAL, r1, r1_rep_exps[i][1])); } if( r2 != r2_rep_exps[j][1] ) { - reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r2, r2_rep_exps[j][1]) ); + reasons.push_back(nm->mkNode(kind::EQUAL, r2, r2_rep_exps[j][1])); } if( isProduct ) { sendInfer( fact, InferenceId::SETS_RELS_PRODUCE_COMPOSE, nm->mkNode(kind::AND, reasons)); } else { - if( r1_rmost != r2_lmost ) { - reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1_rmost, r2_lmost) ); - } sendInfer( fact, InferenceId::SETS_RELS_JOIN_COMPOSE, nm->mkNode(kind::AND, reasons)); } |