diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-09 16:56:56 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-17 12:39:09 -0400 |
| commit | 4b02944c70522de78713f9870d2eccbf348bfcf6 (patch) | |
| tree | 442279fd0c2aa1eac2759f2c2b9fb405afb5d35a /src | |
| parent | fccff6adcc0a69273a54110596214f7927a96033 (diff) | |
use internal skolem numbering
Diffstat (limited to 'src')
| -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, 10 insertions, 1 deletions
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 */ |