Split, refactor and document the theory of sets (#3085)

13 files changed, 3011 insertions, 1607 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4f56be8a9..db92d2b3f 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -618,10 +618,16 @@ libcvc4_add_sources(
   theory/sep/theory_sep_rewriter.cpp
   theory/sep/theory_sep_rewriter.h
   theory/sep/theory_sep_type_rules.h
+  theory/sets/cardinality_extension.cpp
+  theory/sets/cardinality_extension.h
+  theory/sets/inference_manager.cpp
+  theory/sets/inference_manager.h
   theory/sets/normal_form.h
   theory/sets/rels_utils.h
   theory/sets/skolem_cache.cpp
   theory/sets/skolem_cache.h
+  theory/sets/solver_state.cpp
+  theory/sets/solver_state.h
   theory/sets/theory_sets.cpp
   theory/sets/theory_sets.h
   theory/sets/theory_sets_private.cpp
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
new file mode 100644
index 000000000..37dfedd15
--- /dev/null
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -0,0 +1,911 @@
+/*********************                                                        */
+/*! \file cardinality_extension.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 an extension of the theory sets for handling
+ ** cardinality constraints.
+ **/
+
+#include "theory/sets/cardinality_extension.h"
+
+#include "expr/emptyset.h"
+#include "expr/node_algorithm.h"
+#include "options/sets_options.h"
+#include "theory/sets/normal_form.h"
+#include "theory/valuation.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+CardinalityExtension::CardinalityExtension(SolverState& s,
+                                           InferenceManager& im,
+                                           eq::EqualityEngine& e,
+                                           context::Context* c,
+                                           context::UserContext* u)
+    : d_state(s), d_im(im), d_ee(e), d_card_processed(u)
+{
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+  // we do congruence over cardinality
+  d_ee.addFunctionKind(CARD);
+}
+
+void CardinalityExtension::reset()
+{
+  d_eqc_to_card_term.clear();
+  d_t_card_enabled.clear();
+}
+void CardinalityExtension::registerTerm(Node n)
+{
+  Trace("sets-card-debug") << "Register term : " << n << std::endl;
+  Assert(n.getKind() == CARD);
+  TypeNode tnc = n[0].getType().getSetElementType();
+  d_t_card_enabled[tnc] = true;
+  Node r = d_ee.getRepresentative(n[0]);
+  if (d_eqc_to_card_term.find(r) == d_eqc_to_card_term.end())
+  {
+    d_eqc_to_card_term[r] = n;
+    registerCardinalityTerm(n[0]);
+  }
+  if (tnc.isInterpretedFinite())
+  {
+    std::stringstream ss;
+    ss << "ERROR: cannot use cardinality on sets with finite element "
+          "type (term is "
+       << n << ")." << std::endl;
+    throw LogicException(ss.str());
+    // TODO (#1123): extend approach for this case
+  }
+  Trace("sets-card-debug") << "...finished register term" << std::endl;
+}
+
+void CardinalityExtension::check()
+{
+  checkRegister();
+  if (d_im.hasProcessed())
+  {
+    return;
+  }
+  checkMinCard();
+  if (d_im.hasProcessed())
+  {
+    return;
+  }
+  checkCardCycles();
+  if (d_im.hasProcessed())
+  {
+    return;
+  }
+  // The last step will either do nothing (in which case we are SAT), or request
+  // that a new set term is introduced.
+  std::vector<Node> intro_sets;
+  checkNormalForms(intro_sets);
+  if (intro_sets.empty())
+  {
+    return;
+  }
+  Assert(intro_sets.size() == 1);
+  Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl;
+  Trace("sets-intro") << "  Actual Intro : ";
+  d_state.debugPrintSet(intro_sets[0], "sets-nf");
+  Trace("sets-nf") << std::endl;
+  Node k = d_state.getProxy(intro_sets[0]);
+  AlwaysAssert(!k.isNull());
+}
+
+void CardinalityExtension::checkRegister()
+{
+  Trace("sets") << "Cardinality graph..." << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  // first, ensure cardinality relationships are added as lemmas for all
+  // non-basic set terms
+  const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
+  for (const Node& eqc : setEqc)
+  {
+    const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
+    for (Node n : nvsets)
+    {
+      if (!d_state.isCongruent(n))
+      {
+        // if setminus, do for intersection instead
+        if (n.getKind() == SETMINUS)
+        {
+          n = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
+        }
+        registerCardinalityTerm(n);
+      }
+    }
+  }
+  Trace("sets") << "Done cardinality graph" << std::endl;
+}
+
+void CardinalityExtension::registerCardinalityTerm(Node n)
+{
+  TypeNode tnc = n.getType().getSetElementType();
+  if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end())
+  {
+    // if no cardinality constraints for sets of this type, we can ignore
+    return;
+  }
+  if (d_card_processed.find(n) != d_card_processed.end())
+  {
+    // already processed
+    return;
+  }
+  d_card_processed.insert(n);
+  NodeManager* nm = NodeManager::currentNM();
+  Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
+  std::vector<Node> cterms;
+  if (n.getKind() == INTERSECTION)
+  {
+    for (unsigned e = 0; e < 2; e++)
+    {
+      Node s = nm->mkNode(SETMINUS, n[e], n[1 - e]);
+      cterms.push_back(s);
+    }
+    Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, n), d_zero);
+    d_im.assertInference(pos_lem, d_emp_exp, "pcard", 1);
+  }
+  else
+  {
+    cterms.push_back(n);
+  }
+  for (unsigned k = 0, csize = cterms.size(); k < csize; k++)
+  {
+    Node nn = cterms[k];
+    Node nk = d_state.getProxy(nn);
+    Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, nk), d_zero);
+    d_im.assertInference(pos_lem, d_emp_exp, "pcard", 1);
+    if (nn != nk)
+    {
+      Node lem = nm->mkNode(EQUAL, nm->mkNode(CARD, nk), nm->mkNode(CARD, nn));
+      lem = Rewriter::rewrite(lem);
+      Trace("sets-card") << "  " << k << " : " << lem << std::endl;
+      d_im.assertInference(lem, d_emp_exp, "card", 1);
+    }
+  }
+  d_im.flushPendingLemmas();
+}
+
+void CardinalityExtension::checkCardCycles()
+{
+  Trace("sets") << "Check cardinality cycles..." << std::endl;
+  // build order of equivalence classes, also build cardinality graph
+  const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
+  d_oSetEqc.clear();
+  d_card_parent.clear();
+  for (const Node& s : setEqc)
+  {
+    std::vector<Node> curr;
+    std::vector<Node> exp;
+    checkCardCyclesRec(s, curr, exp);
+    if (d_im.hasProcessed())
+    {
+      return;
+    }
+  }
+  Trace("sets") << "Done check cardinality cycles" << std::endl;
+}
+
+void CardinalityExtension::checkCardCyclesRec(Node eqc,
+                                              std::vector<Node>& curr,
+                                              std::vector<Node>& exp)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (std::find(curr.begin(), curr.end(), eqc) != curr.end())
+  {
+    Trace("sets-debug") << "Found venn region loop..." << std::endl;
+    if (curr.size() > 1)
+    {
+      // all regions must be equal
+      std::vector<Node> conc;
+      for (const Node& cc : curr)
+      {
+        conc.push_back(curr[0].eqNode(cc));
+      }
+      Node fact = conc.size() == 1 ? conc[0] : nm->mkNode(AND, conc);
+      d_im.assertInference(fact, exp, "card_cycle");
+      d_im.flushPendingLemmas();
+    }
+    else
+    {
+      // should be guaranteed based on not exploring equal parents
+      Assert(false);
+    }
+    return;
+  }
+  if (std::find(d_oSetEqc.begin(), d_oSetEqc.end(), eqc) != d_oSetEqc.end())
+  {
+    // already processed
+    return;
+  }
+  const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
+  if (nvsets.empty())
+  {
+    // no non-variable sets, trivial
+    d_oSetEqc.push_back(eqc);
+    return;
+  }
+  curr.push_back(eqc);
+  TypeNode tn = eqc.getType();
+  bool is_empty = eqc == d_state.getEmptySetEqClass(tn);
+  Node emp_set = d_state.getEmptySet(tn);
+  for (const Node& n : nvsets)
+  {
+    Kind nk = n.getKind();
+    if (nk != INTERSECTION && nk != SETMINUS)
+    {
+      continue;
+    }
+    Trace("sets-debug") << "Build cardinality parents for " << n << "..."
+                        << std::endl;
+    std::vector<Node> sib;
+    unsigned true_sib = 0;
+    if (n.getKind() == INTERSECTION)
+    {
+      d_localBase[n] = n;
+      for (unsigned e = 0; e < 2; e++)
+      {
+        Node sm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[e], n[1 - e]));
+        sib.push_back(sm);
+      }
+      true_sib = 2;
+    }
+    else
+    {
+      Node si = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
+      sib.push_back(si);
+      d_localBase[n] = si;
+      Node osm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[1], n[0]));
+      sib.push_back(osm);
+      true_sib = 1;
+    }
+    Node u = Rewriter::rewrite(nm->mkNode(UNION, n[0], n[1]));
+    if (!d_ee.hasTerm(u))
+    {
+      u = Node::null();
+    }
+    unsigned n_parents = true_sib + (u.isNull() ? 0 : 1);
+    // if this set is empty
+    if (is_empty)
+    {
+      Assert(d_state.areEqual(n, emp_set));
+      Trace("sets-debug") << "  empty, parents equal siblings" << std::endl;
+      std::vector<Node> conc;
+      // parent equal siblings
+      for (unsigned e = 0; e < true_sib; e++)
+      {
+        if (d_ee.hasTerm(sib[e]) && !d_state.areEqual(n[e], sib[e]))
+        {
+          conc.push_back(n[e].eqNode(sib[e]));
+        }
+      }
+      d_im.assertInference(conc, n.eqNode(emp_set), "cg_emp");
+      d_im.flushPendingLemmas();
+      if (d_im.hasProcessed())
+      {
+        return;
+      }
+      else
+      {
+        // justify why there is no edge to parents (necessary?)
+        for (unsigned e = 0; e < n_parents; e++)
+        {
+          Node p = (e == true_sib) ? u : n[e];
+        }
+      }
+      continue;
+    }
+    std::vector<Node> card_parents;
+    std::vector<int> card_parent_ids;
+    // check if equal to a parent
+    for (unsigned e = 0; e < n_parents; e++)
+    {
+      Trace("sets-debug") << "  check parent " << e << "/" << n_parents
+                          << std::endl;
+      bool is_union = e == true_sib;
+      Node p = (e == true_sib) ? u : n[e];
+      Trace("sets-debug") << "  check relation to parent " << p
+                          << ", isu=" << is_union << "..." << std::endl;
+      // if parent is empty
+      if (d_state.areEqual(p, emp_set))
+      {
+        Trace("sets-debug") << "  it is empty..." << std::endl;
+        Assert(!d_state.areEqual(n, emp_set));
+        d_im.assertInference(n.eqNode(emp_set), p.eqNode(emp_set), "cg_emppar");
+        d_im.flushPendingLemmas();
+        if (d_im.hasProcessed())
+        {
+          return;
+        }
+        // if we are equal to a parent
+      }
+      else if (d_state.areEqual(p, n))
+      {
+        Trace("sets-debug") << "  it is equal to this..." << std::endl;
+        std::vector<Node> conc;
+        std::vector<int> sib_emp_indices;
+        if (is_union)
+        {
+          for (unsigned s = 0; s < sib.size(); s++)
+          {
+            sib_emp_indices.push_back(s);
+          }
+        }
+        else
+        {
+          sib_emp_indices.push_back(e);
+        }
+        // sibling(s) are empty
+        for (unsigned si : sib_emp_indices)
+        {
+          if (!d_state.areEqual(sib[si], emp_set))
+          {
+            conc.push_back(sib[si].eqNode(emp_set));
+          }
+          else
+          {
+            Trace("sets-debug")
+                << "Sibling " << sib[si] << " is already empty." << std::endl;
+          }
+        }
+        if (!is_union && nk == INTERSECTION && !u.isNull())
+        {
+          // union is equal to other parent
+          if (!d_state.areEqual(u, n[1 - e]))
+          {
+            conc.push_back(u.eqNode(n[1 - e]));
+          }
+        }
+        Trace("sets-debug")
+            << "...derived " << conc.size() << " conclusions" << std::endl;
+        d_im.assertInference(conc, n.eqNode(p), "cg_eqpar");
+        d_im.flushPendingLemmas();
+        if (d_im.hasProcessed())
+        {
+          return;
+        }
+      }
+      else
+      {
+        Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
+        // otherwise, we a syntactic subset of p
+        card_parents.push_back(p);
+        card_parent_ids.push_back(is_union ? 2 : e);
+      }
+    }
+    Assert(d_card_parent[n].empty());
+    Trace("sets-debug") << "get parent representatives..." << std::endl;
+    // for each parent, take their representatives
+    for (unsigned k = 0, numcp = card_parents.size(); k < numcp; k++)
+    {
+      Node cpk = card_parents[k];
+      Node eqcc = d_ee.getRepresentative(cpk);
+      Trace("sets-debug") << "Check card parent " << k << "/"
+                          << card_parents.size() << std::endl;
+
+      // if parent is singleton, then we should either be empty to equal to it
+      Node eqccSingleton = d_state.getSingletonEqClass(eqcc);
+      if (!eqccSingleton.isNull())
+      {
+        bool eq_parent = false;
+        std::vector<Node> exps;
+        d_state.addEqualityToExp(cpk, eqccSingleton, exps);
+        if (d_state.areDisequal(n, emp_set))
+        {
+          exps.push_back(n.eqNode(emp_set).negate());
+          eq_parent = true;
+        }
+        else
+        {
+          const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
+          if (!pmemsE.empty())
+          {
+            Node pmem = pmemsE.begin()->second;
+            exps.push_back(pmem);
+            d_state.addEqualityToExp(n, pmem[1], exps);
+            eq_parent = true;
+          }
+        }
+        // must be equal to parent
+        if (eq_parent)
+        {
+          Node conc = n.eqNode(cpk);
+          d_im.assertInference(conc, exps, "cg_par_sing");
+          d_im.flushPendingLemmas();
+        }
+        else
+        {
+          // split on empty
+          Trace("sets-nf") << "Split empty : " << n << std::endl;
+          d_im.split(n.eqNode(emp_set), 1);
+        }
+        Assert(d_im.hasProcessed());
+        return;
+      }
+      else
+      {
+        bool dup = false;
+        for (unsigned l = 0, numcpn = d_card_parent[n].size(); l < numcpn; l++)
+        {
+          Node cpnl = d_card_parent[n][l];
+          if (eqcc != cpnl)
+          {
+            continue;
+          }
+          Trace("sets-debug") << "  parents " << l << " and " << k
+                              << " are equal, ids = " << card_parent_ids[l]
+                              << " " << card_parent_ids[k] << std::endl;
+          dup = true;
+          if (n.getKind() != INTERSECTION)
+          {
+            continue;
+          }
+          Assert(card_parent_ids[l] != 2);
+          std::vector<Node> conc;
+          if (card_parent_ids[k] == 2)
+          {
+            // intersection is equal to other parent
+            unsigned pid = 1 - card_parent_ids[l];
+            if (!d_state.areEqual(n[pid], n))
+            {
+              Trace("sets-debug")
+                  << "  one of them is union, make equal to other..."
+                  << std::endl;
+              conc.push_back(n[pid].eqNode(n));
+            }
+          }
+          else
+          {
+            if (!d_state.areEqual(cpk, n))
+            {
+              Trace("sets-debug")
+                  << "  neither is union, make equal to one parent..."
+                  << std::endl;
+              // intersection is equal to one of the parents
+              conc.push_back(cpk.eqNode(n));
+            }
+          }
+          d_im.assertInference(conc, cpk.eqNode(cpnl), "cg_pareq");
+          d_im.flushPendingLemmas();
+          if (d_im.hasProcessed())
+          {
+            return;
+          }
+        }
+        if (!dup)
+        {
+          d_card_parent[n].push_back(eqcc);
+        }
+      }
+    }
+    // now recurse on parents (to ensure their normal will be computed after
+    // this eqc)
+    exp.push_back(eqc.eqNode(n));
+    for (const Node& cpnc : d_card_parent[n])
+    {
+      checkCardCyclesRec(cpnc, curr, exp);
+      if (d_im.hasProcessed())
+      {
+        return;
+      }
+    }
+    exp.pop_back();
+  }
+  curr.pop_back();
+  // parents now processed, can add to ordered list
+  d_oSetEqc.push_back(eqc);
+}
+
+void CardinalityExtension::checkNormalForms(std::vector<Node>& intro_sets)
+{
+  Trace("sets") << "Check normal forms..." << std::endl;
+  // now, build normal form for each equivalence class
+  // d_oSetEqc is now sorted such that for each d_oSetEqc[i], d_oSetEqc[j],
+  // if d_oSetEqc[i] is a strict syntactic subterm of d_oSetEqc[j], then i<j.
+  d_ff.clear();
+  d_nf.clear();
+  for (int i = (int)(d_oSetEqc.size() - 1); i >= 0; i--)
+  {
+    checkNormalForm(d_oSetEqc[i], intro_sets);
+    if (d_im.hasProcessed() || !intro_sets.empty())
+    {
+      return;
+    }
+  }
+  Trace("sets") << "Done check normal forms" << std::endl;
+}
+
+void CardinalityExtension::checkNormalForm(Node eqc,
+                                           std::vector<Node>& intro_sets)
+{
+  TypeNode tn = eqc.getType();
+  Trace("sets") << "Compute normal form for " << eqc << std::endl;
+  Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
+  if (eqc == d_state.getEmptySetEqClass(tn))
+  {
+    d_nf[eqc].clear();
+    Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
+    return;
+  }
+  // flat/normal forms are sets of equivalence classes
+  Node base;
+  std::vector<Node> comps;
+  std::map<Node, std::map<Node, std::vector<Node> > >::iterator it =
+      d_ff.find(eqc);
+  if (it != d_ff.end())
+  {
+    for (std::pair<const Node, std::vector<Node> >& itf : it->second)
+    {
+      std::sort(itf.second.begin(), itf.second.end());
+      if (base.isNull())
+      {
+        base = itf.first;
+      }
+      else
+      {
+        comps.push_back(itf.first);
+      }
+      Trace("sets-nf") << "  F " << itf.first << " : " << itf.second
+                       << std::endl;
+      Trace("sets-nf-debug") << " ...";
+      d_state.debugPrintSet(itf.first, "sets-nf-debug");
+      Trace("sets-nf-debug") << std::endl;
+    }
+  }
+  else
+  {
+    Trace("sets-nf") << "(no flat forms)" << std::endl;
+  }
+  std::map<Node, std::vector<Node> >& ffeqc = d_ff[eqc];
+  Assert(d_nf.find(eqc) == d_nf.end());
+  std::vector<Node>& nfeqc = d_nf[eqc];
+  NodeManager* nm = NodeManager::currentNM();
+  bool success = true;
+  Node emp_set = d_state.getEmptySet(tn);
+  if (!base.isNull())
+  {
+    for (unsigned j = 0, csize = comps.size(); j < csize; j++)
+    {
+      // compare if equal
+      std::vector<Node> c;
+      c.push_back(base);
+      c.push_back(comps[j]);
+      std::vector<Node> only[2];
+      std::vector<Node> common;
+      Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs "
+                             << comps[j] << std::endl;
+      unsigned k[2] = {0, 0};
+      while (k[0] < ffeqc[c[0]].size() || k[1] < ffeqc[c[1]].size())
+      {
+        bool proc = true;
+        for (unsigned e = 0; e < 2; e++)
+        {
+          if (k[e] == ffeqc[c[e]].size())
+          {
+            for (; k[1 - e] < ffeqc[c[1 - e]].size(); ++k[1 - e])
+            {
+              only[1 - e].push_back(ffeqc[c[1 - e]][k[1 - e]]);
+            }
+            proc = false;
+          }
+        }
+        if (proc)
+        {
+          if (ffeqc[c[0]][k[0]] == ffeqc[c[1]][k[1]])
+          {
+            common.push_back(ffeqc[c[0]][k[0]]);
+            k[0]++;
+            k[1]++;
+          }
+          else if (ffeqc[c[0]][k[0]] < ffeqc[c[1]][k[1]])
+          {
+            only[0].push_back(ffeqc[c[0]][k[0]]);
+            k[0]++;
+          }
+          else
+          {
+            only[1].push_back(ffeqc[c[1]][k[1]]);
+            k[1]++;
+          }
+        }
+      }
+      if (!only[0].empty() || !only[1].empty())
+      {
+        if (Trace.isOn("sets-nf-debug"))
+        {
+          Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
+          for (unsigned e = 0; e < 2; e++)
+          {
+            Trace("sets-nf-debug") << "  " << c[e] << " : { ";
+            for (unsigned l = 0; l < only[e].size(); l++)
+            {
+              if (l > 0)
+              {
+                Trace("sets-nf-debug") << ", ";
+              }
+              Trace("sets-nf-debug") << "[" << only[e][l] << "]";
+            }
+            Trace("sets-nf-debug") << " }" << std::endl;
+          }
+        }
+        // try to make one empty, prefer the unique ones first
+        for (unsigned e = 0; e < 3; e++)
+        {
+          unsigned sz = e == 2 ? common.size() : only[e].size();
+          for (unsigned l = 0; l < sz; l++)
+          {
+            Node r = e == 2 ? common[l] : only[e][l];
+            Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
+            Trace("sets-nf-debug") << "         actual : ";
+            d_state.debugPrintSet(r, "sets-nf-debug");
+            Trace("sets-nf-debug") << std::endl;
+            Assert(!d_state.areEqual(r, emp_set));
+            if (!d_state.areDisequal(r, emp_set) && !d_state.hasMembers(r))
+            {
+              // guess that its equal empty if it has no explicit members
+              Trace("sets-nf") << " Split empty : " << r << std::endl;
+              Trace("sets-nf") << "Actual Split : ";
+              d_state.debugPrintSet(r, "sets-nf");
+              Trace("sets-nf") << std::endl;
+              d_im.split(r.eqNode(emp_set), 1);
+              Assert(d_im.hasProcessed());
+              return;
+            }
+          }
+        }
+        for (const Node& o0 : only[0])
+        {
+          for (const Node& o1 : only[1])
+          {
+            bool disjoint = false;
+            Trace("sets-nf-debug")
+                << "Try split " << o0 << " against " << o1 << std::endl;
+            // split them
+            for (unsigned e = 0; e < 2; e++)
+            {
+              Node r1 = e == 0 ? o0 : o1;
+              Node r2 = e == 0 ? o1 : o0;
+              // check if their intersection exists modulo equality
+              Node r1r2i = d_state.getBinaryOpTerm(INTERSECTION, r1, r2);
+              if (!r1r2i.isNull())
+              {
+                Trace("sets-nf-debug")
+                    << "Split term already exists, but not in cardinality "
+                       "graph : "
+                    << r1r2i << ", should be empty." << std::endl;
+                // their intersection is empty (probably?)
+                // e.g. these are two disjoint venn regions, proceed to next
+                // pair
+                Assert(d_state.areEqual(emp_set, r1r2i));
+                disjoint = true;
+                break;
+              }
+            }
+            if (!disjoint)
+            {
+              // simply introduce their intersection
+              Assert(o0 != o1);
+              Node kca = d_state.getProxy(o0);
+              Node kcb = d_state.getProxy(o1);
+              Node intro =
+                  Rewriter::rewrite(nm->mkNode(INTERSECTION, kca, kcb));
+              Trace("sets-nf") << "   Intro split : " << o0 << " against " << o1
+                               << ", term is " << intro << std::endl;
+              intro_sets.push_back(intro);
+              Assert(!d_ee.hasTerm(intro));
+              return;
+            }
+          }
+        }
+        // should never get here
+        success = false;
+      }
+    }
+    if (success)
+    {
+      // normal form is flat form of base
+      nfeqc.insert(nfeqc.end(), ffeqc[base].begin(), ffeqc[base].end());
+      Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
+    }
+    else
+    {
+      Trace("sets-nf") << "failed to build N " << eqc << std::endl;
+    }
+  }
+  else
+  {
+    // must ensure disequal from empty
+    if (!eqc.isConst() && !d_state.areDisequal(eqc, emp_set)
+        && !d_state.hasMembers(eqc))
+    {
+      Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
+      d_im.split(eqc.eqNode(emp_set));
+      success = false;
+    }
+    else
+    {
+      // normal form is this equivalence class
+      nfeqc.push_back(eqc);
+      Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }"
+                       << std::endl;
+    }
+  }
+  if (!success)
+  {
+    Assert(d_im.hasProcessed());
+    return;
+  }
+  // Send to parents (a parent is a set that contains a term in this equivalence
+  // class as a direct child).
+  const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
+  if (nvsets.empty())
+  {
+    // no non-variable sets
+    return;
+  }
+  std::map<Node, std::map<Node, bool> > parents_proc;
+  for (const Node& n : nvsets)
+  {
+    Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
+    if (d_card_parent[n].empty())
+    {
+      // nothing to do
+      continue;
+    }
+    Assert(d_localBase.find(n) != d_localBase.end());
+    Node cbase = d_localBase[n];
+    Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
+    for (const Node& p : d_card_parent[n])
+    {
+      Trace("sets-nf-debug") << "Check parent " << p << std::endl;
+      if (parents_proc[cbase].find(p) != parents_proc[cbase].end())
+      {
+        Trace("sets-nf-debug") << "..already processed parent " << p << " for "
+                               << cbase << std::endl;
+        continue;
+      }
+      parents_proc[cbase][p] = true;
+      Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p
+                             << "] ), from " << n << "..." << std::endl;
+
+      std::vector<Node>& ffpc = d_ff[p][cbase];
+      for (const Node& nfeqci : nfeqc)
+      {
+        if (std::find(ffpc.begin(), ffpc.end(), nfeqci) == ffpc.end())
+        {
+          ffpc.insert(ffpc.end(), nfeqc.begin(), nfeqc.end());
+        }
+        else
+        {
+          // if it is a duplicate venn region, it must be empty since it is
+          // coming from syntactically disjoint siblings
+        }
+      }
+    }
+  }
+}
+
+void CardinalityExtension::checkMinCard()
+{
+  NodeManager* nm = NodeManager::currentNM();
+  const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
+  for (int i = (int)(setEqc.size() - 1); i >= 0; i--)
+  {
+    Node eqc = setEqc[i];
+    TypeNode tn = eqc.getType().getSetElementType();
+    if (d_t_card_enabled.find(tn) == d_t_card_enabled.end())
+    {
+      // cardinality is not enabled for this type, skip
+      continue;
+    }
+    // get members in class
+    const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
+    if (pmemsE.empty())
+    {
+      // no members, trivial
+      continue;
+    }
+    std::vector<Node> exp;
+    std::vector<Node> members;
+    Node cardTerm;
+    std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
+    if (it != d_eqc_to_card_term.end())
+    {
+      cardTerm = it->second;
+    }
+    else
+    {
+      cardTerm = nm->mkNode(CARD, eqc);
+    }
+    for (const std::pair<const Node, Node>& itmm : pmemsE)
+    {
+      members.push_back(itmm.first);
+      exp.push_back(nm->mkNode(MEMBER, itmm.first, cardTerm[0]));
+    }
+    if (members.size() > 1)
+    {
+      exp.push_back(nm->mkNode(DISTINCT, members));
+    }
+    if (!members.empty())
+    {
+      Node conc =
+          nm->mkNode(GEQ, cardTerm, nm->mkConst(Rational(members.size())));
+      Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
+      d_im.assertInference(conc, expn, "mincard", 1);
+    }
+  }
+  // flush the lemmas
+  d_im.flushPendingLemmas();
+}
+
+bool CardinalityExtension::isModelValueBasic(Node eqc)
+{
+  return d_nf[eqc].size() == 1 && d_nf[eqc][0] == eqc;
+}
+
+void CardinalityExtension::mkModelValueElementsFor(
+    Valuation& val,
+    Node eqc,
+    std::vector<Node>& els,
+    const std::map<Node, Node>& mvals)
+{
+  TypeNode elementType = eqc.getType().getSetElementType();
+  if (isModelValueBasic(eqc))
+  {
+    std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
+    if (it != d_eqc_to_card_term.end())
+    {
+      // slack elements from cardinality value
+      Node v = val.getModelValue(it->second);
+      Trace("sets-model") << "Cardinality of " << eqc << " is " << v
+                          << std::endl;
+      Assert(v.getConst<Rational>() <= LONG_MAX,
+             "Exceeded LONG_MAX in sets model");
+      unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
+      Assert(els.size() <= vu);
+      NodeManager* nm = NodeManager::currentNM();
+      while (els.size() < vu)
+      {
+        els.push_back(nm->mkNode(SINGLETON, nm->mkSkolem("msde", elementType)));
+      }
+    }
+    else
+    {
+      Trace("sets-model") << "No slack elements for " << eqc << std::endl;
+    }
+  }
+  else
+  {
+    Trace("sets-model") << "Build value for " << eqc
+                        << " based on normal form, size = " << d_nf[eqc].size()
+                        << std::endl;
+    // it is union of venn regions
+    for (unsigned j = 0; j < d_nf[eqc].size(); j++)
+    {
+      std::map<Node, Node>::const_iterator itm = mvals.find(d_nf[eqc][j]);
+      if (itm != mvals.end())
+      {
+        els.push_back(itm->second);
+      }
+      else
+      {
+        Assert(false);
+      }
+    }
+  }
+}
+
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h
new file mode 100644
index 000000000..d9c5dd64a
--- /dev/null
+++ b/src/theory/sets/cardinality_extension.h
@@ -0,0 +1,347 @@
+/*********************                                                        */
+/*! \file cardinality_extension.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 An extension of the theory sets for handling cardinality constraints
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SETS__CARDINALITY_EXTENSION_H
+#define CVC4__THEORY__SETS__CARDINALITY_EXTENSION_H
+
+#include "context/cdhashset.h"
+#include "context/context.h"
+#include "theory/sets/inference_manager.h"
+#include "theory/sets/solver_state.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+/**
+ * This class implements a variant of the procedure from Bansal et al, IJCAR
+ * 2016. It is used during a full effort check in the following way:
+ *    reset(); { registerTerm(n,lemmas); | n in CardTerms }  check();
+ * where CardTerms is the set of all applications of CARD in the current
+ * context.
+ *
+ * The remaining public methods are used during model construction, i.e.
+ * the collectModelInfo method of the theory of sets.
+ *
+ * The procedure from Bansal et al IJCAR 2016 introduces the notion of a
+ * "cardinality graph", where the nodes of this graph are sets and (directed)
+ * edges connect sets to their Venn regions wrt to other sets. For example,
+ * if (A \ B) is a term in the current context, then the node A is
+ * connected via an edge to child (A \ B). The node (A ^ B) is a child
+ * of both A and B. The notion of a cardinality graph is loosely followed
+ * in the procedure implemented by this class.
+ *
+ * The main difference wrt Bansal et al IJCAR 2016 is that the nodes of the
+ * cardinality graph considered by this class are not arbitrary set terms, but
+ * are instead representatives of equivalence classes. For more details, see
+ * documentation of the inference schemas in the private methods of this class.
+ *
+ * This variant of the procedure takes inspiration from the procedure
+ * for word equations in Liang et al, CAV 2014. In that procedure, "normal
+ * forms" are generated for String terms by recursively expanding
+ * concatentations modulo equality. This procedure similarly maintains
+ * normal forms, where the normal form for Set terms is a set of (equivalence
+ * class representatives of) Venn regions that do not contain the empty set.
+ */
+class CardinalityExtension
+{
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+  /**
+   * Constructs a new instance of the cardinality solver w.r.t. the provided
+   * contexts.
+   */
+  CardinalityExtension(SolverState& s,
+                       InferenceManager& im,
+                       eq::EqualityEngine& e,
+                       context::Context* c,
+                       context::UserContext* u);
+
+  ~CardinalityExtension() {}
+  /** reset
+   *
+   * Called at the beginning of a full effort check. This resets the data
+   * structures used by this class during a full effort check.
+   */
+  void reset();
+  /** register term
+   *
+   * Register that the term n exists in the current context, where n is an
+   * application of CARD.
+   */
+  void registerTerm(Node n);
+  /** check
+   *
+   * Invoke a full effort check of the cardinality solver. At a high level,
+   * this asserts inferences via the inference manager object d_im. If no
+   * inferences are made, then the current set of assertions is satisfied
+   * with respect to constraints involving set cardinality.
+   *
+   * This method applies various inference schemas in succession until an
+   * inference is made. These inference schemas are given in the private
+   * methods of this class (e.g. checkMinCard, checkCardBuildGraph, etc.).
+   */
+  void check();
+  /** Is model value basic?
+   *
+   * This returns true if equivalence class eqc is a "leaf" in the cardinality
+   * graph.
+   */
+  bool isModelValueBasic(Node eqc);
+  /** get model elements
+   *
+   * This method updates els so that it is the set of elements that occur in
+   * an equivalence class (whose representative is eqc) in the model we are
+   * building. Notice that els may already have elements in it (from explicit
+   * memberships from the base set solver for leaf nodes of the cardinality
+   * graph). This method is used during the collectModelInfo method of theory
+   * of sets.
+   *
+   * The argument v is the Valuation utility of the theory of sets, which is
+   * used by this method to query the value assigned to cardinality terms by
+   * the theory of arithmetic.
+   *
+   * The argument mvals maps set equivalence classes to their model values.
+   * Due to our model construction algorithm, it can be assumed that all
+   * sets in the normal form of eqc occur in the domain of mvals by the order
+   * in which sets are assigned.
+   */
+  void mkModelValueElementsFor(Valuation& v,
+                               Node eqc,
+                               std::vector<Node>& els,
+                               const std::map<Node, Node>& mvals);
+  /** get ordered sets equivalence classes
+   *
+   * Get the ordered set of equivalence classes computed by this class. This
+   * ordering ensures the invariant mentioned above mkModelValueElementsFor.
+   *
+   * This ordering ensures that all children of a node in the cardinality
+   * graph computed by this class occur before it in this list.
+   */
+  const std::vector<Node>& getOrderedSetsEqClasses() { return d_oSetEqc; }
+
+ private:
+  /** constants */
+  Node d_zero;
+  /** the empty vector */
+  std::vector<Node> d_emp_exp;
+  /** Reference to the state object for the theory of sets */
+  SolverState& d_state;
+  /** Reference to the inference manager for the theory of sets */
+  InferenceManager& d_im;
+  /** Reference to the equality engine of theory of sets */
+  eq::EqualityEngine& d_ee;
+  /** register cardinality term
+   *
+   * This method add lemmas corresponding to the definition of
+   * the cardinality of set term n. For example, if n is A^B (denoting set
+   * intersection as ^), then we consider the lemmas card(A^B)>=0,
+   * card(A) = card(A\B) + card(A^B) and card(B) = card(B\A) + card(A^B).
+   *
+   * The exact form of this lemma is modified such that proxy variables are
+   * introduced for set terms as needed (see SolverState::getProxy).
+   */
+  void registerCardinalityTerm(Node n);
+  /** check register
+   *
+   * This ensures that all (non-redundant, relevant) non-variable set terms in
+   * the current context have been passed to registerCardinalityTerm. In other
+   * words, this ensures that the cardinality graph for these terms can be
+   * constructed since the cardinality relationships for these terms have been
+   * elaborated as lemmas.
+   *
+   * Notice a term is redundant in a context if it is congruent to another
+   * term that is already in the context; it is not relevant if no cardinality
+   * constraints exist for its type.
+   */
+  void checkRegister();
+  /** check minimum cardinality
+   *
+   * This adds lemmas to the argument of the method of the form
+   *   distinct(x1,...,xn) ^ member(x1,S) ^ ... ^ member(xn,S) => card(S) >= n
+   * This lemma enforces the rules GUESS_LOWER_BOUND and PROPAGATE_MIN_SIZE
+   * from Bansal et. al IJCAR 2016.
+   *
+   * Notice that member(x1,S) is implied to hold in the current context. This
+   * means that it may be the case that member(x,T) ^ T = S are asserted
+   * literals. Furthermore, x1, ..., xn reside in distinct equivalence classes
+   * but are not necessarily entailed to be distinct.
+   */
+  void checkMinCard();
+  /** check cardinality cycles
+   *
+   * The purpose of this inference schema is to construct two data structures:
+   *
+   * (1) d_card_parent, which maps set terms (A op B) for op in { \, ^ } to
+   * equivalence class representatives of their "parents", where:
+   *   parent( A ^ B ) = A, B
+   *   parent( A \ B ) = A
+   * Additionally, (A union B) is a parent of all three of the above sets
+   * if it exists as a term in the current context. As exceptions,
+   * if A op B = A, then A is not a parent of A ^ B and similarly for B.
+   * If A ^ B is empty, then it has no parents.
+   *
+   * We say the cardinality graph induced by the current set of equalities
+   * is an (irreflexive, acyclic) graph whose nodes are equivalence classes and
+   * which contains a (directed) edge r1 to r2 if there exists a term t2 in r2
+   * that has some parent t1 in r1.
+   *
+   * (2) d_oSetEqc, an ordered set of equivalence classes whose types are set.
+   * These equivalence classes have the property that if r1 is a descendant
+   * of r2 in the cardinality graph, then r1 must come before r2 in d_oSetEqc.
+   *
+   * This inference schema may make various inferences while building these
+   * two data structures if the current equality arrangement of sets is not
+   * as expected. For example, it will infer equalities between sets based on
+   * the emptiness and equalities of sets in adjacent children in the
+   * cardinality graph, to give some examples:
+   *   (A \ B = empty) => A = A ^ B
+   *   A^B = B => B \ A = empty
+   *   A union B = A ^ B => A \ B = empty AND B \ A = empty
+   * and so on.
+   *
+   * It will also recognize when a cycle occurs in the cardinality graph, in
+   * which case an equality chain between sets can be inferred. For an example,
+   * see checkCardCyclesRec below.
+   *
+   * This method is inspired by the checkCycles inference schema in the theory
+   * of strings.
+   */
+  void checkCardCycles();
+  /**
+   * Helper function for above. Called when wish to process equivalence class
+   * eqc.
+   *
+   * Argument curr contains the equivalence classes we are currently processing,
+   * which are descendants of eqc in the cardinality graph, where eqc is the
+   * representative of some equivalence class.
+   *
+   * Argument exp contains an explanation of why the chain of children curr
+   * are descedants of . For example, say we are in context with equivalence
+   * classes:
+   *   { A, B, C^D }, { D, B ^ C,  A ^ E }
+   * We may recursively call this method via the following steps:
+   *   eqc = D, curr = {}, exp = {}
+   *   eqc = A, curr = { D }, exp = { D = B^C }
+   *   eqc = A, curr = { D, A }, exp = { D = B^C, A = C^D }
+   * after which we discover a cycle in the cardinality graph. We infer
+   * that A must be equal to D, where exp is an explanation of the cycle.
+   */
+  void checkCardCyclesRec(Node eqc,
+                          std::vector<Node>& curr,
+                          std::vector<Node>& exp);
+  /** check normal forms
+   *
+   * This method attempts to assign "normal forms" to all set equivalence
+   * classes whose types have cardinality constraints. Normal forms are
+   * defined recursively.
+   *
+   * A "normal form" of an equivalence class [r] (where [r] denotes the
+   * equivalence class whose representative is r) is a set of representatives
+   * U = { r1, ..., rn }. If there exists at least one set in [r] that has a
+   * "flat form", then all sets in the equivalence class have flat form U.
+   * If no set in U has a flat form, then U = { r } if r does not contain
+   * the empty set, and {} otherwise. Notice that the choice of representative
+   * r is determined by the equality engine.
+   *
+   * A "flat form" of a set term T is the union of the normal forms of the
+   * equivalence classes that contain sets whose parent is T.
+   *
+   * In terms of the cardinality graph, the "flat form" of term t is the set
+   * of leaves of t that are descendants of it in the cardinality graph induced
+   * by the current set of assertions. Notice a flat form is only defined if t
+   * has children. If all terms in an equivalence class E with flat forms have
+   * the same flat form, then E is added as a node to the cardinality graph with
+   * edges connecting to all equivalence classes with terms that have a parent
+   * in E.
+   *
+   * In the following inference schema, the argument intro_sets is updated to
+   * contain the set of new set terms that the procedure is requesting to
+   * introduce for the purpose of forcing the flat forms of two equivalent sets
+   * to become identical. If any equivalence class cannot be assigned a normal
+   * form, then the resulting intro_sets is guaranteed to be non-empty.
+   *
+   * As an example, say we have a context with equivalence classes:
+   *   {A, D}, {C, A^B}, {E, C^D}, {C\D}, {D\C}, {A\B}, {empty, B\A},
+   * where assume the first term in each set is its representative. An ordered
+   * list d_oSetEqc for this context:
+   *   A, C, E, C\D, D\C, A\B, empty, ...
+   * The normal form of {empty, B\A} is {}, since it contains the empty set.
+   * The normal forms for each of the singleton equivalence classes are
+   * themselves.
+   * The flat form of each of E and C^D does not exist, hence the normal form
+   * of {E, C^D} is {E}.
+   * The flat form of C is {E, C\D}, noting that C^D and C\D are terms whose
+   * parent is C, hence {E, C\D} is the normal form for class {C, A^B}.
+   * The flat form of A is {E, C\D, A\B} and the flat form of D is {E, D\C}.
+   * Hence, no normal form can be assigned to class {A, D}. Instead this method
+   * will e.g. add (C\D)^E to intro_sets, which will force the solver
+   * to explore a model where the Venn regions (C\D)^E (C\D)\E and E\(C\D) are
+   * considered while constructing flat forms. Splitting on whether these sets
+   * are empty will eventually lead to a model where the flat forms of A and D
+   * are the same.
+   */
+  void checkNormalForms(std::vector<Node>& intro_sets);
+  /**
+   * Called for each equivalence class, in order of d_oSetEqc, by the above
+   * function.
+   */
+  void checkNormalForm(Node eqc, std::vector<Node>& intro_sets);
+  /** element types of sets for which cardinality is enabled */
+  std::map<TypeNode, bool> d_t_card_enabled;
+  /**
+   * This maps equivalence classes r to an application of cardinality of the
+   * form card( t ), where t = r holds in the current context.
+   */
+  std::map<Node, Node> d_eqc_to_card_term;
+  /**
+   * User-context-dependent set of set terms for which we have called
+   * registerCardinalityTerm on.
+   */
+  NodeSet d_card_processed;
+  /** The ordered set of equivalence classes, see checkCardCycles. */
+  std::vector<Node> d_oSetEqc;
+  /**
+   * This maps set terms to the set of representatives of their "parent" sets,
+   * see checkCardCycles.
+   */
+  std::map<Node, std::vector<Node> > d_card_parent;
+  /**
+   * Maps equivalence classes + set terms in that equivalence class to their
+   * "flat form" (see checkNormalForms).
+   */
+  std::map<Node, std::map<Node, std::vector<Node> > > d_ff;
+  /** Maps equivalence classes to their "normal form" (see checkNormalForms). */
+  std::map<Node, std::vector<Node> > d_nf;
+  /** The local base node map
+   *
+   * This maps set terms to the "local base node" of its cardinality graph.
+   * The local base node of S is the intersection node that is either S itself
+   * or is adjacent to S in the cardinality graph. This maps
+   *
+   * For example, the ( A ^ B ) is the local base of each of the sets (A \ B),
+   * ( A ^ B ), and (B \ A).
+   */
+  std::map<Node, Node> d_localBase;
+}; /* class CardinalityExtension */
+
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
new file mode 100644
index 000000000..e29e574be
--- /dev/null
+++ b/src/theory/sets/inference_manager.cpp
@@ -0,0 +1,229 @@
+/*********************                                                        */
+/*! \file inference_manager.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 the inference manager for the theory of sets
+ **/
+
+#include "theory/sets/inference_manager.h"
+
+#include "options/sets_options.h"
+#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+InferenceManager::InferenceManager(TheorySetsPrivate& p,
+                                   SolverState& s,
+                                   eq::EqualityEngine& e,
+                                   context::Context* c,
+                                   context::UserContext* u)
+    : d_parent(p), d_state(s), d_ee(e), d_lemmas_produced(u), d_keep(c)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+void InferenceManager::reset()
+{
+  d_sentLemma = false;
+  d_addedFact = false;
+  d_pendingLemmas.clear();
+}
+
+bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
+{
+  // should we send this fact out as a lemma?
+  if ((options::setsInferAsLemmas() && inferType != -1) || inferType == 1)
+  {
+    if (d_state.isEntailed(fact, true))
+    {
+      return false;
+    }
+    Node lem = fact;
+    if (exp != d_true)
+    {
+      lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
+    }
+    d_pendingLemmas.push_back(lem);
+    return true;
+  }
+  Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
+                     << std::endl;
+  if (fact.isConst())
+  {
+    // either trivial or a conflict
+    if (fact == d_false)
+    {
+      Trace("sets-lemma") << "Conflict : " << exp << std::endl;
+      d_state.setConflict(exp);
+      return true;
+    }
+    return false;
+  }
+  else if (fact.getKind() == AND
+           || (fact.getKind() == NOT && fact[0].getKind() == OR))
+  {
+    bool ret = false;
+    Node f = fact.getKind() == NOT ? fact[0] : fact;
+    for (unsigned i = 0; i < f.getNumChildren(); i++)
+    {
+      Node factc = fact.getKind() == NOT ? f[i].negate() : f[i];
+      bool tret = assertFactRec(factc, exp, inferType);
+      ret = ret || tret;
+      if (d_state.isInConflict())
+      {
+        return true;
+      }
+    }
+    return ret;
+  }
+  bool polarity = fact.getKind() != NOT;
+  TNode atom = polarity ? fact : fact[0];
+  // things we can assert to equality engine
+  if (atom.getKind() == MEMBER
+      || (atom.getKind() == EQUAL && atom[0].getType().isSet()))
+  {
+    // send to equality engine
+    if (d_parent.assertFact(fact, exp))
+    {
+      d_addedFact = true;
+      return true;
+    }
+  }
+  else if (!d_state.isEntailed(fact, true))
+  {
+    // must send as lemma
+    Node lem = fact;
+    if (exp != d_true)
+    {
+      lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
+    }
+    d_pendingLemmas.push_back(lem);
+    return true;
+  }
+  return false;
+}
+void InferenceManager::assertInference(Node fact,
+                                       Node exp,
+                                       const char* c,
+                                       int inferType)
+{
+  d_keep.insert(exp);
+  d_keep.insert(fact);
+  if (assertFactRec(fact, exp, inferType))
+  {
+    Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
+                        << c << std::endl;
+    Trace("sets-assertion")
+        << "(assert (=> " << exp << " " << fact << ")) ; by " << c << std::endl;
+  }
+}
+
+void InferenceManager::assertInference(Node fact,
+                                       std::vector<Node>& exp,
+                                       const char* c,
+                                       int inferType)
+{
+  Node exp_n = exp.empty() ? d_true
+                           : (exp.size() == 1
+                                  ? exp[0]
+                                  : NodeManager::currentNM()->mkNode(AND, exp));
+  assertInference(fact, exp_n, c, inferType);
+}
+
+void InferenceManager::assertInference(std::vector<Node>& conc,
+                                       Node exp,
+                                       const char* c,
+                                       int inferType)
+{
+  if (!conc.empty())
+  {
+    Node fact = conc.size() == 1 ? conc[0]
+                                 : NodeManager::currentNM()->mkNode(AND, conc);
+    assertInference(fact, exp, c, inferType);
+  }
+}
+void InferenceManager::assertInference(std::vector<Node>& conc,
+                                       std::vector<Node>& exp,
+                                       const char* c,
+                                       int inferType)
+{
+  Node exp_n = exp.empty() ? d_true
+                           : (exp.size() == 1
+                                  ? exp[0]
+                                  : NodeManager::currentNM()->mkNode(AND, exp));
+  assertInference(conc, exp_n, c, inferType);
+}
+
+void InferenceManager::split(Node n, int reqPol)
+{
+  n = Rewriter::rewrite(n);
+  Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
+  flushLemma(lem);
+  Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
+  if (reqPol != 0)
+  {
+    Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
+                        << std::endl;
+    d_parent.getOutputChannel()->requirePhase(n, reqPol > 0);
+  }
+}
+void InferenceManager::flushLemmas(std::vector<Node>& lemmas, bool preprocess)
+{
+  for (const Node& l : lemmas)
+  {
+    flushLemma(l, preprocess);
+  }
+  lemmas.clear();
+}
+
+void InferenceManager::flushLemma(Node lem, bool preprocess)
+{
+  if (d_lemmas_produced.find(lem) != d_lemmas_produced.end())
+  {
+    Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
+    return;
+  }
+  Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
+  d_lemmas_produced.insert(lem);
+  d_parent.getOutputChannel()->lemma(lem, false, preprocess);
+  d_sentLemma = true;
+}
+
+void InferenceManager::flushPendingLemmas(bool preprocess)
+{
+  for (const Node& l : d_pendingLemmas)
+  {
+    flushLemma(l, preprocess);
+  }
+  d_pendingLemmas.clear();
+}
+
+bool InferenceManager::hasLemmaCached(Node lem) const
+{
+  return d_lemmas_produced.find(lem) != d_lemmas_produced.end();
+}
+
+bool InferenceManager::hasProcessed() const
+{
+  return d_state.isInConflict() || d_sentLemma || d_addedFact;
+}
+bool InferenceManager::hasSentLemma() const { return d_sentLemma; }
+bool InferenceManager::hasAddedFact() const { return d_addedFact; }
+
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h
new file mode 100644
index 000000000..29b0e2bca
--- /dev/null
+++ b/src/theory/sets/inference_manager.h
@@ -0,0 +1,159 @@
+/*********************                                                        */
+/*! \file inference_manager.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 The inference manager for the theory of sets.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SETS__INFERENCE_MANAGER_H
+#define CVC4__THEORY__SETS__INFERENCE_MANAGER_H
+
+#include "theory/sets/solver_state.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsPrivate;
+
+/** Inference manager
+ *
+ * This class manages inferences produced by the theory of sets. It manages
+ * whether inferences are processed as external lemmas on the output channel
+ * of theory of sets or internally as literals asserted to the equality engine
+ * of theory of sets. The latter literals are referred to as "facts".
+ */
+class InferenceManager
+{
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+  InferenceManager(TheorySetsPrivate& p,
+                   SolverState& s,
+                   eq::EqualityEngine& e,
+                   context::Context* c,
+                   context::UserContext* u);
+  /** reset
+   *
+   * Called at the beginning of a full effort check. Resets the information
+   * related to this class regarding whether facts and lemmas have been
+   * processed.
+   */
+  void reset();
+  /**
+   * Add facts corresponding to ( exp => fact ) via calls to the assertFact
+   * method of TheorySetsPrivate.
+   *
+   * The portions of fact that were unable to be processed as facts are added
+   * to the data member d_pendingLemmas.
+   *
+   * The argument inferType is used for overriding the policy on whether
+   * fact is processed as a lemma, where inferType=1 forces fact to be
+   * set as a lemma, and inferType=-1 forces fact to be processed as a fact
+   * (if possible).
+   *
+   * The argument c is the name of the inference, which is used for debugging.
+   */
+  void assertInference(Node fact, Node exp, const char* c, int inferType = 0);
+  /** same as above, where exp is interpreted as a conjunction */
+  void assertInference(Node fact,
+                       std::vector<Node>& exp,
+                       const char* c,
+                       int inferType = 0);
+  /** same as above, where conc is interpreted as a conjunction */
+  void assertInference(std::vector<Node>& conc,
+                       Node exp,
+                       const char* c,
+                       int inferType = 0);
+  /** same as above, where both exp and conc are interpreted as conjunctions */
+  void assertInference(std::vector<Node>& conc,
+                       std::vector<Node>& exp,
+                       const char* c,
+                       int inferType = 0);
+
+  /** 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);
+  /** Do we have pending lemmas? */
+  bool hasPendingLemmas() const { return !d_pendingLemmas.empty(); }
+  /** Applies flushLemmas on d_pendingLemmas */
+  void flushPendingLemmas(bool preprocess = false);
+  /** flush the splitting lemma ( n OR (NOT n) )
+   *
+   * If reqPol is not 0, then a phase requirement for n is requested with
+   * polarity ( reqPol>0 ).
+   */
+  void split(Node n, int reqPol = 0);
+  /** Have we sent a lemma during the current call to a full effort check? */
+  bool hasSentLemma() const;
+  /** Have we added a fact during the current call to a full effort check? */
+  bool hasAddedFact() const;
+  /** Have we processed an inference (fact, lemma, or conflict)? */
+  bool hasProcessed() const;
+  /** Have we sent lem as a lemma in the current user context? */
+  bool hasLemmaCached(Node lem) const;
+
+ private:
+  /** constants */
+  Node d_true;
+  Node d_false;
+  /** the theory of sets which owns this */
+  TheorySetsPrivate& d_parent;
+  /** Reference to the state object for the theory of sets */
+  SolverState& d_state;
+  /** Reference to the equality engine of theory of sets */
+  eq::EqualityEngine& d_ee;
+  /** pending lemmas */
+  std::vector<Node> d_pendingLemmas;
+  /** sent lemma
+   *
+   * This flag is set to true during a full effort check if this theory
+   * called d_out->lemma(...).
+   */
+  bool d_sentLemma;
+  /** added fact
+   *
+   * This flag is set to true during a full effort check if this theory
+   * added an internal fact to its equality engine.
+   */
+  bool d_addedFact;
+  /** A user-context-dependent cache of all lemmas produced */
+  NodeSet d_lemmas_produced;
+  /**
+   * A set of nodes to ref-count. Nodes that are facts or are explanations of
+   * facts must be added to this set since the equality engine does not
+   * ref count nodes.
+   */
+  NodeSet d_keep;
+  /** Assert fact recursive
+   *
+   * This is a helper function for assertInference, which calls assertFact
+   * in theory of sets and adds to d_pendingLemmas based on fact.
+   * The argument inferType determines the policy on whether fact is processed
+   * as a fact or as a lemma (see assertInference above).
+   */
+  bool assertFactRec(Node fact, Node exp, int inferType = 0);
+};
+
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__SETS__INFERENCE_MANAGER_H */
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
new file mode 100644
index 000000000..76c7c3884
--- /dev/null
+++ b/src/theory/sets/solver_state.cpp
@@ -0,0 +1,580 @@
+/*********************                                                        */
+/*! \file solver_state.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 sets state object
+ **/
+
+#include "theory/sets/solver_state.h"
+
+#include "expr/emptyset.h"
+#include "options/sets_options.h"
+#include "theory/sets/theory_sets_private.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+SolverState::SolverState(TheorySetsPrivate& p,
+                         eq::EqualityEngine& e,
+                         context::Context* c,
+                         context::UserContext* u)
+    : d_conflict(c), d_parent(p), d_ee(e), d_proxy(u), d_proxy_to_term(u)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+void SolverState::reset()
+{
+  d_set_eqc.clear();
+  d_eqc_emptyset.clear();
+  d_eqc_univset.clear();
+  d_eqc_singleton.clear();
+  d_congruent.clear();
+  d_nvar_sets.clear();
+  d_var_set.clear();
+  d_pol_mems[0].clear();
+  d_pol_mems[1].clear();
+  d_members_index.clear();
+  d_singleton_index.clear();
+  d_bop_index.clear();
+  d_op_list.clear();
+}
+
+void SolverState::registerEqc(TypeNode tn, Node r)
+{
+  if (tn.isSet())
+  {
+    d_set_eqc.push_back(r);
+  }
+}
+
+void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
+{
+  Kind nk = n.getKind();
+  if (nk == MEMBER)
+  {
+    if (r.isConst())
+    {
+      Node s = d_ee.getRepresentative(n[1]);
+      Node x = d_ee.getRepresentative(n[0]);
+      int pindex = r == d_true ? 0 : (r == d_false ? 1 : -1);
+      if (pindex != -1)
+      {
+        if (d_pol_mems[pindex][s].find(x) == d_pol_mems[pindex][s].end())
+        {
+          d_pol_mems[pindex][s][x] = n;
+          Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n
+                               << ", pindex = " << pindex << std::endl;
+        }
+        if (d_members_index[s].find(x) == d_members_index[s].end())
+        {
+          d_members_index[s][x] = n;
+          d_op_list[MEMBER].push_back(n);
+        }
+      }
+      else
+      {
+        Assert(false);
+      }
+    }
+  }
+  else if (nk == SINGLETON || nk == UNION || nk == INTERSECTION
+           || nk == SETMINUS || nk == EMPTYSET || nk == UNIVERSE_SET)
+  {
+    if (nk == SINGLETON)
+    {
+      // singleton lemma
+      getProxy(n);
+      Node re = d_ee.getRepresentative(n[0]);
+      if (d_singleton_index.find(re) == d_singleton_index.end())
+      {
+        d_singleton_index[re] = n;
+        d_eqc_singleton[r] = n;
+        d_op_list[SINGLETON].push_back(n);
+      }
+      else
+      {
+        d_congruent[n] = d_singleton_index[re];
+      }
+    }
+    else if (nk == EMPTYSET)
+    {
+      d_eqc_emptyset[tnn] = r;
+    }
+    else if (nk == UNIVERSE_SET)
+    {
+      Assert(options::setsExt());
+      d_eqc_univset[tnn] = r;
+    }
+    else
+    {
+      Node r1 = d_ee.getRepresentative(n[0]);
+      Node r2 = d_ee.getRepresentative(n[1]);
+      std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
+      std::map<Node, Node>::iterator itb = binr1.find(r2);
+      if (itb == binr1.end())
+      {
+        binr1[r2] = n;
+        d_op_list[nk].push_back(n);
+      }
+      else
+      {
+        d_congruent[n] = itb->second;
+      }
+    }
+    d_nvar_sets[r].push_back(n);
+    Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
+  }
+  else if (nk == VARIABLE)
+  {
+    // it is important that we check kind VARIABLE, due to the semantics of the
+    // universe set.
+    if (tnn.isSet())
+    {
+      if (d_var_set.find(r) == d_var_set.end())
+      {
+        d_var_set[r] = n;
+      }
+    }
+  }
+}
+
+bool SolverState::areEqual(Node a, Node b) const
+{
+  if (a == b)
+  {
+    return true;
+  }
+  if (d_ee.hasTerm(a) && d_ee.hasTerm(b))
+  {
+    return d_ee.areEqual(a, b);
+  }
+  return false;
+}
+
+bool SolverState::areDisequal(Node a, Node b) const
+{
+  if (a == b)
+  {
+    return false;
+  }
+  else if (d_ee.hasTerm(a) && d_ee.hasTerm(b))
+  {
+    return d_ee.areDisequal(a, b, false);
+  }
+  return a.isConst() && b.isConst();
+}
+
+void SolverState::setConflict() { d_conflict = true; }
+void SolverState::setConflict(Node conf)
+{
+  d_parent.getOutputChannel()->conflict(conf);
+  d_conflict = true;
+}
+
+void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
+{
+  if (a != b)
+  {
+    Assert(areEqual(a, b));
+    exp.push_back(a.eqNode(b));
+  }
+}
+
+Node SolverState::getEmptySetEqClass(TypeNode tn) const
+{
+  std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
+  if (it != d_eqc_emptyset.end())
+  {
+    return it->second;
+  }
+  return Node::null();
+}
+
+Node SolverState::getUnivSetEqClass(TypeNode tn) const
+{
+  std::map<TypeNode, Node>::const_iterator it = d_univset.find(tn);
+  if (it != d_univset.end())
+  {
+    return it->second;
+  }
+  return Node::null();
+}
+
+Node SolverState::getSingletonEqClass(Node r) const
+{
+  std::map<Node, Node>::const_iterator it = d_eqc_singleton.find(r);
+  if (it != d_eqc_singleton.end())
+  {
+    return it->second;
+  }
+  return Node::null();
+}
+
+Node SolverState::getBinaryOpTerm(Kind k, Node r1, Node r2) const
+{
+  std::map<Kind, std::map<Node, std::map<Node, Node> > >::const_iterator itk =
+      d_bop_index.find(k);
+  if (itk == d_bop_index.end())
+  {
+    return Node::null();
+  }
+  std::map<Node, std::map<Node, Node> >::const_iterator it1 =
+      itk->second.find(r1);
+  if (it1 == itk->second.end())
+  {
+    return Node::null();
+  }
+  std::map<Node, Node>::const_iterator it2 = it1->second.find(r2);
+  if (it2 == it1->second.end())
+  {
+    return Node::null();
+  }
+  return it2->second;
+}
+
+bool SolverState::isEntailed(Node n, bool polarity) const
+{
+  if (n.getKind() == NOT)
+  {
+    return isEntailed(n[0], !polarity);
+  }
+  else if (n.getKind() == EQUAL)
+  {
+    if (polarity)
+    {
+      return areEqual(n[0], n[1]);
+    }
+    return areDisequal(n[0], n[1]);
+  }
+  else if (n.getKind() == MEMBER)
+  {
+    if (areEqual(n, polarity ? d_true : d_false))
+    {
+      return true;
+    }
+    // check members cache
+    if (polarity && d_ee.hasTerm(n[1]))
+    {
+      Node r = d_ee.getRepresentative(n[1]);
+      if (d_parent.isMember(n[0], r))
+      {
+        return true;
+      }
+    }
+  }
+  else if (n.getKind() == AND || n.getKind() == OR)
+  {
+    bool conj = (n.getKind() == AND) == polarity;
+    for (const Node& nc : n)
+    {
+      bool isEnt = isEntailed(nc, polarity);
+      if (isEnt != conj)
+      {
+        return !conj;
+      }
+    }
+    return conj;
+  }
+  else if (n.isConst())
+  {
+    return (polarity && n == d_true) || (!polarity && n == d_false);
+  }
+  return false;
+}
+
+bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
+{
+  Assert(d_ee.hasTerm(r1) && d_ee.getRepresentative(r1) == r1);
+  Assert(d_ee.hasTerm(r2) && d_ee.getRepresentative(r2) == r2);
+  TypeNode tn = r1.getType();
+  Node re = getEmptySetEqClass(tn);
+  for (unsigned e = 0; e < 2; e++)
+  {
+    Node a = e == 0 ? r1 : r2;
+    Node b = e == 0 ? r2 : r1;
+    if (isSetDisequalityEntailedInternal(a, b, re))
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
+bool SolverState::isSetDisequalityEntailedInternal(Node a,
+                                                   Node b,
+                                                   Node re) const
+{
+  // if there are members in a
+  std::map<Node, std::map<Node, Node> >::const_iterator itpma =
+      d_pol_mems[0].find(a);
+  if (itpma == d_pol_mems[0].end())
+  {
+    // no positive members, continue
+    return false;
+  }
+  // if b is empty
+  if (b == re)
+  {
+    if (!itpma->second.empty())
+    {
+      Trace("sets-deq") << "Disequality is satisfied because members are in "
+                        << a << " and " << b << " is empty" << std::endl;
+      return true;
+    }
+    else
+    {
+      // a should not be singleton
+      Assert(d_eqc_singleton.find(a) == d_eqc_singleton.end());
+    }
+    return false;
+  }
+  std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
+  std::map<Node, std::map<Node, Node> >::const_iterator itpmb =
+      d_pol_mems[1].find(b);
+  std::vector<Node> prev;
+  for (const std::pair<const Node, Node>& itm : itpma->second)
+  {
+    // if b is a singleton
+    if (itsb != d_eqc_singleton.end())
+    {
+      if (areDisequal(itm.first, itsb->second[0]))
+      {
+        Trace("sets-deq") << "Disequality is satisfied because of "
+                          << itm.second << ", singleton eq " << itsb->second[0]
+                          << std::endl;
+        return true;
+      }
+      // or disequal with another member
+      for (const Node& p : prev)
+      {
+        if (areDisequal(itm.first, p))
+        {
+          Trace("sets-deq")
+              << "Disequality is satisfied because of disequal members "
+              << itm.first << " " << p << ", singleton eq " << std::endl;
+          return true;
+        }
+      }
+      // if a has positive member that is negative member in b
+    }
+    else if (itpmb != d_pol_mems[1].end())
+    {
+      for (const std::pair<const Node, Node>& itnm : itpmb->second)
+      {
+        if (areEqual(itm.first, itnm.first))
+        {
+          Trace("sets-deq") << "Disequality is satisfied because of "
+                            << itm.second << " " << itnm.second << std::endl;
+          return true;
+        }
+      }
+    }
+    prev.push_back(itm.first);
+  }
+  return false;
+}
+
+Node SolverState::getProxy(Node n)
+{
+  Kind nk = n.getKind();
+  if (nk != EMPTYSET && nk != SINGLETON && nk != INTERSECTION && nk != SETMINUS
+      && nk != UNION)
+  {
+    return n;
+  }
+  NodeMap::const_iterator it = d_proxy.find(n);
+  if (it != d_proxy.end())
+  {
+    return (*it).second;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node k = nm->mkSkolem("sp", n.getType(), "proxy for set");
+  d_proxy[n] = k;
+  d_proxy_to_term[k] = n;
+  Node eq = k.eqNode(n);
+  Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
+  d_parent.getOutputChannel()->lemma(eq);
+  if (nk == SINGLETON)
+  {
+    Node slem = nm->mkNode(MEMBER, n[0], k);
+    Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton"
+                        << std::endl;
+    d_parent.getOutputChannel()->lemma(slem);
+  }
+  return k;
+}
+
+Node SolverState::getCongruent(Node n) const
+{
+  Assert(d_ee.hasTerm(n));
+  std::map<Node, Node>::const_iterator it = d_congruent.find(n);
+  if (it == d_congruent.end())
+  {
+    return n;
+  }
+  return it->second;
+}
+bool SolverState::isCongruent(Node n) const
+{
+  return d_congruent.find(n) != d_congruent.end();
+}
+
+Node SolverState::getEmptySet(TypeNode tn)
+{
+  std::map<TypeNode, Node>::iterator it = d_emptyset.find(tn);
+  if (it != d_emptyset.end())
+  {
+    return it->second;
+  }
+  Node n = NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
+  d_emptyset[tn] = n;
+  return n;
+}
+Node SolverState::getUnivSet(TypeNode tn)
+{
+  std::map<TypeNode, Node>::iterator it = d_univset.find(tn);
+  if (it != d_univset.end())
+  {
+    return it->second;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node n = nm->mkNullaryOperator(tn, UNIVERSE_SET);
+  for (it = d_univset.begin(); it != d_univset.end(); ++it)
+  {
+    Node n1;
+    Node n2;
+    if (tn.isSubtypeOf(it->first))
+    {
+      n1 = n;
+      n2 = it->second;
+    }
+    else if (it->first.isSubtypeOf(tn))
+    {
+      n1 = it->second;
+      n2 = n;
+    }
+    if (!n1.isNull())
+    {
+      Node ulem = nm->mkNode(SUBSET, n1, n2);
+      Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type"
+                          << std::endl;
+      d_parent.getOutputChannel()->lemma(ulem);
+    }
+  }
+  d_univset[tn] = n;
+  return n;
+}
+
+Node SolverState::getTypeConstraintSkolem(Node n, TypeNode tn)
+{
+  std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
+  if (it == d_tc_skolem[n].end())
+  {
+    Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn);
+    d_tc_skolem[n][tn] = k;
+    return k;
+  }
+  return it->second;
+}
+
+const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator it = d_nvar_sets.find(r);
+  if (it == d_nvar_sets.end())
+  {
+    return d_emptyVec;
+  }
+  return it->second;
+}
+
+Node SolverState::getVariableSet(Node r) const
+{
+  std::map<Node, Node>::const_iterator it = d_var_set.find(r);
+  if (it != d_var_set.end())
+  {
+    return it->second;
+  }
+  return Node::null();
+}
+const std::map<Node, Node>& SolverState::getMembers(Node r) const
+{
+  return getMembersInternal(r, 0);
+}
+const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
+{
+  return getMembersInternal(r, 1);
+}
+const std::map<Node, Node>& SolverState::getMembersInternal(Node r,
+                                                            unsigned i) const
+{
+  std::map<Node, std::map<Node, Node> >::const_iterator itp =
+      d_pol_mems[i].find(r);
+  if (itp == d_pol_mems[i].end())
+  {
+    return d_emptyMap;
+  }
+  return itp->second;
+}
+
+bool SolverState::hasMembers(Node r) const
+{
+  std::map<Node, std::map<Node, Node> >::const_iterator it =
+      d_pol_mems[0].find(r);
+  if (it == d_pol_mems[0].end())
+  {
+    return false;
+  }
+  return !it->second.empty();
+}
+const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
+SolverState::getBinaryOpIndex() const
+{
+  return d_bop_index;
+}
+const std::map<Kind, std::vector<Node> >& SolverState::getOperatorList() const
+{
+  return d_op_list;
+}
+
+void SolverState::debugPrintSet(Node s, const char* c) const
+{
+  if (s.getNumChildren() == 0)
+  {
+    NodeMap::const_iterator it = d_proxy_to_term.find(s);
+    if (it != d_proxy_to_term.end())
+    {
+      debugPrintSet((*it).second, c);
+    }
+    else
+    {
+      Trace(c) << s;
+    }
+  }
+  else
+  {
+    Trace(c) << "(" << s.getOperator();
+    for (const Node& sc : s)
+    {
+      Trace(c) << " ";
+      debugPrintSet(sc, c);
+    }
+    Trace(c) << ")";
+  }
+}
+
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h
new file mode 100644
index 000000000..2b4d93ed3
--- /dev/null
+++ b/src/theory/sets/solver_state.h
@@ -0,0 +1,290 @@
+/*********************                                                        */
+/*! \file solver_state.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 Sets state object
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H
+#define CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashset.h"
+#include "theory/sets/skolem_cache.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsPrivate;
+
+/** Sets state
+ *
+ * The purpose of this class is to:
+ * (1) Maintain information concerning the current set of assertions during a
+ * full effort check,
+ * (2) Maintain a database of commonly used terms.
+ *
+ * During a full effort check, the solver for theory of sets should call:
+ *   reset; ( registerEqc | registerTerm )*
+ * to initialize the information in this class regarding full effort checks.
+ * Other query calls are then valid for the remainder of the full effort check.
+ */
+class SolverState
+{
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+
+ public:
+  SolverState(TheorySetsPrivate& p,
+              eq::EqualityEngine& e,
+              context::Context* c,
+              context::UserContext* u);
+  //-------------------------------- initialize
+  /** reset, clears the data structures maintained by this class. */
+  void reset();
+  /** register equivalence class whose type is tn */
+  void registerEqc(TypeNode tn, Node r);
+  /** register term n of type tnn in the equivalence class of r */
+  void registerTerm(Node r, TypeNode tnn, Node n);
+  //-------------------------------- end initialize
+  /** Are we currently in conflict? */
+  bool isInConflict() const { return d_conflict; }
+  /**
+   * Indicate that we are in conflict, without a conflict clause. This is
+   * called, for instance, when we have propagated a conflicting literal.
+   */
+  void setConflict();
+  /** Set conf is a conflict node to be sent on the output channel.  */
+  void setConflict(Node conf);
+  /** Is a=b according to equality reasoning in the current context? */
+  bool areEqual(Node a, Node b) const;
+  /** Is a!=b according to equality reasoning in the current context? */
+  bool areDisequal(Node a, Node b) const;
+  /** add equality to explanation
+   *
+   * This adds a = b to exp if a and b are syntactically disequal. The equality
+   * a = b should hold in the current context.
+   */
+  void addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const;
+  /** Is formula n entailed to have polarity pol in the current context? */
+  bool isEntailed(Node n, bool pol) const;
+  /**
+   * Is the disequality between sets s and t entailed in the current context?
+   */
+  bool isSetDisequalityEntailed(Node s, Node t) const;
+  /**
+   * Get the equivalence class of the empty set of type tn, or null if it does
+   * not exist as a term in the current context.
+   */
+  Node getEmptySetEqClass(TypeNode tn) const;
+  /**
+   * Get the equivalence class of the universe set of type tn, or null if it
+   * does not exist as a term in the current context.
+   */
+  Node getUnivSetEqClass(TypeNode tn) const;
+  /**
+   * Get the singleton set in the equivalence class of representative r if it
+   * exists, or null if none exists.
+   */
+  Node getSingletonEqClass(Node r) const;
+  /** get binary operator term (modulo equality)
+   *
+   * This method returns a non-null node n if and only if a term n that is
+   * congruent to <k>(r1,r2) exists in the current context.
+   */
+  Node getBinaryOpTerm(Kind k, Node r1, Node r2) const;
+  /**
+   * Returns a term that is congruent to n in the current context.
+   *
+   * To ensure that inferences and processing is not redundant,
+   * this class computes congruence over all terms that exist in the current
+   * context. If a set of terms f( t1 ), ... f( tn ) are pairwise congruent
+   * (call this a "congruence class"), it selects one of these terms as a
+   * representative. All other terms return the representative term from
+   * its congruence class.
+   */
+  Node getCongruent(Node n) const;
+  /**
+   * This method returns true if n is not the representative of its congruence
+   * class.
+   */
+  bool isCongruent(Node n) const;
+  /** Get the list of all equivalence classes of set type */
+  const std::vector<Node>& getSetsEqClasses() const { return d_set_eqc; }
+  /**
+   * Get the list of non-variable sets that exists in the equivalence class
+   * whose representative is r.
+   */
+  const std::vector<Node>& getNonVariableSets(Node r) const;
+  /**
+   * Get a variable set in the equivalence class with representative r, or null
+   * if none exist.
+   */
+  Node getVariableSet(Node r) const;
+  /** Get (positive) members of the set equivalence class r
+   *
+   * The members are return as a map, which maps members to their explanation.
+   * For example, if x = y, (member 5 y), (member 6 x), then getMembers(x)
+   * returns the map [ 5 -> (member 5 y), 6 -> (member 6 x)].
+   */
+  const std::map<Node, Node>& getMembers(Node r) const;
+  /** Get negative members of the set equivalence class r, similar to above */
+  const std::map<Node, Node>& getNegativeMembers(Node r) const;
+  /** Is the (positive) members list of set equivalence class r non-empty? */
+  bool hasMembers(Node r) const;
+  /** Get binary operator index
+   *
+   * This returns a mapping from binary operator kinds (INTERSECT, SETMINUS,
+   * UNION) to index of terms of that kind. Each kind k maps to a map whose
+   * entries are of the form [r1 -> r2 -> t], where t is a term in the current
+   * context, and t is of the form <k>(t1,t2) where t1=r1 and t2=r2 hold in the
+   * current context. The term t is the representative of its congruence class.
+   */
+  const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
+  getBinaryOpIndex() const;
+  /** get operator list
+   *
+   * This returns a mapping from set kinds to a list of terms of that kind
+   * that exist in the current context. Each of the terms in the range of this
+   * map is a representative of its congruence class.
+   */
+  const std::map<Kind, std::vector<Node> >& getOperatorList() const;
+
+  // --------------------------------------- commonly used terms
+  /** Get type constraint skolem
+   *
+   * The sets theory solver outputs equality lemmas of the form:
+   *   n = d_tc_skolem[n][tn]
+   * where the type of d_tc_skolem[n][tn] is tn, and the type
+   * of n is not a subtype of tn. This is required to handle benchmarks like
+   *   test/regress/regress0/sets/sets-of-sets-subtypes.smt2
+   * where for s : (Set Int) and t : (Set Real), we have that
+   *   ( s = t ^ y in t ) implies ( exists k : Int. y = k )
+   * The type constraint Skolem for (y, Int) is the skolemization of k above.
+   */
+  Node getTypeConstraintSkolem(Node n, TypeNode tn);
+  /** get the proxy variable for set n
+   *
+   * Proxy variables are used to communicate information that otherwise would
+   * not be possible due to rewriting. For example, the literal
+   *   card( singleton( 0 ) ) = 1
+   * is rewritten to true. Instead, to communicate this fact (e.g. to other
+   * theories), we require introducing a proxy variable x for singleton( 0 ).
+   * Then:
+   *   card( x ) = 1 ^ x = singleton( 0 )
+   * communicates the equivalent of the above literal.
+   */
+  Node getProxy(Node n);
+  /** Get the empty set of type tn */
+  Node getEmptySet(TypeNode tn);
+  /** Get the universe set of type tn */
+  Node getUnivSet(TypeNode tn);
+  /**
+   * Get the skolem cache of this theory, which manages a database of introduced
+   * skolem variables used for various inferences.
+   */
+  SkolemCache& getSkolemCache() { return d_skCache; }
+  // --------------------------------------- end commonly used terms
+  /** debug print set */
+  void debugPrintSet(Node s, const char* c) const;
+
+ private:
+  /** constants */
+  Node d_true;
+  Node d_false;
+  /** the empty vector and map */
+  std::vector<Node> d_emptyVec;
+  std::map<Node, Node> d_emptyMap;
+  /** Whether or not we are in conflict. This flag is SAT context dependent. */
+  context::CDO<bool> d_conflict;
+  /** Reference to the parent theory of sets */
+  TheorySetsPrivate& d_parent;
+  /** Reference to the equality engine of theory of sets */
+  eq::EqualityEngine& d_ee;
+  /** The list of all equivalence classes of type set in the current context */
+  std::vector<Node> d_set_eqc;
+  /** Maps types to the equivalence class containing empty set of that type */
+  std::map<TypeNode, Node> d_eqc_emptyset;
+  /** Maps types to the equivalence class containing univ set of that type */
+  std::map<TypeNode, Node> d_eqc_univset;
+  /** Maps equivalence classes to a singleton set that exists in it. */
+  std::map<Node, Node> d_eqc_singleton;
+  /** Map from terms to the representative of their congruence class */
+  std::map<Node, Node> d_congruent;
+  /** Map from equivalence classes to the list of non-variable sets in it */
+  std::map<Node, std::vector<Node> > d_nvar_sets;
+  /** Map from equivalence classes to a variable sets in it */
+  std::map<Node, Node> d_var_set;
+  /** polarity memberships
+   *
+   * d_pol_mems[0] maps equivalence class to their positive membership list
+   * with explanations (see getMembers), d_pol_mems[1] maps equivalence classes
+   * to their negative memberships.
+   */
+  std::map<Node, std::map<Node, Node> > d_pol_mems[2];
+  // --------------------------------------- commonly used terms
+  /** Map from set terms to their proxy variables */
+  NodeMap d_proxy;
+  /** Backwards map of above */
+  NodeMap d_proxy_to_term;
+  /** Cache of type constraint skolems (see getTypeConstraintSkolem) */
+  std::map<Node, std::map<TypeNode, Node> > d_tc_skolem;
+  /** Map from types to empty set of that type */
+  std::map<TypeNode, Node> d_emptyset;
+  /** Map from types to universe set of that type */
+  std::map<TypeNode, Node> d_univset;
+  // --------------------------------------- end commonly used terms
+  // -------------------------------- term indices
+  /** Term index for MEMBER
+   *
+   * A term index maps equivalence class representatives to the representative
+   * of their congruence class.
+   *
+   * For example, the term index for member may contain an entry
+   * [ r1 -> r2 -> (member t1 t2) ] where r1 and r2 are representatives of their
+   * equivalence classes, (member t1 t2) is the representative of its congruence
+   * class, and r1=t1 and r2=t2 hold in the current context.
+   */
+  std::map<Node, std::map<Node, Node> > d_members_index;
+  /** Term index for SINGLETON */
+  std::map<Node, Node> d_singleton_index;
+  /** Indices for the binary kinds INTERSECT, SETMINUS and UNION. */
+  std::map<Kind, std::map<Node, std::map<Node, Node> > > d_bop_index;
+  // -------------------------------- end term indices
+  std::map<Kind, std::vector<Node> > d_op_list;
+  /** the skolem cache */
+  SkolemCache d_skCache;
+  /** is set disequality entailed internal
+   *
+   * This returns true if disequality between sets a and b is entailed in the
+   * current context. We use an incomplete test based on equality and membership
+   * information.
+   *
+   * re is the representative of the equivalence class of the empty set
+   * whose type is the same as a and b.
+   */
+  bool isSetDisequalityEntailedInternal(Node a, Node b, Node re) const;
+  /**
+   * Get members internal, returns the positive members if i=0, or negative
+   * members if i=1.
+   */
+  const std::map<Node, Node>& getMembersInternal(Node r, unsigned i) const;
+}; /* class TheorySetsPrivate */
+
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H */
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 563a981b1..869cb8926 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -52,10 +52,6 @@ void TheorySets::check(Effort e) {
   d_internal->check(e);
 }
 
-bool TheorySets::needsCheckLastEffort() {
-  return d_internal->needsCheckLastEffort();
-}
-
 bool TheorySets::collectModelInfo(TheoryModel* m)
 {
   return d_internal->collectModelInfo(m);
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 414ba4b28..4c145aedb 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -44,7 +44,6 @@ class TheorySets : public Theory
 
   void addSharedTerm(TNode) override;
   void check(Effort) override;
-  bool needsCheckLastEffort() override;
   bool collectModelInfo(TheoryModel* m) override;
   void computeCareGraph() override;
   Node explain(TNode) override;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 6e71ab2ad..472395e1b 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -40,21 +40,17 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
       d_deq(c),
       d_deq_processed(u),
       d_keep(c),
-      d_sentLemma(false),
-      d_addedFact(false),
       d_full_check_incomplete(false),
-      d_proxy(u),
-      d_proxy_to_term(u),
-      d_lemmas_produced(u),
-      d_card_enabled(false),
-      d_card_processed(u),
-      d_var_elim(u),
       d_external(external),
       d_notify(*this),
       d_equalityEngine(d_notify, c, "theory::sets::ee", true),
-      d_conflict(c),
-      d_rels(new TheorySetsRels(c, u, &d_equalityEngine, *this)),
-      d_rels_enabled(false)
+      d_state(*this, d_equalityEngine, c, u),
+      d_im(*this, d_state, d_equalityEngine, c, u),
+      d_rels(new TheorySetsRels(d_state, d_im, d_equalityEngine, u)),
+      d_cardSolver(
+          new CardinalityExtension(d_state, d_im, d_equalityEngine, c, u)),
+      d_rels_enabled(false),
+      d_card_enabled(false)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
@@ -67,8 +63,6 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
 
   d_equalityEngine.addFunctionKind(kind::MEMBER);
   d_equalityEngine.addFunctionKind(kind::SUBSET);
-
-  d_equalityEngine.addFunctionKind(kind::CARD);
 }
 
 TheorySetsPrivate::~TheorySetsPrivate(){
@@ -89,7 +83,8 @@ void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2){
 }
 
 void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
-  if( !d_conflict ){
+  if (!d_state.isInConflict())
+  {
     Trace("sets-prop-debug") << "Merge " << t1 << " and " << t2 << "..." << std::endl;
     Node s1, s2;
     EqcInfo * e2 = getOrMakeEqcInfo( t2 );
@@ -138,7 +133,8 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
         bool add = true;
         for( int j=0; j<n_members; j++ ){
           Assert( j<(int)d_members_data[t1].size() && d_members_data[t1][j].getKind()==kind::MEMBER );
-          if( ee_areEqual( m2[0], d_members_data[t1][j][0] ) ){
+          if (d_state.areEqual(m2[0], d_members_data[t1][j][0]))
+          {
             add = false;
             break;
           }
@@ -146,7 +142,7 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
         if( add ){
           if( !s1.isNull() && s2.isNull() ){
             Assert( m2[1].getType().isComparableTo( s1.getType() ) );
-            Assert( ee_areEqual( m2[1], s1 ) );
+            Assert(d_state.areEqual(m2[1], s1));
             Node exp = NodeManager::currentNM()->mkNode( kind::AND, m2[1].eqNode( s1 ), m2 );
             if( s1.getKind()==kind::SINGLETON ){
               if( s1[0]!=m2[0] ){
@@ -159,8 +155,7 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
             }else{
               //conflict
               Trace("sets-prop") << "Propagate eq-mem conflict : " << exp << std::endl;
-              d_conflict = true;
-              d_external.d_out->conflict( exp );
+              d_state.setConflict(exp);
               return;
             }
           }
@@ -204,32 +199,8 @@ TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo( TNode n, bool d
   }
 }
 
-
-bool TheorySetsPrivate::ee_areEqual( Node a, Node b ) {
-  if( a==b ){
-    return true;
-  }else{
-    if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
-      return d_equalityEngine.areEqual( a, b );
-    }else{
-      return false;
-    }
-  }
-}
-
-bool TheorySetsPrivate::ee_areDisequal( Node a, Node b ) {
-  if( a==b ){
-    return false;
-  }else{
-    if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
-      return d_equalityEngine.areDisequal( a, b, false );
-    }else{
-      return a.isConst() && b.isConst();
-    }
-  }
-}
-
-bool TheorySetsPrivate::ee_areCareDisequal( Node a, Node b ) {
+bool TheorySetsPrivate::areCareDisequal(Node a, Node b)
+{
   if( d_equalityEngine.isTriggerTerm(a, THEORY_SETS) && d_equalityEngine.isTriggerTerm(b, THEORY_SETS) ){
     TNode a_shared = d_equalityEngine.getTriggerTermRepresentative(a, THEORY_SETS);
     TNode b_shared = d_equalityEngine.getTriggerTermRepresentative(b, THEORY_SETS);
@@ -241,131 +212,33 @@ bool TheorySetsPrivate::ee_areCareDisequal( Node a, Node b ) {
   return false;
 }
 
-bool TheorySetsPrivate::isEntailed( Node n, bool polarity ) {
-  if( n.getKind()==kind::NOT ){
-    return isEntailed( n[0], !polarity );
-  }else if( n.getKind()==kind::EQUAL ){
-    if( polarity ){
-      return ee_areEqual( n[0], n[1] );
-    }else{
-      return ee_areDisequal( n[0], n[1] );
-    }
-  }else if( n.getKind()==kind::MEMBER ){
-    if( ee_areEqual( n, polarity ? d_true : d_false ) ){
-      return true;
-    }
-    //check members cache
-    if( polarity && d_equalityEngine.hasTerm( n[1] ) ){
-      Node r = d_equalityEngine.getRepresentative( n[1] );
-      if( isMember( n[0], r ) ){
-        return true;
-      }
-    }
-  }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
-    bool conj = (n.getKind()==kind::AND)==polarity;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      bool isEnt = isEntailed( n[i], polarity );
-      if( isEnt!=conj ){
-        return !conj;
-      }
-    }
-    return conj;
-  }else if( n.isConst() ){
-    return ( polarity && n==d_true ) || ( !polarity && n==d_false );
-  }
-  return false;
-}
-
 bool TheorySetsPrivate::isMember( Node x, Node s ) {
   Assert( d_equalityEngine.hasTerm( s ) && d_equalityEngine.getRepresentative( s )==s );
   NodeIntMap::iterator mem_i = d_members.find( s );
   if( mem_i != d_members.end() ) {
     for( int i=0; i<(*mem_i).second; i++ ){
-      if( ee_areEqual( d_members_data[s][i][0], x ) ){
+      if (d_state.areEqual(d_members_data[s][i][0], x))
+      {
         return true;
       }
     }
   }
   return false;
 }
-
-bool TheorySetsPrivate::isSetDisequalityEntailed( Node r1, Node r2 ) {
-  Assert( d_equalityEngine.hasTerm( r1 ) && d_equalityEngine.getRepresentative( r1 )==r1 );
-  Assert( d_equalityEngine.hasTerm( r2 ) && d_equalityEngine.getRepresentative( r2 )==r2 );
-  TypeNode tn = r1.getType();
-  Node eqc_es = d_eqc_emptyset[tn];
-  bool is_sat = false;
-  for( unsigned e=0; e<2; e++ ){
-    Node a = e==0 ? r1 : r2;
-    Node b = e==0 ? r2 : r1;
-    //if there are members in a
-    std::map< Node, std::map< Node, Node > >::iterator itpma = d_pol_mems[0].find( a );
-    if( itpma!=d_pol_mems[0].end() ){
-      Assert( !itpma->second.empty() );
-      //if b is empty
-      if( b==eqc_es ){
-        if( !itpma->second.empty() ){
-          is_sat = true;
-          Trace("sets-deq") << "Disequality is satisfied because members are in " << a << " and " << b << " is empty" << std::endl;
-        }else{
-          //a should not be singleton
-          Assert( d_eqc_singleton.find( a )==d_eqc_singleton.end() );
-        }
-      }else{
-        std::map< Node, Node >::iterator itsb = d_eqc_singleton.find( b );
-        std::map< Node, std::map< Node, Node > >::iterator itpmb = d_pol_mems[1].find( b );
-        std::vector< Node > prev;
-        for( std::map< Node, Node >::iterator itm = itpma->second.begin(); itm != itpma->second.end(); ++itm ){
-          //if b is a singleton
-          if( itsb!=d_eqc_singleton.end() ){
-            if( ee_areDisequal( itm->first, itsb->second[0] ) ){
-              Trace("sets-deq") << "Disequality is satisfied because of " << itm->second << ", singleton eq " << itsb->second[0] << std::endl;
-              is_sat = true;
-            }
-            //or disequal with another member
-            for( unsigned k=0; k<prev.size(); k++ ){
-              if( ee_areDisequal( itm->first, prev[k] ) ){
-                Trace("sets-deq") << "Disequality is satisfied because of disequal members " << itm->first << " " << prev[k] << ", singleton eq " << std::endl;
-                is_sat = true;
-                break;
-              }
-            }
-          //TODO: this can be generalized : maintain map to abstract domain ( set -> cardinality )
-          //if a has positive member that is negative member in b 
-          }else if( itpmb!=d_pol_mems[1].end() ){
-            for( std::map< Node, Node >::iterator itnm = itpmb->second.begin(); itnm != itpmb->second.end(); ++itnm ){
-              if( ee_areEqual( itm->first, itnm->first ) ){
-                Trace("sets-deq") << "Disequality is satisfied because of " << itm->second << " " << itnm->second << std::endl;
-                is_sat = true;
-                break;
-              }
-            }
-          }
-          if( is_sat ){
-            break;
-          }
-          prev.push_back( itm->first );
-        }
-      }
-      if( is_sat ){
-        break;
-      }
-    }
-  }
-  return is_sat;
-}
         
 bool TheorySetsPrivate::assertFact( Node fact, Node exp ){
   Trace("sets-assert") << "TheorySets::assertFact : " << fact << ", exp = " << exp << std::endl;
   bool polarity = fact.getKind() != kind::NOT;
   TNode atom = polarity ? fact : fact[0];
-  if( !isEntailed( atom, polarity ) ){
+  if (!d_state.isEntailed(atom, polarity))
+  {
     if( atom.getKind()==kind::EQUAL ){
       d_equalityEngine.assertEquality( atom, polarity, exp );
     }else{
       d_equalityEngine.assertPredicate( atom, polarity, exp );
     }
-    if( !d_conflict ){
+    if (!d_state.isInConflict())
+    {
       if( atom.getKind()==kind::MEMBER && polarity ){
         //check if set has a value, if so, we can propagate
         Node r = d_equalityEngine.getRepresentative( atom[1] );
@@ -384,8 +257,7 @@ bool TheorySetsPrivate::assertFact( Node fact, Node exp ){
               }
             }else{
               Trace("sets-prop") << "Propagate mem-eq conflict : " << exp << std::endl;
-              d_conflict = true;
-              d_external.d_out->conflict( exp );
+              d_state.setConflict(exp);
             }
           }
         }
@@ -404,128 +276,35 @@ bool TheorySetsPrivate::assertFact( Node fact, Node exp ){
       }
     }
     return true;
-  }else{
-    return false;
   }
-}
-
-bool TheorySetsPrivate::assertFactRec( Node fact, Node exp, std::vector< Node >& lemma, int inferType ) {
-  if( ( options::setsInferAsLemmas() && inferType!=-1 ) || inferType==1 ){
-    if( !isEntailed( fact, true ) ){
-      lemma.push_back( exp==d_true ? fact : NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, fact ) );
-      return true;
-    }
-  }else{
-    Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp << std::endl;
-    if( fact.isConst() ){
-      //either trivial or a conflict
-      if( fact==d_false ){
-        Trace("sets-lemma") << "Conflict : " << exp << std::endl;
-        d_conflict = true;
-        d_external.d_out->conflict( exp );
-        return true;
-      }
-    }else if( fact.getKind()==kind::AND || ( fact.getKind()==kind::NOT && fact[0].getKind()==kind::OR ) ){
-      bool ret = false;
-      Node f = fact.getKind()==kind::NOT ? fact[0] : fact;
-      for( unsigned i=0; i<f.getNumChildren(); i++ ){
-        Node factc = fact.getKind()==kind::NOT ? f[i].negate() : f[i];
-        bool tret = assertFactRec( factc, exp, lemma, inferType );
-        ret = ret || tret;
-        if( d_conflict ){
-          return true;
-        }
-      }
-      return ret;
-    }else{
-      bool polarity = fact.getKind() != kind::NOT;
-      TNode atom = polarity ? fact : fact[0];
-      //things we can assert to equality engine
-      if( atom.getKind()==kind::MEMBER || ( atom.getKind()==kind::EQUAL && atom[0].getType().isSet() ) ){
-        //send to equality engine
-        if( assertFact( fact, exp ) ){
-          d_addedFact = true;
-          return true;
-        }
-      }else{
-        if( !isEntailed( fact, true ) ){
-          //must send as lemma
-          lemma.push_back( exp==d_true ? fact : NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, fact ) );
-          return true;
-        }
-      }
-    }
-  }
-  return false;
-}
-void TheorySetsPrivate::assertInference( Node fact, Node exp, std::vector< Node >& lemmas, const char * c, int inferType ) {
-  d_keep.insert( exp );
-  d_keep.insert( fact );
-  if( assertFactRec( fact, exp, lemmas, inferType ) ){
-    Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by " << c << std::endl;
-    Trace("sets-assertion") << "(assert (=> " << exp << " " << fact << ")) ; by " << c << std::endl;
-  }
-}
-
-void TheorySetsPrivate::assertInference( Node fact, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType ){
-  Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ) );
-  assertInference( fact, exp_n, lemmas, c, inferType );
-}
-
-void TheorySetsPrivate::assertInference( std::vector< Node >& conc, Node exp, std::vector< Node >& lemmas, const char * c, int inferType ){
-  if( !conc.empty() ){
-    Node fact = conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::AND, conc );
-    assertInference( fact, exp, lemmas, c, inferType );
+  else
+  {
+    return false;
   }
 }
-void TheorySetsPrivate::assertInference( std::vector< Node >& conc, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType ) {
-  Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ) );
-  assertInference( conc, exp_n, lemmas, c, inferType );
-}
 
-void TheorySetsPrivate::split( Node n, int reqPol ) {
-  n = Rewriter::rewrite( n );
-  Node lem = NodeManager::currentNM()->mkNode( kind::OR, n, n.negate() );
-  std::vector< Node > lemmas;
-  lemmas.push_back( lem );
-  flushLemmas( lemmas );
-  Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
-  if( reqPol!=0 ){
-    Trace("sets-lemma") << "Sets::Require phase "  << n << " " << (reqPol>0) << std::endl;
-    d_external.getOutputChannel().requirePhase( n, reqPol>0 );
-  }
+void TheorySetsPrivate::fullEffortReset()
+{
+  Assert(d_equalityEngine.consistent());
+  d_full_check_incomplete = false;
+  d_most_common_type.clear();
+  d_most_common_type_term.clear();
+  d_card_enabled = false;
+  d_rels_enabled = false;
+  // reset the state object
+  d_state.reset();
+  // reset the inference manager
+  d_im.reset();
+  // reset the cardinality solver
+  d_cardSolver->reset();
 }
 
 void TheorySetsPrivate::fullEffortCheck(){
   Trace("sets") << "----- Full effort check ------" << std::endl;
   do{
     Trace("sets") << "...iterate full effort check..." << std::endl;
-    Assert( d_equalityEngine.consistent() );
-    d_sentLemma = false;
-    d_addedFact = false;
-    d_full_check_incomplete = false;
-    d_set_eqc.clear();
-    d_set_eqc_list.clear();
-    d_eqc_emptyset.clear();
-    d_eqc_univset.clear();
-    d_eqc_singleton.clear();
-    d_congruent.clear();
-    d_nvar_sets.clear();
-    d_var_set.clear();
-    d_most_common_type.clear();
-    d_most_common_type_term.clear();
-    d_pol_mems[0].clear();
-    d_pol_mems[1].clear();
-    d_members_index.clear();
-    d_singleton_index.clear();
-    d_bop_index.clear();
-    d_op_list.clear();
-    d_card_enabled = false;
-    d_t_card_enabled.clear();
-    d_rels_enabled = false;
-    d_eqc_to_card_term.clear();
-
-    std::vector< Node > lemmas;
+    fullEffortReset();
+
     Trace("sets-eqc") << "Equality Engine:" << std::endl;
     std::map<TypeNode, unsigned> eqcTypeCount;
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
@@ -533,13 +312,13 @@ void TheorySetsPrivate::fullEffortCheck(){
       Node eqc = (*eqcs_i);
       bool isSet = false;
       TypeNode tn = eqc.getType();
+      d_state.registerEqc(tn, eqc);
       eqcTypeCount[tn]++;
       //common type node and term
       TypeNode tnc;
       Node tnct;
       if( tn.isSet() ){
         isSet = true;
-        d_set_eqc.push_back( eqc );
         tnc = tn.getSetElementType();
         tnct = eqc;
       }
@@ -561,95 +340,29 @@ void TheorySetsPrivate::fullEffortCheck(){
             tnct = n;
           }
         }
-        if( n.getKind()==kind::MEMBER ){
-          if( eqc.isConst() ){
-            Node s = d_equalityEngine.getRepresentative( n[1] );
-            Node x = d_equalityEngine.getRepresentative( n[0] );
-            int pindex = eqc==d_true ? 0 : ( eqc==d_false ? 1 : -1 );
-            if( pindex!=-1  ){
-              if( d_pol_mems[pindex][s].find( x )==d_pol_mems[pindex][s].end() ){
-                d_pol_mems[pindex][s][x] = n;
-                Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n << ", pindex = " << pindex << std::endl;
-              }
-              if( d_members_index[s].find( x )==d_members_index[s].end() ){
-                d_members_index[s][x] = n;
-                d_op_list[kind::MEMBER].push_back( n );
-              }
-            }else{
-              Assert( false );
-            }
-          }
-        }else if( n.getKind()==kind::SINGLETON || n.getKind()==kind::UNION || n.getKind()==kind::INTERSECTION || 
-                  n.getKind()==kind::SETMINUS || n.getKind()==kind::EMPTYSET || n.getKind()==kind::UNIVERSE_SET ){
-          if( n.getKind()==kind::SINGLETON ){
-            //singleton lemma
-            getProxy( n );
-            Node r = d_equalityEngine.getRepresentative( n[0] );
-            if( d_singleton_index.find( r )==d_singleton_index.end() ){
-              d_singleton_index[r] = n;
-              d_eqc_singleton[eqc] = n;
-              d_op_list[kind::SINGLETON].push_back( n );
-            }else{
-              d_congruent[n] = d_singleton_index[r];
-            }
-          }else if( n.getKind()==kind::EMPTYSET ){
-            d_eqc_emptyset[tnn] = eqc;
-          }else if( n.getKind()==kind::UNIVERSE_SET ){
-            Assert( options::setsExt() );
-            d_eqc_univset[tnn] = eqc;
-          }else{
-            Node r1 = d_equalityEngine.getRepresentative( n[0] );
-            Node r2 = d_equalityEngine.getRepresentative( n[1] );
-            std::map<Node, Node>& binr1 = d_bop_index[n.getKind()][r1];
-            std::map<Node, Node>::iterator itb = binr1.find(r2);
-            if (itb == binr1.end())
-            {
-              binr1[r2] = n;
-              d_op_list[n.getKind()].push_back( n );
-            }else{
-              d_congruent[n] = itb->second;
-            }
-          }
-          d_nvar_sets[eqc].push_back( n );
-          Trace("sets-debug2") << "Non-var-set[" << eqc << "] : " << n << std::endl;
-          d_set_eqc_list[eqc].push_back( n );
-        }else if( n.getKind()==kind::CARD ){
+        // register it with the state
+        d_state.registerTerm(eqc, tnn, n);
+        if (n.getKind() == kind::CARD)
+        {
           d_card_enabled = true;
-          TypeNode tnc = n[0].getType().getSetElementType();
-          d_t_card_enabled[tnc] = true;
-          if( tnc.isInterpretedFinite() ){
-            std::stringstream ss;
-            ss << "ERROR: cannot use cardinality on sets with finite element "
-                  "type (term is "
-               << n << ")." << std::endl;
-            throw LogicException(ss.str());
-            //TODO: extend approach for this case
-          }
+          // register it with the cardinality solver
+          d_cardSolver->registerTerm(n);
           // if we do not handle the kind, set incomplete
           Kind nk = n[0].getKind();
+          // some kinds of cardinality we cannot handle
           if (nk == kind::UNIVERSE_SET || d_rels->isRelationKind(nk))
           {
             d_full_check_incomplete = true;
             Trace("sets-incomplete")
                 << "Sets : incomplete because of " << n << "." << std::endl;
+            // TODO (#1124) handle this case
           }
-          Node r = d_equalityEngine.getRepresentative( n[0] );
-          if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){
-            d_eqc_to_card_term[ r ] = n;
-            registerCardinalityTerm( n[0], lemmas );
-          }
-        }else{
+        }
+        else
+        {
           if( d_rels->isRelationKind( n.getKind() ) ){
             d_rels_enabled = true;
           }
-          if( isSet ){
-            d_set_eqc_list[eqc].push_back( n );
-            if( n.getKind()==kind::VARIABLE ){
-              if( d_var_set.find( eqc )==d_var_set.end() ){
-                d_var_set[eqc] = n;
-              }
-            }
-          }
         }
         ++eqc_i;
       }
@@ -662,6 +375,8 @@ void TheorySetsPrivate::fullEffortCheck(){
       ++eqcs_i;
     }
 
+    Trace("sets-eqc") << "...finished equality engine." << std::endl;
+
     if (Trace.isOn("sets-state"))
     {
       Trace("sets-state") << "Equivalence class counters:" << std::endl;
@@ -672,103 +387,103 @@ void TheorySetsPrivate::fullEffortCheck(){
       }
     }
 
-    flushLemmas( lemmas );
-    if( !hasProcessed() ){
+    // We may have sent lemmas while registering the terms in the loop above,
+    // e.g. the cardinality solver.
+    if (!d_im.hasProcessed())
+    {
       if( Trace.isOn("sets-mem") ){
-        for( unsigned i=0; i<d_set_eqc.size(); i++ ){
-          Node s = d_set_eqc[i];
+        const std::vector<Node>& sec = d_state.getSetsEqClasses();
+        for (const Node& s : sec)
+        {
           Trace("sets-mem") << "Eqc " << s << " : ";
-          std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].find( s );
-          if( it!=d_pol_mems[0].end() ){
+          const std::map<Node, Node>& smem = d_state.getMembers(s);
+          if (!smem.empty())
+          {
             Trace("sets-mem") << "Memberships : ";
-            for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-              Trace("sets-mem") << it2->first << " ";
+            for (const std::pair<const Node, Node>& it2 : smem)
+            {
+              Trace("sets-mem") << it2.first << " ";
             }
           }
-          std::map< Node, Node >::iterator its = d_eqc_singleton.find( s );
-          if( its!=d_eqc_singleton.end() ){
-            Trace("sets-mem") << " : Singleton : " << its->second;
+          Node ss = d_state.getSingletonEqClass(s);
+          if (!ss.isNull())
+          {
+            Trace("sets-mem") << " : Singleton : " << ss;
           }
           Trace("sets-mem") << std::endl;
         }
       }
-      checkSubtypes( lemmas );
-      flushLemmas( lemmas, true );
-      if( !hasProcessed() ){
-      
-        checkDownwardsClosure( lemmas );
+      checkSubtypes();
+      d_im.flushPendingLemmas(true);
+      if (!d_im.hasProcessed())
+      {
+        checkDownwardsClosure();
         if( options::setsInferAsLemmas() ){
-          flushLemmas( lemmas );
+          d_im.flushPendingLemmas();
         }
-        if( !hasProcessed() ){
-          checkUpwardsClosure( lemmas );
-          flushLemmas( lemmas );
-          if( !hasProcessed() ){
-            checkDisequalities(lemmas);
-            flushLemmas(lemmas);
-            if (!hasProcessed() && d_card_enabled)
+        if (!d_im.hasProcessed())
+        {
+          checkUpwardsClosure();
+          d_im.flushPendingLemmas();
+          if (!d_im.hasProcessed())
+          {
+            checkDisequalities();
+            d_im.flushPendingLemmas();
+            if (!d_im.hasProcessed() && d_card_enabled)
             {
-              // for cardinality
-              checkCardBuildGraph( lemmas );
-              flushLemmas( lemmas );
-              if( !hasProcessed() ){
-                checkMinCard( lemmas );
-                flushLemmas( lemmas );
-                if( !hasProcessed() ){
-                  checkCardCycles( lemmas );
-                  flushLemmas( lemmas );
-                  if( !hasProcessed() ){
-                    std::vector<Node> intro_sets;
-                    checkNormalForms( lemmas, intro_sets );
-                    flushLemmas( lemmas );
-                    if (!hasProcessed() && !intro_sets.empty())
-                    {
-                      Assert(intro_sets.size() == 1);
-                      Trace("sets-intro")
-                          << "Introduce term : " << intro_sets[0] << std::endl;
-                      Trace("sets-intro") << "  Actual Intro : ";
-                      debugPrintSet(intro_sets[0], "sets-nf");
-                      Trace("sets-nf") << std::endl;
-                      Node k = getProxy(intro_sets[0]);
-                      d_sentLemma = true;
-                    }
-                  }
-                }
-              }
+              // call the check method of the cardinality solver
+              d_cardSolver->check();
             }
           }
         }
       }
     }
-    if (!hasProcessed())
+    if (!d_im.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;
+    Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
+  } while (!d_im.hasSentLemma() && !d_state.isInConflict()
+           && d_im.hasAddedFact());
+  Trace("sets") << "----- End full effort check, conflict="
+                << d_state.isInConflict() << ", lemma=" << d_im.hasSentLemma()
+                << std::endl;
 }
 
-void TheorySetsPrivate::checkSubtypes( std::vector< Node >& lemmas ) {
- for( unsigned i=0; i<d_set_eqc.size(); i++ ){
-    Node s = d_set_eqc[i];
+void TheorySetsPrivate::checkSubtypes()
+{
+  Trace("sets") << "TheorySetsPrivate: check Subtypes..." << std::endl;
+  const std::vector<Node>& sec = d_state.getSetsEqClasses();
+  for (const Node& s : sec)
+  {
     TypeNode mct = d_most_common_type[s];
-    std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].find( s );
-    if( it!=d_pol_mems[0].end() ){
-      for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-        if (!it2->first.getType().isSubtypeOf(mct))
+    Assert(!mct.isNull());
+    const std::map<Node, Node>& smems = d_state.getMembers(s);
+    if (!smems.empty())
+    {
+      for (const std::pair<const Node, Node>& it2 : smems)
+      {
+        Trace("sets") << "  check subtype " << it2.first << " " << it2.second
+                      << std::endl;
+        Trace("sets") << "    types : " << it2.first.getType() << " " << mct
+                      << std::endl;
+        if (!it2.first.getType().isSubtypeOf(mct))
         {
           Node mctt = d_most_common_type_term[s];
+          Assert(!mctt.isNull());
+          Trace("sets") << "    most common type term is " << mctt << std::endl;
           std::vector< Node > exp;
-          exp.push_back( it2->second );
-          Assert( ee_areEqual( mctt, it2->second[1] ) );
-          exp.push_back( mctt.eqNode( it2->second[1] ) );
-          Node tc_k = getTypeConstraintSkolem(it2->first, mct);
+          exp.push_back(it2.second);
+          Assert(d_state.areEqual(mctt, it2.second[1]));
+          exp.push_back(mctt.eqNode(it2.second[1]));
+          Node tc_k = d_state.getTypeConstraintSkolem(it2.first, mct);
           if (!tc_k.isNull())
           {
-            Node etc = tc_k.eqNode(it2->first);
-            assertInference( etc, exp, lemmas, "subtype-clash" );
-            if( d_conflict ){
+            Node etc = tc_k.eqNode(it2.first);
+            d_im.assertInference(etc, exp, "subtype-clash");
+            if (d_state.isInConflict())
+            {
               return;
             }
           }
@@ -776,19 +491,28 @@ void TheorySetsPrivate::checkSubtypes( std::vector< Node >& lemmas ) {
       }
     }
   }
+  Trace("sets") << "TheorySetsPrivate: finished." << std::endl;
 }
 
-void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) {
-  Trace("sets") << "Downwards closure..." << std::endl;
+void TheorySetsPrivate::checkDownwardsClosure()
+{
+  Trace("sets") << "TheorySetsPrivate: check downwards closure..." << std::endl;
   //downwards closure
-  for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){
-    std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( it->first );
-    if( itn!=d_nvar_sets.end() ){
-      for( unsigned j=0; j<itn->second.size(); j++ ){
-        if( d_congruent.find( itn->second[j] )==d_congruent.end() ){
-          for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ 
-            Node mem = it2->second;
-            Node eq_set = itn->second[j];
+  const std::vector<Node>& sec = d_state.getSetsEqClasses();
+  for (const Node& s : sec)
+  {
+    const std::vector<Node>& nvsets = d_state.getNonVariableSets(s);
+    if (!nvsets.empty())
+    {
+      const std::map<Node, Node>& smem = d_state.getMembers(s);
+      for (const Node& nv : nvsets)
+      {
+        if (!d_state.isCongruent(nv))
+        {
+          for (const std::pair<const Node, Node>& it2 : smem)
+          {
+            Node mem = it2.second;
+            Node eq_set = nv;
             Assert( d_equalityEngine.areEqual( mem[1], eq_set ) );
             if( mem[1]!=eq_set ){
               Trace("sets-debug") << "Downwards closure based on " << mem << ", eq_set = " << eq_set << std::endl;
@@ -798,23 +522,27 @@ void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) {
                 std::vector< Node > exp;
                 exp.push_back( mem );
                 exp.push_back( mem[1].eqNode( eq_set ) );
-                assertInference( nmem, exp, lemmas, "downc" );
-                if( d_conflict ){
+                d_im.assertInference(nmem, exp, "downc");
+                if (d_state.isInConflict())
+                {
                   return;
                 }
               }else{
                 //use proxy set
-                Node k = getProxy( eq_set );
+                Node k = d_state.getProxy(eq_set);
                 Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k );
                 Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
                 nmem = Rewriter::rewrite( nmem );
                 std::vector< Node > exp;
-                if( ee_areEqual( mem, pmem ) ){
+                if (d_state.areEqual(mem, pmem))
+                {
                   exp.push_back( pmem );
-                }else{
+                }
+                else
+                {
                   nmem = NodeManager::currentNM()->mkNode( kind::OR, pmem.negate(), nmem );
                 }
-                assertInference( nmem, exp, lemmas, "downc" );
+                d_im.assertInference(nmem, exp, "downc");
               }
             }
           }
@@ -824,160 +552,176 @@ void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) {
   }
 }
 
-void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) {
+void TheorySetsPrivate::checkUpwardsClosure()
+{
   //upwards closure
-  for( std::map< Kind, std::map< Node, std::map< Node, Node > > >::iterator itb = d_bop_index.begin(); itb != d_bop_index.end(); ++itb ){
-    Kind k = itb->first;
-    Trace("sets") << "Upwards closure " << k << "..." << std::endl;
-    for( std::map< Node, std::map< Node, Node > >::iterator it = itb->second.begin(); it != itb->second.end(); ++it ){
-      Node r1 = it->first;
+  NodeManager* nm = NodeManager::currentNM();
+  const std::map<Kind, std::map<Node, std::map<Node, Node> > >& boi =
+      d_state.getBinaryOpIndex();
+  for (const std::pair<const Kind, std::map<Node, std::map<Node, Node> > >&
+           itb : boi)
+  {
+    Kind k = itb.first;
+    Trace("sets") << "TheorySetsPrivate: check upwards closure " << k << "..."
+                  << std::endl;
+    for (const std::pair<const Node, std::map<Node, Node> >& it : itb.second)
+    {
+      Node r1 = it.first;
       //see if there are members in first argument r1
-      std::map< Node, std::map< Node, Node > >::iterator itm1 = d_pol_mems[0].find( r1 );
-      if( itm1!=d_pol_mems[0].end() || k==kind::UNION ){
-        for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-          Node r2 = it2->first;
+      const std::map<Node, Node>& r1mem = d_state.getMembers(r1);
+      if (!r1mem.empty() || k == kind::UNION)
+      {
+        for (const std::pair<const Node, Node>& it2 : it.second)
+        {
+          Node r2 = it2.first;
+          Node term = it2.second;
           //see if there are members in second argument
-          std::map< Node, std::map< Node, Node > >::iterator itm2 = d_pol_mems[0].find( r2 );
-          std::map< Node, std::map< Node, Node > >::iterator itm2n = d_pol_mems[1].find( r2 );
-          if( itm2!=d_pol_mems[0].end() || k!=kind::INTERSECTION ){
-            Trace("sets-debug") << "Checking " << it2->second << ", members = " << (itm1!=d_pol_mems[0].end()) << ", " << (itm2!=d_pol_mems[0].end()) << std::endl;
+          const std::map<Node, Node>& r2mem = d_state.getMembers(r2);
+          const std::map<Node, Node>& r2nmem = d_state.getNegativeMembers(r2);
+          if (!r2mem.empty() || k != kind::INTERSECTION)
+          {
+            Trace("sets-debug")
+                << "Checking " << term << ", members = " << (!r1mem.empty())
+                << ", " << (!r2mem.empty()) << std::endl;
             //for all members of r1
-            if( itm1!=d_pol_mems[0].end() ){
-              for( std::map< Node, Node >::iterator itm1m = itm1->second.begin(); itm1m != itm1->second.end(); ++itm1m ){
-                Node xr = itm1m->first;
-                Node x = itm1m->second[0];
-                Trace("sets-debug") << "checking membership " << xr << " " << itm1m->second << std::endl;
+            if (!r1mem.empty())
+            {
+              for (const std::pair<const Node, Node>& itm1m : r1mem)
+              {
+                Node xr = itm1m.first;
+                Node x = itm1m.second[0];
+                Trace("sets-debug") << "checking membership " << xr << " "
+                                    << itm1m.second << std::endl;
                 std::vector< Node > exp;
-                exp.push_back( itm1m->second );
-                addEqualityToExp( it2->second[0], itm1m->second[1], exp );
+                exp.push_back(itm1m.second);
+                d_state.addEqualityToExp(term[0], itm1m.second[1], exp);
                 bool valid = false;
                 int inferType = 0;
                 if( k==kind::UNION ){
                   valid = true;
                 }else if( k==kind::INTERSECTION ){
-                  //conclude x is in it2->second
-                  //if also existing in members of r2
-                  bool in_r2 = itm2!=d_pol_mems[0].end() && itm2->second.find( xr )!=itm2->second.end();
-                  if( in_r2 ){
-                    exp.push_back( itm2->second[xr] );
-                    addEqualityToExp( it2->second[1], itm2->second[xr][1], exp );
-                    addEqualityToExp( x, itm2->second[xr][0], exp );
+                  // conclude x is in term
+                  // if also existing in members of r2
+                  std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
+                  if (itm != r2mem.end())
+                  {
+                    exp.push_back(itm->second);
+                    d_state.addEqualityToExp(term[1], itm->second[1], exp);
+                    d_state.addEqualityToExp(x, itm->second[0], exp);
                     valid = true;
-                  }else{
+                  }
+                  else
+                  {
                     // if not, check whether it is definitely not a member, if unknown, split
-                    bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2n->second.end();
-                    if( !not_in_r2 ){
-                      exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ) );
+                    if (r2nmem.find(xr) == r2nmem.end())
+                    {
+                      exp.push_back(nm->mkNode(kind::MEMBER, x, term[1]));
                       valid = true;
                       inferType = 1;
                     }
                   }
                 }else{
                   Assert( k==kind::SETMINUS );
-                  /*
-                  std::map< Node, std::map< Node, Node > >::iterator itnm2 = d_pol_mems[1].find( r2 );
-                  if( itnm2!=d_pol_mems[1].end() ){
-                    bool not_in_r2 = itnm2->second.find( xr )!=itnm2->second.end();
-                    if( not_in_r2 ){
-                      exp.push_back( itnm2->second[xr] );
-                      if( it2->second[1]!=itnm2->second[xr][1] ){
-                        Assert( d_equalityEngine.areEqual( it2->second[1], itnm2->second[xr][1] ) );
-                        exp.push_back( it2->second[1].eqNode( itnm2->second[xr][1] ) );
-                      }
-                      if( x!=itnm2->second[xr][0] ){
-                        Assert( d_equalityEngine.areEqual( x, itnm2->second[xr][0] ) );
-                        exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, x, itnm2->second[xr][0] ) );
-                      }
-                      valid = true;
-                    }
-                  }
-                  */
-                  if( !valid ){
-                    bool in_r2 = itm2!=d_pol_mems[0].end() && itm2->second.find( xr )!=itm2->second.end();
-                    if( !in_r2 ){
-                      // must add lemma for set minus since non-membership in this case is not explained
-                      exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ).negate() );
-                      valid = true;
-                      inferType = 1;
-                    }
+                  std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
+                  if (itm == r2mem.end())
+                  {
+                    // must add lemma for set minus since non-membership in this
+                    // case is not explained
+                    exp.push_back(
+                        nm->mkNode(kind::MEMBER, x, term[1]).negate());
+                    valid = true;
+                    inferType = 1;
                   }
                 }
                 if( valid ){
-                  Node rr = d_equalityEngine.getRepresentative( it2->second );
+                  Node rr = d_equalityEngine.getRepresentative(term);
                   if( !isMember( x, rr ) ){
-                    Node kk = getProxy( it2->second );
-                    Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, x, kk );
-                    assertInference( fact, exp, lemmas, "upc", inferType );
-                    if( d_conflict ){
+                    Node kk = d_state.getProxy(term);
+                    Node fact = nm->mkNode(kind::MEMBER, x, kk);
+                    d_im.assertInference(fact, exp, "upc", inferType);
+                    if (d_state.isInConflict())
+                    {
                       return;
                     }
                   }
                 }
-                Trace("sets-debug") << "done checking membership " << xr << " " << itm1m->second << std::endl;
+                Trace("sets-debug") << "done checking membership " << xr << " "
+                                    << itm1m.second << std::endl;
               }
             }
             if( k==kind::UNION ){
-              if( itm2!=d_pol_mems[0].end() ){
+              if (!r2mem.empty())
+              {
                 //for all members of r2
-                for( std::map< Node, Node >::iterator itm2m = itm2->second.begin(); itm2m != itm2->second.end(); ++itm2m ){
-                  Node x = itm2m->second[0];
-                  Node rr = d_equalityEngine.getRepresentative( it2->second );
+                for (const std::pair<const Node, Node>& itm2m : r2mem)
+                {
+                  Node x = itm2m.second[0];
+                  Node rr = d_equalityEngine.getRepresentative(term);
                   if( !isMember( x, rr ) ){
                     std::vector< Node > exp;
-                    exp.push_back( itm2m->second );
-                    addEqualityToExp( it2->second[1], itm2m->second[1], exp );
-                    Node k = getProxy( it2->second );
-                    Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, x, k );
-                    assertInference( fact, exp, lemmas, "upc2" );
-                    if( d_conflict ){
+                    exp.push_back(itm2m.second);
+                    d_state.addEqualityToExp(term[1], itm2m.second[1], exp);
+                    Node k = d_state.getProxy(term);
+                    Node fact = nm->mkNode(kind::MEMBER, x, k);
+                    d_im.assertInference(fact, exp, "upc2");
+                    if (d_state.isInConflict())
+                    {
                       return;
                     }
                   }
                 }
               }
-            }   
-          }      
+            }
+          }
         }
       }
     }
   }
-  if( !hasProcessed() ){
+  if (!d_im.hasProcessed())
+  {
     if( options::setsExt() ){
       //universal sets
       Trace("sets-debug") << "Check universe sets..." << std::endl;
       //all elements must be in universal set
-      for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){
+      const std::vector<Node>& sec = d_state.getSetsEqClasses();
+      for (const Node& s : sec)
+      {
         //if equivalence class contains a variable
-        std::map< Node, Node >::iterator itv = d_var_set.find( it->first );
-        if( itv!=d_var_set.end() ){
+        Node v = d_state.getVariableSet(s);
+        if (!v.isNull())
+        {
           //the variable in the equivalence class
-          Node v = itv->second;
           std::map< TypeNode, Node > univ_set;
-          for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-            Node e = it2->second[0];
+          const std::map<Node, Node>& smems = d_state.getMembers(s);
+          for (const std::pair<const Node, Node>& it2 : smems)
+          {
+            Node e = it2.second[0];
             TypeNode tn = NodeManager::currentNM()->mkSetType( e.getType() );
             Node u;
             std::map< TypeNode, Node >::iterator itu = univ_set.find( tn );
             if( itu==univ_set.end() ){
-              std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn );
+              Node ueqc = d_state.getUnivSetEqClass(tn);
               // if the universe does not yet exist, or is not in this equivalence class
-              if( itu==d_eqc_univset.end() || itu->second!=it->first ){
-                u = getUnivSet( tn );
+              if (s != ueqc)
+              {
+                u = d_state.getUnivSet(tn);
               }
               univ_set[tn] = u;
             }else{
               u = itu->second;
             }
             if( !u.isNull() ){
-              Assert( it2->second.getKind()==kind::MEMBER );
+              Assert(it2.second.getKind() == kind::MEMBER);
               std::vector< Node > exp;
-              exp.push_back( it2->second );
-              if( v!=it2->second[1] ){
-                exp.push_back( v.eqNode( it2->second[1] ) );
+              exp.push_back(it2.second);
+              if (v != it2.second[1])
+              {
+                exp.push_back(v.eqNode(it2.second[1]));
               }
-              Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, it2->second[0], u );
-              assertInference( fact, exp, lemmas, "upuniv" );
-              if( d_conflict ){
+              Node fact = nm->mkNode(kind::MEMBER, it2.second[0], u);
+              d_im.assertInference(fact, exp, "upuniv");
+              if (d_state.isInConflict())
+              {
                 return;
               }
             }
@@ -988,9 +732,10 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) {
   }
 }
 
-void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) {
+void TheorySetsPrivate::checkDisequalities()
+{
   //disequalities
-  Trace("sets") << "Disequalities..." << std::endl;
+  Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl;
   for(NodeBoolMap::const_iterator it=d_deq.begin(); it !=d_deq.end(); ++it) {
     if( (*it).second ){
       Node deq = (*it).first;
@@ -998,7 +743,7 @@ void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) {
       Assert( d_equalityEngine.hasTerm( deq[0] ) && d_equalityEngine.hasTerm( deq[1] ) );
       Node r1 = d_equalityEngine.getRepresentative( deq[0] );
       Node r2 = d_equalityEngine.getRepresentative( deq[1] );
-      bool is_sat = isSetDisequalityEntailed( r1, r2 );
+      bool is_sat = d_state.isSetDisequalityEntailed(r1, r2);
       /*
       if( !is_sat ){
         //try to make one of them empty
@@ -1021,9 +766,10 @@ void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) {
           Node mem2 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[1] );
           Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::EQUAL, mem1, mem2 ).negate() );
           lem = Rewriter::rewrite( lem );
-          assertInference( lem, d_emp_exp, lemmas, "diseq", 1 );
-          flushLemmas( lemmas );
-          if( hasProcessed() ){
+          d_im.assertInference(lem, d_emp_exp, "diseq", 1);
+          d_im.flushPendingLemmas();
+          if (d_im.hasProcessed())
+          {
             return;
           }
         }
@@ -1032,713 +778,6 @@ void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) {
   }
 }
 
-void TheorySetsPrivate::checkCardBuildGraph( std::vector< Node >& lemmas ) {
-  Trace("sets") << "Cardinality graph..." << std::endl;
-  //first, ensure cardinality relationships are added as lemmas for all non-basic set terms
-  for( unsigned i=0; i<d_set_eqc.size(); i++ ){
-    Node eqc = d_set_eqc[i];
-    std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
-    if( itn!=d_nvar_sets.end() ){
-      for( unsigned j=0; j<itn->second.size(); j++ ){
-        Node n = itn->second[j];
-        if( d_congruent.find( n )==d_congruent.end() ){
-          //if setminus, do for intersection instead
-          if( n.getKind()==kind::SETMINUS ){
-            n = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, n[0], n[1] ) );
-          }
-          registerCardinalityTerm( n, lemmas );
-        }
-      }
-    }
-  }
-  Trace("sets") << "Done cardinality graph" << std::endl;
-}
-
-void TheorySetsPrivate::registerCardinalityTerm( Node n, std::vector< Node >& lemmas ){
-  TypeNode tnc = n.getType().getSetElementType();
-  if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end())
-  {
-    // if no cardinality constraints for sets of this type, we can ignore
-    return;
-  }
-  if( d_card_processed.find( n )==d_card_processed.end() ){
-    d_card_processed.insert( n );
-    Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
-    std::vector< Node > cterms;
-    if( n.getKind()==kind::INTERSECTION ){
-      for( unsigned e=0; e<2; e++ ){
-        Node s = NodeManager::currentNM()->mkNode( kind::SETMINUS, n[e], n[1-e] );
-        cterms.push_back( s );
-      }
-      Node pos_lem = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::CARD, n ), d_zero );
-      assertInference( pos_lem, d_emp_exp, lemmas, "pcard", 1 );
-    }else{
-      cterms.push_back( n );
-    }
-    for( unsigned k=0; k<cterms.size(); k++ ){
-      Node nn = cterms[k];
-      Node nk = getProxy( nn );
-      Node pos_lem = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::CARD, nk ), d_zero );
-      assertInference( pos_lem, d_emp_exp, lemmas, "pcard", 1 );
-      if( nn!=nk ){
-        Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::CARD, nk ),
-                                                                  NodeManager::currentNM()->mkNode( kind::CARD, nn ) );
-        lem = Rewriter::rewrite( lem );
-        Trace("sets-card") << "  " << k << " : " << lem << std::endl;
-        assertInference( lem, d_emp_exp, lemmas, "card", 1 );
-      }
-    }
-  }
-}
-
-void TheorySetsPrivate::checkCardCycles( std::vector< Node >& lemmas ) {
-  Trace("sets") << "Check cardinality cycles..." << std::endl;
-  //build order of equivalence classes, also build cardinality graph
-  std::vector< Node > set_eqc_tmp;
-  set_eqc_tmp.insert( set_eqc_tmp.end(), d_set_eqc.begin(), d_set_eqc.end() );
-  d_set_eqc.clear();
-  d_card_parent.clear();
-  for( unsigned i=0; i<set_eqc_tmp.size(); i++ ){
-    std::vector< Node > curr;
-    std::vector< Node > exp;
-    checkCardCyclesRec( set_eqc_tmp[i], curr, exp, lemmas );
-    flushLemmas( lemmas );
-    if( hasProcessed() ){
-      return;
-    }
-  }
-  Trace("sets") << "Done check cardinality cycles" << std::endl;
-}
-
-void TheorySetsPrivate::checkCardCyclesRec( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp, std::vector< Node >& lemmas ) {
-  if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
-    Trace("sets-debug") << "Found venn region loop..." << std::endl;
-    if( curr.size()>1 ){
-      //all regions must be equal
-      std::vector< Node > conc;
-      for( unsigned i=1; i<curr.size(); i++ ){
-        conc.push_back( curr[0].eqNode( curr[i] ) );
-      }
-      Node fact = conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::AND, conc );
-      assertInference( fact, exp, lemmas, "card_cycle" );
-      flushLemmas( lemmas );
-    }else{
-      //should be guaranteed based on not exploring equal parents
-      Assert( false );
-    }
-  }else if( std::find( d_set_eqc.begin(), d_set_eqc.end(), eqc )==d_set_eqc.end() ){
-    curr.push_back( eqc );
-    TypeNode tn = eqc.getType();
-    bool is_empty = eqc==d_eqc_emptyset[tn];
-    Node emp_set = getEmptySet( tn );
-    std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
-    if( itn!=d_nvar_sets.end() ){
-      for( unsigned j=0; j<itn->second.size(); j++ ){
-        Node n = itn->second[j];
-        if( n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS ){
-          Trace("sets-debug") << "Build cardinality parents for " << n << "..." << std::endl;
-          std::vector< Node > sib;
-          unsigned true_sib = 0;
-          if( n.getKind()==kind::INTERSECTION ){
-            d_card_base[n] = n;
-            for( unsigned e=0; e<2; e++ ){
-              Node sm = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::SETMINUS, n[e], n[1-e] ) );
-              sib.push_back( sm );
-            }
-            true_sib = 2;
-          }else{
-            Node si = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, n[0], n[1] ) );
-            sib.push_back( si );
-            d_card_base[n] = si;
-            Node osm = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::SETMINUS, n[1], n[0] ) );
-            sib.push_back( osm );
-            true_sib = 1;
-          }
-          Node u = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::UNION, n[0], n[1] ) );
-          if( !d_equalityEngine.hasTerm( u ) ){
-            u = Node::null();
-          }
-          unsigned n_parents = true_sib + ( u.isNull() ? 0 : 1 );
-          //if this set is empty
-          if( is_empty ){
-            Assert( ee_areEqual( n, emp_set ) );
-            Trace("sets-debug") << "  empty, parents equal siblings" << std::endl;
-            std::vector< Node > conc;
-            //parent equal siblings
-            for( unsigned e=0; e<true_sib; e++ ){
-              if( d_equalityEngine.hasTerm( sib[e] ) && !ee_areEqual( n[e], sib[e] ) ){
-                conc.push_back( n[e].eqNode( sib[e] ) );
-              }
-            }
-            assertInference( conc, n.eqNode( emp_set ), lemmas, "cg_emp" );
-            flushLemmas( lemmas );
-            if( hasProcessed() ){
-              return;
-            }else{
-              //justify why there is no edge to parents (necessary?)
-              for( unsigned e=0; e<n_parents; e++ ){
-                Node p = (e==true_sib) ? u : n[e];
-                
-              }
-            }
-          }else{
-            std::vector< Node > card_parents;
-            std::vector< int > card_parent_ids;
-            //check if equal to a parent
-            for( unsigned e=0; e<n_parents; e++ ){
-              Trace("sets-debug") << "  check parent " << e << "/" << n_parents << std::endl;
-              bool is_union = e==true_sib;
-              Node p = (e==true_sib) ? u : n[e];
-              Trace("sets-debug") << "  check relation to parent " << p << ", isu=" << is_union << "..." << std::endl;
-              //if parent is empty
-              if( ee_areEqual( p, emp_set ) ){
-                Trace("sets-debug") << "  it is empty..." << std::endl;
-                Assert( !ee_areEqual( n, emp_set ) );
-                assertInference( n.eqNode( emp_set ), p.eqNode( emp_set ), lemmas, "cg_emppar" );
-                if( hasProcessed() ){
-                  return;
-                }
-              //if we are equal to a parent
-              }else if( ee_areEqual( p, n ) ){
-                Trace("sets-debug") << "  it is equal to this..." << std::endl;
-                std::vector< Node > conc;
-                std::vector< int > sib_emp_indices;
-                if( is_union ){
-                  for( unsigned s=0; s<sib.size(); s++ ){
-                    sib_emp_indices.push_back( s );
-                  }
-                }else{
-                  sib_emp_indices.push_back( e );
-                }
-                //sibling(s) are empty
-                for( unsigned s=0; s<sib_emp_indices.size(); s++ ){
-                  unsigned si = sib_emp_indices[s];
-                  if( !ee_areEqual( sib[si], emp_set ) ){
-                    conc.push_back( sib[si].eqNode( emp_set ) );
-                  }else{
-                    Trace("sets-debug") << "Sibling " << sib[si] << " is already empty." << std::endl;
-                  }
-                }
-                if( !is_union && n.getKind()==kind::INTERSECTION && !u.isNull() ){
-                  //union is equal to other parent
-                  if( !ee_areEqual( u, n[1-e] ) ){
-                    conc.push_back( u.eqNode( n[1-e] ) );
-                  }
-                }
-                Trace("sets-debug") << "...derived " << conc.size() << " conclusions" << std::endl;
-                assertInference( conc, n.eqNode( p ), lemmas, "cg_eqpar" );
-                flushLemmas( lemmas );
-                if( hasProcessed() ){
-                  return;
-                }
-              }else{
-                Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
-                //otherwise, we a syntactic subset of p
-                card_parents.push_back( p );
-                card_parent_ids.push_back( is_union ? 2 : e );
-              }
-            }
-            Assert( d_card_parent[n].empty() );
-            Trace("sets-debug") << "get parent representatives..." << std::endl;
-            //for each parent, take their representatives
-            for( unsigned k=0; k<card_parents.size(); k++ ){
-              Node eqcc = d_equalityEngine.getRepresentative( card_parents[k] );
-              Trace("sets-debug") << "Check card parent " << k << "/" << card_parents.size() << std::endl;
-              
-              //if parent is singleton, then we should either be empty to equal to it
-              std::map< Node, Node >::iterator itps = d_eqc_singleton.find( eqcc );
-              if( itps!=d_eqc_singleton.end() ){
-                bool eq_parent = false;
-                std::vector< Node > exp;
-                addEqualityToExp( card_parents[k], itps->second, exp );
-                if( ee_areDisequal( n, emp_set ) ){
-                  exp.push_back( n.eqNode( emp_set ).negate() );
-                  eq_parent = true;
-                }else{
-                  std::map< Node, std::map< Node, Node > >::iterator itpm = d_pol_mems[0].find( eqc );
-                  if( itpm!=d_pol_mems[0].end() && !itpm->second.empty() ){
-                    Node pmem = itpm->second.begin()->second;
-                    exp.push_back( pmem );
-                    addEqualityToExp( n, pmem[1], exp );
-                    eq_parent = true;
-                  }
-                }
-                //must be equal to parent
-                if( eq_parent ){
-                  Node conc = n.eqNode(  card_parents[k] );
-                  assertInference( conc, exp, lemmas, "cg_par_sing" );
-                  flushLemmas( lemmas );
-                }else{
-                  //split on empty
-                  Trace("sets-nf") << "Split empty : " << n << std::endl;
-                  split( n.eqNode( emp_set ), 1 );
-                }
-                Assert( hasProcessed() );
-                return;
-              }else{
-                bool dup = false;
-                for( unsigned l=0; l<d_card_parent[n].size(); l++ ){
-                  if( eqcc==d_card_parent[n][l] ){
-                    Trace("sets-debug") << "  parents " << l << " and " << k << " are equal, ids = " << card_parent_ids[l] << " " << card_parent_ids[k] << std::endl;
-                    dup = true;
-                    if( n.getKind()==kind::INTERSECTION ){
-                      Assert( card_parent_ids[l]!=2 );
-                      std::vector< Node > conc;
-                      if( card_parent_ids[k]==2 ){
-                        //intersection is equal to other parent
-                        unsigned pid = 1-card_parent_ids[l];
-                        if( !ee_areEqual( n[pid], n ) ){
-                          Trace("sets-debug") << "  one of them is union, make equal to other..." << std::endl;
-                          conc.push_back( n[pid].eqNode( n ) );
-                        }
-                      }else{
-                        if( !ee_areEqual( card_parents[k], n ) ){
-                          Trace("sets-debug") << "  neither is union, make equal to one parent..." << std::endl;
-                          //intersection is equal to one of the parents
-                          conc.push_back( card_parents[k].eqNode( n ) );
-                        }
-                      }
-                      assertInference( conc, card_parents[k].eqNode( d_card_parent[n][l] ), lemmas, "cg_pareq" );
-                      flushLemmas( lemmas );
-                      if( hasProcessed() ){
-                        return;
-                      }
-                    }
-                  }
-                }
-                if( !dup ){
-                  d_card_parent[n].push_back( eqcc );
-                }
-              }
-            }
-            //now recurse on parents (to ensure their normal will be computed after this eqc)
-            exp.push_back( eqc.eqNode( n ) );
-            for( unsigned k=0; k<d_card_parent[n].size(); k++ ){
-              checkCardCyclesRec( d_card_parent[n][k], curr, exp, lemmas );
-              if( hasProcessed() ){
-                return;
-              }
-            }
-            exp.pop_back();
-          }
-        }
-      }
-    }
-    curr.pop_back();
-    //parents now processed, can add to ordered list
-    d_set_eqc.push_back( eqc );
-  }else{
-    //already processed
-  }  
-}
-
-void TheorySetsPrivate::checkNormalForms( std::vector< Node >& lemmas, std::vector< Node >& intro_sets ){
-  Trace("sets") << "Check normal forms..." << std::endl;
-  // now, build normal form for each equivalence class
-  //   d_set_eqc is now sorted such that for each d_set_eqc[i], d_set_eqc[j], 
-  //      if d_set_eqc[i] is a strict syntactic subterm of d_set_eqc[j], then i<j.
-  d_ff.clear();
-  d_nf.clear();
-  for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
-    checkNormalForm( d_set_eqc[i], intro_sets );
-    if( hasProcessed() || !intro_sets.empty() ){
-      return;
-    }
-  }
-  Trace("sets") << "Done check normal forms" << std::endl;
-}
-
-void TheorySetsPrivate::checkNormalForm( Node eqc, std::vector< Node >& intro_sets ){
-  TypeNode tn = eqc.getType();
-  Trace("sets") << "Compute normal form for " << eqc << std::endl;
-  Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
-  if( eqc==d_eqc_emptyset[tn] ){
-    d_nf[eqc].clear();
-    Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
-  }else{
-    //flat/normal forms are sets of equivalence classes
-    Node base;
-    std::vector< Node > comps;
-    std::map< Node, std::map< Node, std::vector< Node > > >::iterator it = d_ff.find( eqc );
-    if( it!=d_ff.end() ){
-      for( std::map< Node, std::vector< Node > >::iterator itf = it->second.begin(); itf != it->second.end(); ++itf ){
-        std::sort( itf->second.begin(), itf->second.end() );
-        if( base.isNull() ){
-          base = itf->first;
-        }else{
-          comps.push_back( itf->first );
-        }
-        Trace("sets-nf") << "  F " << itf->first << " : ";
-        if( Trace.isOn("sets-nf") ){
-          Trace("sets-nf") << "{ ";
-          for( unsigned k=0; k<itf->second.size(); k++ ){
-            if( k>0 ){ Trace("sets-nf") << ", "; }
-            Trace("sets-nf") << "[" << itf->second[k] << "]";
-          }
-          Trace("sets-nf") << " }" << std::endl;
-        }
-        Trace("sets-nf-debug") << " ...";
-        debugPrintSet( itf->first, "sets-nf-debug" );
-        Trace("sets-nf-debug") << std::endl;
-      }
-    }else{
-      Trace("sets-nf") << "(no flat forms)" << std::endl;
-    }
-
-    Assert( d_nf.find( eqc )==d_nf.end() );
-    bool success = true;
-    Node emp_set = getEmptySet(tn);
-    if( !base.isNull() ){
-      for( unsigned j=0; j<comps.size(); j++ ){
-        //compare if equal
-        std::vector< Node > c;
-        c.push_back( base );
-        c.push_back( comps[j] );
-        std::vector< Node > only[2];
-        std::vector< Node > common;
-        Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs " << comps[j] << std::endl;
-        unsigned k[2] = { 0, 0 };
-        while( k[0]<d_ff[eqc][c[0]].size() || k[1]<d_ff[eqc][c[1]].size() ){
-          bool proc = true;
-          for( unsigned e=0; e<2; e++ ){
-            if( k[e]==d_ff[eqc][c[e]].size() ){
-              for( ; k[1-e]<d_ff[eqc][c[1-e]].size(); ++k[1-e] ){
-                only[1-e].push_back( d_ff[eqc][c[1-e]][k[1-e]] );
-              }
-              proc = false;
-            }
-          }
-          if( proc ){
-            if( d_ff[eqc][c[0]][k[0]]==d_ff[eqc][c[1]][k[1]] ){
-              common.push_back( d_ff[eqc][c[0]][k[0]] );
-              k[0]++;
-              k[1]++;
-            }else if( d_ff[eqc][c[0]][k[0]]<d_ff[eqc][c[1]][k[1]] ){
-              only[0].push_back( d_ff[eqc][c[0]][k[0]] );
-              k[0]++;
-            }else{
-              only[1].push_back( d_ff[eqc][c[1]][k[1]] );
-              k[1]++;
-            }
-          }
-        }
-        if( !only[0].empty() || !only[1].empty() ){
-          if( Trace.isOn("sets-nf-debug") ){
-            Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
-            for( unsigned e=0; e<2; e++ ){
-              Trace("sets-nf-debug") << "  " << c[e] << " : { ";
-              for( unsigned l=0; l<only[e].size(); l++ ){
-                if( l>0 ){ Trace("sets-nf-debug") << ", "; }
-                Trace("sets-nf-debug") << "[" << only[e][l] << "]";
-              }
-              Trace("sets-nf-debug") << " }" << std::endl;
-            }
-          }
-          //try to make one empty, prefer the unique ones first
-          for( unsigned e=0; e<3; e++ ){
-            unsigned sz = e==2 ? common.size() : only[e].size();
-            for( unsigned l=0; l<sz; l++ ){
-              Node r = e==2 ? common[l] : only[e][l];
-              Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
-              Trace("sets-nf-debug") << "         actual : ";
-              debugPrintSet( r, "sets-nf-debug" );
-              Trace("sets-nf-debug") << std::endl;
-              Assert( !ee_areEqual( r, emp_set ) );
-              if( !ee_areDisequal( r, emp_set ) && ( d_pol_mems[0].find( r )==d_pol_mems[0].end() || d_pol_mems[0][r].empty() ) ){
-                //guess that its equal empty if it has no explicit members
-                Trace("sets-nf") << " Split empty : " << r << std::endl;
-                Trace("sets-nf") << "Actual Split : ";
-                debugPrintSet( r, "sets-nf" );
-                Trace("sets-nf") << std::endl;
-                split( r.eqNode( emp_set ), 1 );
-                Assert( hasProcessed() );
-                return;
-              }
-            }
-          }
-          for( unsigned l=0; l<only[0].size(); l++ ){
-            for( unsigned m=0; m<only[1].size(); m++ ){
-              bool disjoint = false;
-              Trace("sets-nf-debug") << "Try split " << only[0][l] << " against " << only[1][m] << std::endl;
-              //split them
-              for( unsigned e=0; e<2; e++ ){
-                Node r1 = e==0 ? only[0][l] : only[1][m];
-                Node r2 = e==0 ? only[1][m] : only[0][l];
-                //check if their intersection exists modulo equality
-                std::map< Node, Node >::iterator itb = d_bop_index[kind::INTERSECTION][r1].find( r2 );
-                if( itb!=d_bop_index[kind::INTERSECTION][r1].end() ){
-                  Trace("sets-nf-debug") << "Split term already exists, but not in cardinality graph : " << itb->second << ", should be empty." << std::endl;
-                  //their intersection is empty (probably?)
-                  // e.g. these are two disjoint venn regions, proceed to next pair
-                  Assert( ee_areEqual( emp_set, itb->second ) );
-                  disjoint = true;
-                  break;
-                }
-              }
-              if( !disjoint ){
-                //simply introduce their intersection
-                Assert( only[0][l]!=only[1][m] );
-                Node kca = getProxy( only[0][l] );
-                Node kcb = getProxy( only[1][m] );
-                Node intro = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, kca, kcb ) );
-                Trace("sets-nf") << "   Intro split : " << only[0][l] << " against " << only[1][m] << ", term is " << intro << std::endl;
-                intro_sets.push_back( intro );
-                Assert( !d_equalityEngine.hasTerm( intro ) );
-                return;
-              }
-            }
-          }
-          //should never get here
-          success = false;
-        }
-      }
-      if( success ){
-        //normal form is flat form of base
-        d_nf[eqc].insert( d_nf[eqc].end(), d_ff[eqc][base].begin(), d_ff[eqc][base].end() );
-        Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
-      }else{
-        Trace("sets-nf") << "failed to build N " << eqc << std::endl;
-      }
-    }else{
-      // must ensure disequal from empty
-      if (!eqc.isConst() && !ee_areDisequal(eqc, emp_set)
-          && (d_pol_mems[0].find(eqc) == d_pol_mems[0].end()
-              || d_pol_mems[0][eqc].empty()))
-      {
-        Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
-        split(eqc.eqNode(emp_set));
-        success = false;
-      }
-      else
-      {
-        // normal form is this equivalence class
-        d_nf[eqc].push_back(eqc);
-        Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }"
-                         << std::endl;
-      }
-    }
-    if( success ){
-      //send to parents
-      std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
-      if( itn!=d_nvar_sets.end() ){
-        std::map< Node, std::map< Node, bool > > parents_proc;
-        for( unsigned j=0; j<itn->second.size(); j++ ){
-          Node n = itn->second[j];
-          Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
-          if( !d_card_parent[n].empty() ){
-            Assert( d_card_base.find( n )!=d_card_base.end() );
-            Node cbase = d_card_base[n];
-            Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
-            for( unsigned k=0; k<d_card_parent[n].size(); k++ ){
-              Node p = d_card_parent[n][k];
-              Trace("sets-nf-debug") << "Check parent " << p << std::endl;
-              if( parents_proc[cbase].find( p )==parents_proc[cbase].end() ){
-                parents_proc[cbase][p] = true;
-                Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p << "] ), from " << n << "..." << std::endl;
-                //for( unsigned i=0; i<d_nf[eqc].size(); i++ ){
-                //  Assert( std::find( d_ff[p][cbase].begin(), d_ff[p][cbase].end(), d_nf[eqc][i] )==d_ff[p][cbase].end() );
-                //}
-                for( unsigned i=0; i<d_nf[eqc].size(); i++ ){
-                  if( std::find( d_ff[p][cbase].begin(), d_ff[p][cbase].end(), d_nf[eqc][i] )==d_ff[p][cbase].end() ){
-                    d_ff[p][cbase].insert( d_ff[p][cbase].end(), d_nf[eqc].begin(), d_nf[eqc].end() );
-                  }else{
-                    //if it is a duplicate venn region, it must be empty since it is coming from syntactically disjoint siblings TODO?
-                  }
-                }
-              }else{
-                Trace("sets-nf-debug") << "..already processed parent " << p << " for " << cbase << std::endl;
-              }
-            }
-          }
-        }
-      }
-    }else{
-      Assert( hasProcessed() );
-    }
-  }
-}
-
-void TheorySetsPrivate::checkMinCard( std::vector< Node >& lemmas ) {
-
-  for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
-    Node eqc = d_set_eqc[i];
-    TypeNode tn = eqc.getType().getSetElementType();
-    if (d_t_card_enabled.find(tn) == d_t_card_enabled.end())
-    {
-      // cardinality is not enabled for this type, skip
-      continue;
-    }
-    //get members in class
-    std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc );
-    if( itm!=d_pol_mems[0].end() ){
-      std::vector< Node > exp;
-      std::vector< Node > members;
-      Node cardTerm;
-      std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc );
-      if( it!=d_eqc_to_card_term.end() ){
-        cardTerm = it->second;
-      }else{
-        cardTerm = NodeManager::currentNM()->mkNode( kind::CARD, eqc );
-      }
-      for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){
-      /*
-        for( unsigned j=0; j<members.size(); j++ ){
-          if( !ee_areDisequal( members[j], itmm->second ) ){
-            Assert( !ee_areEqual( members[j], itmm->second ) );
-            
-          }
-        }
-      */
-        members.push_back( itmm->first );
-        exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, itmm->first, cardTerm[0] ) );
-      }
-      if( members.size()>1 ){
-        exp.push_back( NodeManager::currentNM()->mkNode( kind::DISTINCT, members ) );
-      }
-      if( !members.empty() ){
-        Node conc = NodeManager::currentNM()->mkNode( kind::GEQ, cardTerm, NodeManager::currentNM()->mkConst( Rational( members.size() ) ) );
-        Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ), conc );
-        Trace("sets-lemma") << "Sets::Lemma : " << lem << " by mincard" << std::endl;
-        lemmas.push_back( lem );
-      }
-    }
-  }
-}
-
-void TheorySetsPrivate::flushLemmas( std::vector< Node >& lemmas, bool preprocess ) {
-  for( unsigned i=0; i<lemmas.size(); i++ ){
-    flushLemma( lemmas[i], preprocess );
-  }
-  lemmas.clear();
-}
-
-void TheorySetsPrivate::flushLemma( Node lem, bool preprocess ) {
-  if( d_lemmas_produced.find(lem)==d_lemmas_produced.end() ){
-    Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
-    d_lemmas_produced.insert(lem);
-    d_external.d_out->lemma(lem, false, preprocess);
-    d_sentLemma = true;
-  }else{
-    Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
-  }
-}
-
-Node TheorySetsPrivate::getProxy( Node n ) {
-  if( n.getKind()==kind::EMPTYSET || n.getKind()==kind::SINGLETON || n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS || n.getKind()==kind::UNION ){
-    NodeMap::const_iterator it = d_proxy.find( n );
-    if( it==d_proxy.end() ){
-      Node k = NodeManager::currentNM()->mkSkolem( "sp", n.getType(), "proxy for set" );
-      d_proxy[n] = k;
-      d_proxy_to_term[k] = n;
-      Node eq = k.eqNode( n );
-      Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
-      d_external.d_out->lemma( eq );
-      if( n.getKind()==kind::SINGLETON ){
-        Node slem = NodeManager::currentNM()->mkNode( kind::MEMBER, n[0], k );
-        Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton" << std::endl;
-        d_external.d_out->lemma( slem );
-        d_sentLemma = true;
-      }
-      return k;
-    }else{
-      return (*it).second;
-    }
-  }else{
-    return n;
-  }
-}
-
-Node TheorySetsPrivate::getCongruent( Node n ) {
-  Assert( d_equalityEngine.hasTerm( n ) );
-  std::map< Node, Node >::iterator it = d_congruent.find( n );
-  if( it==d_congruent.end() ){
-    return n;
-  }else{
-    return it->second;
-  }
-}
-
-Node TheorySetsPrivate::getEmptySet( TypeNode tn ) {
-  std::map< TypeNode, Node >::iterator it = d_emptyset.find( tn );
-  if( it==d_emptyset.end() ){
-    Node n = NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
-    d_emptyset[tn] = n;
-    return n;
-  }else{
-    return it->second;
-  }
-}
-Node TheorySetsPrivate::getUnivSet( TypeNode tn ) {
-  std::map< TypeNode, Node >::iterator it = d_univset.find( tn );
-  if( it==d_univset.end() ){
-    Node n = NodeManager::currentNM()->mkNullaryOperator(tn, kind::UNIVERSE_SET);
-    for( it = d_univset.begin(); it != d_univset.end(); ++it ){
-      Node n1;
-      Node n2;
-      if( tn.isSubtypeOf( it->first ) ){
-        n1 = n;
-        n2 = it->second;
-      }else if( it->first.isSubtypeOf( tn ) ){
-        n1 = it->second;
-        n2 = n;
-      }
-      if( !n1.isNull() ){
-        Node ulem = NodeManager::currentNM()->mkNode( kind::SUBSET, n1, n2 );
-        Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" << std::endl;
-        d_external.d_out->lemma( ulem );
-        d_sentLemma = true;
-      }
-    }
-    d_univset[tn] = n;
-    return n;
-  }else{
-    return it->second;
-  }
-}
-
-bool TheorySetsPrivate::hasLemmaCached( Node lem ) {
-  return d_lemmas_produced.find(lem)!=d_lemmas_produced.end();
-}
-
-bool TheorySetsPrivate::hasProcessed() {
-  return d_conflict || d_sentLemma || d_addedFact;
-}
-
-void TheorySetsPrivate::debugPrintSet( Node s, const char * c ) {
-  if( s.getNumChildren()==0 ){
-    NodeMap::const_iterator it = d_proxy_to_term.find( s );
-    if( it!=d_proxy_to_term.end() ){
-      debugPrintSet( (*it).second, c );
-    }else{
-      Trace(c) << s;
-    }
-  }else{
-    Trace(c) << "(" << s.getOperator();
-    for( unsigned i=0; i<s.getNumChildren(); i++ ){
-      Trace(c) << " ";
-      debugPrintSet( s[i], c );
-    }
-    Trace(c) << ")";
-  }
-}
-
-void TheorySetsPrivate::lastCallEffortCheck() {
-  Trace("sets") << "----- Last call effort check ------" << std::endl;
-
-}
-
-Node TheorySetsPrivate::getTypeConstraintSkolem(Node n, TypeNode tn)
-{
-  std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
-  if (it == d_tc_skolem[n].end())
-  {
-    Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn);
-    d_tc_skolem[n][tn] = k;
-    return k;
-  }
-  return it->second;
-}
-
 /**************************** TheorySetsPrivate *****************************/
 /**************************** TheorySetsPrivate *****************************/
 /**************************** TheorySetsPrivate *****************************/
@@ -1746,10 +785,10 @@ Node TheorySetsPrivate::getTypeConstraintSkolem(Node n, TypeNode tn)
 void TheorySetsPrivate::check(Theory::Effort level) {
   Trace("sets-check") << "Sets check effort " << level << std::endl;
   if( level == Theory::EFFORT_LAST_CALL ){
-    lastCallEffortCheck();
     return;
   }
-  while(!d_external.done() && !d_conflict) {
+  while (!d_external.done() && !d_state.isInConflict())
+  {
     // Get all the assertions
     Assertion assertion = d_external.get();
     TNode fact = assertion.assertion;
@@ -1757,14 +796,15 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     //assert the fact
     assertFact( fact, fact );
   }
-  d_sentLemma = false;
   Trace("sets-check") << "Sets finished assertions effort " << level << std::endl;
   //invoke full effort check, relations check
-  if( !d_conflict ){
+  if (!d_state.isInConflict())
+  {
     if( level == Theory::EFFORT_FULL ){
       if( !d_external.d_valuation.needCheck() ){
         fullEffortCheck();
-        if (!d_conflict && !d_sentLemma && d_full_check_incomplete)
+        if (!d_state.isInConflict() && !d_im.hasSentLemma()
+            && d_full_check_incomplete)
         {
           d_external.d_out->setIncomplete();
         }
@@ -1774,19 +814,13 @@ void TheorySetsPrivate::check(Theory::Effort level) {
   Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
 }/* TheorySetsPrivate::check() */
 
-bool TheorySetsPrivate::needsCheckLastEffort() {
-  if( !d_var_elim.empty() ){
-    return true;
-  }
-  return false;
-}
-
 /************************ Sharing ************************/
 /************************ Sharing ************************/
 /************************ Sharing ************************/
 
 void TheorySetsPrivate::addSharedTerm(TNode n) {
-  Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
+  Debug("sets") << "[sets] TheorySetsPrivate::addSharedTerm( " << n << ")"
+                << std::endl;
   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
 }
 
@@ -1800,7 +834,8 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
     if( t2!=NULL ){
       Node f1 = t1->getData();
       Node f2 = t2->getData();
-      if( !ee_areEqual( f1, f2 ) ){
+      if (!d_state.areEqual(f1, f2))
+      {
         Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
         vector< pair<TNode, TNode> > currentPairs;
         for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
@@ -1808,8 +843,8 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
           TNode y = f2[k];
           Assert( d_equalityEngine.hasTerm(x) );
           Assert( d_equalityEngine.hasTerm(y) );
-          Assert( !ee_areDisequal( x, y ) );
-          Assert( !ee_areCareDisequal( x, y ) );
+          Assert(!d_state.areDisequal(x, y));
+          Assert(!areCareDisequal(x, y));
           if( !d_equalityEngine.areEqual( x, y ) ){
             Trace("sets-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
             if( d_equalityEngine.isTriggerTerm(x, THEORY_SETS) && d_equalityEngine.isTriggerTerm(y, THEORY_SETS) ){
@@ -1820,9 +855,10 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
               //splitting on sets (necessary for handling set of sets properly)
               if( x.getType().isSet() ){
                 Assert( y.getType().isSet() );
-                if( !ee_areDisequal( x, y ) ){
+                if (!d_state.areDisequal(x, y))
+                {
                   Trace("sets-cg-lemma") << "Should split on : " << x << "==" << y << std::endl;
-                  split( x.eqNode( y ) );
+                  d_im.split(x.eqNode(y));
                 }
               }
             }
@@ -1853,7 +889,8 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
         ++it2;
         for( ; it2 != t1->d_data.end(); ++it2 ){
           if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
-            if( !ee_areCareDisequal(it->first, it2->first) ){
+            if (!areCareDisequal(it->first, it2->first))
+            {
               addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
             }
           }
@@ -1867,7 +904,7 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
         {
           if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
           {
-            if (!ee_areCareDisequal(tt1.first, tt2.first))
+            if (!areCareDisequal(tt1.first, tt2.first))
             {
               addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
             }
@@ -1879,16 +916,22 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
 }
 
 void TheorySetsPrivate::computeCareGraph() {
-  for( std::map< Kind, std::vector< Node > >::iterator it = d_op_list.begin(); it != d_op_list.end(); ++it ){
-    if( it->first==kind::SINGLETON || it->first==kind::MEMBER ){
+  const std::map<Kind, std::vector<Node> >& ol = d_state.getOperatorList();
+  for (const std::pair<const Kind, std::vector<Node> >& it : ol)
+  {
+    Kind k = it.first;
+    if (k == kind::SINGLETON || k == kind::MEMBER)
+    {
       unsigned n_pairs = 0;
-      Trace("sets-cg-summary") << "Compute graph for sets, op=" << it->first << "..." << it->second.size() << std::endl;
-      Trace("sets-cg") << "Build index for " << it->first << "..." << std::endl;
+      Trace("sets-cg-summary") << "Compute graph for sets, op=" << k << "..."
+                               << it.second.size() << std::endl;
+      Trace("sets-cg") << "Build index for " << k << "..." << std::endl;
       std::map<TypeNode, TNodeTrie> index;
       unsigned arity = 0;
       //populate indices
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        TNode f1 = it->second[i];
+      for (TNode f1 : it.second)
+      {
+        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)
@@ -1978,50 +1021,41 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
     return false;
   }
 
+  NodeManager* nm = NodeManager::currentNM();
   std::map< Node, Node > mvals;
-  for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
-    Node eqc = d_set_eqc[i];
+  // If cardinality is enabled, we need to use the ordered equivalence class
+  // list computed by the cardinality solver, where sets equivalence classes
+  // are assigned model values based on their position in the cardinality
+  // graph.
+  const std::vector<Node>& sec = d_card_enabled
+                                     ? d_cardSolver->getOrderedSetsEqClasses()
+                                     : d_state.getSetsEqClasses();
+  Valuation& val = getValuation();
+  for (int i = (int)(sec.size() - 1); i >= 0; i--)
+  {
+    Node eqc = sec[i];
     if( termSet.find( eqc )==termSet.end() ){
       Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl;
     }else{
       std::vector< Node > els;
-      bool is_base = !d_card_enabled || ( d_nf[eqc].size()==1 && d_nf[eqc][0]==eqc );
+      bool is_base = !d_card_enabled || d_cardSolver->isModelValueBasic(eqc);
       if( is_base ){
         Trace("sets-model") << "Collect elements of base eqc " << eqc << std::endl;
         // members that must be in eqc
-        std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc );
-        if( itm!=d_pol_mems[0].end() ){
-          for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){
-            Node t = NodeManager::currentNM()->mkNode( kind::SINGLETON, itmm->first );
+        const std::map<Node, Node>& emems = d_state.getMembers(eqc);
+        if (!emems.empty())
+        {
+          for (const std::pair<const Node, Node>& itmm : emems)
+          {
+            Node t = nm->mkNode(kind::SINGLETON, itmm.first);
             els.push_back( t );
           }
         }
       }
       if( d_card_enabled ){
-        TypeNode elementType = eqc.getType().getSetElementType();
-        if( is_base ){
-          std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc );
-          if( it!=d_eqc_to_card_term.end() ){
-            //slack elements from cardinality value
-            Node v = d_external.d_valuation.getModelValue(it->second);
-            Trace("sets-model") << "Cardinality of " << eqc << " is " << v << std::endl;
-            Assert(v.getConst<Rational>() <= LONG_MAX, "Exceeded LONG_MAX in sets model");
-            unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
-            Assert( els.size()<=vu );
-            while( els.size()<vu ){
-              els.push_back( NodeManager::currentNM()->mkNode( kind::SINGLETON, NodeManager::currentNM()->mkSkolem( "msde", elementType ) ) );
-            }
-          }else{
-            Trace("sets-model") << "No slack elements for " << eqc << std::endl;
-          }
-        }else{
-          Trace("sets-model") << "Build value for " << eqc << " based on normal form, size = " << d_nf[eqc].size() << std::endl;
-          //it is union of venn regions
-          for( unsigned j=0; j<d_nf[eqc].size(); j++ ){
-            Assert( mvals.find( d_nf[eqc][j] )!=mvals.end() );
-            els.push_back( mvals[d_nf[eqc][j]] );
-          }
-        }
+        // make the slack elements for the equivalence class based on set
+        // cardinality
+        d_cardSolver->mkModelValueElementsFor(val, eqc, els, mvals);
       }
       Node rep = NormalForm::mkBop( kind::UNION, els, eqc.getType() );
       rep = Rewriter::rewrite( rep );
@@ -2041,13 +1075,6 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
 /********************** Helper functions ***************************/
 /********************** Helper functions ***************************/
 
-void TheorySetsPrivate::addEqualityToExp( Node a, Node b, std::vector< Node >& exp ) {
-  if( a!=b ){
-    Assert( ee_areEqual( a, b ) );
-    exp.push_back( a.eqNode( b ) );
-  }
-}
-
 Node mkAnd(const std::vector<TNode>& conjunctions) {
   Assert(conjunctions.size() > 0);
 
@@ -2079,52 +1106,9 @@ Node mkAnd(const std::vector<TNode>& conjunctions) {
     conjunction << *it;
     ++ it;
   }
-
   return conjunction;
 }/* mkAnd() */
 
-
-TheorySetsPrivate::Statistics::Statistics() :
-  d_getModelValueTime("theory::sets::getModelValueTime")
-  , d_mergeTime("theory::sets::merge_nodes::time")
-  , d_processCard2Time("theory::sets::processCard2::time")
-  , d_memberLemmas("theory::sets::lemmas::member", 0)
-  , d_disequalityLemmas("theory::sets::lemmas::disequality", 0)
-  , d_numVertices("theory::sets::vertices", 0)
-  , d_numVerticesMax("theory::sets::vertices-max", 0)
-  , d_numMergeEq1or2("theory::sets::merge1or2", 0)
-  , d_numMergeEq3("theory::sets::merge3", 0)
-  , d_numLeaves("theory::sets::leaves", 0)
-  , d_numLeavesMax("theory::sets::leaves-max", 0)
-{
-  smtStatisticsRegistry()->registerStat(&d_getModelValueTime);
-  smtStatisticsRegistry()->registerStat(&d_mergeTime);
-  smtStatisticsRegistry()->registerStat(&d_processCard2Time);
-  smtStatisticsRegistry()->registerStat(&d_memberLemmas);
-  smtStatisticsRegistry()->registerStat(&d_disequalityLemmas);
-  smtStatisticsRegistry()->registerStat(&d_numVertices);
-  smtStatisticsRegistry()->registerStat(&d_numVerticesMax);
-  smtStatisticsRegistry()->registerStat(&d_numMergeEq1or2);
-  smtStatisticsRegistry()->registerStat(&d_numMergeEq3);
-  smtStatisticsRegistry()->registerStat(&d_numLeaves);
-  smtStatisticsRegistry()->registerStat(&d_numLeavesMax);
-}
-
-
-TheorySetsPrivate::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_getModelValueTime);
-  smtStatisticsRegistry()->unregisterStat(&d_mergeTime);
-  smtStatisticsRegistry()->unregisterStat(&d_processCard2Time);
-  smtStatisticsRegistry()->unregisterStat(&d_memberLemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_disequalityLemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_numVertices);
-  smtStatisticsRegistry()->unregisterStat(&d_numVerticesMax);
-  smtStatisticsRegistry()->unregisterStat(&d_numMergeEq1or2);
-  smtStatisticsRegistry()->unregisterStat(&d_numMergeEq3);
-  smtStatisticsRegistry()->unregisterStat(&d_numLeaves);
-  smtStatisticsRegistry()->unregisterStat(&d_numLeavesMax);
-}
-
 void TheorySetsPrivate::propagate(Theory::Effort effort) {
 
 }
@@ -2133,7 +1117,8 @@ bool TheorySetsPrivate::propagate(TNode literal) {
   Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
 
   // If already in conflict, no more propagation
-  if (d_conflict) {
+  if (d_state.isInConflict())
+  {
     Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
     return false;
   }
@@ -2141,37 +1126,19 @@ bool TheorySetsPrivate::propagate(TNode literal) {
   // Propagate out
   bool ok = d_external.d_out->propagate(literal);
   if (!ok) {
-    d_conflict = true;
+    d_state.setConflict();
   }
 
   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;
 }
 
+Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; }
+
 void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
@@ -2179,12 +1146,11 @@ void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 
 void TheorySetsPrivate::conflict(TNode a, TNode b)
 {
-  d_conflictNode = explain(a.eqNode(b));
-  d_external.d_out->conflict(d_conflictNode);
-  Debug("sets") << "[sets] conflict: " << a << " iff " << b
-                << ", explaination " << d_conflictNode << std::endl;
-  Trace("sets-lemma") << "Equality Conflict : " << d_conflictNode << std::endl;
-  d_conflict = true;
+  Node conf = explain(a.eqNode(b));
+  d_state.setConflict(conf);
+  Debug("sets") << "[sets] conflict: " << a << " iff " << b << ", explanation "
+                << conf << std::endl;
+  Trace("sets-lemma") << "Equality Conflict : " << conf << std::endl;
 }
 
 Node TheorySetsPrivate::explain(TNode literal)
@@ -2254,7 +1220,6 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou
   //TODO: allow variable elimination for sets when setsExt = true
   
   //this is based off of Theory::ppAssert
-  Node var;
   if (in.getKind() == kind::EQUAL)
   {
     if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
@@ -2263,7 +1228,6 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou
       if (!in[0].getType().isSet() || !options::setsExt())
       {
         outSubstitutions.addSubstitution(in[0], in[1]);
-        var = in[0];
         status = Theory::PP_ASSERT_STATUS_SOLVED;
       }
     }
@@ -2273,7 +1237,6 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou
       if (!in[1].getType().isSet() || !options::setsExt())
       {
         outSubstitutions.addSubstitution(in[1], in[0]);
-        var = in[1];
         status = Theory::PP_ASSERT_STATUS_SOLVED;
       }
     }
@@ -2285,25 +1248,10 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou
       }
     }
   }
-
-  if( status==Theory::PP_ASSERT_STATUS_SOLVED ){
-    Trace("sets-var-elim") << "Sets : ppAssert variable eliminated : " << in << ", var = " << var << std::endl;
-    /*
-    if( var.getType().isSet() ){
-      //we must ensure that subs is included in the universe set
-      d_var_elim[var] = true;
-    } 
-    */
-    if( options::setsExt() ){
-      Assert( !var.getType().isSet() ); 
-    }
-  }
   return status;
 }
-  
-void TheorySetsPrivate::presolve() {
-  d_op_list.clear();
-}
+
+void TheorySetsPrivate::presolve() { d_state.reset(); }
 
 /**************************** eq::NotifyClass *****************************/
 /**************************** eq::NotifyClass *****************************/
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index fcb5859d4..0468e5fb7 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -22,7 +22,9 @@
 #include "context/cdhashset.h"
 #include "context/cdqueue.h"
 #include "expr/node_trie.h"
-#include "theory/sets/skolem_cache.h"
+#include "theory/sets/cardinality_extension.h"
+#include "theory/sets/inference_manager.h"
+#include "theory/sets/solver_state.h"
 #include "theory/sets/theory_sets_rels.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -32,51 +34,73 @@ namespace theory {
 namespace sets {
 
 /** Internal classes, forward declared here */
-class TheorySetsTermInfoManager;
 class TheorySets;
-class TheorySetsScrutinize;
 
 class TheorySetsPrivate {
-//new implementation
   typedef context::CDHashMap< Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-  typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
-public:
+
+ public:
   void eqNotifyNewClass(TNode t);
   void eqNotifyPreMerge(TNode t1, TNode t2);
   void eqNotifyPostMerge(TNode t1, TNode t2);
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
-private:
-  bool ee_areEqual( Node a, Node b );
-  bool ee_areDisequal( Node a, Node b );
-  bool ee_areCareDisequal( Node a, Node b );
+  /** Assert fact holds in the current context with explanation exp.
+   *
+   * exp should be explainable by the equality engine of this class, and fact
+   * should be a literal.
+   */
+  bool assertFact(Node fact, Node exp);
+
+ private:
+  /** Are a and b trigger terms in the equality engine that may be disequal? */
+  bool areCareDisequal(Node a, Node b);
   NodeIntMap d_members;
   std::map< Node, std::vector< Node > > d_members_data;
-  bool assertFact( Node fact, Node exp );
-  // inferType : 1 : must send out as lemma, -1 : do internal inferences if possible, 0 : default.
-  bool assertFactRec( Node fact, Node exp, std::vector< Node >& lemma, int inferType = 0 );
-  // add inferences corresponding to ( exp => fact ) to lemmas, equality engine
-  void assertInference( Node fact, Node exp, std::vector< Node >& lemmas, const char * c, int inferType = 0 );
-  void assertInference( Node fact, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType = 0 );
-  void assertInference( std::vector< Node >& conc, Node exp, std::vector< Node >& lemmas, const char * c, int inferType = 0 );
-  void assertInference( std::vector< Node >& conc, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType = 0 );
-  // send lemma ( n OR (NOT n) ) immediately
-  void split( Node n, int reqPol=0 );
+  /**
+   * Invoke the decision procedure for this theory, which is run at
+   * full effort. This will either send a lemma or conflict on the output
+   * channel of this class, or otherwise the current set of constraints is
+   * satisfiable w.r.t. the theory of sets.
+   */
   void fullEffortCheck();
-  void checkSubtypes( std::vector< Node >& lemmas );
-  void checkDownwardsClosure( std::vector< Node >& lemmas );
-  void checkUpwardsClosure( std::vector< Node >& lemmas );
-  void checkDisequalities( std::vector< Node >& lemmas );
-  bool isMember( Node x, Node s );
-  bool isSetDisequalityEntailed( Node s, Node t );
-
-  Node getProxy( Node n );
-  Node getCongruent( Node n );
-  Node getEmptySet( TypeNode tn );
-  Node getUnivSet( TypeNode tn );
-  bool hasLemmaCached( Node lem );
-  bool hasProcessed();
+  /**
+   * Reset the information for a full effort check.
+   */
+  void fullEffortReset();
+  /**
+   * This ensures that subtype constraints are met for all set terms. In
+   * particular, for a set equivalence class E, let Set(T) be the most
+   * common type among the types of terms in that class. In other words,
+   * if E contains two terms of Set(Int) and Set(Real), then Set(Int) is the
+   * most common type. Then, for each membership x in S where S is a set in
+   * this equivalence class, we ensure x has type T by asserting:
+   *   x = k
+   * for a fresh constant k of type T. This is done only if the type of x is not
+   * a subtype of Int (e.g. if x is of type Real). We call k the "type
+   * constraint skolem for x of type Int".
+   */
+  void checkSubtypes();
+  /**
+   * This implements an inference schema based on the "downwards closure" of
+   * set membership. This roughly corresponds to the rules UNION DOWN I and II,
+   * INTER DOWN I and II from Bansal et al IJCAR 2016, as well as rules for set
+   * difference.
+   */
+  void checkDownwardsClosure();
+  /**
+   * This implements an inference schema based on the "upwards closure" of
+   * set membership. This roughly corresponds to the rules UNION UP, INTER
+   * UP I and II from Bansal et al IJCAR 2016, as well as rules for set
+   * difference.
+   */
+  void checkUpwardsClosure();
+  /**
+   * This implements a strategy for splitting for set disequalities which
+   * roughly corresponds the SET DISEQUALITY rule from Bansal et al IJCAR 2016.
+   */
+  void checkDisequalities();
 
   void addCarePairs(TNodeTrie* t1,
                     TNodeTrie* t2,
@@ -105,23 +129,7 @@ private:
   std::map< Node, EqcInfo* > d_eqc_info;
   /** get or make eqc info */
   EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
-  
-  void addEqualityToExp( Node a, Node b, std::vector< Node >& exp );
-  
-  void debugPrintSet( Node s, const char * c );
 
-  /** sent lemma
-   *
-   * This flag is set to true during a full effort check if this theory
-   * called d_out->lemma(...).
-   */
-  bool d_sentLemma;
-  /** added fact
-   *
-   * This flag is set to true during a full effort check if this theory
-   * added an internal fact to its equality engine.
-   */
-  bool d_addedFact;
   /** full check incomplete
    *
    * This flag is set to true during a full effort check if this theory
@@ -129,69 +137,8 @@ private:
    * with a relation or extended function kind).
    */
   bool d_full_check_incomplete;
-  NodeMap d_proxy;  
-  NodeMap d_proxy_to_term;  
-  NodeSet d_lemmas_produced;
-  std::vector< Node > d_set_eqc;
-  std::map< Node, bool > d_set_eqc_relevant;
-  std::map< Node, std::vector< Node > > d_set_eqc_list;
-  std::map< TypeNode, Node > d_eqc_emptyset;
-  std::map< TypeNode, Node > d_eqc_univset;
-  std::map< Node, Node > d_eqc_singleton;
-  std::map< TypeNode, Node > d_emptyset;
-  std::map< TypeNode, Node > d_univset;
-  std::map< Node, Node > d_congruent;
-  std::map< Node, std::vector< Node > > d_nvar_sets;
-  std::map< Node, Node > d_var_set;
   std::map< Node, TypeNode > d_most_common_type;
   std::map< Node, Node > d_most_common_type_term;
-  std::map< Node, std::map< Node, Node > > d_pol_mems[2];
-  std::map< Node, std::map< Node, Node > > d_members_index;
-  std::map< Node, Node > d_singleton_index;
-  std::map< Kind, std::map< Node, std::map< Node, Node > > > d_bop_index;
-  std::map< Kind, std::vector< Node > > d_op_list;
-  //cardinality
- private:
-  /** is cardinality enabled?
-   *
-   * This flag is set to true during a full effort check if any constraint
-   * involving cardinality constraints is asserted to this theory.
-   */
-  bool d_card_enabled;
-  /** element types of sets for which cardinality is enabled */
-  std::map<TypeNode, bool> d_t_card_enabled;
-  std::map< Node, Node > d_eqc_to_card_term;
-  NodeSet d_card_processed;
-  std::map< Node, std::vector< Node > > d_card_parent;
-  std::map< Node, std::map< Node, std::vector< Node > > > d_ff;
-  std::map< Node, std::vector< Node > > d_nf;
-  std::map< Node, Node > d_card_base;
-  void checkCardBuildGraph( std::vector< Node >& lemmas );
-  void registerCardinalityTerm( Node n, std::vector< Node >& lemmas );
-  void checkCardCycles( std::vector< Node >& lemmas );
-  void checkCardCyclesRec( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp, std::vector< Node >& lemmas );
-  void checkNormalForms( std::vector< Node >& lemmas, std::vector< Node >& intro_sets );
-  void checkNormalForm( Node eqc, std::vector< Node >& intro_sets );
-  void checkMinCard( std::vector< Node >& lemmas );
-private: //for universe set
-  NodeBoolMap d_var_elim;
-  void lastCallEffortCheck();
-
- private:
-  /** type constraint skolems
-   *
-   * The sets theory solver outputs equality lemmas of the form:
-   *   n = d_tc_skolem[n][tn]
-   * where the type of d_tc_skolem[n][tn] is tn, and the type
-   * of n is not a subtype of tn. This is required to handle benchmarks like
-   *   test/regress/regress0/sets/sets-of-sets-subtypes.smt2
-   * where for s : (Set Int) and t : (Set Real), we have that
-   *   ( s = t ^ y in t ) implies ( exists k : Int. y = k )
-   * The type constraint Skolem for (y, Int) is the skolemization of k above.
-   */
-  std::map<Node, std::map<TypeNode, Node> > d_tc_skolem;
-  /** get type constraint skolem for n and tn */
-  Node getTypeConstraintSkolem(Node n, TypeNode tn);
 
  public:
 
@@ -210,8 +157,6 @@ private: //for universe set
   void addSharedTerm(TNode);
 
   void check(Theory::Effort);
-  
-  bool needsCheckLastEffort();
 
   bool collectModelInfo(TheoryModel* m);
 
@@ -221,12 +166,6 @@ 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
@@ -266,58 +205,14 @@ private: //for universe set
 
   void propagate(Theory::Effort);
 
-  /** 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();
+  /** get the valuation */
+  Valuation& getValuation();
 
  private:
   TheorySets& d_external;
 
-  class Statistics {
-  public:
-    TimerStat d_getModelValueTime;
-    TimerStat d_mergeTime;
-    TimerStat d_processCard2Time;
-    IntStat d_memberLemmas;
-    IntStat d_disequalityLemmas;
-    IntStat d_numVertices;
-    IntStat d_numVerticesMax;
-    IntStat d_numMergeEq1or2;
-    IntStat d_numMergeEq3;
-    IntStat d_numLeaves;
-    IntStat d_numLeavesMax;
-
-    Statistics();
-    ~Statistics();
-  } d_statistics;
-
   /** Functions to handle callbacks from equality engine */
   class NotifyClass : public eq::EqualityEngineNotify {
     TheorySetsPrivate& d_theory;
@@ -340,9 +235,6 @@ private: //for universe set
   /** Equality engine */
   eq::EqualityEngine d_equalityEngine;
 
-  context::CDO<bool> d_conflict;
-  Node d_conflictNode;
-
   /** Proagate out to output channel */
   bool propagate(TNode);
 
@@ -350,20 +242,34 @@ private: //for universe set
   void conflict(TNode, TNode);
   
   bool isCareArg( Node n, unsigned a );
-public:
-  bool isEntailed( Node n, bool pol );
+
+ public:
+  /** Is formula n entailed to have polarity pol in the current context? */
+  bool isEntailed(Node n, bool pol) { return d_state.isEntailed(n, pol); }
+  /** Is x entailed to be a member of set s in the current context? */
+  bool isMember(Node x, Node s);
 
  private:
+  /** The state of the sets solver at full effort */
+  SolverState d_state;
+  /** The inference manager of the sets solver */
+  InferenceManager d_im;
   /** subtheory solver for the theory of relations */
   std::unique_ptr<TheorySetsRels> d_rels;
-  /** the skolem cache */
-  SkolemCache d_skCache;
+  /** subtheory solver for the theory of sets with cardinality */
+  std::unique_ptr<CardinalityExtension> d_cardSolver;
   /** are relations enabled?
    *
    * This flag is set to true during a full effort check if any constraint
    * involving relational constraints is asserted to this theory.
    */
   bool d_rels_enabled;
+  /** is cardinality enabled?
+   *
+   * This flag is set to true during a full effort check if any constraint
+   * involving cardinality constraints is asserted to this theory.
+   */
+  bool d_card_enabled;
 };/* class TheorySetsPrivate */
 
 
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 2bbaa3bc8..e2b779cbd 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -32,24 +32,21 @@ 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;
 
-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)
+TheorySetsRels::TheorySetsRels(SolverState& s,
+                               InferenceManager& im,
+                               eq::EqualityEngine& e,
+                               context::UserContext* u)
+    : d_state(s), d_im(im), d_ee(e), d_shared_terms(u)
 {
-  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);
+  d_trueNode = NodeManager::currentNM()->mkConst(true);
+  d_falseNode = NodeManager::currentNM()->mkConst(false);
+  d_ee.addFunctionKind(PRODUCT);
+  d_ee.addFunctionKind(JOIN);
+  d_ee.addFunctionKind(TRANSPOSE);
+  d_ee.addFunctionKind(TCLOSURE);
+  d_ee.addFunctionKind(JOIN_IMAGE);
+  d_ee.addFunctionKind(IDEN);
+  d_ee.addFunctionKind(APPLY_CONSTRUCTOR);
 }
 
 TheorySetsRels::~TheorySetsRels() {}
@@ -188,10 +185,10 @@ void TheorySetsRels::check(Theory::Effort level)
 
   void TheorySetsRels::collectRelsInfo() {
     Trace("rels") << "[sets-rels] Start collecting relational terms..." << std::endl;
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine );
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_ee);
     while( !eqcs_i.isFinished() ){
       Node                      eqc_rep  = (*eqcs_i);
-      eq::EqClassIterator       eqc_i   = eq::EqClassIterator( eqc_rep, d_eqEngine );
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc_rep, &d_ee);
 
       TypeNode erType = eqc_rep.getType();
       Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << " with type " << eqc_rep.getType() << std::endl;
@@ -307,7 +304,7 @@ void TheorySetsRels::check(Theory::Effort level)
                                                              NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR,
                                                                                                Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ),
                                                              join_image_term);
-      if (d_sets_theory.isEntailed(new_membership, true))
+      if (d_state.isEntailed(new_membership, true))
       {
         ++mem_rep_it;
         ++mem_rep_exp_it;
@@ -793,7 +790,7 @@ void TheorySetsRels::check(Theory::Effort level)
     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 = d_sets_theory.getSkolemCache().mkTypedSkolemCached(
+    Node shared_x = d_state.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();
@@ -1058,41 +1055,65 @@ void TheorySetsRels::check(Theory::Effort level)
   void TheorySetsRels::doPendingInfers()
   {
     // process the inferences in d_pending
-    if (!d_sets_theory.isInConflict())
+    if (!d_state.isInConflict())
     {
-      std::vector<Node> lemmas;
       for (const Node& p : d_pending)
       {
-        d_sets_theory.processInference(p, "rels", lemmas);
-        if (d_sets_theory.isInConflict())
+        if (p.getKind() == IMPLIES)
+        {
+          processInference(p[1], p[0], "rels");
+        }
+        else
+        {
+          processInference(p, d_trueNode, "rels");
+        }
+        if (d_state.isInConflict())
         {
           break;
         }
       }
       // if we are still not in conflict, send lemmas
-      if (!d_sets_theory.isInConflict())
+      if (!d_state.isInConflict())
       {
-        d_sets_theory.flushLemmas(lemmas);
+        d_im.flushPendingLemmas();
       }
     }
     d_pending.clear();
   }
 
+  void TheorySetsRels::processInference(Node conc, Node exp, const char* c)
+  {
+    Trace("sets-pinfer") << "Process inference: " << exp << " => " << conc
+                         << std::endl;
+    if (!d_state.isEntailed(exp, true))
+    {
+      Trace("sets-pinfer") << "  must assert as lemma" << std::endl;
+      // we wrap the spurious explanation into a splitting lemma
+      Node lem = NodeManager::currentNM()->mkNode(OR, exp.negate(), conc);
+      d_im.assertInference(lem, d_trueNode, c, 1);
+      return;
+    }
+    // try to assert it as a fact
+    d_im.assertInference(conc, exp, c);
+  }
+
   bool TheorySetsRels::isRelationKind( Kind k ) {
-    return k == kind::TRANSPOSE || k == kind::PRODUCT || k == kind::JOIN || k == kind::TCLOSURE;
+    return k == TRANSPOSE || k == PRODUCT || k == JOIN || k == TCLOSURE
+           || k == IDEN || k == JOIN_IMAGE;
   }
 
   Node TheorySetsRels::getRepresentative( Node t ) {
-    if( d_eqEngine->hasTerm( t ) ){
-      return d_eqEngine->getRepresentative( t );
-    }else{
+    if (d_ee.hasTerm(t))
+    {
+      return d_ee.getRepresentative(t);
+    }
+    else
+    {
       return t;
     }
   }
 
-  bool TheorySetsRels::hasTerm( Node a ){
-    return d_eqEngine->hasTerm( a );
-  }
+  bool TheorySetsRels::hasTerm(Node a) { return d_ee.hasTerm(a); }
 
   bool TheorySetsRels::areEqual( Node a, Node b ){
     Assert(a.getType() == b.getType());
@@ -1100,7 +1121,7 @@ void TheorySetsRels::check(Theory::Effort level)
     if(a == b) {
       return true;
     } else if( hasTerm( a ) && hasTerm( b ) ){
-      return d_eqEngine->areEqual( a, b );
+      return d_ee.areEqual(a, b);
     } else if(a.getType().isTuple()) {
       bool equal = true;
       for(unsigned int i = 0; i < a.getType().getTupleLength(); i++) {
@@ -1146,7 +1167,8 @@ void TheorySetsRels::check(Theory::Effort level)
       Node skEq =
           skolem.eqNode(NodeManager::currentNM()->mkNode(kind::SINGLETON, n));
       // force lemma to be sent immediately
-      d_sets_theory.getOutputChannel()->lemma(skEq);
+      d_im.assertInference(skEq, d_trueNode, "shared-term");
+      d_im.flushPendingLemmas();
       d_shared_terms.insert(n);
     }
   }
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index d4a91007b..3a0458309 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -21,7 +21,9 @@
 
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
+#include "theory/sets/inference_manager.h"
 #include "theory/sets/rels_utils.h"
+#include "theory/sets/solver_state.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
@@ -63,10 +65,10 @@ class TheorySetsRels {
   typedef context::CDHashMap< Node, Node, NodeHashFunction >      NodeMap;
 
 public:
- TheorySetsRels(context::Context* c,
-                context::UserContext* u,
-                eq::EqualityEngine* eq,
-                TheorySetsPrivate& set);
+ TheorySetsRels(SolverState& s,
+                InferenceManager& im,
+                eq::EqualityEngine& e,
+                context::UserContext* u);
 
  ~TheorySetsRels();
  /**
@@ -83,10 +85,13 @@ private:
   /** True and false constant nodes */
   Node                          d_trueNode;
   Node                          d_falseNode;
-  /** The parent theory of sets object */
-  TheorySetsPrivate& d_sets_theory;
-  /** pointer to the equality engine of the theory of sets */
-  eq::EqualityEngine* d_eqEngine;
+
+  /** Reference to the state object for the theory of sets */
+  SolverState& d_state;
+  /** Reference to the inference manager for the theory of sets */
+  InferenceManager& d_im;
+  /** Reference to the equality engine of theory of sets */
+  eq::EqualityEngine& d_ee;
   /** A list of pending inferences to process */
   std::vector<Node> d_pending;
   NodeSet                       d_shared_terms;
@@ -113,8 +118,6 @@ private:
   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;
 
-  context::Context* d_satContext;
-
  private:
   /** Send infer
    *
@@ -133,6 +136,14 @@ private:
    * the equality engine.
    */
   void doPendingInfers();
+  /** Process inference
+   *
+   * A wrapper around d_im.assertInference that ensures that we do not send
+   * inferences with explanations that are not entailed.
+   *
+   * Argument c is used for debugging, typically the name of the inference.
+   */
+  void processInference(Node conc, Node exp, const char* c);
 
   /** Methods used in full effort */
   void check();