Split term registry from theory state in sets (#5037)

Currently, the theory state object SolverState in sets sends lemmas and has a reference to the parent theory. This PR is work towards eliminating these dependencies.

This adds a TermRegistry object which is responsible for some of the tasks currently done by SolverState, including all those involving lemmas.

Notice this also makes a bug fix in getUnivSetEqClass where the universe set was being returned instead of its representative.

A followup PR will make SolverState maintain SAT-context-dependent membership lists which is also required for breaking the dependence on the parent theory.

13 files changed, 351 insertions, 232 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6cd2c24d1..5a06df28b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -709,6 +709,8 @@ libcvc4_add_sources(
   theory/sets/skolem_cache.h
   theory/sets/solver_state.cpp
   theory/sets/solver_state.h
+  theory/sets/term_registry.cpp
+  theory/sets/term_registry.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
index 321559f5a..447782ba2 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -30,9 +30,12 @@ namespace CVC4 {
 namespace theory {
 namespace sets {
 
-CardinalityExtension::CardinalityExtension(SolverState& s, InferenceManager& im)
+CardinalityExtension::CardinalityExtension(SolverState& s,
+                                           InferenceManager& im,
+                                           TermRegistry& treg)
     : d_state(s),
       d_im(im),
+      d_treg(treg),
       d_card_processed(s.getUserContext()),
       d_finite_type_constants_processed(false)
 {
@@ -101,7 +104,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
 
   // here we call getUnivSet instead of getUnivSetEqClass to generate
   // a univset term for finite types even if they are not used in the input
-  Node univ = d_state.getUnivSet(setType);
+  Node univ = d_treg.getUnivSet(setType);
   std::map<Node, Node>::iterator it = d_univProxy.find(univ);
 
   Node proxy;
@@ -109,7 +112,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
   if (it == d_univProxy.end())
   {
     // Force cvc4 to build the cardinality graph for the universe set
-    proxy = d_state.getProxy(univ);
+    proxy = d_treg.getProxy(univ);
     d_univProxy[univ] = proxy;
   }
   else
@@ -208,9 +211,9 @@ void CardinalityExtension::check()
   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");
+  d_treg.debugPrintSet(intro_sets[0], "sets-nf");
   Trace("sets-nf") << std::endl;
-  Node k = d_state.getProxy(intro_sets[0]);
+  Node k = d_treg.getProxy(intro_sets[0]);
   AlwaysAssert(!k.isNull());
 }
 
@@ -274,7 +277,7 @@ void CardinalityExtension::registerCardinalityTerm(Node n)
   for (unsigned k = 0, csize = cterms.size(); k < csize; k++)
   {
     Node nn = cterms[k];
-    Node nk = d_state.getProxy(nn);
+    Node nk = d_treg.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)
@@ -361,7 +364,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
   curr.push_back(eqc);
   TypeNode tn = eqc.getType();
   bool is_empty = eqc == d_state.getEmptySetEqClass(tn);
-  Node emp_set = d_state.getEmptySet(tn);
+  Node emp_set = d_treg.getEmptySet(tn);
   for (const Node& n : nvsets)
   {
     Kind nk = n.getKind();
@@ -683,7 +686,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
       Trace("sets-nf") << "  F " << itf.first << " : " << itf.second
                        << std::endl;
       Trace("sets-nf-debug") << " ...";
-      d_state.debugPrintSet(itf.first, "sets-nf-debug");
+      d_treg.debugPrintSet(itf.first, "sets-nf-debug");
       Trace("sets-nf-debug") << std::endl;
     }
   }
@@ -696,7 +699,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
   std::vector<Node>& nfeqc = d_nf[eqc];
   NodeManager* nm = NodeManager::currentNM();
   bool success = true;
-  Node emp_set = d_state.getEmptySet(tn);
+  Node emp_set = d_treg.getEmptySet(tn);
   if (!base.isNull())
   {
     for (unsigned j = 0, csize = comps.size(); j < csize; j++)
@@ -772,7 +775,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
             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");
+            d_treg.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))
@@ -780,7 +783,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
               // 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");
+              d_treg.debugPrintSet(r, "sets-nf");
               Trace("sets-nf") << std::endl;
               d_im.split(r.eqNode(emp_set), 1);
               Assert(d_im.hasSent());
@@ -820,8 +823,8 @@ void CardinalityExtension::checkNormalForm(Node eqc,
             {
               // simply introduce their intersection
               Assert(o0 != o1);
-              Node kca = d_state.getProxy(o0);
-              Node kcb = d_state.getProxy(o1);
+              Node kca = d_treg.getProxy(o0);
+              Node kcb = d_treg.getProxy(o1);
               Node intro =
                   Rewriter::rewrite(nm->mkNode(INTERSECTION, kca, kcb));
               Trace("sets-nf") << "   Intro split : " << o0 << " against " << o1
diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h
index c257f45c5..38f259919 100644
--- a/src/theory/sets/cardinality_extension.h
+++ b/src/theory/sets/cardinality_extension.h
@@ -21,6 +21,7 @@
 #include "context/context.h"
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/solver_state.h"
+#include "theory/sets/term_registry.h"
 #include "theory/type_set.h"
 #include "theory/uf/equality_engine.h"
 
@@ -67,7 +68,9 @@ class CardinalityExtension
    * Constructs a new instance of the cardinality solver w.r.t. the provided
    * contexts.
    */
-  CardinalityExtension(SolverState& s, InferenceManager& im);
+  CardinalityExtension(SolverState& s,
+                       InferenceManager& im,
+                       TermRegistry& treg);
 
   ~CardinalityExtension() {}
   /** reset
@@ -160,6 +163,8 @@ class CardinalityExtension
   SolverState& d_state;
   /** Reference to the inference manager for the theory of sets */
   InferenceManager& d_im;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
   /** register cardinality term
    *
    * This method add lemmas corresponding to the definition of
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 7254bca78..941f59bc6 100644
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -27,8 +27,9 @@ namespace sets {
 
 SolverState::SolverState(context::Context* c,
                          context::UserContext* u,
-                         Valuation val)
-    : TheoryState(c, u, val), d_parent(nullptr), d_proxy(u), d_proxy_to_term(u)
+                         Valuation val,
+                         SkolemCache& skc)
+    : TheoryState(c, u, val), d_skCache(skc), d_parent(nullptr)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -98,8 +99,6 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
   {
     if (nk == SINGLETON)
     {
-      // singleton lemma
-      getProxy(n);
       Node re = d_ee->getRepresentative(n[0]);
       if (d_singleton_index.find(re) == d_singleton_index.end())
       {
@@ -186,8 +185,8 @@ Node SolverState::getEmptySetEqClass(TypeNode tn) const
 
 Node SolverState::getUnivSetEqClass(TypeNode tn) const
 {
-  std::map<TypeNode, Node>::const_iterator it = d_univset.find(tn);
-  if (it != d_univset.end())
+  std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
+  if (it != d_eqc_univset.end())
   {
     return it->second;
   }
@@ -368,37 +367,6 @@ bool SolverState::isSetDisequalityEntailedInternal(Node a,
   return false;
 }
 
-Node SolverState::getProxy(Node n)
-{
-  Kind nk = n.getKind();
-  if (nk != EMPTYSET && nk != SINGLETON && nk != INTERSECTION && nk != SETMINUS
-      && nk != UNION && nk != UNIVERSE_SET)
-  {
-    return n;
-  }
-  NodeMap::const_iterator it = d_proxy.find(n);
-  if (it != d_proxy.end())
-  {
-    return (*it).second;
-  }
-  NodeManager* nm = NodeManager::currentNM();
-  Node k = d_skCache.mkTypedSkolemCached(
-      n.getType(), n, SkolemCache::SK_PURIFY, "sp");
-  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));
@@ -413,65 +381,6 @@ 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));
-  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);
@@ -547,32 +456,6 @@ const std::vector<Node>& SolverState::getComprehensionSets() const
   return d_allCompSets;
 }
 
-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) << ")";
-  }
-}
-
 const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
 {
   vector<Node> representatives;
diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h
index 1786c414b..245ad93f6 100644
--- a/src/theory/sets/solver_state.h
+++ b/src/theory/sets/solver_state.h
@@ -20,7 +20,6 @@
 #include <map>
 #include <vector>
 
-#include "context/cdhashset.h"
 #include "theory/sets/skolem_cache.h"
 #include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
@@ -33,10 +32,8 @@ 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.
+ * The purpose of this class is to maintain information concerning the current
+ * set of assertions during a full effort check.
  *
  * During a full effort check, the solver for theory of sets should call:
  *   reset; ( registerEqc | registerTerm )*
@@ -45,10 +42,11 @@ class TheorySetsPrivate;
  */
 class SolverState : public TheoryState
 {
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
-
  public:
-  SolverState(context::Context* c, context::UserContext* u, Valuation val);
+  SolverState(context::Context* c,
+              context::UserContext* u,
+              Valuation val,
+              SkolemCache& skc);
   /** Set parent */
   void setParent(TheorySetsPrivate* p);
   //-------------------------------- initialize per check
@@ -158,44 +156,6 @@ class SolverState : public TheoryState
   /** Get the list of all comprehension sets in the current context */
   const std::vector<Node>& getComprehensionSets() 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 if it exists or create a new one */
-  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;
@@ -203,6 +163,8 @@ class SolverState : public TheoryState
   /** the empty vector and map */
   std::vector<Node> d_emptyVec;
   std::map<Node, Node> d_emptyMap;
+  /** Reference to skolem cache */
+  SkolemCache& d_skCache;
   /** Pointer to the parent theory of sets */
   TheorySetsPrivate* d_parent;
   /** The list of all equivalence classes of type set in the current context */
@@ -228,18 +190,6 @@ class SolverState : public TheoryState
    * 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
    *
@@ -260,8 +210,6 @@ class SolverState : public TheoryState
   std::vector<Node> d_allCompSets;
   // -------------------------------- 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
diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp
new file mode 100644
index 000000000..301d5a85b
--- /dev/null
+++ b/src/theory/sets/term_registry.cpp
@@ -0,0 +1,154 @@
+/*********************                                                        */
+/*! \file term_registry.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 term registry object
+ **/
+
+#include "theory/sets/term_registry.h"
+
+#include "expr/emptyset.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+TermRegistry::TermRegistry(SolverState& state,
+                           InferenceManager& im,
+                           SkolemCache& skc)
+    : d_im(im),
+      d_skCache(skc),
+      d_proxy(state.getUserContext()),
+      d_proxy_to_term(state.getUserContext())
+{
+}
+
+Node TermRegistry::getProxy(Node n)
+{
+  Kind nk = n.getKind();
+  if (nk != EMPTYSET && nk != SINGLETON && nk != INTERSECTION && nk != SETMINUS
+      && nk != UNION && nk != UNIVERSE_SET)
+  {
+    return n;
+  }
+  NodeMap::const_iterator it = d_proxy.find(n);
+  if (it != d_proxy.end())
+  {
+    return (*it).second;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node k = d_skCache.mkTypedSkolemCached(
+      n.getType(), n, SkolemCache::SK_PURIFY, "sp");
+  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_im.lemma(eq, LemmaProperty::NONE, false);
+  if (nk == SINGLETON)
+  {
+    Node slem = nm->mkNode(MEMBER, n[0], k);
+    Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton"
+                        << std::endl;
+    d_im.lemma(slem, LemmaProperty::NONE, false);
+  }
+  return k;
+}
+
+Node TermRegistry::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));
+  d_emptyset[tn] = n;
+  return n;
+}
+
+Node TermRegistry::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_im.lemma(ulem, LemmaProperty::NONE, false);
+    }
+  }
+  d_univset[tn] = n;
+  return n;
+}
+
+Node TermRegistry::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;
+}
+
+void TermRegistry::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/term_registry.h b/src/theory/sets/term_registry.h
new file mode 100644
index 000000000..8779c7a19
--- /dev/null
+++ b/src/theory/sets/term_registry.h
@@ -0,0 +1,94 @@
+/*********************                                                        */
+/*! \file term_registry.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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__TERM_REGISTRY_H
+#define CVC4__THEORY__SETS__TERM_REGISTRY_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "theory/sets/inference_manager.h"
+#include "theory/sets/skolem_cache.h"
+#include "theory/sets/solver_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+/**
+ * Term registry, the purpose of this class is to maintain a database of
+ * commonly used terms, and mappings from sets to their "proxy variables".
+ */
+class TermRegistry
+{
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+
+ public:
+  TermRegistry(SolverState& state, InferenceManager& im, SkolemCache& skc);
+  /** 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 if it exists or create a new one */
+  Node getUnivSet(TypeNode tn);
+  /** debug print set */
+  void debugPrintSet(Node s, const char* c) const;
+
+ private:
+  /** The inference manager */
+  InferenceManager& d_im;
+  /** Reference to the skolem cache */
+  SkolemCache& d_skCache;
+  /** 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;
+}; /* class TheorySetsPrivate */
+
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__SETS__TERM_REGISTRY_H */
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 8b969de39..fe5e56aa6 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -34,9 +34,10 @@ TheorySets::TheorySets(context::Context* c,
                        const LogicInfo& logicInfo,
                        ProofNodeManager* pnm)
     : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
-      d_state(c, u, valuation),
+      d_skCache(),
+      d_state(c, u, valuation, d_skCache),
       d_im(*this, d_state, pnm),
-      d_internal(new TheorySetsPrivate(*this, d_state, d_im)),
+      d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)),
       d_notify(*d_internal.get())
 {
   // use the official theory state and inference manager objects
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index fed74b1bb..fce57ca6c 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -22,6 +22,7 @@
 #include <memory>
 
 #include "theory/sets/inference_manager.h"
+#include "theory/sets/skolem_cache.h"
 #include "theory/sets/solver_state.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -98,6 +99,8 @@ class TheorySets : public Theory
    private:
     TheorySetsPrivate& d_theory;
   };
+  /** The skolem cache */
+  SkolemCache d_skCache;
   /** The state of the sets solver at full effort */
   SolverState d_state;
   /** The inference manager */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 5e78e7ed5..a88374980 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -36,7 +36,8 @@ namespace sets {
 
 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
                                      SolverState& state,
-                                     InferenceManager& im)
+                                     InferenceManager& im,
+                                     SkolemCache& skc)
     : d_members(state.getSatContext()),
       d_deq(state.getSatContext()),
       d_termProcessed(state.getUserContext()),
@@ -44,8 +45,10 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
       d_external(external),
       d_state(state),
       d_im(im),
-      d_rels(new TheorySetsRels(d_state, d_im)),
-      d_cardSolver(new CardinalityExtension(d_state, d_im)),
+      d_skCache(skc),
+      d_treg(state, im, skc),
+      d_rels(new TheorySetsRels(state, im, skc, d_treg)),
+      d_cardSolver(new CardinalityExtension(state, im, d_treg)),
       d_rels_enabled(false),
       d_card_enabled(false)
 {
@@ -334,15 +337,21 @@ void TheorySetsPrivate::fullEffortCheck()
         }
         // register it with the state
         d_state.registerTerm(eqc, tnn, n);
-        if (n.getKind() == kind::CARD)
+        Kind nk = n.getKind();
+        if (nk == kind::SINGLETON)
+        {
+          // ensure the proxy has been introduced
+          d_treg.getProxy(n);
+        }
+        else if (nk == kind::CARD)
         {
           d_card_enabled = true;
           // register it with the cardinality solver
           d_cardSolver->registerTerm(n);
           // if we do not handle the kind, set incomplete
-          Kind nk = n[0].getKind();
+          Kind nk0 = n[0].getKind();
           // some kinds of cardinality we cannot handle
-          if (d_rels->isRelationKind(nk))
+          if (d_rels->isRelationKind(nk0))
           {
             d_full_check_incomplete = true;
             Trace("sets-incomplete")
@@ -358,12 +367,9 @@ void TheorySetsPrivate::fullEffortCheck()
             // 4- Supporting cardinality for relations (hard)
           }
         }
-        else
+        else if (d_rels->isRelationKind(nk))
         {
-          if (d_rels->isRelationKind(n.getKind()))
-          {
-            d_rels_enabled = true;
-          }
+          d_rels_enabled = true;
         }
         ++eqc_i;
       }
@@ -501,7 +507,7 @@ void TheorySetsPrivate::checkSubtypes()
           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);
+          Node tc_k = d_treg.getTypeConstraintSkolem(it2.first, mct);
           if (!tc_k.isNull())
           {
             Node etc = tc_k.eqNode(it2.first);
@@ -559,7 +565,7 @@ void TheorySetsPrivate::checkDownwardsClosure()
               else
               {
                 // use proxy set
-                Node k = d_state.getProxy(eq_set);
+                Node k = d_treg.getProxy(eq_set);
                 Node pmem =
                     NodeManager::currentNM()->mkNode(kind::MEMBER, mem[0], k);
                 Node nmem = NodeManager::currentNM()->mkNode(
@@ -677,7 +683,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
                   Node rr = d_equalityEngine->getRepresentative(term);
                   if (!isMember(x, rr))
                   {
-                    Node kk = d_state.getProxy(term);
+                    Node kk = d_treg.getProxy(term);
                     Node fact = nm->mkNode(kind::MEMBER, x, kk);
                     d_im.assertInference(fact, exp, "upc", inferType);
                     if (d_state.isInConflict())
@@ -704,7 +710,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
                     std::vector<Node> exp;
                     exp.push_back(itm2m.second);
                     d_state.addEqualityToExp(term[1], itm2m.second[1], exp);
-                    Node r = d_state.getProxy(term);
+                    Node r = d_treg.getProxy(term);
                     Node fact = nm->mkNode(kind::MEMBER, x, r);
                     d_im.assertInference(fact, exp, "upc2");
                     if (d_state.isInConflict())
@@ -750,7 +756,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
               // equivalence class
               if (s != ueqc)
               {
-                u = d_state.getUnivSet(tn);
+                u = d_treg.getUnivSet(tn);
               }
               univ_set[tn] = u;
             }
@@ -819,7 +825,7 @@ void TheorySetsPrivate::checkDisequalities()
     d_termProcessed.insert(deq[1].eqNode(deq[0]));
     Trace("sets") << "Process Disequality : " << deq.negate() << std::endl;
     TypeNode elementType = deq[0].getType().getSetElementType();
-    Node x = d_state.getSkolemCache().mkTypedSkolemCached(
+    Node x = d_skCache.mkTypedSkolemCached(
         elementType, deq[0], deq[1], SkolemCache::SK_DISEQUAL, "sde");
     Node mem1 = nm->mkNode(MEMBER, x, deq[0]);
     Node mem2 = nm->mkNode(MEMBER, x, deq[1]);
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index bd1d5f058..1c038e02f 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -25,6 +25,7 @@
 #include "theory/sets/cardinality_extension.h"
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/solver_state.h"
+#include "theory/sets/term_registry.h"
 #include "theory/sets/theory_sets_rels.h"
 #include "theory/sets/theory_sets_rewriter.h"
 #include "theory/theory.h"
@@ -149,7 +150,8 @@ class TheorySetsPrivate {
    */
   TheorySetsPrivate(TheorySets& external,
                     SolverState& state,
-                    InferenceManager& im);
+                    InferenceManager& im,
+                    SkolemCache& skc);
 
   ~TheorySetsPrivate();
 
@@ -231,6 +233,10 @@ class TheorySetsPrivate {
   SolverState& d_state;
   /** The inference manager of the sets solver */
   InferenceManager& d_im;
+  /** Reference to the skolem cache */
+  SkolemCache& d_skCache;
+  /** The term registry */
+  TermRegistry d_treg;
 
   /** Pointer to the equality engine of theory of sets */
   eq::EqualityEngine* d_equalityEngine;
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 838d29045..209c3c973 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -31,8 +31,15 @@ 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(SolverState& s, InferenceManager& im)
-    : d_state(s), d_im(im), d_shared_terms(s.getUserContext())
+TheorySetsRels::TheorySetsRels(SolverState& s,
+                               InferenceManager& im,
+                               SkolemCache& skc,
+                               TermRegistry& treg)
+    : d_state(s),
+      d_im(im),
+      d_skCache(skc),
+      d_treg(treg),
+      d_shared_terms(s.getUserContext())
 {
   d_trueNode = NodeManager::currentNM()->mkConst(true);
   d_falseNode = NodeManager::currentNM()->mkConst(false);
@@ -542,17 +549,16 @@ void TheorySetsRels::check(Theory::Effort level)
     }
     Node fst_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
     Node snd_element = RelsUtils::nthElementOfTuple( exp[0], 1 );
-    SkolemCache& sc = d_state.getSkolemCache();
-    Node sk_1 = sc.mkTypedSkolemCached(fst_element.getType(),
-                                       exp[0],
-                                       tc_rel[0],
-                                       SkolemCache::SK_TCLOSURE_DOWN1,
-                                       "stc1");
-    Node sk_2 = sc.mkTypedSkolemCached(fst_element.getType(),
-                                       exp[0],
-                                       tc_rel[0],
-                                       SkolemCache::SK_TCLOSURE_DOWN2,
-                                       "stc2");
+    Node sk_1 = d_skCache.mkTypedSkolemCached(fst_element.getType(),
+                                              exp[0],
+                                              tc_rel[0],
+                                              SkolemCache::SK_TCLOSURE_DOWN1,
+                                              "stc1");
+    Node sk_2 = d_skCache.mkTypedSkolemCached(fst_element.getType(),
+                                              exp[0],
+                                              tc_rel[0],
+                                              SkolemCache::SK_TCLOSURE_DOWN2,
+                                              "stc2");
     Node mem_of_r = nm->mkNode(MEMBER, exp[0], tc_rel[0]);
     Node sk_eq = nm->mkNode(EQUAL, sk_1, sk_2);
     Node reason   = exp;
@@ -815,7 +821,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_state.getSkolemCache().mkTypedSkolemCached(
+    Node shared_x = d_skCache.mkTypedSkolemCached(
         shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj");
     const DType& dt1 = join_rel[0].getType().getSetElementType().getDType();
     unsigned int s1_len         = join_rel[0].getType().getSetElementType().getTupleLength();
@@ -1185,7 +1191,7 @@ void TheorySetsRels::check(Theory::Effort level)
     Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl;
     // force a proxy lemma to be sent for the singleton containing n
     Node ss = NodeManager::currentNM()->mkNode(SINGLETON, n);
-    d_state.getProxy(ss);
+    d_treg.getProxy(ss);
     d_shared_terms.insert(n);
   }
 
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index f48aaf9c5..2912e5e47 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -24,6 +24,7 @@
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/rels_utils.h"
 #include "theory/sets/solver_state.h"
+#include "theory/sets/term_registry.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
@@ -65,7 +66,10 @@ class TheorySetsRels {
   typedef context::CDHashMap< Node, Node, NodeHashFunction >      NodeMap;
 
 public:
- TheorySetsRels(SolverState& s, InferenceManager& im);
+ TheorySetsRels(SolverState& s,
+                InferenceManager& im,
+                SkolemCache& skc,
+                TermRegistry& treg);
 
  ~TheorySetsRels();
  /**
@@ -87,6 +91,10 @@ private:
   SolverState& d_state;
   /** Reference to the inference manager for the theory of sets */
   InferenceManager& d_im;
+  /** Reference to the skolem cache */
+  SkolemCache& d_skCache;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
   /** A list of pending inferences to process */
   std::vector<Node> d_pending;
   NodeSet                       d_shared_terms;