From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 9 Apr 2014 20:56:56 +0000 (-0400)
Subject: use internal skolem numbering
X-Git-Tag: cvc5-1.0.0~6956^2~9
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4b02944c70522de78713f9870d2eccbf348bfcf6;p=cvc5.git

use internal skolem numbering
---

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f56f509b2..a4a5f76d4 100644
--- 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 7e9d60905..4f2c3c173 100644
--- 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 */