diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-11 16:05:16 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-11 16:05:16 -0400 |
commit | 3c2458b633501345fba2679c611ce9e5c7a9f538 (patch) | |
tree | 17c3b4ce720c0d00facf93975665f8361e8da528 /src/theory | |
parent | 00a56716a656ace849be6fd00a3f018f3ab2eacf (diff) | |
parent | b402d8442fbdb50920d8d12188afd0e3eaab74e7 (diff) |
Merge pull request #31 from kbansal/sets
Sets
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 8 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 4 |
2 files changed, 5 insertions, 7 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 9b628ede2..f768bd62d 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -90,7 +90,9 @@ void TheorySetsPrivate::check(Theory::Effort level) { finishPropagation(); Debug("sets") << "[sets] in conflict = " << d_conflict << std::endl; - Assert( d_conflict ^ d_equalityEngine.consistent() ); + // Assert( d_conflict ^ d_equalityEngine.consistent() ); + // ^ doesn't hold when we propagate equality/disequality between shared terms + // and that leads to conflict (externally). if(d_conflict) { return; } Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; } @@ -831,8 +833,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_propagationQueue(c), d_settermPropagationQueue(c), d_nodeSaver(c), - d_pending(u), - d_pendingDisequal(u), + d_pending(c), + d_pendingDisequal(c), d_pendingEverInserted(u), d_scrutinize(NULL) { diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index bcfbc46ae..7b02c1bfb 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -117,10 +117,6 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { node[1].getKind() == kind::EMPTYSET) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; return RewriteResponse(REWRITE_DONE, node[0]); - } else if (node[0] > node[1]) { - Node newNode = nm->mkNode(node.getKind(), node[1], node[0]); - Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; - return RewriteResponse(REWRITE_DONE, newNode); } break; }//kind::INTERSECION |