Refactoring skolems for sets (#3381)

This refactors skolems introduced in the theory of sets. This is analogous to how skolems are treated for the theory of strings.

A key change that this commit enables is to identify "variable" sets based on those that weren't introduced by the SkolemCache (instead of via a check that their kind is `VARIABLE`, which is done currently and is error prone).

5 files changed, 109 insertions, 65 deletions

diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp
index 99e6588ca..a70e6dc51 100644
--- a/src/theory/sets/skolem_cache.cpp
+++ b/src/theory/sets/skolem_cache.cpp
@@ -39,6 +39,13 @@ Node SkolemCache::mkTypedSkolemCached(
   }
   return it->second;
 }
+Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
+                                      Node a,
+                                      SkolemId id,
+                                      const char* c)
+{
+  return mkTypedSkolemCached(tn, a, Node::null(), id, c);
+}
 
 Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
 {
diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h
index 74a8073d4..f1f2a82c0 100644
--- a/src/theory/sets/skolem_cache.h
+++ b/src/theory/sets/skolem_cache.h
@@ -43,6 +43,14 @@ class SkolemCache
    */
   enum SkolemId
   {
+    // exists k. k = a
+    SK_PURIFY,
+    // a != b => exists k. ( k in a != k in b )
+    SK_DISEQUAL,
+    // a in tclosure(b) => exists k1 k2. ( a.1, k1 ) in b ^ ( k2, a.2 ) in b ^
+    //                                   ( k1 = k2 V ( k1, k2 ) in tclosure(b) )
+    SK_TCLOSURE_DOWN1,
+    SK_TCLOSURE_DOWN2,
     // (a,b) in join(A,B) => exists k. (a,k) in A ^ (k,b) in B
     // This is cached by the nodes corresponding to (a,b) and join(A,B).
     SK_JOIN,
@@ -54,6 +62,8 @@ class SkolemCache
    */
   Node mkTypedSkolemCached(
       TypeNode tn, Node a, Node b, SkolemId id, const char* c);
+  /** same as above, cached based on key (a,null,id) */
+  Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c);
   /** Same as above, but without caching. */
   Node mkTypedSkolem(TypeNode tn, const char* c);
   /** Returns true if n is a skolem allocated by this class */
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 76c7c3884..7756fe081 100644
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -137,10 +137,10 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
     d_nvar_sets[r].push_back(n);
     Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
   }
-  else if (nk == VARIABLE)
+  else if (n.isVar() && !d_skCache.isSkolem(n))
   {
-    // it is important that we check kind VARIABLE, due to the semantics of the
-    // universe set.
+    // it is important that we check it is a variable, but not an internally
+    // introduced skolem, due to the semantics of the universe set.
     if (tnn.isSet())
     {
       if (d_var_set.find(r) == d_var_set.end())
@@ -401,7 +401,8 @@ Node SolverState::getProxy(Node n)
     return (*it).second;
   }
   NodeManager* nm = NodeManager::currentNM();
-  Node k = nm->mkSkolem("sp", n.getType(), "proxy for set");
+  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);
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 472395e1b..3b52da338 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -736,44 +736,50 @@ void TheorySetsPrivate::checkDisequalities()
 {
   //disequalities
   Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
   for(NodeBoolMap::const_iterator it=d_deq.begin(); it !=d_deq.end(); ++it) {
-    if( (*it).second ){
-      Node deq = (*it).first;
-      //check if it is already satisfied
-      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 = d_state.isSetDisequalityEntailed(r1, r2);
-      /*
-      if( !is_sat ){
-        //try to make one of them empty
-        for( unsigned e=0; e<2; e++ ){
-        }
-      }
-      */
-      Trace("sets-debug") << "Check disequality " << deq << ", is_sat = " << is_sat << std::endl;
-      //will process regardless of sat/processed/unprocessed
-      d_deq[deq] = false;
-      
-      if( !is_sat ){
-        if( d_deq_processed.find( deq )==d_deq_processed.end() ){
-          d_deq_processed.insert( deq );
-          d_deq_processed.insert( deq[1].eqNode( deq[0] ) );
-          Trace("sets") << "Process Disequality : " << deq.negate() << std::endl;
-          TypeNode elementType = deq[0].getType().getSetElementType();
-          Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType);
-          Node mem1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[0] );
-          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 );
-          d_im.assertInference(lem, d_emp_exp, "diseq", 1);
-          d_im.flushPendingLemmas();
-          if (d_im.hasProcessed())
-          {
-            return;
-          }
-        }
-      }
+    if (!(*it).second)
+    {
+      // not active
+      continue;
+    }
+    Node deq = (*it).first;
+    // check if it is already satisfied
+    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 = d_state.isSetDisequalityEntailed(r1, r2);
+    Trace("sets-debug") << "Check disequality " << deq
+                        << ", is_sat = " << is_sat << std::endl;
+    // will process regardless of sat/processed/unprocessed
+    d_deq[deq] = false;
+
+    if (is_sat)
+    {
+      // already satisfied
+      continue;
+    }
+    if (d_deq_processed.find(deq) != d_deq_processed.end())
+    {
+      // already added lemma
+      continue;
+    }
+    d_deq_processed.insert(deq);
+    d_deq_processed.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(
+        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]);
+    Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate());
+    lem = Rewriter::rewrite(lem);
+    d_im.assertInference(lem, d_emp_exp, "diseq", 1);
+    d_im.flushPendingLemmas();
+    if (d_im.hasProcessed())
+    {
+      return;
     }
   }
 }
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 382cb671b..65cff2418 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -510,6 +510,8 @@ void TheorySetsRels::check(Theory::Effort level)
                               << " or can be infered by TC_Graph of tc_rel[0]! " << std::endl;
       return;
     }
+    NodeManager* nm = NodeManager::currentNM();
+
     // add mem_rep to d_tcrRep_tcGraph
     TC_IT tc_it = d_tcr_tcGraph.find( tc_rel );
     Node mem_rep_fst = getRepresentative( RelsUtils::nthElementOfTuple( mem_rep, 0 ) );
@@ -544,25 +546,45 @@ void TheorySetsRels::check(Theory::Effort level)
       exp_map[mem_rep_tup] = exp;
       d_tcr_tcGraph_exps[tc_rel] = exp_map;
     }
-
     Node fst_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
     Node snd_element = RelsUtils::nthElementOfTuple( exp[0], 1 );
-    Node sk_1     = NodeManager::currentNM()->mkSkolem("stc", fst_element.getType());
-    Node sk_2     = NodeManager::currentNM()->mkSkolem("stc", snd_element.getType());
-    Node mem_of_r = NodeManager::currentNM()->mkNode(kind::MEMBER, exp[0], tc_rel[0]);
-    Node sk_eq    = NodeManager::currentNM()->mkNode(kind::EQUAL, sk_1, sk_2);
+    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 mem_of_r = nm->mkNode(MEMBER, exp[0], tc_rel[0]);
+    Node sk_eq = nm->mkNode(EQUAL, sk_1, sk_2);
     Node reason   = exp;
 
     if( tc_rel != exp[1] ) {
-      reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel, exp[1]));
-    }
-
-    Node conclusion = NodeManager::currentNM()->mkNode(kind::OR, mem_of_r,
-                                                     (NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, fst_element, sk_1), tc_rel[0]),
-                                                     (NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, sk_2, snd_element), tc_rel[0]),
-                                                     (NodeManager::currentNM()->mkNode(kind::OR, sk_eq, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, sk_1, sk_2), tc_rel))))))));
-
-    Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, conclusion );
+      reason = nm->mkNode(AND, reason, nm->mkNode(EQUAL, tc_rel, exp[1]));
+    }
+
+    Node conc = nm->mkNode(
+        OR,
+        mem_of_r,
+        nm->mkNode(
+            AND,
+            nm->mkNode(MEMBER,
+                       RelsUtils::constructPair(tc_rel, fst_element, sk_1),
+                       tc_rel[0]),
+            nm->mkNode(MEMBER,
+                       RelsUtils::constructPair(tc_rel, sk_2, snd_element),
+                       tc_rel[0]),
+            nm->mkNode(OR,
+                       sk_eq,
+                       nm->mkNode(MEMBER,
+                                  RelsUtils::constructPair(tc_rel, sk_1, sk_2),
+                                  tc_rel))));
+
+    Node tc_lemma = nm->mkNode(IMPLIES, reason, conc);
     d_pending.push_back(tc_lemma);
   }
 
@@ -1168,17 +1190,15 @@ void TheorySetsRels::check(Theory::Effort level)
   }
 
   void TheorySetsRels::makeSharedTerm( Node n ) {
-    if(d_shared_terms.find(n) == d_shared_terms.end()) {
-      Trace("rels-share") << " [sets-rels] making shared term " << n
-                          << std::endl;
-      Node skolem = NodeManager::currentNM()->mkSkolem( "sts", NodeManager::currentNM()->mkSetType( n.getType() ) );
-      Node skEq =
-          skolem.eqNode(NodeManager::currentNM()->mkNode(kind::SINGLETON, n));
-      // force lemma to be sent immediately
-      d_im.assertInference(skEq, d_trueNode, "shared-term");
-      d_im.flushPendingLemmas();
-      d_shared_terms.insert(n);
+    if (d_shared_terms.find(n) != d_shared_terms.end())
+    {
+      return;
     }
+    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_shared_terms.insert(n);
   }
 
   /*