From a389690dae7889c1bca8cba60e6460cfb8645e55 Mon Sep 17 00:00:00 2001
From: Paul Meng <baolmeng@gmail.com>
Date: Tue, 30 Aug 2016 17:38:32 -0500
Subject: [PATCH] Computed members for tp and product rels even they are not
 used in membership constraints

---
 src/theory/sets/theory_sets_rels.cpp | 24 +++++++++++++++---------
 src/theory/sets/theory_sets_rels.h   |  2 +-
 2 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 40298b1ef..2829e4483 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -114,11 +114,17 @@ int TheorySetsRels::EqcInfo::counter        = 0;
         KIND_TERM_IT k_t_it = t_it->second.begin();
 
         while(k_t_it != t_it->second.end()) {
-          if(k_t_it->first == Kind::JOIN) {
-            std::vector<Node>::iterator join_term_it = k_t_it->second.begin();
-            while(join_term_it != k_t_it->second.end()) {
-              computeMembersForRel(*join_term_it);
-              join_term_it++;
+          if(k_t_it->first == Kind::JOIN || k_t_it->first == Kind::PRODUCT) {
+            std::vector<Node>::iterator term_it = k_t_it->second.begin();
+            while(term_it != k_t_it->second.end()) {
+              computeMembersForRel(*term_it);
+              term_it++;
+            }
+          } else if ( k_t_it->first == Kind::TRANSPOSE ) {
+            std::vector<Node>::iterator term_it = k_t_it->second.begin();
+            while(term_it != k_t_it->second.end()) {
+              computeMembersForTpRel(*term_it);
+              term_it++;
             }
           }
           k_t_it++;
@@ -639,7 +645,7 @@ int TheorySetsRels::EqcInfo::counter        = 0;
     Trace("rels-debug") << "\n[sets-rels] computeJoinOrProductRelations for relation  " << n << std::endl;
     switch(n[0].getKind()) {
     case kind::TRANSPOSE:
-      computeTpRel(n[0]);
+      computeMembersForTpRel(n[0]);
       break;
     case kind::JOIN:
     case kind::PRODUCT:
@@ -651,7 +657,7 @@ int TheorySetsRels::EqcInfo::counter        = 0;
 
     switch(n[1].getKind()) {
     case kind::TRANSPOSE:
-      computeTpRel(n[1]);
+      computeMembersForTpRel(n[1]);
       break;
     case kind::JOIN:
     case kind::PRODUCT:
@@ -667,10 +673,10 @@ int TheorySetsRels::EqcInfo::counter        = 0;
     composeTupleMemForRel(n);
   }
 
-  void TheorySetsRels::computeTpRel(Node n) {
+  void TheorySetsRels::computeMembersForTpRel(Node n) {
     switch(n[0].getKind()) {
     case kind::TRANSPOSE:
-      computeTpRel(n[0]);
+      computeMembersForTpRel(n[0]);
       break;
     case kind::JOIN:
     case kind::PRODUCT:
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 86fc2c4cb..b785dba9c 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -194,7 +194,7 @@ private:
   void applyTCRule( Node, Node );
   std::map< Node, std::hash_set< Node, NodeHashFunction > > constructTCGraph( Node, Node, Node );
   void computeMembersForRel( Node );
-  void computeTpRel( Node );
+  void computeMembersForTpRel( Node );
   void finalizeTCInference();
   void inferTC( Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >& );
   void inferTC( Node, Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >&,
-- 
2.30.2