diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-17 18:01:10 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 17:18:58 -0400 |
commit | c8b948c37364104bf5f9ca5eca83120247b693a4 (patch) | |
tree | a4fba0d7ba7b8a1f93ff44878414fdda2e9ed941 /src | |
parent | dead33e1660596c75f2bfc5ee86ed39600a92a45 (diff) |
Fix for registration issues of term appearing in a shared lemma
(brought to attention by lianah -- fix currently just adapted using
arrays -- this is to remind me to raise why do we even have this
isPreregistered bussiness)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 4 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 18 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 2 |
4 files changed, 26 insertions, 0 deletions
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 73176ff8b..3a5b61390 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -34,6 +34,10 @@ TheorySets::~TheorySets() { delete d_internal; } +void TheorySets::addSharedTerm(TNode n) { + d_internal->addSharedTerm(n); +} + void TheorySets::check(Effort e) { d_internal->check(e); } diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 8900b0e38..f40031514 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -46,6 +46,8 @@ public: ~TheorySets(); + void addSharedTerm(TNode); + void check(Effort); void collectModelInfo(TheoryModel*, bool fullModel); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 17eaf80aa..b45874bf2 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -54,6 +54,19 @@ void TheorySetsPrivate::check(Theory::Effort level) { bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; + if (!assertion.isPreregistered) { + if (atom.getKind() == kind::EQUAL) { + if (!d_equalityEngine.hasTerm(atom[0])) { + Assert(atom[0].isConst()); + d_equalityEngine.addTerm(atom[0]); + } + if (!d_equalityEngine.hasTerm(atom[1])) { + Assert(atom[1].isConst()); + d_equalityEngine.addTerm(atom[1]); + } + } + } + // Solve each switch(atom.getKind()) { case kind::EQUAL: @@ -710,6 +723,11 @@ bool TheorySetsPrivate::propagate(TNode literal) { }/* TheorySetsPropagate::propagate(TNode) */ +void TheorySetsPrivate::addSharedTerm(TNode n) { + Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl; + d_equalityEngine.addTriggerTerm(n, THEORY_SETS); +} + void TheorySetsPrivate::conflict(TNode a, TNode b) { if (a.getKind() == kind::CONST_BOOLEAN) { diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 1f43ede42..58000e435 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -47,6 +47,8 @@ public: ~TheorySetsPrivate(); + void addSharedTerm(TNode); + void check(Theory::Effort); void collectModelInfo(TheoryModel*, bool fullModel); |