From 08e68bd440dae2893d58c39875e3f2bf776b0354 Mon Sep 17 00:00:00 2001 From: PaulMeng Date: Tue, 1 Mar 2016 14:22:35 -0600 Subject: [PATCH] small fix for naming --- src/theory/sets/theory_sets_rels.cpp | 18 +++++++++--------- src/theory/sets/theory_sets_rels.h | 4 +--- 2 files changed, 10 insertions(+), 12 deletions(-) diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 986c4cf00..384432f04 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -230,7 +230,7 @@ typedef std::map >::iterator mem_it; sendInfer(f2, reason, "product-split"); } else { // ONLY need to explicitly compute joins if there are negative literals involving PRODUCT - computeJoinOrProductRelations(product_term); + computeRels(product_term); } } @@ -307,7 +307,7 @@ typedef std::map >::iterator mem_it; sendInfer(f2, reason, "join-split"); } else { // ONLY need to explicitly compute joins if there are negative literals involving JOIN - computeJoinOrProductRelations(join_term); + computeRels(join_term); } } @@ -332,14 +332,14 @@ typedef std::map >::iterator mem_it; != d_terms_cache[getRepresentative(fact[1])].end()) { std::vector join_terms = d_terms_cache[getRepresentative(fact[1])][kind::JOIN]; for(unsigned int i = 0; i < join_terms.size(); i++) { - computeJoinOrProductRelations(join_terms[i]); + computeRels(join_terms[i]); } } if(d_terms_cache[getRepresentative(fact[1])].find(kind::PRODUCT) != d_terms_cache[getRepresentative(fact[1])].end()) { std::vector product_terms = d_terms_cache[getRepresentative(fact[1])][kind::PRODUCT]; for(unsigned int i = 0; i < product_terms.size(); i++) { - computeJoinOrProductRelations(product_terms[i]); + computeRels(product_terms[i]); } } fact = fact.negate(); @@ -347,7 +347,7 @@ typedef std::map >::iterator mem_it; sendInfer(fact, exp, "transpose-rule"); } - void TheorySetsRels::computeJoinOrProductRelations(Node n) { + void TheorySetsRels::computeRels(Node n) { Trace("rels-debug") << "\n[sets-rels] computeJoinOrProductRelations for relation " << n << std::endl; switch(n[0].getKind()) { case kind::TRANSPOSE: @@ -355,7 +355,7 @@ typedef std::map >::iterator mem_it; break; case kind::JOIN: case kind::PRODUCT: - computeJoinOrProductRelations(n[0]); + computeRels(n[0]); break; default: break; @@ -367,7 +367,7 @@ typedef std::map >::iterator mem_it; break; case kind::JOIN: case kind::PRODUCT: - computeJoinOrProductRelations(n[1]); + computeRels(n[1]); break; default: break; @@ -382,13 +382,13 @@ typedef std::map >::iterator mem_it; void TheorySetsRels::computeTransposeRelations(Node n) { switch(n[0].getKind()) { case kind::JOIN: - computeJoinOrProductRelations(n[0]); + computeRels(n[0]); break; case kind::TRANSPOSE: computeTransposeRelations(n[0]); break; case kind::PRODUCT: - computeJoinOrProductRelations(n[0]); + computeRels(n[0]); break; default: break; diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 827caf69f..dbb48ffcd 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -71,13 +71,11 @@ private: void check(); void collectRelationalInfo(); void assertMembership( Node fact, Node reason, bool polarity ); - void composeProductRelations( Node ); - void composeJoinRelations( Node ); void composeTuplesForRels( Node ); void applyTransposeRule( Node, Node, Node ); void applyJoinRule( Node, Node, Node ); void applyProductRule( Node, Node, Node ); - void computeJoinOrProductRelations( Node ); + void computeRels( Node ); void computeTransposeRelations( Node ); Node reverseTuple( Node ); -- 2.30.2