From 004678b6386e66cfa6a079215a3644efca59cdf7 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 28 Apr 2014 18:18:07 -0400
Subject: [PATCH] nodemanager robust skolem numbering

---
 src/expr/node_manager.cpp               |  8 +++++---
 src/expr/node_manager.h                 | 13 +++++++++++--
 src/theory/sets/theory_sets_private.cpp |  9 +--------
 src/theory/sets/theory_sets_private.h   |  2 --
 4 files changed, 17 insertions(+), 15 deletions(-)

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index ecd3df084..4c61550b9 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -89,7 +89,8 @@ NodeManager::NodeManager(context::Context* ctxt,
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
   d_inReclaimZombies(false),
-  d_abstractValueCount(0) {
+  d_abstractValueCount(0),
+  d_skolemCounter(0) {
   init();
 }
 
@@ -103,7 +104,8 @@ NodeManager::NodeManager(context::Context* ctxt,
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
   d_inReclaimZombies(false),
-  d_abstractValueCount(0) {
+  d_abstractValueCount(0),
+  d_skolemCounter(0) {
   init();
 }
 
@@ -310,7 +312,7 @@ Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, cons
   setAttribute(n, TypeCheckedAttr(), true);
   if((flags & SKOLEM_EXACT_NAME) == 0) {
     stringstream name;
-    name << prefix << '_' << n.getId();
+    name << prefix << '_' << ++d_skolemCounter;
     setAttribute(n, expr::VarNameAttr(), name.str());
   } else {
     setAttribute(n, expr::VarNameAttr(), prefix);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index f533d3ab9..f75ed9559 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -163,6 +163,15 @@ class NodeManager {
    */
   unsigned d_abstractValueCount;
 
+  /**
+   * A counter used to produce unique skolem names.
+   *
+   * Note that it is NOT incremented when skolems are created using
+   * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
+   * by this node manager.
+   */
+  unsigned d_skolemCounter;
+
   /**
    * Look up a NodeValue in the pool associated to this NodeManager.
    * The NodeValue argument need not be a "completely-constructed"
@@ -425,10 +434,10 @@ public:
    * Create a skolem constant with the given name, type, and comment.
    *
    * @param prefix the name of the new skolem variable is the prefix
-   * appended with the Node ID.  This way a family of skolem variables
+   * appended with a unique ID.  This way a family of skolem variables
    * can be made with unique identifiers, used in dump, tracing, and
    * debugging output.  Use SKOLEM_EXECT_NAME flag if you don't want
-   * Node ID appended and use prefix as the name.
+   * a unique ID appended and use prefix as the name.
    *
    * @param type the type of the skolem variable to create
    *
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index edb245d99..9d00cde7b 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -760,12 +760,6 @@ 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());
 
@@ -786,7 +780,7 @@ Node TheorySetsPrivate::getLemma() {
     d_pendingEverInserted.insert(n);
 
     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
-    Node x = newSkolem( n[0].getType().getSetElementType() );
+    Node x = NodeManager::currentNM()->mkSkolem("sde_", 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));
@@ -812,7 +806,6 @@ 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 4f2c3c173..7e9d60905 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -158,11 +158,9 @@ 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 */
-- 
2.30.2