From 030f39b6a65d1488bb41db1daa387d8859251b7b Mon Sep 17 00:00:00 2001 From: PaulMeng Date: Mon, 21 Mar 2016 21:09:27 -0500 Subject: [PATCH] minor fix --- src/theory/sets/theory_sets_rels.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 42473e4f2..fc1c1c666 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -83,9 +83,11 @@ typedef std::map >::iterator mem_it; } if(kind_terms.find(kind::JOIN) != kind_terms.end()) { std::vector join_terms = kind_terms[kind::JOIN]; + Trace("rels-debug") << "[sets-rels] apply join rules on join terms with size = " << join_terms.size() << std::endl; // exp is a membership term and join_terms contains all // terms involving "join" operator that are in the same equivalence class with the right hand side of exp for(unsigned int j = 0; j < join_terms.size(); j++) { + Trace("rels-debug") << "[sets-rels] join term = " << join_terms[j] << std::endl; applyJoinRule(exp, join_terms[j]); } } @@ -149,13 +151,12 @@ typedef std::map >::iterator mem_it; rel_terms[n.getKind()] = terms; d_terms_cache[r] = rel_terms; } else { - rel_terms = d_terms_cache[r]; // No n's kind record is found - if( rel_terms.find(n.getKind()) == rel_terms.end() ) { + if( d_terms_cache[r].find(n.getKind()) == d_terms_cache[r].end() ) { terms.push_back(n); - rel_terms[n.getKind()] = terms; + d_terms_cache[r][n.getKind()] = terms; } else { - rel_terms[n.getKind()].push_back(n); + d_terms_cache[r][n.getKind()].push_back(n); } } } -- 2.30.2