diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 18:18:07 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 18:18:07 -0400 |
commit | 004678b6386e66cfa6a079215a3644efca59cdf7 (patch) | |
tree | af7e8ba930b15ffc2ba901f35704c82abeb81e0e /src/theory/sets | |
parent | c28d0a243dbfd4295f785a017890251bd2670ce8 (diff) |
nodemanager robust skolem numbering
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 9 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 2 |
2 files changed, 1 insertions, 10 deletions
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 */ |