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 <boost/foreach.hpp>
19 #include "theory/theory_model.h"
20 #include "theory/sets/theory_sets.h"
21 #include "theory/sets/theory_sets_private.h"
23 #include "theory/sets/options.h"
24 #include "theory/sets/expr_patterns.h" // ONLY included here
26 #include "util/emptyset.h"
27 #include "util/result.h"
30 using namespace CVC4::expr::pattern
;
36 const char* element_of_str
= " \u2208 ";
38 /**************************** TheorySetsPrivate *****************************/
39 /**************************** TheorySetsPrivate *****************************/
40 /**************************** TheorySetsPrivate *****************************/
42 void TheorySetsPrivate::check(Theory::Effort level
) {
44 CodeTimer
checkCodeTimer(d_statistics
.d_checkTime
);
46 while(!d_external
.done() && !d_conflict
) {
47 // Get all the assertions
48 Assertion assertion
= d_external
.get();
49 TNode fact
= assertion
.assertion
;
51 Debug("sets") << "\n\n[sets] TheorySetsPrivate::check(): processing "
54 bool polarity
= fact
.getKind() != kind::NOT
;
55 TNode atom
= polarity
? fact
: fact
[0];
57 if (!assertion
.isPreregistered
) {
58 if (atom
.getKind() == kind::EQUAL
) {
59 if (!d_equalityEngine
.hasTerm(atom
[0])) {
60 Assert(atom
[0].isConst());
61 d_equalityEngine
.addTerm(atom
[0]);
63 if (!d_equalityEngine
.hasTerm(atom
[1])) {
64 Assert(atom
[1].isConst());
65 d_equalityEngine
.addTerm(atom
[1]);
71 switch(atom
.getKind()) {
73 Debug("sets") << atom
[0] << " should " << (polarity
? "":"NOT ")
74 << "be equal to " << atom
[1] << std::endl
;
75 assertEquality(fact
, fact
, /* learnt = */ false);
79 Debug("sets") << atom
[0] << " should " << (polarity
? "":"NOT ")
80 << "be in " << atom
[1] << std::endl
;
81 assertMemebership(fact
, fact
, /* learnt = */ false);
85 Unhandled(fact
.getKind());
89 Debug("sets") << "[sets] in conflict = " << d_conflict
<< std::endl
;
90 Assert( d_conflict
^ d_equalityEngine
.consistent() );
91 if(d_conflict
) return;
92 Debug("sets") << "[sets] is complete = " << isComplete() << std::endl
;
95 if( (Theory::EFFORT_FULL
|| options::setsEagerLemmas() ) && !isComplete()) {
96 d_external
.d_out
->lemma(getLemma());
100 }/* TheorySetsPrivate::check() */
103 void TheorySetsPrivate::assertEquality(TNode fact
, TNode reason
, bool learnt
)
105 Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
107 << ", " << learnt
<< std::endl
;
109 bool polarity
= fact
.getKind() != kind::NOT
;
110 TNode atom
= polarity
? fact
: fact
[0];
112 // fact already holds
113 if( holds(atom
, polarity
) ) {
114 Debug("sets-assert") << "[sets-assert] already present, skipping" << std::endl
;
118 // assert fact & check for conflict
120 registerReason(reason
, /*save=*/ true);
122 d_equalityEngine
.assertEquality(atom
, polarity
, reason
);
124 if(!d_equalityEngine
.consistent()) {
125 Debug("sets-assert") << "[sets-assert] running into a conflict" << std::endl
;
130 if(!polarity
&& atom
[0].getType().isSet()) {
134 }/* TheorySetsPrivate::assertEquality() */
137 void TheorySetsPrivate::assertMemebership(TNode fact
, TNode reason
, bool learnt
)
139 Debug("sets-assert") << "\n[sets-assert] adding membership: " << fact
141 << ", " << learnt
<< std::endl
;
143 bool polarity
= fact
.getKind() == kind::NOT
? false : true;
144 TNode atom
= polarity
? fact
: fact
[0];
146 // fact already holds
147 if( holds(atom
, polarity
) ) {
148 Debug("sets-assert") << "[sets-assert] already present, skipping" << std::endl
;
152 // assert fact & check for conflict
154 registerReason(reason
, true);
156 d_equalityEngine
.assertPredicate(atom
, polarity
, reason
);
158 if(!d_equalityEngine
.consistent()) {
159 Debug("sets-assert") << "[sets-assert] running into a conflict" << std::endl
;
164 // update term info data structures
165 d_termInfoManager
->notifyMembership(fact
);
168 TNode x
= d_equalityEngine
.getRepresentative(atom
[0]);
169 eq::EqClassIterator
j(d_equalityEngine
.getRepresentative(atom
[1]),
172 Node cur_atom
= MEMBER(x
, S
);
175 * It is sufficient to do emptyset propagation outside the loop as
176 * constant term is guaranteed to be class representative.
178 if(polarity
&& S
.getKind() == kind::EMPTYSET
) {
179 Debug("sets-prop") << "[sets-prop] something in empty set? conflict."
181 learnLiteral(cur_atom
, false, cur_atom
);
186 for(; !j
.isFinished(); ++j
) {
188 Node cur_atom
= MEMBER(x
, S
);
190 // propagation : children
191 Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
192 << x
<< element_of_str
<< S
<< std::endl
;
193 if(S
.getKind() == kind::UNION
||
194 S
.getKind() == kind::INTERSECTION
||
195 S
.getKind() == kind::SETMINUS
||
196 S
.getKind() == kind::SET_SINGLETON
) {
197 doSettermPropagation(x
, S
);
198 if(d_conflict
) return;
199 }// propagation: children
202 // propagation : parents
203 Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
204 << x
<< element_of_str
<< S
<< std::endl
;
205 const CDTNodeList
* parentList
= d_termInfoManager
->getParents(S
);
206 for(typeof(parentList
->begin()) k
= parentList
->begin();
207 k
!= parentList
->end(); ++k
) {
208 doSettermPropagation(x
, *k
);
209 if(d_conflict
) return;
210 }// propagation : parents
215 }/* TheorySetsPrivate::assertMemebership() */
218 void TheorySetsPrivate::doSettermPropagation(TNode x
, TNode S
)
220 Debug("sets-prop") << "[sets-prop] doSettermPropagation("
221 << x
<< ", " << S
<< std::endl
;
223 Assert(S
.getType().isSet() && S
.getType().getSetElementType() == x
.getType());
225 Node literal
, left_literal
, right_literal
;
227 // axiom: literal <=> left_literal AND right_literal
228 switch(S
.getKind()) {
229 case kind::INTERSECTION
:
230 literal
= MEMBER(x
, S
) ;
231 left_literal
= MEMBER(x
, S
[0]) ;
232 right_literal
= MEMBER(x
, S
[1]) ;
235 literal
= NOT( MEMBER(x
, S
) );
236 left_literal
= NOT( MEMBER(x
, S
[0]) );
237 right_literal
= NOT( MEMBER(x
, S
[1]) );
240 literal
= MEMBER(x
, S
) ;
241 left_literal
= MEMBER(x
, S
[0]) ;
242 right_literal
= NOT( MEMBER(x
, S
[1]) );
244 case kind::SET_SINGLETON
: {
245 Node atom
= MEMBER(x
, S
);
246 if(holds(atom
, true)) {
247 learnLiteral(EQUAL(x
, S
[0]), true, atom
);
248 } else if(holds(atom
, false)) {
249 learnLiteral(EQUAL(x
, S
[0]), false, NOT(atom
));
257 Debug("sets-prop-details")
258 << "[sets-prop-details] " << literal
<< " IFF " << left_literal
259 << " AND " << right_literal
<< std::endl
;
261 Debug("sets-prop-details")
262 << "[sets-prop-details] "
263 << (holds(literal
) ? "yes" : (holds(literal
.negate()) ? " no" : " _ "))
265 << (holds(left_literal
) ? "yes" : (holds(left_literal
.negate()) ? "no " : " _ "))
267 << (holds(right_literal
) ? "yes" : (holds(right_literal
.negate()) ? "no " : " _ "))
270 Assert( present( MEMBER(x
, S
) ) ||
271 present( MEMBER(x
, S
[0]) ) ||
272 present( MEMBER(x
, S
[1]) ) );
274 if( holds(literal
) ) {
275 // 1a. literal => left_literal
276 Debug("sets-prop") << "[sets-prop] ... via case 1a. ..." << std::endl
;
277 learnLiteral(left_literal
, literal
);
278 if(d_conflict
) return;
280 // 1b. literal => right_literal
281 Debug("sets-prop") << "[sets-prop] ... via case 1b. ..." << std::endl
;
282 learnLiteral(right_literal
, literal
);
283 if(d_conflict
) return;
285 // subsumption requirement met, exit
288 else if( holds(literal
.negate() ) ) {
289 // 4. neg(literal), left_literal => neg(right_literal)
290 if( holds(left_literal
) ) {
291 Debug("sets-prop") << "[sets-prop] ... via case 4. ..." << std::endl
;
292 learnLiteral(right_literal
.negate(), AND( literal
.negate(),
294 if(d_conflict
) return;
297 // 5. neg(literal), right_literal => neg(left_literal)
298 if( holds(right_literal
) ) {
299 Debug("sets-prop") << "[sets-prop] ... via case 5. ..." << std::endl
;
300 learnLiteral(left_literal
.negate(), AND( literal
.negate(),
302 if(d_conflict
) return;
306 // 2,3. neg(left_literal) v neg(right_literal) => neg(literal)
307 if(holds(left_literal
.negate())) {
308 Debug("sets-prop") << "[sets-prop] ... via case 2. ..." << std::endl
;
309 learnLiteral(literal
.negate(), left_literal
.negate());
310 if(d_conflict
) return;
312 else if(holds(right_literal
.negate())) {
313 Debug("sets-prop") << "[sets-prop] ... via case 3. ..." << std::endl
;
314 learnLiteral(literal
.negate(), right_literal
.negate());
315 if(d_conflict
) return;
318 // 6. the axiom itself:
319 else if(holds(left_literal
) && holds(right_literal
)) {
320 Debug("sets-prop") << "[sets-prop] ... via case 6. ..." << std::endl
;
321 learnLiteral(literal
, AND(left_literal
, right_literal
) );
322 if(d_conflict
) return;
326 // check fulfilling rule
328 switch(S
.getKind()) {
330 if( holds(MEMBER(x
, S
)) &&
331 !present( MEMBER(x
, S
[0]) ) )
332 addToPending( MEMBER(x
, S
[0]) );
334 case kind::SETMINUS
: // intentional fallthrough
335 case kind::INTERSECTION
:
336 if( holds(MEMBER(x
, S
[0])) &&
337 !present( MEMBER(x
, S
[1]) ))
338 addToPending( MEMBER(x
, S
[1]) );
341 Assert(false, "MembershipEngine::doSettermPropagation");
346 void TheorySetsPrivate::learnLiteral(TNode atom
, bool polarity
, Node reason
) {
347 Debug("sets-learn") << "[sets-learn] learnLiteral(" << atom
348 << ", " << polarity
<< ")" << std::endl
;
350 if( holds(atom
, polarity
) ) {
351 Debug("sets-learn") << "[sets-learn] \u2514 already known, skipping" << std::endl
;
355 if( holds(atom
, !polarity
) ) {
356 Debug("sets-learn") << "[sets-learn] \u2514 conflict found" << std::endl
;
358 registerReason(reason
, /*save=*/ true);
360 if(atom
.getKind() == kind::EQUAL
) {
361 d_equalityEngine
.assertEquality(atom
, polarity
, reason
);
363 d_equalityEngine
.assertPredicate(atom
, polarity
, reason
);
365 Assert(d_conflict
); // should be marked due to equality engine
369 Assert(atom
.getKind() == kind::EQUAL
|| atom
.getKind() == kind::MEMBER
);
371 Node learnt_literal
= polarity
? Node(atom
) : NOT(atom
);
372 d_propagationQueue
.push_back( make_pair(learnt_literal
, reason
) );
373 }/*TheorySetsPrivate::learnLiteral(...)*/
376 /******************** Model generation ********************/
377 /******************** Model generation ********************/
378 /******************** Model generation ********************/
380 const TheorySetsPrivate::Elements
& TheorySetsPrivate::getElements
381 (TNode setterm
, SettermElementsMap
& settermElementsMap
) const {
382 SettermElementsMap::const_iterator it
= settermElementsMap
.find(setterm
);
383 bool alreadyCalculated
= (it
!= settermElementsMap
.end());
384 if( !alreadyCalculated
) {
386 Kind k
= setterm
.getKind();
387 unsigned numChildren
= setterm
.getNumChildren();
389 if(numChildren
== 2) {
390 const Elements
& left
= getElements(setterm
[0], settermElementsMap
);
391 const Elements
& right
= getElements(setterm
[1], settermElementsMap
);
394 if(left
.size() >= right
.size()) {
395 cur
= left
; cur
.insert(right
.begin(), right
.end());
397 cur
= right
; cur
.insert(left
.begin(), left
.end());
400 case kind::INTERSECTION
:
401 std::set_intersection(left
.begin(), left
.end(), right
.begin(), right
.end(),
402 std::inserter(cur
, cur
.begin()) );
405 std::set_difference(left
.begin(), left
.end(), right
.begin(), right
.end(),
406 std::inserter(cur
, cur
.begin()) );
412 Assert(k
== kind::VARIABLE
|| k
== kind::APPLY_UF
);
413 /* assign emptyset, which is default */
416 it
= settermElementsMap
.insert(SettermElementsMap::value_type(setterm
, cur
)).first
;
423 void TheorySetsPrivate::checkModel(const SettermElementsMap
& settermElementsMap
, TNode S
) const {
425 Debug("sets-model") << "[sets-model] checkModel(..., " << S
<< "): "
428 Assert(S
.getType().isSet());
430 Elements emptySetOfElements
;
431 const Elements
& saved
=
432 d_equalityEngine
.getRepresentative(S
).getKind() == kind::EMPTYSET
?
434 settermElementsMap
.find(d_equalityEngine
.getRepresentative(S
))->second
;
435 Debug("sets-model") << "[sets-model] saved : { ";
436 BOOST_FOREACH(TNode element
, saved
) { Debug("sets-model") << element
<< ", "; }
437 Debug("sets-model") << " }" << std::endl
;
439 if(S
.getNumChildren() == 2) {
441 Elements cur
, left
, right
;
442 left
= settermElementsMap
.find(d_equalityEngine
.getRepresentative(S
[0]))->second
;
443 right
= settermElementsMap
.find(d_equalityEngine
.getRepresentative(S
[1]))->second
;
444 switch(S
.getKind()) {
446 if(left
.size() >= right
.size()) {
447 cur
= left
; cur
.insert(right
.begin(), right
.end());
449 cur
= right
; cur
.insert(left
.begin(), left
.end());
452 case kind::INTERSECTION
:
453 std::set_intersection(left
.begin(), left
.end(), right
.begin(), right
.end(),
454 std::inserter(cur
, cur
.begin()) );
457 std::set_difference(left
.begin(), left
.end(), right
.begin(), right
.end(),
458 std::inserter(cur
, cur
.begin()) );
464 Debug("sets-model") << "[sets-model] cur : { ";
465 BOOST_FOREACH(TNode element
, cur
) { Debug("sets-model") << element
<< ", "; }
466 Debug("sets-model") << " }" << std::endl
;
469 Debug("sets-model") << "[sets-model] *** ERRROR *** cur != saved "
471 Debug("sets-model") << "[sets-model] FYI: "
472 << " [" << S
<< "] = " << d_equalityEngine
.getRepresentative(S
) << ", "
473 << " [" << S
[0] << "] = " << d_equalityEngine
.getRepresentative(S
[0]) << ", "
474 << " [" << S
[1] << "] = " << d_equalityEngine
.getRepresentative(S
[1]) << "\n";
477 Assert( saved
== cur
);
481 Node
TheorySetsPrivate::elementsToShape(Elements elements
, TypeNode setType
) const
483 NodeManager
* nm
= NodeManager::currentNM();
485 if(elements
.size() == 0) {
486 return nm
->mkConst(EmptySet(nm
->toType(setType
)));
488 Elements::iterator it
= elements
.begin();
489 Node cur
= SET_SINGLETON(*it
);
490 while( ++it
!= elements
.end() ) {
491 cur
= nm
->mkNode(kind::UNION
, cur
, SET_SINGLETON(*it
));
497 void TheorySetsPrivate::collectModelInfo(TheoryModel
* m
, bool fullModel
)
499 Debug("sets-model") << "[sets-model] collectModelInfo(..., fullModel="
500 << (fullModel
? "true)" : "false)") << std::endl
;
504 // Compute terms appearing assertions and shared terms
505 d_external
.computeRelevantTerms(terms
);
507 // Compute for each setterm elements that it contains
508 SettermElementsMap settermElementsMap
;
509 TNode true_atom
= NodeManager::currentNM()->mkConst
<bool>(true);
510 TNode false_atom
= NodeManager::currentNM()->mkConst
<bool>(false);
511 for(eq::EqClassIterator
it_eqclasses(true_atom
, &d_equalityEngine
);
512 ! it_eqclasses
.isFinished() ; ++it_eqclasses
) {
513 TNode n
= (*it_eqclasses
);
514 if(n
.getKind() == kind::MEMBER
) {
515 Assert(d_equalityEngine
.areEqual(n
, true_atom
));
516 TNode x
= d_equalityEngine
.getRepresentative(n
[0]);
517 TNode S
= d_equalityEngine
.getRepresentative(n
[1]);
518 settermElementsMap
[S
].insert(x
);
522 // Assert equalities and disequalities to the model
523 m
->assertEqualityEngine(&d_equalityEngine
, &terms
);
525 // Loop over terms to collect set-terms for which we generate models
526 set
<Node
> settermsModEq
;
527 BOOST_FOREACH(TNode term
, terms
) {
528 TNode n
= term
.getKind() == kind::NOT
? term
[0] : term
;
530 Debug("sets-model-details") << "[sets-model-details] > " << n
<< std::endl
;
532 if(n
.getType().isSet()) {
533 n
= d_equalityEngine
.getRepresentative(n
);
535 settermsModEq
.insert(n
);
541 if(Debug
.isOn("sets-model")) {
542 BOOST_FOREACH( TNode node
, settermsModEq
) {
543 Debug("sets-model") << "[sets-model] " << node
<< std::endl
;
547 BOOST_FOREACH( SettermElementsMap::value_type
&it
, settermElementsMap
) {
548 BOOST_FOREACH( TNode element
, it
.second
/* elements */ ) {
549 Debug("sets-model-details") << "[sets-model-details] > " <<
550 (it
.first
/* setterm */) << ": " << element
<< std::endl
;
554 // assign representatives to equivalence class
555 BOOST_FOREACH( TNode setterm
, settermsModEq
) {
556 Elements elements
= getElements(setterm
, settermElementsMap
);
557 Node shape
= elementsToShape(elements
, setterm
.getType());
558 m
->assertEquality(shape
, setterm
, true);
559 m
->assertRepresentative(shape
);
562 #ifdef CVC4_ASSERTIONS
563 BOOST_FOREACH(TNode term
, terms
) {
564 if( term
.getType().isSet() ) {
565 checkModel(settermElementsMap
, term
);
572 /********************** Helper functions ***************************/
573 /********************** Helper functions ***************************/
574 /********************** Helper functions ***************************/
576 Node
mkAnd(const std::vector
<TNode
>& conjunctions
) {
577 Assert(conjunctions
.size() > 0);
581 for (unsigned i
= 0; i
< conjunctions
.size(); ++i
) {
582 TNode t
= conjunctions
[i
];
584 if (t
.getKind() == kind::AND
) {
585 for(TNode::iterator child_it
= t
.begin();
586 child_it
!= t
.end(); ++child_it
) {
587 Assert((*child_it
).getKind() != kind::AND
);
588 all
.insert(*child_it
);
597 Assert(all
.size() > 0);
599 if (all
.size() == 1) {
600 // All the same, or just one
601 return conjunctions
[0];
604 NodeBuilder
<> conjunction(kind::AND
);
605 std::set
<TNode
>::const_iterator it
= all
.begin();
606 std::set
<TNode
>::const_iterator it_end
= all
.end();
607 while (it
!= it_end
) {
616 TheorySetsPrivate::Statistics::Statistics() :
617 d_checkTime("theory::sets::time") {
619 StatisticsRegistry::registerStat(&d_checkTime
);
623 TheorySetsPrivate::Statistics::~Statistics() {
624 StatisticsRegistry::unregisterStat(&d_checkTime
);
628 bool TheorySetsPrivate::present(TNode atom
) {
629 return holds(atom
) || holds(atom
.notNode());
633 bool TheorySetsPrivate::holds(TNode atom
, bool polarity
) {
634 Node polarity_atom
= NodeManager::currentNM()->mkConst
<bool>(polarity
);
636 Node atomModEq
= NodeManager::currentNM()->mkNode
637 (atom
.getKind(), d_equalityEngine
.getRepresentative(atom
[0]),
638 d_equalityEngine
.getRepresentative(atom
[1]) );
640 d_equalityEngine
.addTerm(atomModEq
);
642 return d_equalityEngine
.areEqual(atomModEq
, polarity_atom
);
646 void TheorySetsPrivate::registerReason(TNode reason
, bool save
)
648 if(save
) d_nodeSaver
.insert(reason
);
650 if(reason
.getKind() == kind::AND
) {
651 Assert(reason
.getNumChildren() == 2);
652 registerReason(reason
[0], false);
653 registerReason(reason
[1], false);
654 } else if(reason
.getKind() == kind::NOT
) {
655 registerReason(reason
[0], false);
656 } else if(reason
.getKind() == kind::MEMBER
) {
657 d_equalityEngine
.addTerm(reason
);
658 Assert(present(reason
));
659 } else if(reason
.getKind() == kind::EQUAL
) {
660 d_equalityEngine
.addTerm(reason
);
661 Assert(present(reason
));
662 } else if(reason
.getKind() == kind::CONST_BOOLEAN
) {
663 // That's OK, already in EqEngine
669 void TheorySetsPrivate::finishPropagation()
671 while(!d_conflict
&& !d_settermPropagationQueue
.empty()) {
672 std::pair
<TNode
,TNode
> np
= d_settermPropagationQueue
.front();
673 d_settermPropagationQueue
.pop();
674 doSettermPropagation(np
.first
, np
.second
);
676 while(!d_conflict
&& !d_propagationQueue
.empty()) {
677 std::pair
<Node
,Node
> np
= d_propagationQueue
.front();
678 d_propagationQueue
.pop();
679 TNode atom
= np
.first
.getKind() == kind::NOT
? np
.first
[0] : np
.first
;
680 if(atom
.getKind() == kind::MEMBER
) {
681 assertMemebership(np
.first
, np
.second
, /* learnt = */ true);
683 assertEquality(np
.first
, np
.second
, /* learnt = */ true);
688 void TheorySetsPrivate::addToPending(Node n
) {
689 Debug("sets-pending") << "[sets-pending] addToPending " << n
<< std::endl
;
690 if(d_pendingEverInserted
.find(n
) == d_pendingEverInserted
.end()) {
691 if(n
.getKind() == kind::MEMBER
) {
692 Debug("sets-pending") << "[sets-pending] \u2514 added to member queue"
696 Debug("sets-pending") << "[sets-pending] \u2514 added to equality queue"
698 Assert(n
.getKind() == kind::EQUAL
);
699 d_pendingDisequal
.push(n
);
704 bool TheorySetsPrivate::isComplete() {
705 while(!d_pending
.empty() && present(d_pending
.front())) {
706 Debug("sets-pending") << "[sets-pending] removing as already present: "
707 << d_pending
.front() << std::endl
;
710 return d_pending
.empty() && d_pendingDisequal
.empty();
713 Node
TheorySetsPrivate::getLemma() {
714 Assert(!d_pending
.empty() || !d_pendingDisequal
.empty());
718 if(!d_pending
.empty()) {
719 Node n
= d_pending
.front();
721 d_pendingEverInserted
.insert(n
);
724 Assert(n
.getKind() == kind::MEMBER
);
726 lemma
= OR(n
, NOT(n
));
728 Node n
= d_pendingDisequal
.front();
729 d_pendingDisequal
.pop();
730 d_pendingEverInserted
.insert(n
);
732 Assert(n
.getKind() == kind::EQUAL
&& n
[0].getType().isSet());
733 Node x
= NodeManager::currentNM()->mkSkolem("sde_$$", n
[0].getType().getSetElementType());
734 Node l1
= MEMBER(x
, n
[0]), l2
= MEMBER(x
, n
[1]);
736 lemma
= OR(n
, AND(l1
, NOT(l2
)), AND(NOT(l1
), l2
));
739 Debug("sets-lemma") << "[sets-lemma] " << lemma
<< std::endl
;
745 TheorySetsPrivate::TheorySetsPrivate(TheorySets
& external
,
747 context::UserContext
* u
):
748 d_external(external
),
750 d_equalityEngine(d_notify
, c
, "theory::sets::TheorySetsPrivate"),
752 d_termInfoManager(NULL
),
753 d_propagationQueue(c
),
754 d_settermPropagationQueue(c
),
757 d_pendingDisequal(u
),
758 d_pendingEverInserted(u
)
760 d_termInfoManager
= new TermInfoManager(*this, c
, &d_equalityEngine
);
762 d_equalityEngine
.addFunctionKind(kind::UNION
);
763 d_equalityEngine
.addFunctionKind(kind::INTERSECTION
);
764 d_equalityEngine
.addFunctionKind(kind::SETMINUS
);
766 d_equalityEngine
.addFunctionKind(kind::MEMBER
);
767 d_equalityEngine
.addFunctionKind(kind::SUBSET
);
768 }/* TheorySetsPrivate::TheorySetsPrivate() */
771 TheorySetsPrivate::~TheorySetsPrivate()
773 delete d_termInfoManager
;
777 bool TheorySetsPrivate::propagate(TNode literal
) {
778 Debug("sets-prop") << " propagate(" << literal
<< ")" << std::endl
;
780 // If already in conflict, no more propagation
782 Debug("sets-prop") << "TheoryUF::propagate(" << literal
<< "): already in conflict" << std::endl
;
787 bool ok
= d_external
.d_out
->propagate(literal
);
793 }/* TheorySetsPropagate::propagate(TNode) */
796 void TheorySetsPrivate::addSharedTerm(TNode n
) {
797 Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n
<< ")" << std::endl
;
798 d_equalityEngine
.addTriggerTerm(n
, THEORY_SETS
);
801 void TheorySetsPrivate::conflict(TNode a
, TNode b
)
803 if (a
.getKind() == kind::CONST_BOOLEAN
) {
804 d_conflictNode
= explain(a
.iffNode(b
));
806 d_conflictNode
= explain(a
.eqNode(b
));
808 d_external
.d_out
->conflict(d_conflictNode
);
809 Debug("sets") << "[sets] conflict: " << a
<< " iff " << b
810 << ", explaination " << d_conflictNode
<< std::endl
;
814 Node
TheorySetsPrivate::explain(TNode literal
)
816 Debug("sets") << "TheorySetsPrivate::explain(" << literal
<< ")"
819 bool polarity
= literal
.getKind() != kind::NOT
;
820 TNode atom
= polarity
? literal
: literal
[0];
821 std::vector
<TNode
> assumptions
;
823 if(atom
.getKind() == kind::EQUAL
|| atom
.getKind() == kind::IFF
) {
824 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
825 } else if(atom
.getKind() == kind::MEMBER
) {
826 if( !d_equalityEngine
.hasTerm(atom
)) {
827 d_equalityEngine
.addTerm(atom
);
829 d_equalityEngine
.explainPredicate(atom
, polarity
, assumptions
);
831 Debug("sets") << "unhandled: " << literal
<< "; (" << atom
<< ", "
832 << polarity
<< "); kind" << atom
.getKind() << std::endl
;
836 return mkAnd(assumptions
);
839 void TheorySetsPrivate::preRegisterTerm(TNode node
)
841 Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node
<< ")"
844 switch(node
.getKind()) {
846 // TODO: what's the point of this
847 d_equalityEngine
.addTriggerEquality(node
);
850 // TODO: what's the point of this
851 d_equalityEngine
.addTriggerPredicate(node
);
854 d_termInfoManager
->addTerm(node
);
855 d_equalityEngine
.addTriggerTerm(node
, THEORY_SETS
);
856 // d_equalityEngine.addTerm(node);
858 if(node
.getKind() == kind::SET_SINGLETON
) {
859 Node true_node
= NodeManager::currentNM()->mkConst
<bool>(true);
860 learnLiteral(MEMBER(node
[0], node
), true, true_node
);
861 //intentional fallthrough
867 /**************************** eq::NotifyClass *****************************/
868 /**************************** eq::NotifyClass *****************************/
869 /**************************** eq::NotifyClass *****************************/
872 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality
, bool value
)
874 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
875 << " value = " << value
<< std::endl
;
877 return d_theory
.propagate(equality
);
879 // We use only literal triggers so taking not is safe
880 return d_theory
.propagate(equality
.notNode());
884 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate
, bool value
)
886 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
887 << " value = " << value
<< std::endl
;
889 return d_theory
.propagate(predicate
);
891 return d_theory
.propagate(predicate
.notNode());
895 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
)
897 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
898 << " t1 = " << t1
<< " t2 = " << t2
<< " value = " << value
<< std::endl
;
900 d_theory
.d_termInfoManager
->mergeTerms(t1
, t2
);
905 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1
, TNode t2
)
907 Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1
<< " t2 = " << t2
<< std::endl
;
908 d_theory
.conflict(t1
, t2
);
911 // void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
913 // Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
916 // void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
918 // Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
921 // void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
923 // Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
926 // void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
928 // Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
932 /**************************** TermInfoManager *****************************/
933 /**************************** TermInfoManager *****************************/
934 /**************************** TermInfoManager *****************************/
936 void TheorySetsPrivate::TermInfoManager::mergeLists
937 (CDTNodeList
* la
, const CDTNodeList
* lb
) const {
938 // straight from theory/arrays/array_info.cpp
939 std::set
<TNode
> temp
;
940 CDTNodeList::const_iterator it
;
941 for(it
= la
->begin() ; it
!= la
->end(); it
++ ) {
945 for(it
= lb
->begin() ; it
!= lb
->end(); it
++ ) {
946 if(temp
.count(*it
) == 0) {
952 TheorySetsPrivate::TermInfoManager::TermInfoManager
953 (TheorySetsPrivate
& theory
, context::Context
* satContext
, eq::EqualityEngine
* eq
):
955 d_context(satContext
),
961 TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
962 for( typeof(d_info
.begin()) it
= d_info
.begin();
963 it
!= d_info
.end(); ++it
) {
968 void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact
) {
969 bool polarity
= fact
.getKind() != kind::NOT
;
970 TNode atom
= polarity
? fact
: fact
[0];
972 TNode x
= d_eqEngine
->getRepresentative(atom
[0]);
973 TNode S
= d_eqEngine
->getRepresentative(atom
[1]);
975 Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
976 << " in " << S
<< " " << polarity
<< std::endl
;
978 d_info
[S
]->addToElementList(x
, polarity
);
981 const CDTNodeList
* TheorySetsPrivate::TermInfoManager::getParents(TNode x
) {
982 return d_info
[x
]->parents
;
985 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n
) {
986 unsigned numChild
= n
.getNumChildren();
988 if(!d_terms
.contains(n
)) {
990 d_info
[n
] = new TheorySetsTermInfo(d_context
);
993 if(n
.getKind() == kind::UNION
||
994 n
.getKind() == kind::INTERSECTION
||
995 n
.getKind() == kind::SETMINUS
||
996 n
.getKind() == kind::SET_SINGLETON
) {
998 for(unsigned i
= 0; i
< numChild
; ++i
) {
999 if(d_terms
.contains(n
[i
])) {
1000 Debug("sets-parent") << "Adding " << n
<< " to parent list of "
1001 << n
[i
] << std::endl
;
1002 d_info
[n
[i
]]->parents
->push_back(n
);
1009 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1010 (CDTNodeList
* l
, TNode S
, bool polarity
)
1012 for(typeof(l
->begin()) i
= l
->begin(); i
!= l
->end(); ++i
) {
1013 Debug("sets-prop") << "[sets-terminfo] setterm todo: "
1014 << MEMBER(*i
, d_eqEngine
->getRepresentative(S
))
1017 d_eqEngine
->addTerm(MEMBER(d_eqEngine
->getRepresentative(*i
),
1018 d_eqEngine
->getRepresentative(S
)));
1020 for(eq::EqClassIterator
j(d_eqEngine
->getRepresentative(S
), d_eqEngine
);
1021 !j
.isFinished(); ++j
) {
1025 Node cur_atom
= MEMBER(x
, S
);
1027 // propagation : empty set
1028 if(polarity
&& S
.getKind() == kind::EMPTYSET
) {
1029 Debug("sets-prop") << "[sets-prop] something in empty set? conflict."
1031 d_theory
.learnLiteral(cur_atom
, false, cur_atom
);
1033 }// propagation: empty set
1035 // propagation : children
1036 if(S
.getKind() == kind::UNION
||
1037 S
.getKind() == kind::INTERSECTION
||
1038 S
.getKind() == kind::SETMINUS
||
1039 S
.getKind() == kind::SET_SINGLETON
) {
1040 d_theory
.d_settermPropagationQueue
.push_back(std::make_pair(x
, S
));
1041 }// propagation: children
1043 // propagation : parents
1044 const CDTNodeList
* parentList
= getParents(S
);
1045 for(typeof(parentList
->begin()) k
= parentList
->begin();
1046 k
!= parentList
->end(); ++k
) {
1047 d_theory
.d_settermPropagationQueue
.push_back(std::make_pair(x
, *k
));
1048 }// propagation : parents
1057 void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a
, TNode b
) {
1060 if(!a
.getType().isSet()) return;
1062 Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
1063 << ", b = " << b
<< std::endl
;
1064 Debug("sets-terminfo") << "[sets-terminfo] reps"
1065 << ", a: " << d_eqEngine
->getRepresentative(a
)
1066 << ", b: " << d_eqEngine
->getRepresentative(b
)
1069 typeof(d_info
.begin()) ita
= d_info
.find(a
);
1070 typeof(d_info
.begin()) itb
= d_info
.find(b
);
1072 Assert(ita
!= d_info
.end());
1073 Assert(itb
!= d_info
.end());
1075 pushToSettermPropagationQueue( (*ita
).second
->elementsInThisSet
, b
, true );
1076 pushToSettermPropagationQueue( (*ita
).second
->elementsNotInThisSet
, b
, false );
1077 pushToSettermPropagationQueue( (*itb
).second
->elementsNotInThisSet
, a
, false );
1078 pushToSettermPropagationQueue( (*itb
).second
->elementsInThisSet
, a
, true );
1080 mergeLists((*ita
).second
->elementsInThisSet
,
1081 (*itb
).second
->elementsInThisSet
);
1083 mergeLists((*ita
).second
->elementsNotInThisSet
,
1084 (*itb
).second
->elementsNotInThisSet
);
1088 }/* CVC4::theory::sets namespace */
1089 }/* CVC4::theory namespace */
1090 }/* CVC4 namespace */