From 02ecbe40a286e314f3e6775b93bed3bf135c8173 Mon Sep 17 00:00:00 2001 From: PaulMeng Date: Tue, 22 Mar 2016 10:30:46 -0500 Subject: [PATCH] minor fix --- src/theory/sets/theory_sets_rels.cpp | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index fc1c1c666..bb9f10d16 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -259,7 +259,7 @@ typedef std::map >::iterator mem_it; Node r1_rep = getRepresentative(join_term[0]); Node r2_rep = getRepresentative(join_term[1]); - if(polarity && d_lemma.find(exp) != d_lemma.end()) { + if(polarity && d_lemma.find(exp) == d_lemma.end()) { Trace("rels-debug") << "\n[sets-rels] Apply JOIN-SPLIT rule on term: " << join_term << " with explaination: " << exp << std::endl; @@ -292,16 +292,15 @@ typedef std::map >::iterator mem_it; computeTupleReps(t2); std::vector elements = d_membership_trie[r1_rep].findTerms(d_tuple_reps[t1]); - if(elements.size() != 0) { - for(unsigned int j = 0; j < elements.size(); j++) { - std::vector new_tup; - new_tup.push_back(elements[j]); - new_tup.insert(new_tup.end(), d_tuple_reps[t2].begin()+1, d_tuple_reps[t2].end()); - if(d_membership_trie[r2_rep].existsTerm(new_tup) != Node::null()) { - return; - } + for(unsigned int j = 0; j < elements.size(); j++) { + std::vector new_tup; + new_tup.push_back(elements[j]); + new_tup.insert(new_tup.end(), d_tuple_reps[t2].begin()+1, d_tuple_reps[t2].end()); + if(d_membership_trie[r2_rep].existsTerm(new_tup) != Node::null()) { + return; } } + Node fact; Node reason = atom[1] == join_term ? exp : AND(exp, EQUAL(atom[1], join_term)); Node reasons = reason; -- 2.30.2