Towards refactoring relations (#3078)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cc13dec6d1ed41adde3065f6c56c8d585471092f..058e848d6b197e26a0bf503861f351f0029effea 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -614,6 +614,8 @@ libcvc4_add_sources(
   theory/sep/theory_sep_type_rules.h
   theory/sets/normal_form.h
   theory/sets/rels_utils.h
+  theory/sets/skolem_cache.cpp
+  theory/sets/skolem_cache.h
   theory/sets/theory_sets.cpp
   theory/sets/theory_sets.h
   theory/sets/theory_sets_private.cpp

diff --git a/src/options/sets_options.toml b/src/options/sets_options.toml
index 3d46b3be387f21ee1cbfb68d8e9eea37b94232c2..766da793a15b965c3d4c7f176a2e3721acb3eaea 100644 (file)
--- a/src/options/sets_options.toml
+++ b/src/options/sets_options.toml
@@ -20,15 +20,6 @@ header = "options/sets_options.h"
   read_only  = true
   help       = "send inferences as lemmas"
 
-[[option]]
-  name       = "setsRelEager"
-  category   = "regular"
-  long       = "sets-rel-eager"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "standard effort checks for relations"
-
 [[option]]
   name       = "setsExt"
   category   = "regular"

diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp
new file mode 100644 (file)
index 0000000..99e6588
--- /dev/null
+++ b/src/theory/sets/skolem_cache.cpp
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file skolem_cache.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of a cache of skolems for theory of sets.
+ **/
+
+#include "theory/sets/skolem_cache.h"
+
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+SkolemCache::SkolemCache() {}
+
+Node SkolemCache::mkTypedSkolemCached(
+    TypeNode tn, Node a, Node b, SkolemId id, const char* c)
+{
+  a = a.isNull() ? a : Rewriter::rewrite(a);
+  b = b.isNull() ? b : Rewriter::rewrite(b);
+
+  std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
+  if (it == d_skolemCache[a][b].end())
+  {
+    Node sk = mkTypedSkolem(tn, c);
+    d_skolemCache[a][b][id] = sk;
+    return sk;
+  }
+  return it->second;
+}
+
+Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
+{
+  Node n = NodeManager::currentNM()->mkSkolem(c, tn, "sets skolem");
+  d_allSkolems.insert(n);
+  return n;
+}
+
+bool SkolemCache::isSkolem(Node n) const
+{
+  return d_allSkolems.find(n) != d_allSkolems.end();
+}
+
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC4

diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h
new file mode 100644 (file)
index 0000000..74a8073
--- /dev/null
+++ b/src/theory/sets/skolem_cache.h
@@ -0,0 +1,73 @@
+/*********************                                                        */
+/*! \file skolem_cache.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A cache of skolems for theory of sets.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SETS__SKOLEM_CACHE_H
+#define CVC4__THEORY__SETS__SKOLEM_CACHE_H
+
+#include <map>
+#include <unordered_set>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+/**
+ * A cache of all set skolems generated by the TheorySets class. This
+ * cache is used to ensure that duplicate skolems are not generated when
+ * possible, and helps identify what skolems were allocated in the current run.
+ */
+class SkolemCache
+{
+ public:
+  SkolemCache();
+  /** Identifiers for skolem types
+   *
+   * The comments below document the properties of each skolem introduced by
+   * inference in the sets solver, where by skolem we mean the fresh
+   * set variable that witnesses each of "exists k".
+   */
+  enum SkolemId
+  {
+    // (a,b) in join(A,B) => exists k. (a,k) in A ^ (k,b) in B
+    // This is cached by the nodes corresponding to (a,b) and join(A,B).
+    SK_JOIN,
+  };
+
+  /**
+   * Makes a skolem of type tn that is cached based on the key (a,b,id).
+   * Argument c is the variable name of the skolem.
+   */
+  Node mkTypedSkolemCached(
+      TypeNode tn, Node a, Node b, SkolemId id, const char* c);
+  /** Same as above, but without caching. */
+  Node mkTypedSkolem(TypeNode tn, const char* c);
+  /** Returns true if n is a skolem allocated by this class */
+  bool isSkolem(Node n) const;
+
+ private:
+  /** map from node pairs and identifiers to skolems */
+  std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
+  /** the set of all skolems we have generated */
+  std::unordered_set<Node, NodeHashFunction> d_allSkolems;
+};
+
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index a62a235c31fda2c55be17d86e96f472d3e042fa8..6e71ab2ad6f49fd066eb8ba2b2c8f7db24cbec5b 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -26,9 +26,8 @@
 #include "theory/theory_model.h"
 #include "util/result.h"
 
-#define AJR_IMPLEMENTATION
-
 using namespace std;
+using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
@@ -54,8 +53,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
       d_notify(*this),
       d_equalityEngine(d_notify, c, "theory::sets::ee", true),
       d_conflict(c),
-      d_rels(
-          new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external)),
+      d_rels(new TheorySetsRels(c, u, &d_equalityEngine, *this)),
       d_rels_enabled(false)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
@@ -84,9 +82,6 @@ void TheorySetsPrivate::eqNotifyNewClass(TNode t) {
     EqcInfo * e = getOrMakeEqcInfo( t, true );
     e->d_singleton = t;
   }
-  if( options::setsRelEager() ){
-    d_rels->eqNotifyNewClass( t );
-  }
 }
 
 void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2){
@@ -179,9 +174,6 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
       }
       d_members[t1] = n_members;
     }
-    if( options::setsRelEager() ){
-      d_rels->eqNotifyPostMerge( t1, t2 );
-    }
   }
 }
 
@@ -535,11 +527,13 @@ void TheorySetsPrivate::fullEffortCheck(){
 
     std::vector< Node > lemmas;
     Trace("sets-eqc") << "Equality Engine:" << std::endl;
+    std::map<TypeNode, unsigned> eqcTypeCount;
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
     while( !eqcs_i.isFinished() ){
       Node eqc = (*eqcs_i);
       bool isSet = false;
       TypeNode tn = eqc.getType();
+      eqcTypeCount[tn]++;
       //common type node and term
       TypeNode tnc;
       Node tnct;
@@ -667,7 +661,17 @@ void TheorySetsPrivate::fullEffortCheck(){
       Trace("sets-eqc") << std::endl;
       ++eqcs_i;
     }
-    
+
+    if (Trace.isOn("sets-state"))
+    {
+      Trace("sets-state") << "Equivalence class counters:" << std::endl;
+      for (std::pair<const TypeNode, unsigned>& ec : eqcTypeCount)
+      {
+        Trace("sets-state")
+            << "  " << ec.first << " -> " << ec.second << std::endl;
+      }
+    }
+
     flushLemmas( lemmas );
     if( !hasProcessed() ){
       if( Trace.isOn("sets-mem") ){
@@ -736,6 +740,11 @@ void TheorySetsPrivate::fullEffortCheck(){
         }
       }
     }
+    if (!hasProcessed())
+    {
+      // invoke relations solver
+      d_rels->check(Theory::EFFORT_FULL);
+    }
   }while( !d_sentLemma && !d_conflict && d_addedFact );
   Trace("sets") << "----- End full effort check, conflict=" << d_conflict << ", lemma=" << d_sentLemma << std::endl;
 }
@@ -1755,19 +1764,11 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     if( level == Theory::EFFORT_FULL ){
       if( !d_external.d_valuation.needCheck() ){
         fullEffortCheck();
-        if( !d_conflict && !d_sentLemma ){
-          //invoke relations solver
-          d_rels->check(level);
-        }
         if (!d_conflict && !d_sentLemma && d_full_check_incomplete)
         {
           d_external.d_out->setIncomplete();
         }
       }
-    }else{
-      if( options::setsRelEager() ){
-        d_rels->check(level);  
-      }
     }
   }
   Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
@@ -1888,8 +1889,8 @@ void TheorySetsPrivate::computeCareGraph() {
       //populate indices
       for( unsigned i=0; i<it->second.size(); i++ ){
         TNode f1 = it->second[i];
-        Assert(d_equalityEngine.hasTerm(f1));
         Trace("sets-cg-debug") << "...build for " << f1 << std::endl;
+        Assert(d_equalityEngine.hasTerm(f1));
         //break into index based on operator, and type of first argument (since some operators are parametric)
         TypeNode tn = f1[0].getType();
         std::vector< TNode > reps;
@@ -2146,6 +2147,30 @@ bool TheorySetsPrivate::propagate(TNode literal) {
   return ok;
 }/* TheorySetsPrivate::propagate(TNode) */
 
+void TheorySetsPrivate::processInference(Node lem,
+                                         const char* c,
+                                         std::vector<Node>& lemmas)
+{
+  Trace("sets-pinfer") << "Process inference: " << lem << std::endl;
+  if (lem.getKind() != IMPLIES || !isEntailed(lem[0], true))
+  {
+    Trace("sets-pinfer") << "  must assert as lemma" << std::endl;
+    lemmas.push_back(lem);
+    return;
+  }
+  // try to assert it as a fact
+  Trace("sets-pinfer") << "Process conclusion: " << lem[1] << std::endl;
+  Trace("sets-pinfer") << "  assert as fact" << std::endl;
+  assertInference(lem[1], lem[0], lemmas, c);
+}
+
+bool TheorySetsPrivate::isInConflict() const { return d_conflict.get(); }
+bool TheorySetsPrivate::sentLemma() const { return d_sentLemma; }
+
+OutputChannel* TheorySetsPrivate::getOutputChannel()
+{
+  return d_external.d_out;
+}
 
 void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 3014b2f2aefdd9a84c4289b536495c41784caaa5..cb3189e81a1e398cd63a53f3736bfe4686297196 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -22,6 +22,7 @@
 #include "context/cdhashset.h"
 #include "context/cdqueue.h"
 #include "expr/node_trie.h"
+#include "theory/sets/skolem_cache.h"
 #include "theory/sets/theory_sets_rels.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -69,9 +70,7 @@ private:
   void checkDisequalities( std::vector< Node >& lemmas );
   bool isMember( Node x, Node s );
   bool isSetDisequalityEntailed( Node s, Node t );
-  
-  void flushLemmas( std::vector< Node >& lemmas, bool preprocess = false );
-  void flushLemma( Node lem, bool preprocess = false );
+
   Node getProxy( Node n );
   Node getCongruent( Node n );
   Node getEmptySet( TypeNode tn );
@@ -222,6 +221,12 @@ private: //for universe set
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+  /**
+   * Get the skolem cache of this theory, which manages a database of introduced
+   * skolem variables used for various inferences.
+   */
+  SkolemCache& getSkolemCache() { return d_skCache; }
+
   void preRegisterTerm(TNode node);
 
   /** expandDefinition
@@ -262,7 +267,38 @@ private: //for universe set
 
   void propagate(Theory::Effort);
 
-private:
+  /** Process inference
+   *
+   * Argument lem specifies an inference inferred by this theory. If lem is
+   * an IMPLIES node, then its antecendant is the explanation of the conclusion.
+   *
+   * Argument c is used for debugging, typically the name of the inference.
+   *
+   * This method may add facts to the equality engine of theory of sets.
+   * Any (portion of) the conclusion of lem that is not sent to the equality
+   * engine is added to the argument lemmas, which should be processed via the
+   * caller of this method.
+   */
+  void processInference(Node lem, const char* c, std::vector<Node>& lemmas);
+  /** Flush lemmas
+   *
+   * This sends lemmas on the output channel of the theory of sets.
+   *
+   * The argument preprocess indicates whether preprocessing should be applied
+   * (by TheoryEngine) on each of lemmas.
+   */
+  void flushLemmas(std::vector<Node>& lemmas, bool preprocess = false);
+  /** singular version of above */
+  void flushLemma(Node lem, bool preprocess = false);
+  /** Are we currently in conflict? */
+  bool isInConflict() const;
+  /** Have we sent out a lemma during a call to a full effort check? */
+  bool sentLemma() const;
+
+  /** get default output channel */
+  OutputChannel* getOutputChannel();
+
+ private:
   TheorySets& d_external;
 
   class Statistics {
@@ -321,6 +357,8 @@ public:
  private:
   /** subtheory solver for the theory of relations */
   std::unique_ptr<TheorySetsRels> d_rels;
+  /** the skolem cache */
+  SkolemCache d_skCache;
   /** are relations enabled?
    *
    * This flag is set to true during a full effort check if any constraint

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 74d0e5bd83bf53f66b8ded06940051060f432155..2bbaa3bc8b3d5d2ba5af05ab68508ddad05fe94d 100644 (file)
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -20,6 +20,7 @@
 #include "theory/sets/theory_sets.h"
 
 using namespace std;
+using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
@@ -31,19 +32,45 @@ typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator
 typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator               TERM_IT;
 typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator   TC_IT;
 
-  void TheorySetsRels::check(Theory::Effort level) {
-    Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver, effort = " << level << " *******************************\n" << std::endl;
-    if(Theory::fullEffort(level)) {
-      collectRelsInfo();
-      check();
-      doPendingLemmas();
-      Assert( d_lemmas_out.empty() );
-      Assert( d_pending_facts.empty() );
-    } else {
-      doPendingMerge();
-    }
-    Trace("rels") << "\n[sets-rels] ******************************* Done with the relational solver *******************************\n" << std::endl;
+TheorySetsRels::TheorySetsRels(context::Context* c,
+                               context::UserContext* u,
+                               eq::EqualityEngine* eq,
+                               TheorySetsPrivate& set)
+    : d_eqEngine(eq),
+      d_sets_theory(set),
+      d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)),
+      d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)),
+      d_shared_terms(u),
+      d_satContext(c)
+{
+  d_eqEngine->addFunctionKind(PRODUCT);
+  d_eqEngine->addFunctionKind(JOIN);
+  d_eqEngine->addFunctionKind(TRANSPOSE);
+  d_eqEngine->addFunctionKind(TCLOSURE);
+  d_eqEngine->addFunctionKind(JOIN_IMAGE);
+  d_eqEngine->addFunctionKind(IDEN);
+  d_eqEngine->addFunctionKind(APPLY_CONSTRUCTOR);
+}
+
+TheorySetsRels::~TheorySetsRels() {}
+
+void TheorySetsRels::check(Theory::Effort level)
+{
+  Trace("rels") << "\n[sets-rels] ******************************* Start the "
+                   "relational solver, effort = "
+                << level << " *******************************\n"
+                << std::endl;
+  if (Theory::fullEffort(level))
+  {
+    collectRelsInfo();
+    check();
+    doPendingInfers();
   }
+  Assert(d_pending.empty());
+  Trace("rels") << "\n[sets-rels] ******************************* Done with "
+                   "the relational solver *******************************\n"
+                << std::endl;
+}
 
   void TheorySetsRels::check() {
     MEM_IT m_it = d_rReps_memberReps_cache.begin();
@@ -54,41 +81,42 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
       for(unsigned int i = 0; i < m_it->second.size(); i++) {
         Node    mem     = d_rReps_memberReps_cache[rel_rep][i];
         Node    exp     = d_rReps_memberReps_exp_cache[rel_rep][i];
-        std::map<kind::Kind_t, std::vector<Node> >    kind_terms      = d_terms_cache[rel_rep];
+        std::map<kind::Kind_t, std::vector<Node> >& kind_terms =
+            d_terms_cache[rel_rep];
 
         if( kind_terms.find(kind::TRANSPOSE) != kind_terms.end() ) {
-          std::vector<Node> tp_terms = kind_terms[kind::TRANSPOSE];
+          std::vector<Node>& tp_terms = kind_terms[TRANSPOSE];
           if( tp_terms.size() > 0 ) {
             applyTransposeRule( tp_terms );
             applyTransposeRule( tp_terms[0], rel_rep, exp );
           }
         }
         if( kind_terms.find(kind::JOIN) != kind_terms.end() ) {
-          std::vector<Node> join_terms = kind_terms[kind::JOIN];
+          std::vector<Node>& join_terms = kind_terms[JOIN];
           for( unsigned int j = 0; j < join_terms.size(); j++ ) {
             applyJoinRule( join_terms[j], rel_rep, exp );
           }
         }
         if( kind_terms.find(kind::PRODUCT) != kind_terms.end() ) {
-          std::vector<Node> product_terms = kind_terms[kind::PRODUCT];
+          std::vector<Node>& product_terms = kind_terms[PRODUCT];
           for( unsigned int j = 0; j < product_terms.size(); j++ ) {
             applyProductRule( product_terms[j], rel_rep, exp );
           }
         }
         if( kind_terms.find(kind::TCLOSURE) != kind_terms.end() ) {
-          std::vector<Node> tc_terms = kind_terms[kind::TCLOSURE];
+          std::vector<Node>& tc_terms = kind_terms[TCLOSURE];
           for( unsigned int j = 0; j < tc_terms.size(); j++ ) {
             applyTCRule( mem, tc_terms[j], rel_rep, exp );
           }
         }
         if( kind_terms.find(kind::JOIN_IMAGE) != kind_terms.end() ) {
-          std::vector<Node> join_image_terms = kind_terms[kind::JOIN_IMAGE];
+          std::vector<Node>& join_image_terms = kind_terms[JOIN_IMAGE];
           for( unsigned int j = 0; j < join_image_terms.size(); j++ ) {
             applyJoinImageRule( mem, join_image_terms[j], exp );
           }
         }
         if( kind_terms.find(kind::IDEN) != kind_terms.end() ) {
-          std::vector<Node> iden_terms = kind_terms[kind::IDEN];
+          std::vector<Node>& iden_terms = kind_terms[IDEN];
           for( unsigned int j = 0; j < iden_terms.size(); j++ ) {
             applyIdenRule( mem, iden_terms[j], exp );
           }
@@ -141,6 +169,17 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
       t_it++;
     }
     doTCInference();
+
+    // clean up
+    d_tuple_reps.clear();
+    d_rReps_memberReps_exp_cache.clear();
+    d_terms_cache.clear();
+    d_membership_trie.clear();
+    d_rel_nodes.clear();
+    d_rReps_memberReps_cache.clear();
+    d_rRep_tcGraph.clear();
+    d_tcr_tcGraph_exps.clear();
+    d_tcr_tcGraph.clear();
   }
 
   /*
@@ -154,6 +193,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
       Node                      eqc_rep  = (*eqcs_i);
       eq::EqClassIterator       eqc_i   = eq::EqClassIterator( eqc_rep, d_eqEngine );
 
+      TypeNode erType = eqc_rep.getType();
       Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << " with type " << eqc_rep.getType() << std::endl;
 
       while( !eqc_i.isFinished() ){
@@ -161,9 +201,8 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
 
         Trace("rels-ee") << "  term : " << eqc_node << std::endl;
 
-        if( getRepresentative(eqc_rep) == getRepresentative(d_trueNode) ||
-            getRepresentative(eqc_rep) == getRepresentative(d_falseNode) ) {
-
+        if (erType.isBoolean() && eqc_rep.isConst())
+        {
           // collect membership info
           if( eqc_node.getKind() == kind::MEMBER && eqc_node[1].getType().getSetElementType().isTuple()) {
             Node tup_rep = getRepresentative( eqc_node[0] );
@@ -173,19 +212,21 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
               reduceTupleVar( eqc_node );
             }
 
-            bool is_true_eq    = areEqual( eqc_rep, d_trueNode );
+            bool is_true_eq = eqc_rep.getConst<bool>();
             Node reason        = is_true_eq ? eqc_node : eqc_node.negate();
 
             if( is_true_eq ) {
               if( safelyAddToMap(d_rReps_memberReps_cache, rel_rep, tup_rep) ) {
-                addToMap(d_rReps_memberReps_exp_cache, rel_rep, reason);
+                d_rReps_memberReps_exp_cache[rel_rep].push_back(reason);
                 computeTupleReps(tup_rep);
                 d_membership_trie[rel_rep].addTerm(tup_rep, d_tuple_reps[tup_rep]);
               }
             }
           }
         // collect relational terms info
-        } else if( eqc_rep.getType().isSet() && eqc_rep.getType().getSetElementType().isTuple() ) {
+        }
+        else if (erType.isSet() && erType.getSetElementType().isTuple())
+        {
           if( eqc_node.getKind() == kind::TRANSPOSE || eqc_node.getKind() == kind::JOIN ||
               eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE ||
               eqc_node.getKind() == kind::JOIN_IMAGE || eqc_node.getKind() == kind::IDEN ) {
@@ -209,8 +250,11 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
             }
           }
         // need to add all tuple elements as shared terms
-        } else if( eqc_node.getType().isTuple() && !eqc_node.isConst() && !eqc_node.isVar() ) {
-          for( unsigned int i = 0; i < eqc_node.getType().getTupleLength(); i++ ) {
+        }
+        else if (erType.isTuple() && !eqc_node.isConst() && !eqc_node.isVar())
+        {
+          for (unsigned i = 0, tlen = erType.getTupleLength(); i < tlen; i++)
+          {
             Node element = RelsUtils::nthElementOfTuple( eqc_node, i );
 
             if( !element.isConst() ) {
@@ -238,6 +282,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     if( rel_mem_it == d_rReps_memberReps_cache.end() ) {
       return;
     }
+    NodeManager* nm = NodeManager::currentNM();
 
     Node join_image_rel = join_image_term[0];
     std::unordered_set< Node, NodeHashFunction > hasChecked;
@@ -262,7 +307,8 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
                                                              NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR,
                                                                                                Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ),
                                                              join_image_term);
-      if( holds( new_membership ) ) {
+      if (d_sets_theory.isEntailed(new_membership, true))
+      {
         ++mem_rep_it;
         ++mem_rep_exp_it;
         continue;
@@ -302,7 +348,10 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
                 new_membership = NodeManager::currentNM()->mkNode( kind::OR, new_membership, NodeManager::currentNM()->mkNode( kind::NOT, NodeManager::currentNM()->mkNode( kind::DISTINCT, existing_members ) ));
               }
               Assert(reasons.size() >= 1);
-              sendInfer( new_membership, reasons.size() > 1 ? NodeManager::currentNM()->mkNode( kind::AND, reasons) : reasons[0], "JOIN-IMAGE UP" );
+              sendInfer(
+                  new_membership,
+                  reasons.size() > 1 ? nm->mkNode(AND, reasons) : reasons[0],
+                  "JOIN-IMAGE UP");
               break;
             }
           }
@@ -359,7 +408,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     if( distinct_skolems.size() >= 2 ) {
       conclusion =  NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) );
     }
-    sendInfer( conclusion, reason, "JOIN-IMAGE DOWN" );
+    sendInfer(conclusion, reason, "JOIN-IMAGE DOWN");
     Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl;
 
   }
@@ -374,6 +423,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
   void TheorySetsRels::applyIdenRule( Node mem_rep, Node iden_term, Node exp) {
     Trace("rels-debug") << "\n[Theory::Rels] *********** applyIdenRule on " << iden_term
                         << " with mem_rep = " << mem_rep  << " and exp = " << exp << std::endl;
+    NodeManager* nm = NodeManager::currentNM();
     if( d_rel_nodes.find( iden_term ) == d_rel_nodes.end() ) {
       computeMembersForIdenTerm( iden_term );
       d_rel_nodes.insert( iden_term );
@@ -387,7 +437,9 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     if( exp[1] != iden_term ) {
       reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], iden_term ) );
     }
-    sendInfer( NodeManager::currentNM()->mkNode( kind::AND, fact, NodeManager::currentNM()->mkNode( kind::EQUAL, fst_mem, snd_mem ) ), reason, "IDENTITY-DOWN" );
+    sendInfer(nm->mkNode(AND, fact, nm->mkNode(EQUAL, fst_mem, snd_mem)),
+              reason,
+              "IDENTITY-DOWN");
     Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyIdenRule on " << iden_term << std::endl;
   }
 
@@ -405,6 +457,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     if( d_rReps_memberReps_cache.find( iden_term_rel_rep ) == d_rReps_memberReps_cache.end() ) {
       return;
     }
+    NodeManager* nm = NodeManager::currentNM();
 
     MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( iden_term_rel_rep );
     std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin();
@@ -417,7 +470,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
       if( (*mem_rep_exp_it)[1] != iden_term_rel ) {
         reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it)[1], iden_term_rel ) );
       }
-      sendInfer( NodeManager::currentNM()->mkNode( kind::MEMBER, new_mem, iden_term ), reason, "IDENTITY-UP" );
+      sendInfer(nm->mkNode(MEMBER, new_mem, iden_term), reason, "IDENTITY-UP");
       ++mem_rep_exp_it;
     }
     Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for Iden Term = " << iden_term << std::endl;
@@ -513,10 +566,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
                                                      (NodeManager::currentNM()->mkNode(kind::OR, sk_eq, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, sk_1, sk_2), tc_rel))))))));
 
     Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, conclusion );
-    std::vector< Node > require_phase;
-    require_phase.push_back(Rewriter::rewrite(mem_of_r));
-    require_phase.push_back(Rewriter::rewrite(sk_eq));
-    d_tc_lemmas_last[tc_lemma] = require_phase;
+    d_pending.push_back(tc_lemma);
   }
 
   bool TheorySetsRels::isTCReachable( Node mem_rep, Node tc_rel ) {
@@ -617,6 +667,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
 
   void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
                                        std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) {
+    NodeManager* nm = NodeManager::currentNM();
     Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) );
     std::vector< Node > all_reasons( reasons );
 
@@ -634,9 +685,13 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
       all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel[0], reasons.back()[1]) );
     }
     if( all_reasons.size() > 1) {
-      sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tc_mem, tc_rel), NodeManager::currentNM()->mkNode(kind::AND, all_reasons), "TCLOSURE-Forward");
+      sendInfer(nm->mkNode(MEMBER, tc_mem, tc_rel),
+                nm->mkNode(AND, all_reasons),
+                "TCLOSURE-Forward");
     } else {
-      sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tc_mem, tc_rel), all_reasons.front(), "TCLOSURE-Forward");
+      sendInfer(nm->mkNode(MEMBER, tc_mem, tc_rel),
+                all_reasons.front(),
+                "TCLOSURE-Forward");
     }
 
     // check if cur_node has been traversed or not
@@ -706,8 +761,8 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     if( pt_rel != exp[1] ) {
       reason = NodeManager::currentNM()->mkNode(kind::AND, exp, NodeManager::currentNM()->mkNode(kind::EQUAL, pt_rel, exp[1]));
     }
-    sendInfer( fact_1, reason, "product-split" );
-    sendInfer( fact_2, reason, "product-split" );
+    sendInfer(fact_1, reason, "product-split");
+    sendInfer(fact_2, reason, "product-split");
   }
 
   /* join-split rule:           (a, b) IS_IN (X JOIN Y)
@@ -738,7 +793,8 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     Node r1_rep = getRepresentative(join_rel[0]);
     Node r2_rep = getRepresentative(join_rel[1]);
     TypeNode     shared_type    = r2_rep.getType().getSetElementType().getTupleTypes()[0];
-    Node         shared_x       = NodeManager::currentNM()->mkSkolem("srj_", shared_type);
+    Node shared_x = d_sets_theory.getSkolemCache().mkTypedSkolemCached(
+        shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj");
     Datatype     dt             = join_rel[0].getType().getSetElementType().getDatatype();
     unsigned int s1_len         = join_rel[0].getType().getSetElementType().getTupleLength();
     unsigned int tup_len        = join_rel.getType().getSetElementType().getTupleLength();
@@ -776,9 +832,9 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
       reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, join_rel, exp[1]));
     }
     Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem1, join_rel[0]);
-    sendInfer( fact, reason, "JOIN-Split" );
+    sendInfer(fact, reason, "JOIN-Split-1");
     fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, join_rel[1]);
-    sendInfer( fact, reason, "JOIN-Split" );
+    sendInfer(fact, reason, "JOIN-Split-2");
     makeSharedTerm( shared_x );
   }
 
@@ -796,9 +852,12 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     if( tp_terms.size() < 1) {
       return;
     }
+    NodeManager* nm = NodeManager::currentNM();
     for( unsigned int i = 1; i < tp_terms.size(); i++ ) {
       Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE-Equal rule on transposed term = " << tp_terms[0] << " and " << tp_terms[i] << std::endl;
-      sendInfer(NodeManager::currentNM()->mkNode(kind::EQUAL, tp_terms[0][0], tp_terms[i][0]), NodeManager::currentNM()->mkNode(kind::EQUAL, tp_terms[0], tp_terms[i]), "TRANSPOSE-Equal");
+      sendInfer(nm->mkNode(EQUAL, tp_terms[0][0], tp_terms[i][0]),
+                nm->mkNode(EQUAL, tp_terms[0], tp_terms[i]),
+                "TRANSPOSE-Equal");
     }
   }
 
@@ -806,6 +865,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE rule on transposed term = " << tp_rel
                         << ", its representative = " << tp_rel_rep
                         << " with explanation = " << exp << std::endl;
+    NodeManager* nm = NodeManager::currentNM();
 
     if(d_rel_nodes.find( tp_rel ) == d_rel_nodes.end()) {
       Trace("rels-debug") <<  "\n[Theory::Rels] Apply TRANSPOSE-Compose rule on term: " << tp_rel
@@ -821,7 +881,9 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     if( tp_rel != exp[1] ) {
       reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tp_rel, exp[1]));
     }
-    sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, reversed_mem, tp_rel[0]), reason, "TRANSPOSE-Reverse" );
+    sendInfer(nm->mkNode(MEMBER, reversed_mem, tp_rel[0]),
+              reason,
+              "TRANSPOSE-Reverse");
   }
 
   void TheorySetsRels::doTCInference() {
@@ -892,8 +954,12 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     }
 
     Node rel0_rep  = getRepresentative(rel[0]);
-    if(d_rReps_memberReps_cache.find( rel0_rep ) == d_rReps_memberReps_cache.end())
+    if (d_rReps_memberReps_cache.find(rel0_rep)
+        == d_rReps_memberReps_cache.end())
+    {
       return;
+    }
+    NodeManager* nm = NodeManager::currentNM();
 
     std::vector<Node>   members = d_rReps_memberReps_cache[rel0_rep];
     std::vector<Node>   exps    = d_rReps_memberReps_exp_cache[rel0_rep];
@@ -906,7 +972,9 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
         if( rel[0] != exps[i][1] ) {
           reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, rel[0], exps[i][1]));
         }
-        sendInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel), reason, "TRANSPOSE-reverse");
+        sendInfer(nm->mkNode(MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel),
+                  reason,
+                  "TRANSPOSE-reverse");
       }
     }
   }
@@ -927,6 +995,7 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
        d_rReps_memberReps_cache.find( r2_rep ) == d_rReps_memberReps_cache.end() ) {
       return;
     }
+    NodeManager* nm = NodeManager::currentNM();
 
     std::vector<Node> r1_rep_exps = d_rReps_memberReps_exp_cache[r1_rep];
     std::vector<Node> r2_rep_exps = d_rReps_memberReps_exp_cache[r2_rep];
@@ -971,12 +1040,14 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
             reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r2, r2_rep_exps[j][1]) );
           }
           if( isProduct ) {
-            sendInfer( fact, NodeManager::currentNM()->mkNode(kind::AND, reasons), "PRODUCT-Compose" );
+            sendInfer(fact,
+                      nm->mkNode(kind::AND, reasons),
+                      "PRODUCT-Compose");
           } else {
             if( r1_rmost != r2_lmost ) {
               reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1_rmost, r2_lmost) );
             }
-            sendInfer( fact, NodeManager::currentNM()->mkNode(kind::AND, reasons), "JOIN-Compose" );
+            sendInfer(fact, nm->mkNode(kind::AND, reasons), "JOIN-Compose");
           }
         }
       }
@@ -984,104 +1055,33 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
 
   }
 
-  void TheorySetsRels::doPendingLemmas() {
-    Trace("rels-debug") << "[Theory::Rels] **************** Start doPendingLemmas !" << std::endl;
-    if( !(*d_conflict) ){
-      if ( (!d_lemmas_out.empty() || !d_pending_facts.empty()) ) {
-        for( unsigned i=0; i < d_lemmas_out.size(); i++ ){
-          Assert(d_lemmas_out[i].getKind() == kind::IMPLIES);
-          if(holds( d_lemmas_out[i][1] )) {
-            Trace("rels-lemma-skip") << "[sets-rels-lemma-skip] Skip an already held lemma: "
-                                     << d_lemmas_out[i]<< std::endl;
-            continue;
-          }
-          d_sets_theory.d_out->lemma( d_lemmas_out[i] );
-          Trace("rels-lemma") << "[sets-rels-lemma] Send out a lemma : "
-                              << d_lemmas_out[i] << std::endl;
-        }
-        for( std::map<Node, Node>::iterator pending_it = d_pending_facts.begin();
-             pending_it != d_pending_facts.end(); pending_it++ ) {
-          if( holds( pending_it->first ) ) {
-            Trace("rels-lemma-skip") << "[sets-rels-fact-lemma-skip] Skip an already held fact,: "
-                                     << pending_it->first << std::endl;
-            continue;
-          }
-          Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, pending_it->second, pending_it->first);
-          if( d_lemmas_produced.find( lemma ) == d_lemmas_produced.end() ) {
-            d_sets_theory.d_out->lemma(NodeManager::currentNM()->mkNode(kind::IMPLIES, pending_it->second, pending_it->first));
-            Trace("rels-lemma") << "[sets-rels-fact-lemma] Send out a fact as lemma : "
-                                << pending_it->first << " with reason " << pending_it->second << std::endl;
-            d_lemmas_produced.insert( lemma );
-          }
+  void TheorySetsRels::doPendingInfers()
+  {
+    // process the inferences in d_pending
+    if (!d_sets_theory.isInConflict())
+    {
+      std::vector<Node> lemmas;
+      for (const Node& p : d_pending)
+      {
+        d_sets_theory.processInference(p, "rels", lemmas);
+        if (d_sets_theory.isInConflict())
+        {
+          break;
         }
       }
+      // if we are still not in conflict, send lemmas
+      if (!d_sets_theory.isInConflict())
+      {
+        d_sets_theory.flushLemmas(lemmas);
+      }
     }
-    doTCLemmas();
-    Trace("rels-debug") << "[Theory::Rels] **************** Done with doPendingLemmas !" << std::endl;
-    d_tuple_reps.clear();
-    d_rReps_memberReps_exp_cache.clear();
-    d_terms_cache.clear();
-    d_lemmas_out.clear();
-    d_membership_trie.clear();
-    d_rel_nodes.clear();
-    d_pending_facts.clear();
-    d_rReps_memberReps_cache.clear();
-    d_rRep_tcGraph.clear();
-    d_tcr_tcGraph_exps.clear();
-    d_tcr_tcGraph.clear();
-    d_tc_lemmas_last.clear();
+    d_pending.clear();
   }
 
-
   bool TheorySetsRels::isRelationKind( Kind k ) {
     return k == kind::TRANSPOSE || k == kind::PRODUCT || k == kind::JOIN || k == kind::TCLOSURE;
   }
 
-  void TheorySetsRels::doTCLemmas() {
-    Trace("rels-debug") << "[Theory::Rels] **************** Start doTCLemmas !" << std::endl;
-    std::map< Node, std::vector< Node > >::iterator tc_lemma_it = d_tc_lemmas_last.begin();
-    while( tc_lemma_it != d_tc_lemmas_last.end() ) {
-      if( !holds( tc_lemma_it->first[1] ) ) {
-        if( d_lemmas_produced.find( tc_lemma_it->first ) == d_lemmas_produced.end() ) {
-          d_sets_theory.d_out->lemma( tc_lemma_it->first );
-          d_lemmas_produced.insert( tc_lemma_it->first );
-
-          for( unsigned int i = 0; i < (tc_lemma_it->second).size(); i++ ) {
-            if( (tc_lemma_it->second)[i] == d_falseNode ) {
-              d_sets_theory.d_out->requirePhase((tc_lemma_it->second)[i], true);
-            }
-          }
-          Trace("rels-lemma") << "[Theory::Rels] **** Send out a TC lemma = " << tc_lemma_it->first << " by " << "TCLOSURE-Forward"<< std::endl;
-        }
-      }
-      ++tc_lemma_it;
-    }
-    Trace("rels-debug") << "[Theory::Rels] **************** Done with doTCLemmas !" << std::endl;
-  }
-
-  void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) {
-    if( !holds( conc ) ) {
-      Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
-      if( d_lemmas_produced.find( lemma ) == d_lemmas_produced.end() ) {
-        d_lemmas_out.push_back( lemma );
-        d_lemmas_produced.insert( lemma );
-        Trace("rels-send-lemma") << "[Theory::Rels] **** Generate a lemma conclusion = " << conc << " with reason = " << ant << " by " << c << std::endl;
-      }
-    }
-  }
-
-  void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) {
-    if( !holds( fact ) ) {
-      Trace("rels-send-lemma") << "[Theory::Rels] **** Generate an infered fact "
-                               << fact << " with reason " << exp << " by "<< c << std::endl;
-      d_pending_facts[fact] = exp;
-    } else {
-      Trace("rels-send-lemma-debug") << "[Theory::Rels] **** Generate an infered fact "
-                                     << fact << " with reason " << exp << " by "<< c
-                                     << ", but it holds already, thus skip it!" << std::endl;
-    }
-  }
-
   Node TheorySetsRels::getRepresentative( Node t ) {
     if( d_eqEngine->hasTerm( t ) ){
       return d_eqEngine->getRepresentative( t );
@@ -1138,37 +1138,19 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     return false;
   }
 
-  void TheorySetsRels::addToMap(std::map< Node, std::vector<Node> >& map, Node rel_rep, Node member) {
-    if(map.find(rel_rep) == map.end()) {
-      std::vector<Node> members;
-      members.push_back(member);
-      map[rel_rep] = members;
-    } else {
-      map[rel_rep].push_back(member);
-    }
-  }
-
-  void TheorySetsRels::addSharedTerm( TNode n ) {
-    Trace("rels-debug") << "[sets-rels] Add a shared term:  " << n << std::endl;
-    d_sets_theory.addSharedTerm(n);
-    d_eqEngine->addTriggerTerm(n, THEORY_SETS);
-  }
-
   void TheorySetsRels::makeSharedTerm( Node n ) {
-    Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl;
     if(d_shared_terms.find(n) == d_shared_terms.end()) {
+      Trace("rels-share") << " [sets-rels] making shared term " << n
+                          << std::endl;
       Node skolem = NodeManager::currentNM()->mkSkolem( "sts", NodeManager::currentNM()->mkSetType( n.getType() ) );
-      sendLemma(skolem.eqNode(NodeManager::currentNM()->mkNode(kind::SINGLETON,n)), d_trueNode, "share-term");
+      Node skEq =
+          skolem.eqNode(NodeManager::currentNM()->mkNode(kind::SINGLETON, n));
+      // force lemma to be sent immediately
+      d_sets_theory.getOutputChannel()->lemma(skEq);
       d_shared_terms.insert(n);
     }
   }
 
-  bool TheorySetsRels::holds(Node node) {
-    bool polarity       = node.getKind() != kind::NOT;
-    Node atom           = polarity ? node : node[0];
-    return d_sets_theory.isEntailed( atom, polarity );
-  }
-
   /*
    * For each tuple n, we store a mapping between n and a list of its elements representatives
    * in d_tuple_reps. This would later be used for applying JOIN operator.
@@ -1198,42 +1180,11 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
       Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
       tuple_reduct = NodeManager::currentNM()->mkNode(kind::MEMBER,tuple_reduct, n[1]);
       Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::EQUAL, n, tuple_reduct);
-      sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction");
+      sendInfer(tuple_reduction_lemma, d_trueNode, "tuple-reduction");
       d_symbolic_tuples.insert(n);
     }
   }
 
-  TheorySetsRels::TheorySetsRels( context::Context* c,
-                                  context::UserContext* u,
-                                  eq::EqualityEngine* eq,
-                                  context::CDO<bool>* conflict,
-                                  TheorySets& d_set ):
-    d_eqEngine(eq),
-    d_conflict(conflict),
-    d_sets_theory(d_set),
-    d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)),
-    d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)),
-    d_pending_merge(c),
-    d_lemmas_produced(u),
-    d_shared_terms(u)
-  {
-    d_eqEngine->addFunctionKind(kind::PRODUCT);
-    d_eqEngine->addFunctionKind(kind::JOIN);
-    d_eqEngine->addFunctionKind(kind::TRANSPOSE);
-    d_eqEngine->addFunctionKind(kind::TCLOSURE);
-    d_eqEngine->addFunctionKind(kind::JOIN_IMAGE);
-    d_eqEngine->addFunctionKind(kind::IDEN);
-  }
-
-  TheorySetsRels::~TheorySetsRels() {
-    for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end();
-        i != iend; ++i){
-      EqcInfo* current = (*i).second;
-      Assert(current != NULL);
-      delete current;
-    }
-  }
-
   std::vector<Node> TupleTrie::findTerms( std::vector< Node >& reps, int argIndex ) {
     std::vector<Node>                           nodes;
     std::map< Node, TupleTrie >::iterator       it;
@@ -1317,368 +1268,12 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     }
   }
 
-  TheorySetsRels::EqcInfo::EqcInfo( context::Context* c ) :
-  d_mem(c), d_mem_exp(c), d_tp(c), d_pt(c), d_tc(c), d_rel_tc(c) {}
-
-  void TheorySetsRels::eqNotifyNewClass( Node n ) {
-    Trace("rels-std") << "[sets-rels] eqNotifyNewClass:" << " t = " << n << std::endl;
-    if(n.getKind() == kind::TRANSPOSE || n.getKind() == kind::PRODUCT || n.getKind() == kind::TCLOSURE) {
-      getOrMakeEqcInfo( n, true );
-      if( n.getKind() == kind::TCLOSURE ) {
-        Node relRep_of_tc = getRepresentative( n[0] );
-        EqcInfo*  rel_ei = getOrMakeEqcInfo( relRep_of_tc, true );
-
-        if( rel_ei->d_rel_tc.get().isNull() ) {
-          rel_ei->d_rel_tc = n;
-          Node exp = relRep_of_tc == n[0] ? d_trueNode : NodeManager::currentNM()->mkNode( kind::EQUAL, relRep_of_tc, n[0] );
-          for( NodeSet::const_iterator mem_it = rel_ei->d_mem.begin(); mem_it != rel_ei->d_mem.end(); mem_it++ ) {
-            Node mem_exp = (*rel_ei->d_mem_exp.find(*mem_it)).second;
-            exp = NodeManager::currentNM()->mkNode( kind::AND, exp, mem_exp);
-            if( mem_exp[1] != relRep_of_tc ) {
-              exp = NodeManager::currentNM()->mkNode( kind::AND, exp, NodeManager::currentNM()->mkNode(kind::EQUAL, relRep_of_tc, mem_exp[1] ) );
-            }
-            sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, mem_exp[0], n), exp, "TCLOSURE-UP I" );
-          }
-        }
-      }
-    }
-  }
-
-  // Merge t2 into t1, t1 will be the rep of the new eqc
-  void TheorySetsRels::eqNotifyPostMerge( Node t1, Node t2 ) {
-    Trace("rels-std") << "[sets-rels-std] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
-
-    // Merge membership constraint with "true" eqc
-    if( t1 == d_trueNode && t2.getKind() == kind::MEMBER && t2[0].getType().isTuple() ) {
-      Node      mem_rep  = getRepresentative( t2[0] );
-      Node      t2_1rep  = getRepresentative( t2[1] );
-      EqcInfo*  ei       = getOrMakeEqcInfo( t2_1rep, true );
-      if(ei->d_mem.contains(mem_rep)) {
-        return;
-      }
-      Node exp = t2;
-
-      ei->d_mem.insert( mem_rep );
-      ei->d_mem_exp.insert( mem_rep, exp );
-
-      // Process a membership constraint that a tuple is a member of transpose of rel
-      if( !ei->d_tp.get().isNull() ) {
-        if( ei->d_tp.get() != t2[1] ) {
-          exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_tp.get(), t2[1]), t2 );
-        }
-        sendInferTranspose( t2[0], ei->d_tp.get(), exp );
-      }
-      // Process a membership constraint that a tuple is a member of product of rel
-      if( !ei->d_pt.get().isNull() ) {
-        if( ei->d_pt.get() != t2[1] ) {
-          exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_pt.get(), t2[1]), t2 );
-        }
-        sendInferProduct( t2[0], ei->d_pt.get(), exp );
-      }
-
-      if( !ei->d_rel_tc.get().isNull() ) {
-        if( ei->d_rel_tc.get()[0] != t2[1] ) {
-          exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_rel_tc.get()[0], t2[1]), t2 );
-        }
-        sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t2[0], ei->d_rel_tc.get()), exp, "TCLOSURE-UP I");
-      }
-      // Process a membership constraint that a tuple is a member of transitive closure of rel
-      if( !ei->d_tc.get().isNull() ) {
-        sendInferTClosure( t2, ei );
-      }
-
-    // Merge two relation eqcs
-    } else if( t1.getType().isSet() && t2.getType().isSet() && t1.getType().getSetElementType().isTuple() ) {
-      EqcInfo* t1_ei = getOrMakeEqcInfo( t1 );
-      EqcInfo* t2_ei = getOrMakeEqcInfo( t2 );
-
-      if( t1_ei != NULL && t2_ei != NULL ) {
-        if( !t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) {
-          sendInferTranspose(t1_ei->d_tp.get(), t2_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::EQUAL, t1_ei->d_tp.get(), t2_ei->d_tp.get() ) );
-        }
-        std::vector< Node > t2_new_mems;
-        std::vector< Node > t2_new_exps;
-        NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin();
-        NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin();
-
-        for( ; t2_mem_it != t2_ei->d_mem.end(); t2_mem_it++ ) {
-          if( !t1_ei->d_mem.contains( *t2_mem_it ) ) {
-            Node t2_mem_exp = (*t2_ei->d_mem_exp.find(*t2_mem_it)).second;
-
-            if( t2_ei->d_tp.get().isNull() && !t1_ei->d_tp.get().isNull() ) {
-              Node reason = t1_ei->d_tp.get() == (t2_mem_exp)[1]
-                            ? (t2_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t2_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_mem_exp)[1], t1_ei->d_tp.get()));
-              sendInferTranspose( t2_mem_exp[0], t1_ei->d_tp.get(), reason );
-            }
-            if( t2_ei->d_pt.get().isNull() && !t1_ei->d_pt.get().isNull() ) {
-              Node reason = t1_ei->d_pt.get() == (t2_mem_exp)[1]
-                            ? (t2_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t2_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_mem_exp)[1], t1_ei->d_pt.get()));
-              sendInferProduct( t2_mem_exp[0], t1_ei->d_pt.get(), reason );
-            }
-            if( t2_ei->d_tc.get().isNull() && !t1_ei->d_tc.get().isNull() ) {
-              sendInferTClosure( t2_mem_exp, t1_ei );
-            }
-            if( t2_ei->d_rel_tc.get().isNull() && !t1_ei->d_rel_tc.get().isNull() ) {
-              Node reason = t1_ei->d_rel_tc.get()[0] == t2_mem_exp[1] ?
-                            t2_mem_exp : NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, t1_ei->d_rel_tc.get()[0], t2_mem_exp[1]), t2_mem_exp );
-              sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t2_mem_exp[0], t1_ei->d_rel_tc.get()), reason, "TCLOSURE-UP I");
-            }
-            t2_new_mems.push_back( *t2_mem_it );
-            t2_new_exps.push_back( t2_mem_exp );
-          }
-        }
-        for( ; t1_mem_it != t1_ei->d_mem.end(); t1_mem_it++ ) {
-          if( !t2_ei->d_mem.contains( *t1_mem_it ) ) {
-            Node t1_mem_exp = (*t1_ei->d_mem_exp.find(*t1_mem_it)).second;
-            if( t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) {
-              Node reason = t2_ei->d_tp.get() == (t1_mem_exp)[1]
-                            ? (t1_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t1_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_mem_exp)[1], t2_ei->d_tp.get()));
-              sendInferTranspose( (t1_mem_exp)[0], t2_ei->d_tp.get(), reason );
-            }
-            if( t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) {
-              Node reason = t2_ei->d_pt.get() == (t1_mem_exp)[1]
-                            ? (t1_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t1_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_mem_exp)[1], t2_ei->d_pt.get()));
-              sendInferProduct( (t1_mem_exp)[0], t2_ei->d_pt.get(), reason );
-            }
-            if( t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) {
-              sendInferTClosure(t1_mem_exp, t2_ei );
-            }
-            if( t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) {
-              Node reason = t2_ei->d_rel_tc.get()[0] == t1_mem_exp[1] ?
-                            t1_mem_exp : NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, t2_ei->d_rel_tc.get()[0], t1_mem_exp[1]), t1_mem_exp );
-              sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t1_mem_exp[0], t2_ei->d_rel_tc.get()), reason, "TCLOSURE-UP I");
-            }
-          }
-        }
-        std::vector< Node >::iterator t2_new_mem_it = t2_new_mems.begin();
-        std::vector< Node >::iterator t2_new_exp_it = t2_new_exps.begin();
-        for( ; t2_new_mem_it != t2_new_mems.end(); t2_new_mem_it++, t2_new_exp_it++ ) {
-          t1_ei->d_mem.insert( *t2_new_mem_it );
-          t1_ei->d_mem_exp.insert( *t2_new_mem_it, *t2_new_exp_it );
-        }
-        if( t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) {
-          t1_ei->d_tp.set(t2_ei->d_tp.get());
-        }
-        if( t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) {
-          t1_ei->d_pt.set(t2_ei->d_pt.get());
-        }
-        if( t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) {
-          t1_ei->d_tc.set(t2_ei->d_tc.get());
-        }
-        if( t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) {
-          t1_ei->d_rel_tc.set(t2_ei->d_rel_tc.get());
-        }
-      } else if( t1_ei != NULL ) {
-        if( (t2.getKind() == kind::TRANSPOSE && t1_ei->d_tp.get().isNull()) ||
-            (t2.getKind() == kind::PRODUCT && t1_ei->d_pt.get().isNull()) ||
-            (t2.getKind() == kind::TCLOSURE && t1_ei->d_tc.get().isNull()) ) {
-          NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin();
-
-          if( t2.getKind() == kind::TRANSPOSE ) {
-            t1_ei->d_tp = t2;
-          } else if( t2.getKind() == kind::PRODUCT ) {
-            t1_ei->d_pt = t2;
-          } else if( t2.getKind() == kind::TCLOSURE ) {
-            t1_ei->d_tc = t2;
-          }
-          for( ; t1_mem_it != t1_ei->d_mem.end(); t1_mem_it++ ) {
-            Node t1_exp = (*t1_ei->d_mem_exp.find(*t1_mem_it)).second;
-            if( t2.getKind() == kind::TRANSPOSE ) {
-              Node reason = t2 == t1_exp[1]
-                            ? (t1_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t1_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_exp)[1], t2));
-              sendInferTranspose( (t1_exp)[0], t2, reason );
-            } else if( t2.getKind() == kind::PRODUCT ) {
-              Node reason = t2 == (t1_exp)[1]
-                            ? (t1_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t1_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_exp)[1], t2));
-              sendInferProduct( (t1_exp)[0], t2, reason );
-            } else if( t2.getKind() == kind::TCLOSURE ) {
-              sendInferTClosure( t1_exp, t1_ei );
-            }
-          }
-        }
-      } else if( t2_ei != NULL ) {
-        EqcInfo* new_t1_ei = getOrMakeEqcInfo( t1, true );
-        if( new_t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) {
-          new_t1_ei->d_tp.set(t2_ei->d_tp.get());
-        }
-        if( new_t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) {
-          new_t1_ei->d_pt.set(t2_ei->d_pt.get());
-        }
-        if( new_t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) {
-          new_t1_ei->d_tc.set(t2_ei->d_tc.get());
-        }
-        if( new_t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) {
-          new_t1_ei->d_rel_tc.set(t2_ei->d_rel_tc.get());
-        }
-        if( (t1.getKind() == kind::TRANSPOSE && t2_ei->d_tp.get().isNull()) ||
-            (t1.getKind() == kind::PRODUCT && t2_ei->d_pt.get().isNull()) ||
-            (t1.getKind() == kind::TCLOSURE && t2_ei->d_tc.get().isNull()) ) {
-          NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin();
-
-          for( ; t2_mem_it != t2_ei->d_mem.end(); t2_mem_it++ ) {
-            Node t2_exp = (*t1_ei->d_mem_exp.find(*t2_mem_it)).second;
-
-            if( t1.getKind() == kind::TRANSPOSE ) {
-              Node reason = t1 == (t2_exp)[1]
-                            ? (t2_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t2_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_exp)[1], t1));
-              sendInferTranspose( (t2_exp)[0], t1, reason );
-            } else if( t1.getKind() == kind::PRODUCT ) {
-              Node reason = t1 == (t2_exp)[1]
-                            ? (t2_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t2_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_exp)[1], t1));
-              sendInferProduct( (t2_exp)[0], t1, reason );
-            } else if( t1.getKind() == kind::TCLOSURE ) {
-              sendInferTClosure( t2_exp, new_t1_ei );
-            }
-          }
-        }
-      }
-    }
-
-    Trace("rels-std") << "[sets-rels] done with eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
-  }
-
-  void TheorySetsRels::sendInferTClosure( Node new_mem_exp, EqcInfo* ei ) {
-    NodeSet::const_iterator mem_it = ei->d_mem.begin();
-    Node mem_rep = getRepresentative( new_mem_exp[0] );
-    Node new_mem_rel = new_mem_exp[1];
-    Node new_mem_fst = RelsUtils::nthElementOfTuple( new_mem_exp[0], 0 );
-    Node new_mem_snd = RelsUtils::nthElementOfTuple( new_mem_exp[0], 1 );
-    for( ; mem_it != ei->d_mem.end(); mem_it++ ) {
-      if( *mem_it == mem_rep ) {
-        continue;
-      }
-      Node d_mem_exp = (*ei->d_mem_exp.find(*mem_it)).second;
-      Node d_mem_fst = RelsUtils::nthElementOfTuple( d_mem_exp[0], 0 );
-      Node d_mem_snd = RelsUtils::nthElementOfTuple( d_mem_exp[0], 1 );
-      Node d_mem_rel = d_mem_exp[1];
-      if( areEqual( new_mem_fst, d_mem_snd) ) {
-        Node reason = NodeManager::currentNM()->mkNode( kind::AND, new_mem_exp, d_mem_exp );
-        reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_fst, d_mem_snd ) );
-        if( new_mem_rel != ei->d_tc.get() ) {
-          reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_rel, ei->d_tc.get() ) );
-        }
-        if( d_mem_rel != ei->d_tc.get() ) {
-          reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, d_mem_rel, ei->d_tc.get() ) );
-        }
-        Node new_membership = NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( d_mem_rel, d_mem_fst, new_mem_snd ), ei->d_tc.get() );
-        sendMergeInfer( new_membership, reason, "TCLOSURE-UP II" );
-      }
-      if( areEqual( new_mem_snd, d_mem_fst ) ) {
-        Node reason = NodeManager::currentNM()->mkNode( kind::AND, new_mem_exp, d_mem_exp );
-        reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_snd, d_mem_fst ) );
-        if( new_mem_rel != ei->d_tc.get() ) {
-          reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_rel, ei->d_tc.get() ) );
-        }
-        if( d_mem_rel != ei->d_tc.get() ) {
-          reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, d_mem_rel, ei->d_tc.get() ) );
-        }
-        Node new_membership = NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( d_mem_rel, new_mem_fst, d_mem_snd ), ei->d_tc.get() );
-        sendMergeInfer( new_membership, reason, "TCLOSURE-UP II" );
-      }
-    }
-  }
-
-
-  void TheorySetsRels::doPendingMerge() {
-    for( NodeList::const_iterator itr = d_pending_merge.begin(); itr != d_pending_merge.end(); itr++ ) {
-      if( !holds(*itr) ) {
-        if( d_lemmas_produced.find(*itr)==d_lemmas_produced.end() ) {
-          Trace("rels-std-lemma") << "[std-sets-rels-lemma] Send out a merge fact as lemma: "
-                              << *itr << std::endl;
-          d_sets_theory.d_out->lemma( *itr );
-          d_lemmas_produced.insert(*itr);
-        }
-      }
-    }
-  }
-
-  // t1 and t2 can be both relations
-  // or t1 is a tuple, t2 is a transposed relation
-  void TheorySetsRels::sendInferTranspose( Node t1, Node t2, Node exp ) {
-    Assert( t2.getKind() == kind::TRANSPOSE );
-
-    if( isRel(t1) && isRel(t2) ) {
-      Assert(t1.getKind() == kind::TRANSPOSE);
-      sendMergeInfer(NodeManager::currentNM()->mkNode(kind::EQUAL, t1[0], t2[0]), exp, "Transpose-Equal");
-      return;
-    }
-    sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(t1), t2[0]), exp, "Transpose-Rule");
-  }
-
-  void TheorySetsRels::sendMergeInfer( Node fact, Node reason, const char * c ) {
-    if( !holds( fact ) ) {
-      Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, reason, fact);
-      d_pending_merge.push_back(lemma);
-      Trace("rels-std") << "[std-rels-lemma] Generate a lemma by applying " << c
-                        << ": " << lemma << std::endl;
-    }
-  }
-
-  void TheorySetsRels::sendInferProduct( Node member, Node pt_rel, Node exp ) {
-    Assert( pt_rel.getKind() == kind::PRODUCT );
-
-    std::vector<Node>   r1_element;
-    std::vector<Node>   r2_element;
-    Node                r1      = pt_rel[0];
-    Node                r2      = pt_rel[1];
-    Datatype            dt      = r1.getType().getSetElementType().getDatatype();
-    unsigned int        i       = 0;
-    unsigned int        s1_len  = r1.getType().getSetElementType().getTupleLength();
-    unsigned int        tup_len = pt_rel.getType().getSetElementType().getTupleLength();
-
-    r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
-    for( ; i < s1_len; ++i ) {
-      r1_element.push_back( RelsUtils::nthElementOfTuple( member, i ) );
-    }
-
-    dt = r2.getType().getSetElementType().getDatatype();
-    r2_element.push_back( Node::fromExpr( dt[0].getConstructor() ) );
-    for( ; i < tup_len; ++i ) {
-      r2_element.push_back( RelsUtils::nthElementOfTuple(member, i) );
-    }
-
-    Node tuple_1 = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, r1_element );
-    Node tuple_2 = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, r2_element );
-    sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_1, r1), exp, "Product-Split" );
-    sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_2, r2), exp, "Product-Split" );
-  }
-
-  TheorySetsRels::EqcInfo* TheorySetsRels::getOrMakeEqcInfo( Node n, bool doMake ){
-    std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
-    if( eqc_i == d_eqc_info.end() ){
-      if( doMake ){
-        EqcInfo* ei;
-        if( eqc_i!=d_eqc_info.end() ){
-          ei = eqc_i->second;
-        }else{
-          ei = new EqcInfo(d_sets_theory.getSatContext());
-          d_eqc_info[n] = ei;
-        }
-        if( n.getKind() == kind::TRANSPOSE ){
-          ei->d_tp = n;
-        } else if( n.getKind() == kind::PRODUCT ) {
-          ei->d_pt = n;
-        } else if( n.getKind() == kind::TCLOSURE ) {
-          ei->d_tc = n;
-        }
-        return ei;
-      }else{
-        return NULL;
-      }
-    }else{
-      return (*eqc_i).second;
-    }
-  }
-
-  void TheorySetsRels::printNodeMap(const char* fst,
-                                    const char* snd,
-                                    const NodeMap& map)
+  void TheorySetsRels::sendInfer(Node fact, Node reason, const char* c)
   {
-    for (const auto& key_data : map)
-    {
-      Trace("rels-debug") << fst << " " << key_data.first << " " << snd << " "
-                          << key_data.second << std::endl;
-    }
+    Trace("rels-lemma") << "Rels::lemma " << fact << " from " << reason
+                        << " by " << c << std::endl;
+    Node lemma = NodeManager::currentNM()->mkNode(IMPLIES, reason, fact);
+    d_pending.push_back(lemma);
   }
 }
 }

diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 7cad0f18d06b78c9d8dc78d61f51abc0e7affe6a..d4a91007b5b2a5b4abc5208a3a375dcf0fac21a5 100644 (file)
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -29,8 +29,7 @@ namespace CVC4 {
 namespace theory {
 namespace sets {
 
-class TheorySets;
-
+class TheorySetsPrivate;
 
 class TupleTrie {
 public:
@@ -45,63 +44,52 @@ public:
   void clear() { d_data.clear(); }
 };/* class TupleTrie */
 
+/** The relations extension of the theory of sets
+ *
+ * This class implements inference schemes described in Meng et al. CADE 2017
+ * for handling quantifier-free constraints in the theory of relations.
+ *
+ * In CVC4, relations are represented as sets of tuples. The theory of
+ * relations includes constraints over operators, e.g. TRANSPOSE, JOIN and so
+ * on, which apply to sets of tuples.
+ *
+ * Since relations are a special case of sets, this class is implemented as an
+ * extension of the theory of sets. That is, it shares many components of the
+ * TheorySets object which owns it.
+ */
 class TheorySetsRels {
   typedef context::CDList<Node> NodeList;
   typedef context::CDHashSet< Node, NodeHashFunction >            NodeSet;
   typedef context::CDHashMap< Node, Node, NodeHashFunction >      NodeMap;
 
 public:
-  TheorySetsRels(context::Context* c,
-                 context::UserContext* u,
-                 eq::EqualityEngine*,
-                 context::CDO<bool>*,
-                 TheorySets&);
-
-  ~TheorySetsRels();
-  void check(Theory::Effort);
-  void doPendingLemmas();
-
-  bool isRelationKind( Kind k );
-private:
-  /** equivalence class info
-   * d_mem tuples that are members of this equivalence class
-   * d_not_mem tuples that are not members of this equivalence class
-   * d_tp is a node of kind TRANSPOSE (if any) in this equivalence class,
-   * d_pt is a node of kind PRODUCT (if any) in this equivalence class,
-   * d_tc is a node of kind TCLOSURE (if any) in this equivalence class,
-   */
-  class EqcInfo
-  {
-  public:
-    EqcInfo( context::Context* c );
-    ~EqcInfo(){}
-    NodeSet                     d_mem;
-    NodeMap                     d_mem_exp;
-    context::CDO< Node >        d_tp;
-    context::CDO< Node >        d_pt;
-    context::CDO< Node >        d_tc;
-    context::CDO< Node >        d_rel_tc;
-  };
+ TheorySetsRels(context::Context* c,
+                context::UserContext* u,
+                eq::EqualityEngine* eq,
+                TheorySetsPrivate& set);
+
+ ~TheorySetsRels();
+ /**
+  * Invoke the check method with effort level e. At a high level, this class
+  * will make calls to TheorySetsPrivate::processInference to assert facts,
+  * lemmas, and conflicts. If this class makes no such call, then the current
+  * set of assertions is satisfiable with respect to relations.
+  */
+ void check(Theory::Effort e);
+ /** Is kind k a kind that belongs to the relation theory? */
+ static bool isRelationKind(Kind k);
 
 private:
-
-  /** has eqc info */
-  bool hasEqcInfo( TNode n ) { return d_eqc_info.find( n )!=d_eqc_info.end(); }
-
-  eq::EqualityEngine            *d_eqEngine;
-  context::CDO<bool>            *d_conflict;
-  TheorySets&                   d_sets_theory;
-
   /** True and false constant nodes */
   Node                          d_trueNode;
   Node                          d_falseNode;
-
-  /** Facts and lemmas to be sent to EE */
-  NodeList                      d_pending_merge;
-  NodeSet                       d_lemmas_produced;
+  /** The parent theory of sets object */
+  TheorySetsPrivate& d_sets_theory;
+  /** pointer to the equality engine of the theory of sets */
+  eq::EqualityEngine* d_eqEngine;
+  /** A list of pending inferences to process */
+  std::vector<Node> d_pending;
   NodeSet                       d_shared_terms;
-  std::vector< Node >           d_lemmas_out;
-  std::map< Node, Node >        d_pending_facts;
 
 
   std::unordered_set< Node, NodeHashFunction >       d_rel_nodes;
@@ -124,24 +112,27 @@ private:
   std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > >     d_rRep_tcGraph;
   std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > >     d_tcr_tcGraph;
   std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps;
-  std::map< Node, std::vector< Node > > d_tc_lemmas_last;
 
-  std::map< Node, EqcInfo* > d_eqc_info;
-
-public:
-  /** Standard effort notifications */
-  void eqNotifyNewClass(Node t);
-  void eqNotifyPostMerge(Node t1, Node t2);
-
-private:
-
-  /** Methods used in standard effort */
-  void doPendingMerge();
-  void sendInferProduct(Node member, Node pt_rel, Node exp);
-  void sendInferTranspose(Node t1, Node t2, Node exp );
-  void sendInferTClosure( Node mem_rep, EqcInfo* ei );
-  void sendMergeInfer( Node fact, Node reason, const char * c );
-  EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false );
+  context::Context* d_satContext;
+
+ private:
+  /** Send infer
+   *
+   * Called when we have inferred fact from explanation reason, where the
+   * latter should be a conjunction of facts that hold in the current context.
+   *
+   * The argument c is used for debugging, to give the name of the inference
+   * rule being used.
+   *
+   * This method adds the node (=> reason exp) to the pending vector d_pending.
+   */
+  void sendInfer(Node fact, Node reason, const char* c);
+  /**
+   * This method flushes the inferences in the pending vector d_pending to
+   * theory of sets, which may process them as lemmas or as facts to assert to
+   * the equality engine.
+   */
+  void doPendingInfers();
 
   /** Methods used in full effort */
   void check();
@@ -169,14 +160,7 @@ private:
   void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
                     std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable );
 
-
-  void addSharedTerm( TNode n );
-  void sendInfer( Node fact, Node exp, const char * c );
-  void sendLemma( Node fact, Node reason, const char * c );
-  void doTCLemmas();
-
   /** Helper functions */
-  bool holds( Node );
   bool hasTerm( Node a );
   void makeSharedTerm( Node );
   void reduceTupleVar( Node );
@@ -184,13 +168,8 @@ private:
   void computeTupleReps( Node );
   bool areEqual( Node a, Node b );
   Node getRepresentative( Node t );
-  bool exists( std::vector<Node>&, Node );
   inline void addToMembershipDB( Node, Node, Node  );
-  static void printNodeMap(const char* fst,
-                           const char* snd,
-                           const NodeMap& map);
   inline Node constructPair(Node tc_rep, Node a, Node b);
-  void addToMap( std::map< Node, std::vector<Node> >&, Node, Node );
   bool safelyAddToMap( std::map< Node, std::vector<Node> >&, Node, Node );
   bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();}
 };

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index a21edd8eb34eaf41751e30a84bad3182e5f14ca7..1bd8bb24705b4cfd821603863ca560c5e4c68c34 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1566,8 +1566,22 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
   if( !d_conflict ){
     if( options::ufssMode()==UF_SS_FULL ){
       Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl;
-      if( level==Theory::EFFORT_FULL && Debug.isOn( "uf-ss-debug" ) ){
-        debugPrint( "uf-ss-debug" );
+      if (level == Theory::EFFORT_FULL)
+      {
+        if (Debug.isOn("uf-ss-debug"))
+        {
+          debugPrint("uf-ss-debug");
+        }
+        if (Trace.isOn("uf-ss-state"))
+        {
+          Trace("uf-ss-state")
+              << "StrongSolverTheoryUF::check " << level << std::endl;
+          for (std::pair<const TypeNode, SortModel*>& rm : d_rep_model)
+          {
+            Trace("uf-ss-state") << "  " << rm.first << " has cardinality "
+                                 << rm.second->getCardinality() << std::endl;
+          }
+        }
       }
       for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
         it->second->check( level, d_out );