1 /********************* */
2 /*! \file theory_sets_private.cpp
4 ** Original author: Kshitij Bansal
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2013-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Sets theory implementation.
14 ** Sets theory implementation.
17 #include "theory/sets/theory_sets.h"
18 #include "theory/sets/theory_sets_private.h"
20 #include "theory/sets/options.h"
21 #include "theory/sets/expr_patterns.h" // ONLY included here
23 #include "util/result.h"
26 using namespace CVC4::expr::pattern
;
32 const char* element_of_str
= " \u2208 ";
34 /**************************** TheorySetsPrivate *****************************/
35 /**************************** TheorySetsPrivate *****************************/
36 /**************************** TheorySetsPrivate *****************************/
38 void TheorySetsPrivate::check(Theory::Effort level
) {
40 CodeTimer
checkCodeTimer(d_statistics
.d_checkTime
);
42 while(!d_external
.done() && !d_conflict
) {
43 // Get all the assertions
44 Assertion assertion
= d_external
.get();
45 TNode fact
= assertion
.assertion
;
47 Debug("sets") << "\n\n[sets] TheorySetsPrivate::check(): processing "
50 bool polarity
= fact
.getKind() != kind::NOT
;
51 TNode atom
= polarity
? fact
: fact
[0];
54 switch(atom
.getKind()) {
56 Debug("sets") << atom
[0] << " should " << (polarity
? "":"NOT ")
57 << "be equal to " << atom
[1] << std::endl
;
58 assertEquality(fact
, fact
, /* learnt = */ false);
62 Debug("sets") << atom
[0] << " should " << (polarity
? "":"NOT ")
63 << "be in " << atom
[1] << std::endl
;
64 assertMemebership(fact
, fact
, /* learnt = */ false);
68 Unhandled(fact
.getKind());
72 Debug("sets") << "[sets] in conflict = " << d_conflict
<< std::endl
;
74 if(d_conflict
&& !d_equalityEngine
.consistent()) return;
76 Assert(d_equalityEngine
.consistent());
79 Debug("sets") << "[sets] is complete = " << isComplete() << std::endl
;
81 if( (Theory::EFFORT_FULL
|| options::setsEagerLemmas() ) && !isComplete()) {
82 d_external
.d_out
->lemma(getLemma());
86 }/* TheorySetsPrivate::check() */
89 void TheorySetsPrivate::assertEquality(TNode fact
, TNode reason
, bool learnt
)
91 Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
93 << ", " << learnt
<< std::endl
;
95 bool polarity
= fact
.getKind() != kind::NOT
;
96 TNode atom
= polarity
? fact
: fact
[0];
99 if( holds(atom
, polarity
) ) {
100 Debug("sets-assert") << "[sets-assert] already present, skipping" << std::endl
;
104 // assert fact & check for conflict
106 registerReason(reason
, /*save=*/ true);
108 d_equalityEngine
.assertEquality(atom
, polarity
, reason
);
110 if(!d_equalityEngine
.consistent()) {
111 Debug("sets-assert") << "[sets-assert] running into a conflict" << std::endl
;
116 if(!polarity
&& atom
[0].getType().isSet()) {
120 }/* TheorySetsPrivate::assertEquality() */
123 void TheorySetsPrivate::assertMemebership(TNode fact
, TNode reason
, bool learnt
)
125 Debug("sets-assert") << "\n[sets-assert] adding membership: " << fact
127 << ", " << learnt
<< std::endl
;
129 bool polarity
= fact
.getKind() == kind::NOT
? false : true;
130 TNode atom
= polarity
? fact
: fact
[0];
132 // fact already holds
133 if( holds(atom
, polarity
) ) {
134 Debug("sets-assert") << "[sets-assert] already present, skipping" << std::endl
;
138 // assert fact & check for conflict
140 registerReason(reason
, true);
142 d_equalityEngine
.assertPredicate(atom
, polarity
, reason
);
144 if(!d_equalityEngine
.consistent()) {
145 Debug("sets-assert") << "[sets-assert] running into a conflict" << std::endl
;
150 // update term info data structures
151 d_termInfoManager
->notifyMembership(fact
);
154 TNode x
= d_equalityEngine
.getRepresentative(atom
[0]);
155 eq::EqClassIterator
j(d_equalityEngine
.getRepresentative(atom
[1]),
158 Node cur_atom
= IN(x
, S
);
161 * It is sufficient to do emptyset propagation outside the loop as
162 * constant term is guaranteed to be class representative.
164 if(polarity
&& S
.getKind() == kind::EMPTYSET
) {
165 Debug("sets-prop") << "[sets-prop] something in empty set? conflict."
167 learnLiteral(cur_atom
, false, cur_atom
);
172 for(; !j
.isFinished(); ++j
) {
174 Node cur_atom
= IN(x
, S
);
176 // propagation : children
177 Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
178 << x
<< element_of_str
<< S
<< std::endl
;
179 if(S
.getKind() == kind::UNION
||
180 S
.getKind() == kind::INTERSECTION
||
181 S
.getKind() == kind::SETMINUS
||
182 S
.getKind() == kind::SET_SINGLETON
) {
183 doSettermPropagation(x
, S
);
184 if(d_conflict
) return;
185 }// propagation: children
188 // propagation : parents
189 Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
190 << x
<< element_of_str
<< S
<< std::endl
;
191 const CDTNodeList
* parentList
= d_termInfoManager
->getParents(S
);
192 for(typeof(parentList
->begin()) k
= parentList
->begin();
193 k
!= parentList
->end(); ++k
) {
194 doSettermPropagation(x
, *k
);
195 if(d_conflict
) return;
196 }// propagation : parents
201 }/* TheorySetsPrivate::assertMemebership() */
204 void TheorySetsPrivate::doSettermPropagation(TNode x
, TNode S
)
206 Debug("sets-prop") << "[sets-prop] doSettermPropagation("
207 << x
<< ", " << S
<< std::endl
;
209 Assert(S
.getType().isSet() && S
.getType().getSetElementType() == x
.getType());
211 Node literal
, left_literal
, right_literal
;
213 // axiom: literal <=> left_literal AND right_literal
214 switch(S
.getKind()) {
215 case kind::INTERSECTION
:
217 left_literal
= IN(x
, S
[0]) ;
218 right_literal
= IN(x
, S
[1]) ;
221 literal
= NOT( IN(x
, S
) );
222 left_literal
= NOT( IN(x
, S
[0]) );
223 right_literal
= NOT( IN(x
, S
[1]) );
227 left_literal
= IN(x
, S
[0]) ;
228 right_literal
= NOT( IN(x
, S
[1]) );
230 case kind::SET_SINGLETON
: {
231 Node atom
= IN(x
, S
);
232 if(holds(atom
, true)) {
233 learnLiteral(EQUAL(x
, S
[0]), true, atom
);
234 } else if(holds(atom
, false)) {
235 learnLiteral(EQUAL(x
, S
[0]), false, NOT(atom
));
243 Debug("sets-prop-details")
244 << "[sets-prop-details] " << literal
<< " IFF " << left_literal
245 << " AND " << right_literal
<< std::endl
;
247 Debug("sets-prop-details")
248 << "[sets-prop-details] "
249 << (holds(literal
) ? "yes" : (holds(literal
.negate()) ? " no" : " _ "))
251 << (holds(left_literal
) ? "yes" : (holds(left_literal
.negate()) ? "no " : " _ "))
253 << (holds(right_literal
) ? "yes" : (holds(right_literal
.negate()) ? "no " : " _ "))
256 Assert( present( IN(x
, S
) ) ||
257 present( IN(x
, S
[0]) ) ||
258 present( IN(x
, S
[1]) ) );
260 if( holds(literal
) ) {
261 // 1a. literal => left_literal
262 Debug("sets-prop") << "[sets-prop] ... via case 1a. ..." << std::endl
;
263 learnLiteral(left_literal
, literal
);
264 if(d_conflict
) return;
266 // 1b. literal => right_literal
267 Debug("sets-prop") << "[sets-prop] ... via case 1b. ..." << std::endl
;
268 learnLiteral(right_literal
, literal
);
269 if(d_conflict
) return;
271 // subsumption requirement met, exit
274 else if( holds(literal
.negate() ) ) {
275 // 4. neg(literal), left_literal => neg(right_literal)
276 if( holds(left_literal
) ) {
277 Debug("sets-prop") << "[sets-prop] ... via case 4. ..." << std::endl
;
278 learnLiteral(right_literal
.negate(), AND( literal
.negate(),
280 if(d_conflict
) return;
283 // 5. neg(literal), right_literal => neg(left_literal)
284 if( holds(right_literal
) ) {
285 Debug("sets-prop") << "[sets-prop] ... via case 5. ..." << std::endl
;
286 learnLiteral(left_literal
.negate(), AND( literal
.negate(),
288 if(d_conflict
) return;
292 // 2,3. neg(left_literal) v neg(right_literal) => neg(literal)
293 if(holds(left_literal
.negate())) {
294 Debug("sets-prop") << "[sets-prop] ... via case 2. ..." << std::endl
;
295 learnLiteral(literal
.negate(), left_literal
.negate());
296 if(d_conflict
) return;
298 else if(holds(right_literal
.negate())) {
299 Debug("sets-prop") << "[sets-prop] ... via case 3. ..." << std::endl
;
300 learnLiteral(literal
.negate(), right_literal
.negate());
301 if(d_conflict
) return;
304 // 6. the axiom itself:
305 else if(holds(left_literal
) && holds(right_literal
)) {
306 Debug("sets-prop") << "[sets-prop] ... via case 6. ..." << std::endl
;
307 learnLiteral(literal
, AND(left_literal
, right_literal
) );
308 if(d_conflict
) return;
312 // check fulfilling rule
314 switch(S
.getKind()) {
316 if( holds(IN(x
, S
)) &&
317 !present( IN(x
, S
[0]) ) )
318 addToPending( IN(x
, S
[0]) );
320 case kind::SETMINUS
: // intentional fallthrough
321 case kind::INTERSECTION
:
322 if( holds(IN(x
, S
[0])) &&
323 !present( IN(x
, S
[1]) ))
324 addToPending( IN(x
, S
[1]) );
327 Assert(false, "MembershipEngine::doSettermPropagation");
332 void TheorySetsPrivate::learnLiteral(TNode atom
, bool polarity
, Node reason
) {
333 Debug("sets-learn") << "[sets-learn] learnLiteral(" << atom
334 << ", " << polarity
<< ")" << std::endl
;
336 if( holds(atom
, polarity
) ) {
337 Debug("sets-learn") << "[sets-learn] \u2514 already known, skipping" << std::endl
;
341 if( holds(atom
, !polarity
) ) {
342 Debug("sets-learn") << "[sets-learn] \u2514 conflict found" << std::endl
;
344 registerReason(reason
, /*save=*/ true);
346 if(atom
.getKind() == kind::EQUAL
) {
347 d_equalityEngine
.assertEquality(atom
, polarity
, reason
);
349 d_equalityEngine
.assertPredicate(atom
, polarity
, reason
);
351 Assert(d_conflict
); // should be marked due to equality engine
355 Assert(atom
.getKind() == kind::EQUAL
|| atom
.getKind() == kind::IN
);
357 Node learnt_literal
= polarity
? Node(atom
) : NOT(atom
);
358 d_propagationQueue
.push_back( make_pair(learnt_literal
, reason
) );
361 /********************** Helper functions ***************************/
362 /********************** Helper functions ***************************/
363 /********************** Helper functions ***************************/
365 Node
mkAnd(const std::vector
<TNode
>& conjunctions
) {
366 Assert(conjunctions
.size() > 0);
370 for (unsigned i
= 0; i
< conjunctions
.size(); ++i
) {
371 TNode t
= conjunctions
[i
];
373 if (t
.getKind() == kind::AND
) {
374 for(TNode::iterator child_it
= t
.begin();
375 child_it
!= t
.end(); ++child_it
) {
376 Assert((*child_it
).getKind() != kind::AND
);
377 all
.insert(*child_it
);
386 Assert(all
.size() > 0);
388 if (all
.size() == 1) {
389 // All the same, or just one
390 return conjunctions
[0];
393 NodeBuilder
<> conjunction(kind::AND
);
394 std::set
<TNode
>::const_iterator it
= all
.begin();
395 std::set
<TNode
>::const_iterator it_end
= all
.end();
396 while (it
!= it_end
) {
405 TheorySetsPrivate::Statistics::Statistics() :
406 d_checkTime("theory::sets::time") {
407 StatisticsRegistry::registerStat(&d_checkTime
);
411 TheorySetsPrivate::Statistics::~Statistics() {
412 StatisticsRegistry::unregisterStat(&d_checkTime
);
416 bool TheorySetsPrivate::present(TNode atom
) {
417 return holds(atom
) || holds(atom
.notNode());
421 bool TheorySetsPrivate::holds(TNode atom
, bool polarity
) {
422 Node polarity_atom
= NodeManager::currentNM()->mkConst
<bool>(polarity
);
424 Node atomModEq
= NodeManager::currentNM()->mkNode
425 (atom
.getKind(), d_equalityEngine
.getRepresentative(atom
[0]),
426 d_equalityEngine
.getRepresentative(atom
[1]) );
428 d_equalityEngine
.addTerm(atomModEq
);
430 return d_equalityEngine
.areEqual(atomModEq
, polarity_atom
);
434 void TheorySetsPrivate::registerReason(TNode reason
, bool save
)
436 if(save
) d_nodeSaver
.insert(reason
);
438 if(reason
.getKind() == kind::AND
) {
439 Assert(reason
.getNumChildren() == 2);
440 registerReason(reason
[0], false);
441 registerReason(reason
[1], false);
442 } else if(reason
.getKind() == kind::NOT
) {
443 registerReason(reason
[0], false);
444 } else if(reason
.getKind() == kind::IN
) {
445 d_equalityEngine
.addTerm(reason
);
446 Assert(present(reason
));
447 } else if(reason
.getKind() == kind::EQUAL
) {
448 d_equalityEngine
.addTerm(reason
);
449 Assert(present(reason
));
450 } else if(reason
.getKind() == kind::CONST_BOOLEAN
) {
451 // That's OK, already in EqEngine
457 void TheorySetsPrivate::finishPropagation()
459 while(!d_conflict
&& !d_settermPropagationQueue
.empty()) {
460 std::pair
<TNode
,TNode
> np
= d_settermPropagationQueue
.front();
461 d_settermPropagationQueue
.pop();
462 doSettermPropagation(np
.first
, np
.second
);
464 while(!d_conflict
&& !d_propagationQueue
.empty()) {
465 std::pair
<Node
,Node
> np
= d_propagationQueue
.front();
466 d_propagationQueue
.pop();
467 TNode atom
= np
.first
.getKind() == kind::NOT
? np
.first
[0] : np
.first
;
468 if(atom
.getKind() == kind::IN
) {
469 assertMemebership(np
.first
, np
.second
, /* learnt = */ true);
471 assertEquality(np
.first
, np
.second
, /* learnt = */ true);
476 void TheorySetsPrivate::addToPending(Node n
) {
477 if(d_pendingEverInserted
.find(n
) == d_pendingEverInserted
.end()) {
478 if(n
.getKind() == kind::IN
) {
481 Assert(n
.getKind() == kind::EQUAL
);
482 d_pendingDisequal
.push(n
);
484 d_pendingEverInserted
.insert(n
);
488 bool TheorySetsPrivate::isComplete() {
489 while(!d_pending
.empty() && present(d_pending
.front()))
491 return d_pending
.empty() && d_pendingDisequal
.empty();
494 Node
TheorySetsPrivate::getLemma() {
495 Assert(!d_pending
.empty() || !d_pendingDisequal
.empty());
499 if(!d_pending
.empty()) {
500 Node n
= d_pending
.front();
504 Assert(n
.getKind() == kind::IN
);
506 lemma
= OR(n
, NOT(n
));
508 Node n
= d_pendingDisequal
.front();
509 d_pendingDisequal
.pop();
511 Assert(n
.getKind() == kind::EQUAL
&& n
[0].getType().isSet());
512 Node x
= NodeManager::currentNM()->mkSkolem("sde_$$", n
[0].getType().getSetElementType());
513 Node l1
= IN(x
, n
[0]), l2
= IN(x
, n
[1]);
515 // d_equalityEngine.addTerm(x);
516 // d_equalityEngine.addTerm(l1);
517 // d_equalityEngine.addTerm(l2);
518 // d_terms.insert(x);
520 lemma
= OR(n
, AND(l1
, NOT(l2
)), AND(NOT(l1
), l2
));
523 Debug("sets-lemma") << "[sets-lemma] " << lemma
<< std::endl
;
529 TheorySetsPrivate::TheorySetsPrivate(TheorySets
& external
,
531 context::UserContext
* u
):
532 d_external(external
),
534 d_equalityEngine(d_notify
, c
, "theory::sets::TheorySetsPrivate"),
536 d_termInfoManager(NULL
),
537 d_propagationQueue(c
),
538 d_settermPropagationQueue(c
),
541 d_pendingDisequal(u
),
542 d_pendingEverInserted(u
)
544 d_termInfoManager
= new TermInfoManager(*this, c
, &d_equalityEngine
);
546 d_equalityEngine
.addFunctionKind(kind::UNION
);
547 d_equalityEngine
.addFunctionKind(kind::INTERSECTION
);
548 d_equalityEngine
.addFunctionKind(kind::SETMINUS
);
550 d_equalityEngine
.addFunctionKind(kind::IN
);
551 d_equalityEngine
.addFunctionKind(kind::SUBSET
);
552 }/* TheorySetsPrivate::TheorySetsPrivate() */
554 TheorySetsPrivate::~TheorySetsPrivate()
556 delete d_termInfoManager
;
561 void TheorySetsPrivate::propagate(Theory::Effort e
)
566 bool TheorySetsPrivate::propagate(TNode literal
) {
567 Debug("sets-prop") << " propagate(" << literal
<< ")" << std::endl
;
569 // If already in conflict, no more propagation
571 Debug("sets-prop") << "TheoryUF::propagate(" << literal
<< "): already in conflict" << std::endl
;
576 bool ok
= d_external
.d_out
->propagate(literal
);
582 }/* TheorySetsPropagate::propagate(TNode) */
585 void TheorySetsPrivate::conflict(TNode a
, TNode b
)
587 if (a
.getKind() == kind::CONST_BOOLEAN
) {
588 d_conflictNode
= explain(a
.iffNode(b
));
590 d_conflictNode
= explain(a
.eqNode(b
));
592 d_external
.d_out
->conflict(d_conflictNode
);
593 Debug("sets") << "[sets] conflict: " << a
<< " iff " << b
594 << ", explaination " << d_conflictNode
<< std::endl
;
598 Node
TheorySetsPrivate::explain(TNode literal
)
600 Debug("sets") << "TheorySetsPrivate::explain(" << literal
<< ")"
603 bool polarity
= literal
.getKind() != kind::NOT
;
604 TNode atom
= polarity
? literal
: literal
[0];
605 std::vector
<TNode
> assumptions
;
607 if(atom
.getKind() == kind::EQUAL
|| atom
.getKind() == kind::IFF
) {
608 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
609 } else if(atom
.getKind() == kind::IN
) {
610 if( !d_equalityEngine
.hasTerm(atom
)) {
611 d_equalityEngine
.addTerm(atom
);
613 d_equalityEngine
.explainPredicate(atom
, polarity
, assumptions
);
615 Debug("sets") << "unhandled: " << literal
<< "; (" << atom
<< ", "
616 << polarity
<< "); kind" << atom
.getKind() << std::endl
;
620 return mkAnd(assumptions
);
623 void TheorySetsPrivate::preRegisterTerm(TNode node
)
625 Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node
<< ")"
628 switch(node
.getKind()) {
630 // TODO: what's the point of this
631 d_equalityEngine
.addTriggerEquality(node
);
634 // TODO: what's the point of this
635 d_equalityEngine
.addTriggerPredicate(node
);
638 d_termInfoManager
->addTerm(node
);
639 d_equalityEngine
.addTriggerTerm(node
, THEORY_SETS
);
640 // d_equalityEngine.addTerm(node);
642 if(node
.getKind() == kind::SET_SINGLETON
) {
643 Node true_node
= NodeManager::currentNM()->mkConst
<bool>(true);
644 learnLiteral(IN(node
[0], node
), true, true_node
);
645 //intentional fallthrough
651 /**************************** eq::NotifyClass *****************************/
652 /**************************** eq::NotifyClass *****************************/
653 /**************************** eq::NotifyClass *****************************/
656 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality
, bool value
)
658 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
<< " value = " << value
<< std::endl
;
660 return d_theory
.propagate(equality
);
662 // We use only literal triggers so taking not is safe
663 return d_theory
.propagate(equality
.notNode());
667 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate
, bool value
)
669 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
<< " value = " << value
<< std::endl
;
671 return d_theory
.propagate(predicate
);
673 return d_theory
.propagate(predicate
.notNode());
677 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
)
679 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
<< " t1 = " << t1
<< " t2 = " << t2
<< " value = " << value
<< std::endl
;
681 d_theory
.d_termInfoManager
->mergeTerms(t1
, t2
);
686 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1
, TNode t2
)
688 Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1
<< " t2 = " << t2
<< std::endl
;
689 d_theory
.conflict(t1
, t2
);
692 void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t
)
694 Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t
<< std::endl
;
697 void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1
, TNode t2
)
699 Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1
<< " t2 = " << t2
<< std::endl
;
702 void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1
, TNode t2
)
704 Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1
<< " t2 = " << t2
<< std::endl
;
707 void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
)
709 Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1
<< " t2 = " << t2
<< " reason = " << reason
<< std::endl
;
713 /**************************** TermInfoManager *****************************/
714 /**************************** TermInfoManager *****************************/
715 /**************************** TermInfoManager *****************************/
717 void TheorySetsPrivate::TermInfoManager::mergeLists
718 (CDTNodeList
* la
, const CDTNodeList
* lb
) const {
719 // straight from theory/arrays/array_info.cpp
720 std::set
<TNode
> temp
;
721 CDTNodeList::const_iterator it
;
722 for(it
= la
->begin() ; it
!= la
->end(); it
++ ) {
726 for(it
= lb
->begin() ; it
!= lb
->end(); it
++ ) {
727 if(temp
.count(*it
) == 0) {
733 TheorySetsPrivate::TermInfoManager::TermInfoManager
734 (TheorySetsPrivate
& theory
, context::Context
* satContext
, eq::EqualityEngine
* eq
):
736 d_context(satContext
),
742 TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
743 for( typeof(d_info
.begin()) it
= d_info
.begin();
744 it
!= d_info
.end(); ++it
) {
749 void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact
) {
750 bool polarity
= fact
.getKind() != kind::NOT
;
751 TNode atom
= polarity
? fact
: fact
[0];
753 TNode x
= d_eqEngine
->getRepresentative(atom
[0]);
754 TNode S
= d_eqEngine
->getRepresentative(atom
[1]);
756 Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
757 << " in " << S
<< " " << polarity
<< std::endl
;
759 d_info
[S
]->addToElementList(x
, polarity
);
762 const CDTNodeList
* TheorySetsPrivate::TermInfoManager::getParents(TNode x
) {
763 return d_info
[x
]->parents
;
766 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n
) {
767 unsigned numChild
= n
.getNumChildren();
769 if(!d_terms
.contains(n
)) {
771 d_info
[n
] = new TheorySetsTermInfo(d_context
);
774 if(n
.getKind() == kind::UNION
||
775 n
.getKind() == kind::INTERSECTION
||
776 n
.getKind() == kind::SETMINUS
||
777 n
.getKind() == kind::SET_SINGLETON
) {
779 for(unsigned i
= 0; i
< numChild
; ++i
) {
780 if(d_terms
.contains(n
[i
])) {
781 Debug("sets-parent") << "Adding " << n
<< " to parent list of "
782 << n
[i
] << std::endl
;
783 d_info
[n
[i
]]->parents
->push_back(n
);
790 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
791 (CDTNodeList
* l
, TNode S
, bool polarity
)
793 for(typeof(l
->begin()) i
= l
->begin(); i
!= l
->end(); ++i
) {
794 Debug("sets-prop") << "[sets-terminfo] setterm todo: "
795 << IN(*i
, d_eqEngine
->getRepresentative(S
))
798 d_eqEngine
->addTerm(IN(d_eqEngine
->getRepresentative(*i
),
799 d_eqEngine
->getRepresentative(S
)));
801 for(eq::EqClassIterator
j(d_eqEngine
->getRepresentative(S
), d_eqEngine
);
802 !j
.isFinished(); ++j
) {
806 Node cur_atom
= IN(x
, S
);
808 // propagation : empty set
809 if(polarity
&& S
.getKind() == kind::EMPTYSET
) {
810 Debug("sets-prop") << "[sets-prop] something in empty set? conflict."
812 d_theory
.learnLiteral(cur_atom
, false, cur_atom
);
814 }// propagation: empty set
816 // propagation : children
817 if(S
.getKind() == kind::UNION
||
818 S
.getKind() == kind::INTERSECTION
||
819 S
.getKind() == kind::SETMINUS
||
820 S
.getKind() == kind::SET_SINGLETON
) {
821 d_theory
.d_settermPropagationQueue
.push_back(std::make_pair(x
, S
));
822 }// propagation: children
824 // propagation : parents
825 const CDTNodeList
* parentList
= getParents(S
);
826 for(typeof(parentList
->begin()) k
= parentList
->begin();
827 k
!= parentList
->end(); ++k
) {
828 d_theory
.d_settermPropagationQueue
.push_back(std::make_pair(x
, *k
));
829 }// propagation : parents
838 void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a
, TNode b
) {
841 if(!a
.getType().isSet()) return;
843 Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
844 << ", b = " << b
<< std::endl
;
845 Debug("sets-terminfo") << "[sets-terminfo] reps"
846 << ", a: " << d_eqEngine
->getRepresentative(a
)
847 << ", b: " << d_eqEngine
->getRepresentative(b
)
850 typeof(d_info
.begin()) ita
= d_info
.find(a
);
851 typeof(d_info
.begin()) itb
= d_info
.find(b
);
853 Assert(ita
!= d_info
.end());
854 Assert(itb
!= d_info
.end());
856 pushToSettermPropagationQueue( (*ita
).second
->elementsInThisSet
, b
, true );
857 pushToSettermPropagationQueue( (*ita
).second
->elementsNotInThisSet
, b
, false );
858 pushToSettermPropagationQueue( (*itb
).second
->elementsNotInThisSet
, a
, false );
859 pushToSettermPropagationQueue( (*itb
).second
->elementsInThisSet
, a
, true );
861 mergeLists((*ita
).second
->elementsInThisSet
,
862 (*itb
).second
->elementsInThisSet
);
864 mergeLists((*ita
).second
->elementsNotInThisSet
,
865 (*itb
).second
->elementsNotInThisSet
);
869 }/* CVC4::theory::sets namespace */
870 }/* CVC4::theory namespace */
871 }/* CVC4 namespace */