use internal skolem numbering

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f56f509b23f0a8ec1adb25edd8753c2e614f07fd..a4a5f76d499c2906045e0db341f6808daf407bcd 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -760,6 +760,12 @@ bool TheorySetsPrivate::isComplete() {
   return d_pending.empty() && d_pendingDisequal.empty();
 }
 
+Node TheorySetsPrivate::newSkolem(TypeNode t) {
+  ostringstream oss;
+  oss << "sde_" << (++d_skolemCounter);
+  return NodeManager::currentNM()->mkSkolem(oss.str(), t, "", NodeManager::SKOLEM_EXACT_NAME);
+}
+
 Node TheorySetsPrivate::getLemma() {
   Assert(!d_pending.empty() || !d_pendingDisequal.empty());
 
@@ -780,7 +786,7 @@ Node TheorySetsPrivate::getLemma() {
     d_pendingEverInserted.insert(n);
 
     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
-    Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType());
+    Node x = newSkolem( n[0].getType().getSetElementType() );
     Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
 
     lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
@@ -806,6 +812,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_pending(u),
   d_pendingDisequal(u),
   d_pendingEverInserted(u),
+  d_skolemCounter(0),
   d_scrutinize(NULL)
 {
   d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 7e9d609053081027f8921759311aba55a4a813bc..4f2c3c173ef32a69e4f4d6da12deaea76518b8e2 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -158,9 +158,11 @@ private:
   context::CDQueue <TNode> d_pending;
   context::CDQueue <TNode> d_pendingDisequal;
   context::CDHashSet <Node, NodeHashFunction> d_pendingEverInserted;
+  int d_skolemCounter;
 
   void addToPending(Node n);
   bool isComplete();
+  Node newSkolem(TypeNode);
   Node getLemma();
 
   /** model generation and helper function */