diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-10-14 18:02:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-14 18:02:27 -0500 |
commit | ae8e63d4be5fb217766ae7ef8a8dd37fd6b3f189 (patch) | |
tree | 7c17346a84ef3584656bab066eb7b6c74d3aa597 /src/theory/sets | |
parent | 42dd10f9936c6a9be158842f482cc7ebd4a972ed (diff) |
Fix issue #5269 (#5270)
This PR fixes issue #5269 of unnecessary calling TheorySetsRels::areEqual in a product relation (which compares the rightmost element of the first child with the leftmost element in the second child). This may violate an assertion in TheorySetsRels::areEqual that the types of the 2 elements should be the same
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 617b458c9..ebb7f845d 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -1040,8 +1040,14 @@ void TheorySetsRels::check(Theory::Effort level) Node r2_lmost = RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 ); tuple_elements.push_back(tn.getDType()[0].getConstructor()); - if( (areEqual(r1_rmost, r2_lmost) && rel.getKind() == kind::JOIN) || - rel.getKind() == kind::PRODUCT ) { + 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))) + { bool isProduct = rel.getKind() == kind::PRODUCT; unsigned int k = 0; unsigned int l = 1; |