projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Sets subtypes (#1095)
[cvc5.git] / src / theory / sets / theory_sets_private.cpp
1 /********************* */
2 /*! \file theory_sets_private.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Kshitij Bansal, Paul Meng
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief Sets theory implementation.
13 **
14 ** Sets theory implementation.
15 **/
16
17 #include <algorithm>
18 #include "theory/sets/theory_sets_private.h"
19
20 #include "expr/emptyset.h"
21 #include "options/sets_options.h"
22 #include "smt/smt_statistics_registry.h"
23 #include "theory/sets/theory_sets.h"
24 #include "theory/sets/normal_form.h"
25 #include "theory/theory_model.h"
26 #include "util/result.h"
27 #include "theory/quantifiers/term_database.h"
28
29 #define AJR_IMPLEMENTATION
30
31 using namespace std;
32
33 namespace CVC4 {
34 namespace theory {
35 namespace sets {
36
37 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
38 context::Context* c,
39 context::UserContext* u):
40 d_rels(NULL),
41 d_members(c),
42 d_deq(c),
43 d_deq_processed(u),
44 d_keep(c),
45 d_proxy(u),
46 d_proxy_to_term(u),
47 d_lemmas_produced(u),
48 d_card_processed(u),
49 d_var_elim(u),
50 d_external(external),
51 d_notify(*this),
52 d_equalityEngine(d_notify, c, "theory::sets::ee", true),
53 d_conflict(c)
54 {
55
56 d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external);
57
58 d_true = NodeManager::currentNM()->mkConst( true );
59 d_false = NodeManager::currentNM()->mkConst( false );
60 d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
61
62 d_equalityEngine.addFunctionKind(kind::SINGLETON);
63 d_equalityEngine.addFunctionKind(kind::UNION);
64 d_equalityEngine.addFunctionKind(kind::INTERSECTION);
65 d_equalityEngine.addFunctionKind(kind::SETMINUS);
66
67 d_equalityEngine.addFunctionKind(kind::MEMBER);
68 d_equalityEngine.addFunctionKind(kind::SUBSET);
69
70 // If cardinality is on.
71 d_equalityEngine.addFunctionKind(kind::CARD);
72
73 d_card_enabled = false;
74 d_rels_enabled = false;
75
76 }/* TheorySetsPrivate::TheorySetsPrivate() */
77
78 TheorySetsPrivate::~TheorySetsPrivate(){
79 delete d_rels;
80 for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) {
81 delete current_pair.second;
82 }
83 }/* TheorySetsPrivate::~TheorySetsPrivate() */
84
85
86 void TheorySetsPrivate::eqNotifyNewClass(TNode t) {
87 if( t.getKind()==kind::SINGLETON || t.getKind()==kind::EMPTYSET ){
88 EqcInfo * e = getOrMakeEqcInfo( t, true );
89 e->d_singleton = t;
90 }
91 if( options::setsRelEager() ){
92 d_rels->eqNotifyNewClass( t );
93 }
94 }
95
96 void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2){
97
98 }
99
100 void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
101 if( !d_conflict ){
102 Trace("sets-prop-debug") << "Merge " << t1 << " and " << t2 << "..." << std::endl;
103 Node s1, s2;
104 EqcInfo * e2 = getOrMakeEqcInfo( t2 );
105 if( e2 ){
106 s2 = e2->d_singleton;
107 EqcInfo * e1 = getOrMakeEqcInfo( t1 );
108 Node s1;
109 Trace("sets-prop-debug") << "Merging singletons..." << std::endl;
110 if( e1 ){
111 s1 = e1->d_singleton;
112 if( !s1.isNull() && !s2.isNull() ){
113 if( s1.getKind()==s2.getKind() ){
114 Trace("sets-prop") << "Propagate eq inference : " << s1 << " == " << s2 << std::endl;
115 //infer equality between elements of singleton
116 Node exp = s1.eqNode( s2 );
117 Node eq = s1[0].eqNode( s2[0] );
118 d_keep.insert( exp );
119 d_keep.insert( eq );
120 assertFact( eq, exp );
121 }else{
122 //singleton equal to emptyset, conflict
123 Trace("sets-prop") << "Propagate conflict : " << s1 << " == " << s2 << std::endl;
124 conflict( s1, s2 );
125 return;
126 }
127 }
128 }else{
129 //copy information
130 e1 = getOrMakeEqcInfo( t1, true );
131 e1->d_singleton.set( e2->d_singleton );
132 }
133 }
134 //merge membership list
135 Trace("sets-prop-debug") << "Copying membership list..." << std::endl;
136 NodeIntMap::iterator mem_i2 = d_members.find( t2 );
137 if( mem_i2 != d_members.end() ) {
138 NodeIntMap::iterator mem_i1 = d_members.find( t1 );
139 int n_members = 0;
140 if( mem_i1 != d_members.end() ) {
141 n_members = (*mem_i1).second;
142 }
143 for( int i=0; i<(*mem_i2).second; i++ ){
144 Assert( i<(int)d_members_data[t2].size() && d_members_data[t2][i].getKind()==kind::MEMBER );
145 Node m2 = d_members_data[t2][i];
146 //check if redundant
147 bool add = true;
148 for( int j=0; j<n_members; j++ ){
149 Assert( j<(int)d_members_data[t1].size() && d_members_data[t1][j].getKind()==kind::MEMBER );
150 if( ee_areEqual( m2[0], d_members_data[t1][j][0] ) ){
151 add = false;
152 break;
153 }
154 }
155 if( add ){
156 if( !s1.isNull() && s2.isNull() ){
157 Assert( m2[1].getType().isComparableTo( s1.getType() ) );
158 Assert( ee_areEqual( m2[1], s1 ) );
159 Node exp = NodeManager::currentNM()->mkNode( kind::AND, m2[1].eqNode( s1 ), m2 );
160 if( s1.getKind()==kind::SINGLETON ){
161 if( s1[0]!=m2[0] ){
162 Node eq = s1[0].eqNode( m2[0] );
163 d_keep.insert( exp );
164 d_keep.insert( eq );
165 Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp << " => " << eq << std::endl;
166 assertFact( eq, exp );
167 }
168 }else{
169 //conflict
170 Trace("sets-prop") << "Propagate eq-mem conflict : " << exp << std::endl;
171 d_conflict = true;
172 d_external.d_out->conflict( exp );
173 return;
174 }
175 }
176 if( n_members<(int)d_members_data[t1].size() ){
177 d_members_data[t1][n_members] = m2;
178 }else{
179 d_members_data[t1].push_back( m2 );
180 }
181 n_members++;
182 }
183 }
184 d_members[t1] = n_members;
185 }
186 if( options::setsRelEager() ){
187 d_rels->eqNotifyPostMerge( t1, t2 );
188 }
189 }
190 }
191
192 void TheorySetsPrivate::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
193 if( t1.getType().isSet() ){
194 Node eq = t1.eqNode( t2 );
195 if( d_deq.find( eq )==d_deq.end() ){
196 d_deq[eq] = true;
197 }
198 }
199 }
200
201 TheorySetsPrivate::EqcInfo::EqcInfo( context::Context* c ) : d_singleton( c ){
202
203 }
204
205 TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo( TNode n, bool doMake ){
206 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
207 if( eqc_i==d_eqc_info.end() ){
208 EqcInfo* ei = NULL;
209 if( doMake ){
210 ei = new EqcInfo( d_external.getSatContext() );
211 d_eqc_info[n] = ei;
212 }
213 return ei;
214 }else{
215 return eqc_i->second;
216 }
217 }
218
219
220 bool TheorySetsPrivate::ee_areEqual( Node a, Node b ) {
221 if( a==b ){
222 return true;
223 }else{
224 if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
225 return d_equalityEngine.areEqual( a, b );
226 }else{
227 return false;
228 }
229 }
230 }
231
232 bool TheorySetsPrivate::ee_areDisequal( Node a, Node b ) {
233 if( a==b ){
234 return false;
235 }else{
236 if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
237 return d_equalityEngine.areDisequal( a, b, false );
238 }else{
239 return a.isConst() && b.isConst();
240 }
241 }
242 }
243
244 bool TheorySetsPrivate::ee_areCareDisequal( Node a, Node b ) {
245 if( d_equalityEngine.isTriggerTerm(a, THEORY_SETS) && d_equalityEngine.isTriggerTerm(b, THEORY_SETS) ){
246 TNode a_shared = d_equalityEngine.getTriggerTermRepresentative(a, THEORY_SETS);
247 TNode b_shared = d_equalityEngine.getTriggerTermRepresentative(b, THEORY_SETS);
248 EqualityStatus eqStatus = d_external.d_valuation.getEqualityStatus(a_shared, b_shared);
249 if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
250 return true;
251 }
252 }
253 return false;
254 }
255
256 bool TheorySetsPrivate::isEntailed( Node n, bool polarity ) {
257 if( n.getKind()==kind::NOT ){
258 return isEntailed( n[0], !polarity );
259 }else if( n.getKind()==kind::EQUAL ){
260 if( polarity ){
261 return ee_areEqual( n[0], n[1] );
262 }else{
263 return ee_areDisequal( n[0], n[1] );
264 }
265 }else if( n.getKind()==kind::MEMBER ){
266 if( ee_areEqual( n, polarity ? d_true : d_false ) ){
267 return true;
268 }
269 //check members cache
270 if( polarity && d_equalityEngine.hasTerm( n[1] ) ){
271 Node r = d_equalityEngine.getRepresentative( n[1] );
272 if( isMember( n[0], r ) ){
273 return true;
274 }
275 }
276 }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
277 bool conj = (n.getKind()==kind::AND)==polarity;
278 for( unsigned i=0; i<n.getNumChildren(); i++ ){
279 bool isEnt = isEntailed( n[i], polarity );
280 if( isEnt!=conj ){
281 return !conj;
282 }
283 }
284 return conj;
285 }else if( n.isConst() ){
286 return ( polarity && n==d_true ) || ( !polarity && n==d_false );
287 }
288 return false;
289 }
290
291 bool TheorySetsPrivate::isMember( Node x, Node s ) {
292 Assert( d_equalityEngine.hasTerm( s ) && d_equalityEngine.getRepresentative( s )==s );
293 NodeIntMap::iterator mem_i = d_members.find( s );
294 if( mem_i != d_members.end() ) {
295 for( int i=0; i<(*mem_i).second; i++ ){
296 if( ee_areEqual( d_members_data[s][i][0], x ) ){
297 return true;
298 }
299 }
300 }
301 return false;
302 }
303
304 bool TheorySetsPrivate::isSetDisequalityEntailed( Node r1, Node r2 ) {
305 Assert( d_equalityEngine.hasTerm( r1 ) && d_equalityEngine.getRepresentative( r1 )==r1 );
306 Assert( d_equalityEngine.hasTerm( r2 ) && d_equalityEngine.getRepresentative( r2 )==r2 );
307 TypeNode tn = r1.getType();
308 Node eqc_es = d_eqc_emptyset[tn];
309 bool is_sat = false;
310 for( unsigned e=0; e<2; e++ ){
311 Node a = e==0 ? r1 : r2;
312 Node b = e==0 ? r2 : r1;
313 //if there are members in a
314 std::map< Node, std::map< Node, Node > >::iterator itpma = d_pol_mems[0].find( a );
315 if( itpma!=d_pol_mems[0].end() ){
316 Assert( !itpma->second.empty() );
317 //if b is empty
318 if( b==eqc_es ){
319 if( !itpma->second.empty() ){
320 is_sat = true;
321 Trace("sets-deq") << "Disequality is satisfied because members are in " << a << " and " << b << " is empty" << std::endl;
322 }else{
323 //a should not be singleton
324 Assert( d_eqc_singleton.find( a )==d_eqc_singleton.end() );
325 }
326 }else{
327 std::map< Node, Node >::iterator itsb = d_eqc_singleton.find( b );
328 std::map< Node, std::map< Node, Node > >::iterator itpmb = d_pol_mems[1].find( b );
329 std::vector< Node > prev;
330 for( std::map< Node, Node >::iterator itm = itpma->second.begin(); itm != itpma->second.end(); ++itm ){
331 //if b is a singleton
332 if( itsb!=d_eqc_singleton.end() ){
333 if( ee_areDisequal( itm->first, itsb->second[0] ) ){
334 Trace("sets-deq") << "Disequality is satisfied because of " << itm->second << ", singleton eq " << itsb->second[0] << std::endl;
335 is_sat = true;
336 }
337 //or disequal with another member
338 for( unsigned k=0; k<prev.size(); k++ ){
339 if( ee_areDisequal( itm->first, prev[k] ) ){
340 Trace("sets-deq") << "Disequality is satisfied because of disequal members " << itm->first << " " << prev[k] << ", singleton eq " << std::endl;
341 is_sat = true;
342 break;
343 }
344 }
345 //TODO: this can be generalized : maintain map to abstract domain ( set -> cardinality )
346 //if a has positive member that is negative member in b
347 }else if( itpmb!=d_pol_mems[1].end() ){
348 for( std::map< Node, Node >::iterator itnm = itpmb->second.begin(); itnm != itpmb->second.end(); ++itnm ){
349 if( ee_areEqual( itm->first, itnm->first ) ){
350 Trace("sets-deq") << "Disequality is satisfied because of " << itm->second << " " << itnm->second << std::endl;
351 is_sat = true;
352 break;
353 }
354 }
355 }
356 if( is_sat ){
357 break;
358 }
359 prev.push_back( itm->first );
360 }
361 }
362 if( is_sat ){
363 break;
364 }
365 }
366 }
367 return is_sat;
368 }
369
370 bool TheorySetsPrivate::assertFact( Node fact, Node exp ){
371 Trace("sets-assert") << "TheorySets::assertFact : " << fact << ", exp = " << exp << std::endl;
372 bool polarity = fact.getKind() != kind::NOT;
373 TNode atom = polarity ? fact : fact[0];
374 if( !isEntailed( atom, polarity ) ){
375 if( atom.getKind()==kind::EQUAL ){
376 d_equalityEngine.assertEquality( atom, polarity, exp );
377 }else{
378 d_equalityEngine.assertPredicate( atom, polarity, exp );
379 }
380 if( !d_conflict ){
381 if( atom.getKind()==kind::MEMBER && polarity ){
382 //check if set has a value, if so, we can propagate
383 Node r = d_equalityEngine.getRepresentative( atom[1] );
384 EqcInfo * e = getOrMakeEqcInfo( r, true );
385 if( e ){
386 Node s = e->d_singleton;
387 if( !s.isNull() ){
388 Node exp = NodeManager::currentNM()->mkNode( kind::AND, atom, atom[1].eqNode( s ) );
389 d_keep.insert( exp );
390 if( s.getKind()==kind::SINGLETON ){
391 if( s[0]!=atom[0] ){
392 Trace("sets-prop") << "Propagate mem-eq : " << exp << std::endl;
393 Node eq = s[0].eqNode( atom[0] );
394 d_keep.insert( eq );
395 assertFact( eq, exp );
396 }
397 }else{
398 Trace("sets-prop") << "Propagate mem-eq conflict : " << exp << std::endl;
399 d_conflict = true;
400 d_external.d_out->conflict( exp );
401 }
402 }
403 }
404 //add to membership list
405 NodeIntMap::iterator mem_i = d_members.find( r );
406 int n_members = 0;
407 if( mem_i != d_members.end() ) {
408 n_members = (*mem_i).second;
409 }
410 d_members[r] = n_members + 1;
411 if( n_members<(int)d_members_data[r].size() ){
412 d_members_data[r][n_members] = atom;
413 }else{
414 d_members_data[r].push_back( atom );
415 }
416 }
417 }
418 return true;
419 }else{
420 return false;
421 }
422 }
423
424 bool TheorySetsPrivate::assertFactRec( Node fact, Node exp, std::vector< Node >& lemma, int inferType ) {
425 if( ( options::setsInferAsLemmas() && inferType!=-1 ) || inferType==1 ){
426 if( !isEntailed( fact, true ) ){
427 lemma.push_back( exp==d_true ? fact : NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, fact ) );
428 return true;
429 }
430 }else{
431 Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp << std::endl;
432 if( fact.isConst() ){
433 //either trivial or a conflict
434 if( fact==d_false ){
435 Trace("sets-lemma") << "Conflict : " << exp << std::endl;
436 d_conflict = true;
437 d_external.d_out->conflict( exp );
438 return true;
439 }
440 }else if( fact.getKind()==kind::AND || ( fact.getKind()==kind::NOT && fact[0].getKind()==kind::OR ) ){
441 bool ret = false;
442 Node f = fact.getKind()==kind::NOT ? fact[0] : fact;
443 for( unsigned i=0; i<f.getNumChildren(); i++ ){
444 Node factc = fact.getKind()==kind::NOT ? f[i].negate() : f[i];
445 bool tret = assertFactRec( factc, exp, lemma, inferType );
446 ret = ret || tret;
447 if( d_conflict ){
448 return true;
449 }
450 }
451 return ret;
452 }else{
453 bool polarity = fact.getKind() != kind::NOT;
454 TNode atom = polarity ? fact : fact[0];
455 //things we can assert to equality engine
456 if( atom.getKind()==kind::MEMBER || ( atom.getKind()==kind::EQUAL && atom[0].getType().isSet() ) ){
457 //send to equality engine
458 if( assertFact( fact, exp ) ){
459 d_addedFact = true;
460 return true;
461 }
462 }else{
463 if( !isEntailed( fact, true ) ){
464 //must send as lemma
465 lemma.push_back( exp==d_true ? fact : NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, fact ) );
466 return true;
467 }
468 }
469 }
470 }
471 return false;
472 }
473 void TheorySetsPrivate::assertInference( Node fact, Node exp, std::vector< Node >& lemmas, const char * c, int inferType ) {
474 d_keep.insert( exp );
475 d_keep.insert( fact );
476 if( assertFactRec( fact, exp, lemmas, inferType ) ){
477 Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by " << c << std::endl;
478 Trace("sets-assertion") << "(assert (=> " << exp << " " << fact << ")) ; by " << c << std::endl;
479 }
480 }
481
482 void TheorySetsPrivate::assertInference( Node fact, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType ){
483 Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ) );
484 assertInference( fact, exp_n, lemmas, c, inferType );
485 }
486
487 void TheorySetsPrivate::assertInference( std::vector< Node >& conc, Node exp, std::vector< Node >& lemmas, const char * c, int inferType ){
488 if( !conc.empty() ){
489 Node fact = conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::AND, conc );
490 assertInference( fact, exp, lemmas, c, inferType );
491 }
492 }
493 void TheorySetsPrivate::assertInference( std::vector< Node >& conc, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType ) {
494 Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ) );
495 assertInference( conc, exp_n, lemmas, c, inferType );
496 }
497
498 void TheorySetsPrivate::split( Node n, int reqPol ) {
499 n = Rewriter::rewrite( n );
500 Node lem = NodeManager::currentNM()->mkNode( kind::OR, n, n.negate() );
501 std::vector< Node > lemmas;
502 lemmas.push_back( lem );
503 flushLemmas( lemmas );
504 Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
505 if( reqPol!=0 ){
506 Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol>0) << std::endl;
507 d_external.getOutputChannel().requirePhase( n, reqPol>0 );
508 }
509 }
510
511 void TheorySetsPrivate::fullEffortCheck(){
512 Trace("sets") << "----- Full effort check ------" << std::endl;
513 do{
514 Trace("sets") << "...iterate full effort check..." << std::endl;
515 Assert( d_equalityEngine.consistent() );
516 d_sentLemma = false;
517 d_addedFact = false;
518 d_full_check_incomplete = false;
519 d_set_eqc.clear();
520 d_set_eqc_list.clear();
521 d_eqc_emptyset.clear();
522 d_eqc_univset.clear();
523 d_eqc_singleton.clear();
524 d_congruent.clear();
525 d_nvar_sets.clear();
526 d_var_set.clear();
527 d_most_common_type.clear();
528 d_most_common_type_term.clear();
529 d_pol_mems[0].clear();
530 d_pol_mems[1].clear();
531 d_members_index.clear();
532 d_singleton_index.clear();
533 d_bop_index.clear();
534 d_op_list.clear();
535 d_card_enabled = false;
536 d_rels_enabled = false;
537 d_eqc_to_card_term.clear();
538
539 std::vector< Node > lemmas;
540 Trace("sets-eqc") << "Equality Engine:" << std::endl;
541 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
542 while( !eqcs_i.isFinished() ){
543 Node eqc = (*eqcs_i);
544 bool isSet = false;
545 TypeNode tn = eqc.getType();
546 //common type node and term
547 TypeNode tnc;
548 Node tnct;
549 if( tn.isSet() ){
550 isSet = true;
551 d_set_eqc.push_back( eqc );
552 tnc = tn.getSetElementType();
553 tnct = eqc;
554 }
555 Trace("sets-eqc") << "[" << eqc << "] : ";
556 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
557 while( !eqc_i.isFinished() ) {
558 Node n = (*eqc_i);
559 if( n!=eqc ){
560 Trace("sets-eqc") << n << " ";
561 }
562 TypeNode tnn = n.getType();
563 if( isSet ){
564 Assert( tnn.isSet() );
565 TypeNode tnnel = tnn.getSetElementType();
566 tnc = TypeNode::mostCommonTypeNode( tnc, tnnel );
567 Assert( !tnc.isNull() );
568 //update the common type term
569 if( tnc==tnnel ){
570 tnct = n;
571 }
572 }
573 if( n.getKind()==kind::MEMBER ){
574 if( eqc.isConst() ){
575 Node s = d_equalityEngine.getRepresentative( n[1] );
576 Node x = d_equalityEngine.getRepresentative( n[0] );
577 int pindex = eqc==d_true ? 0 : ( eqc==d_false ? 1 : -1 );
578 if( pindex!=-1 ){
579 if( d_pol_mems[pindex][s].find( x )==d_pol_mems[pindex][s].end() ){
580 d_pol_mems[pindex][s][x] = n;
581 Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n << ", pindex = " << pindex << std::endl;
582 }
583 if( d_members_index[s].find( x )==d_members_index[s].end() ){
584 d_members_index[s][x] = n;
585 d_op_list[kind::MEMBER].push_back( n );
586 }
587 }else{
588 Assert( false );
589 }
590 }
591 }else if( n.getKind()==kind::SINGLETON || n.getKind()==kind::UNION || n.getKind()==kind::INTERSECTION ||
592 n.getKind()==kind::SETMINUS || n.getKind()==kind::EMPTYSET || n.getKind()==kind::UNIVERSE_SET ){
593 if( n.getKind()==kind::SINGLETON ){
594 //singleton lemma
595 getProxy( n );
596 Node r = d_equalityEngine.getRepresentative( n[0] );
597 if( d_singleton_index.find( r )==d_singleton_index.end() ){
598 d_singleton_index[r] = n;
599 d_eqc_singleton[eqc] = n;
600 d_op_list[kind::SINGLETON].push_back( n );
601 }else{
602 d_congruent[n] = d_singleton_index[r];
603 }
604 }else if( n.getKind()==kind::EMPTYSET ){
605 d_eqc_emptyset[tnn] = eqc;
606 }else if( n.getKind()==kind::UNIVERSE_SET ){
607 Assert( options::setsExt() );
608 d_eqc_univset[tnn] = eqc;
609 }else{
610 Node r1 = d_equalityEngine.getRepresentative( n[0] );
611 Node r2 = d_equalityEngine.getRepresentative( n[1] );
612 if( d_bop_index[n.getKind()][r1].find( r2 )==d_bop_index[n.getKind()][r1].end() ){
613 d_bop_index[n.getKind()][r1][r2] = n;
614 d_op_list[n.getKind()].push_back( n );
615 }else{
616 d_congruent[n] = d_bop_index[n.getKind()][r1][r2];
617 }
618 }
619 d_nvar_sets[eqc].push_back( n );
620 Trace("sets-debug2") << "Non-var-set[" << eqc << "] : " << n << std::endl;
621 d_set_eqc_list[eqc].push_back( n );
622 }else if( n.getKind()==kind::CARD ){
623 d_card_enabled = true;
624 TypeNode tnc = n[0].getType().getSetElementType();
625 if( tnc.isInterpretedFinite() ){
626 std::stringstream ss;
627 ss << "ERROR: cannot use cardinality on sets with finite element type." << std::endl;
628 throw LogicException(ss.str());
629 //TODO: extend approach for this case
630 }
631 Node r = d_equalityEngine.getRepresentative( n[0] );
632 if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){
633 d_eqc_to_card_term[ r ] = n;
634 registerCardinalityTerm( n[0], lemmas );
635 }
636 }else{
637 if( d_rels->isRelationKind( n.getKind() ) ){
638 d_rels_enabled = true;
639 }
640 if( isSet ){
641 d_set_eqc_list[eqc].push_back( n );
642 if( n.getKind()==kind::VARIABLE ){
643 if( d_var_set.find( eqc )==d_var_set.end() ){
644 d_var_set[eqc] = n;
645 }
646 }
647 }
648 }
649 ++eqc_i;
650 }
651 if( isSet ){
652 Assert( tnct.getType().getSetElementType()==tnc );
653 d_most_common_type[eqc] = tnc;
654 d_most_common_type_term[eqc] = tnct;
655 }
656 Trace("sets-eqc") << std::endl;
657 ++eqcs_i;
658 }
659
660 flushLemmas( lemmas );
661 if( !hasProcessed() ){
662 if( Trace.isOn("sets-mem") ){
663 for( unsigned i=0; i<d_set_eqc.size(); i++ ){
664 Node s = d_set_eqc[i];
665 Trace("sets-mem") << "Eqc " << s << " : ";
666 std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].find( s );
667 if( it!=d_pol_mems[0].end() ){
668 Trace("sets-mem") << "Memberships : ";
669 for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
670 Trace("sets-mem") << it2->first << " ";
671 }
672 }
673 std::map< Node, Node >::iterator its = d_eqc_singleton.find( s );
674 if( its!=d_eqc_singleton.end() ){
675 Trace("sets-mem") << " : Singleton : " << its->second;
676 }
677 Trace("sets-mem") << std::endl;
678 }
679 }
680 checkSubtypes( lemmas );
681 flushLemmas( lemmas, true );
682 if( !hasProcessed() ){
683
684 checkDownwardsClosure( lemmas );
685 if( options::setsInferAsLemmas() ){
686 flushLemmas( lemmas );
687 }
688 if( !hasProcessed() ){
689 checkUpwardsClosure( lemmas );
690 flushLemmas( lemmas );
691 if( !hasProcessed() ){
692 std::vector< Node > intro_sets;
693 //for cardinality
694 if( d_card_enabled ){
695 checkCardBuildGraph( lemmas );
696 flushLemmas( lemmas );
697 if( !hasProcessed() ){
698 checkMinCard( lemmas );
699 flushLemmas( lemmas );
700 if( !hasProcessed() ){
701 checkCardCycles( lemmas );
702 flushLemmas( lemmas );
703 if( !hasProcessed() ){
704 checkNormalForms( lemmas, intro_sets );
705 flushLemmas( lemmas );
706 }
707 }
708 }
709 }
710 if( !hasProcessed() ){
711 checkDisequalities( lemmas );
712 flushLemmas( lemmas );
713 if( !hasProcessed() ){
714 //introduce splitting on venn regions (absolute last resort)
715 if( d_card_enabled && !hasProcessed() && !intro_sets.empty() ){
716 Assert( intro_sets.size()==1 );
717 Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl;
718 Trace("sets-intro") << " Actual Intro : ";
719 debugPrintSet( intro_sets[0], "sets-nf" );
720 Trace("sets-nf") << std::endl;
721 Node k = getProxy( intro_sets[0] );
722 d_sentLemma = true;
723 }
724 }
725 }
726 }
727 }
728 }
729 }
730 }while( !d_sentLemma && !d_conflict && d_addedFact );
731 Trace("sets") << "----- End full effort check, conflict=" << d_conflict << ", lemma=" << d_sentLemma << std::endl;
732 }
733
734 void TheorySetsPrivate::checkSubtypes( std::vector< Node >& lemmas ) {
735 for( unsigned i=0; i<d_set_eqc.size(); i++ ){
736 Node s = d_set_eqc[i];
737 TypeNode mct = d_most_common_type[s];
738 std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].find( s );
739 if( it!=d_pol_mems[0].end() ){
740 for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
741 if (!it2->first.getType().isSubtypeOf(mct))
742 {
743 Node mctt = d_most_common_type_term[s];
744 std::vector< Node > exp;
745 exp.push_back( it2->second );
746 Assert( ee_areEqual( mctt, it2->second[1] ) );
747 exp.push_back( mctt.eqNode( it2->second[1] ) );
748 Node tc_k = getTypeConstraintSkolem(it2->first, mct);
749 if (!tc_k.isNull())
750 {
751 Node etc = tc_k.eqNode(it2->first);
752 assertInference( etc, exp, lemmas, "subtype-clash" );
753 if( d_conflict ){
754 return;
755 }
756 }
757 }
758 }
759 }
760 }
761 }
762
763 void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) {
764 Trace("sets") << "Downwards closure..." << std::endl;
765 //downwards closure
766 for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){
767 std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( it->first );
768 if( itn!=d_nvar_sets.end() ){
769 for( unsigned j=0; j<itn->second.size(); j++ ){
770 if( d_congruent.find( itn->second[j] )==d_congruent.end() ){
771 for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
772 Node mem = it2->second;
773 Node eq_set = itn->second[j];
774 Assert( d_equalityEngine.areEqual( mem[1], eq_set ) );
775 if( mem[1]!=eq_set ){
776 Trace("sets-debug") << "Downwards closure based on " << mem << ", eq_set = " << eq_set << std::endl;
777 if( !options::setsProxyLemmas() ){
778 Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
779 nmem = Rewriter::rewrite( nmem );
780 std::vector< Node > exp;
781 exp.push_back( mem );
782 exp.push_back( mem[1].eqNode( eq_set ) );
783 assertInference( nmem, exp, lemmas, "downc" );
784 if( d_conflict ){
785 return;
786 }
787 }else{
788 //use proxy set
789 Node k = getProxy( eq_set );
790 Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k );
791 Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
792 nmem = Rewriter::rewrite( nmem );
793 std::vector< Node > exp;
794 if( ee_areEqual( mem, pmem ) ){
795 exp.push_back( pmem );
796 }else{
797 nmem = NodeManager::currentNM()->mkNode( kind::OR, pmem.negate(), nmem );
798 }
799 assertInference( nmem, exp, lemmas, "downc" );
800 }
801 }
802 }
803 }
804 }
805 }
806 }
807 }
808
809 void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) {
810 //upwards closure
811 for( std::map< Kind, std::map< Node, std::map< Node, Node > > >::iterator itb = d_bop_index.begin(); itb != d_bop_index.end(); ++itb ){
812 Kind k = itb->first;
813 Trace("sets") << "Upwards closure " << k << "..." << std::endl;
814 for( std::map< Node, std::map< Node, Node > >::iterator it = itb->second.begin(); it != itb->second.end(); ++it ){
815 Node r1 = it->first;
816 //see if there are members in first argument r1
817 std::map< Node, std::map< Node, Node > >::iterator itm1 = d_pol_mems[0].find( r1 );
818 if( itm1!=d_pol_mems[0].end() || k==kind::UNION ){
819 for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
820 Node r2 = it2->first;
821 //see if there are members in second argument
822 std::map< Node, std::map< Node, Node > >::iterator itm2 = d_pol_mems[0].find( r2 );
823 std::map< Node, std::map< Node, Node > >::iterator itm2n = d_pol_mems[1].find( r2 );
824 if( itm2!=d_pol_mems[0].end() || k!=kind::INTERSECTION ){
825 Trace("sets-debug") << "Checking " << it2->second << ", members = " << (itm1!=d_pol_mems[0].end()) << ", " << (itm2!=d_pol_mems[0].end()) << std::endl;
826 //for all members of r1
827 if( itm1!=d_pol_mems[0].end() ){
828 for( std::map< Node, Node >::iterator itm1m = itm1->second.begin(); itm1m != itm1->second.end(); ++itm1m ){
829 Node xr = itm1m->first;
830 Node x = itm1m->second[0];
831 Trace("sets-debug") << "checking membership " << xr << " " << itm1m->second << std::endl;
832 std::vector< Node > exp;
833 exp.push_back( itm1m->second );
834 addEqualityToExp( it2->second[0], itm1m->second[1], exp );
835 bool valid = false;
836 int inferType = 0;
837 if( k==kind::UNION ){
838 valid = true;
839 }else if( k==kind::INTERSECTION ){
840 //conclude x is in it2->second
841 //if also existing in members of r2
842 bool in_r2 = itm2!=d_pol_mems[0].end() && itm2->second.find( xr )!=itm2->second.end();
843 if( in_r2 ){
844 exp.push_back( itm2->second[xr] );
845 addEqualityToExp( it2->second[1], itm2->second[xr][1], exp );
846 addEqualityToExp( x, itm2->second[xr][0], exp );
847 valid = true;
848 }else{
849 // if not, check whether it is definitely not a member, if unknown, split
850 bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2n->second.end();
851 if( !not_in_r2 ){
852 exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ) );
853 valid = true;
854 inferType = 1;
855 }
856 }
857 }else{
858 Assert( k==kind::SETMINUS );
859 /*
860 std::map< Node, std::map< Node, Node > >::iterator itnm2 = d_pol_mems[1].find( r2 );
861 if( itnm2!=d_pol_mems[1].end() ){
862 bool not_in_r2 = itnm2->second.find( xr )!=itnm2->second.end();
863 if( not_in_r2 ){
864 exp.push_back( itnm2->second[xr] );
865 if( it2->second[1]!=itnm2->second[xr][1] ){
866 Assert( d_equalityEngine.areEqual( it2->second[1], itnm2->second[xr][1] ) );
867 exp.push_back( it2->second[1].eqNode( itnm2->second[xr][1] ) );
868 }
869 if( x!=itnm2->second[xr][0] ){
870 Assert( d_equalityEngine.areEqual( x, itnm2->second[xr][0] ) );
871 exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, x, itnm2->second[xr][0] ) );
872 }
873 valid = true;
874 }
875 }
876 */
877 if( !valid ){
878 bool in_r2 = itm2!=d_pol_mems[0].end() && itm2->second.find( xr )!=itm2->second.end();
879 if( !in_r2 ){
880 // must add lemma for set minus since non-membership in this case is not explained
881 exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ).negate() );
882 valid = true;
883 inferType = 1;
884 }
885 }
886 }
887 if( valid ){
888 Node rr = d_equalityEngine.getRepresentative( it2->second );
889 if( !isMember( x, rr ) ){
890 Node kk = getProxy( it2->second );
891 Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, x, kk );
892 assertInference( fact, exp, lemmas, "upc", inferType );
893 if( d_conflict ){
894 return;
895 }
896 }
897 }
898 Trace("sets-debug") << "done checking membership " << xr << " " << itm1m->second << std::endl;
899 }
900 }
901 if( k==kind::UNION ){
902 if( itm2!=d_pol_mems[0].end() ){
903 //for all members of r2
904 for( std::map< Node, Node >::iterator itm2m = itm2->second.begin(); itm2m != itm2->second.end(); ++itm2m ){
905 Node x = itm2m->second[0];
906 Node rr = d_equalityEngine.getRepresentative( it2->second );
907 if( !isMember( x, rr ) ){
908 std::vector< Node > exp;
909 exp.push_back( itm2m->second );
910 addEqualityToExp( it2->second[1], itm2m->second[1], exp );
911 Node k = getProxy( it2->second );
912 Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, x, k );
913 assertInference( fact, exp, lemmas, "upc2" );
914 if( d_conflict ){
915 return;
916 }
917 }
918 }
919 }
920 }
921 }
922 }
923 }
924 }
925 }
926 if( !hasProcessed() ){
927 if( options::setsExt() ){
928 //universal sets
929 Trace("sets-debug") << "Check universe sets..." << std::endl;
930 //all elements must be in universal set
931 for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){
932 //if equivalence class contains a variable
933 std::map< Node, Node >::iterator itv = d_var_set.find( it->first );
934 if( itv!=d_var_set.end() ){
935 //the variable in the equivalence class
936 Node v = itv->second;
937 std::map< TypeNode, Node > univ_set;
938 for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
939 Node e = it2->second[0];
940 TypeNode tn = NodeManager::currentNM()->mkSetType( e.getType() );
941 Node u;
942 std::map< TypeNode, Node >::iterator itu = univ_set.find( tn );
943 if( itu==univ_set.end() ){
944 std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn );
945 // if the universe does not yet exist, or is not in this equivalence class
946 if( itu==d_eqc_univset.end() || itu->second!=it->first ){
947 u = getUnivSet( tn );
948 }
949 univ_set[tn] = u;
950 }else{
951 u = itu->second;
952 }
953 if( !u.isNull() ){
954 Assert( it2->second.getKind()==kind::MEMBER );
955 std::vector< Node > exp;
956 exp.push_back( it2->second );
957 if( v!=it2->second[1] ){
958 exp.push_back( v.eqNode( it2->second[1] ) );
959 }
960 Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, it2->second[0], u );
961 assertInference( fact, exp, lemmas, "upuniv" );
962 if( d_conflict ){
963 return;
964 }
965 }
966 }
967 }
968 }
969 }
970 }
971 }
972
973 void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) {
974 //disequalities
975 Trace("sets") << "Disequalities..." << std::endl;
976 for(NodeBoolMap::const_iterator it=d_deq.begin(); it !=d_deq.end(); ++it) {
977 if( (*it).second ){
978 Node deq = (*it).first;
979 //check if it is already satisfied
980 Assert( d_equalityEngine.hasTerm( deq[0] ) && d_equalityEngine.hasTerm( deq[1] ) );
981 Node r1 = d_equalityEngine.getRepresentative( deq[0] );
982 Node r2 = d_equalityEngine.getRepresentative( deq[1] );
983 bool is_sat = isSetDisequalityEntailed( r1, r2 );
984 /*
985 if( !is_sat ){
986 //try to make one of them empty
987 for( unsigned e=0; e<2; e++ ){
988 }
989 }
990 */
991 Trace("sets-debug") << "Check disequality " << deq << ", is_sat = " << is_sat << std::endl;
992 //will process regardless of sat/processed/unprocessed
993 d_deq[deq] = false;
994
995 if( !is_sat ){
996 if( d_deq_processed.find( deq )==d_deq_processed.end() ){
997 d_deq_processed.insert( deq );
998 d_deq_processed.insert( deq[1].eqNode( deq[0] ) );
999 Trace("sets") << "Process Disequality : " << deq.negate() << std::endl;
1000 TypeNode elementType = deq[0].getType().getSetElementType();
1001 Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType);
1002 Node mem1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[0] );
1003 Node mem2 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[1] );
1004 Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::EQUAL, mem1, mem2 ).negate() );
1005 lem = Rewriter::rewrite( lem );
1006 assertInference( lem, d_emp_exp, lemmas, "diseq", 1 );
1007 flushLemmas( lemmas );
1008 if( hasProcessed() ){
1009 return;
1010 }
1011 }
1012 }
1013 }
1014 }
1015 }
1016
1017 void TheorySetsPrivate::checkCardBuildGraph( std::vector< Node >& lemmas ) {
1018 Trace("sets") << "Cardinality graph..." << std::endl;
1019 //first, ensure cardinality relationships are added as lemmas for all non-basic set terms
1020 for( unsigned i=0; i<d_set_eqc.size(); i++ ){
1021 Node eqc = d_set_eqc[i];
1022 std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
1023 if( itn!=d_nvar_sets.end() ){
1024 for( unsigned j=0; j<itn->second.size(); j++ ){
1025 Node n = itn->second[j];
1026 if( d_congruent.find( n )==d_congruent.end() ){
1027 //if setminus, do for intersection instead
1028 if( n.getKind()==kind::SETMINUS ){
1029 n = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, n[0], n[1] ) );
1030 }
1031 registerCardinalityTerm( n, lemmas );
1032 }
1033 }
1034 }
1035 }
1036 Trace("sets") << "Done cardinality graph" << std::endl;
1037 }
1038
1039 void TheorySetsPrivate::registerCardinalityTerm( Node n, std::vector< Node >& lemmas ){
1040 if( d_card_processed.find( n )==d_card_processed.end() ){
1041 d_card_processed.insert( n );
1042 Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
1043 std::vector< Node > cterms;
1044 if( n.getKind()==kind::INTERSECTION ){
1045 for( unsigned e=0; e<2; e++ ){
1046 Node s = NodeManager::currentNM()->mkNode( kind::SETMINUS, n[e], n[1-e] );
1047 cterms.push_back( s );
1048 }
1049 Node pos_lem = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::CARD, n ), d_zero );
1050 assertInference( pos_lem, d_emp_exp, lemmas, "pcard", 1 );
1051 }else{
1052 cterms.push_back( n );
1053 }
1054 for( unsigned k=0; k<cterms.size(); k++ ){
1055 Node nn = cterms[k];
1056 Node nk = getProxy( nn );
1057 Node pos_lem = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::CARD, nk ), d_zero );
1058 assertInference( pos_lem, d_emp_exp, lemmas, "pcard", 1 );
1059 if( nn!=nk ){
1060 Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::CARD, nk ),
1061 NodeManager::currentNM()->mkNode( kind::CARD, nn ) );
1062 lem = Rewriter::rewrite( lem );
1063 Trace("sets-card") << " " << k << " : " << lem << std::endl;
1064 assertInference( lem, d_emp_exp, lemmas, "card", 1 );
1065 }
1066 }
1067 }
1068 }
1069
1070 void TheorySetsPrivate::checkCardCycles( std::vector< Node >& lemmas ) {
1071 Trace("sets") << "Check cardinality cycles..." << std::endl;
1072 //build order of equivalence classes, also build cardinality graph
1073 std::vector< Node > set_eqc_tmp;
1074 set_eqc_tmp.insert( set_eqc_tmp.end(), d_set_eqc.begin(), d_set_eqc.end() );
1075 d_set_eqc.clear();
1076 d_card_parent.clear();
1077 for( unsigned i=0; i<set_eqc_tmp.size(); i++ ){
1078 std::vector< Node > curr;
1079 std::vector< Node > exp;
1080 checkCardCyclesRec( set_eqc_tmp[i], curr, exp, lemmas );
1081 flushLemmas( lemmas );
1082 if( hasProcessed() ){
1083 return;
1084 }
1085 }
1086 Trace("sets") << "Done check cardinality cycles" << std::endl;
1087 }
1088
1089 void TheorySetsPrivate::checkCardCyclesRec( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp, std::vector< Node >& lemmas ) {
1090 if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
1091 Trace("sets-debug") << "Found venn region loop..." << std::endl;
1092 if( curr.size()>1 ){
1093 //all regions must be equal
1094 std::vector< Node > conc;
1095 for( unsigned i=1; i<curr.size(); i++ ){
1096 conc.push_back( curr[0].eqNode( curr[i] ) );
1097 }
1098 Node fact = conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::AND, conc );
1099 assertInference( fact, exp, lemmas, "card_cycle" );
1100 flushLemmas( lemmas );
1101 }else{
1102 //should be guaranteed based on not exploring equal parents
1103 Assert( false );
1104 }
1105 }else if( std::find( d_set_eqc.begin(), d_set_eqc.end(), eqc )==d_set_eqc.end() ){
1106 curr.push_back( eqc );
1107 TypeNode tn = eqc.getType();
1108 bool is_empty = eqc==d_eqc_emptyset[tn];
1109 Node emp_set = getEmptySet( tn );
1110 std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
1111 if( itn!=d_nvar_sets.end() ){
1112 for( unsigned j=0; j<itn->second.size(); j++ ){
1113 Node n = itn->second[j];
1114 if( n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS ){
1115 Trace("sets-debug") << "Build cardinality parents for " << n << "..." << std::endl;
1116 std::vector< Node > sib;
1117 unsigned true_sib = 0;
1118 if( n.getKind()==kind::INTERSECTION ){
1119 d_card_base[n] = n;
1120 for( unsigned e=0; e<2; e++ ){
1121 Node sm = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::SETMINUS, n[e], n[1-e] ) );
1122 sib.push_back( sm );
1123 }
1124 true_sib = 2;
1125 }else{
1126 Node si = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, n[0], n[1] ) );
1127 sib.push_back( si );
1128 d_card_base[n] = si;
1129 Node osm = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::SETMINUS, n[1], n[0] ) );
1130 sib.push_back( osm );
1131 true_sib = 1;
1132 }
1133 Node u = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::UNION, n[0], n[1] ) );
1134 if( !d_equalityEngine.hasTerm( u ) ){
1135 u = Node::null();
1136 }
1137 unsigned n_parents = true_sib + ( u.isNull() ? 0 : 1 );
1138 //if this set is empty
1139 if( is_empty ){
1140 Assert( ee_areEqual( n, emp_set ) );
1141 Trace("sets-debug") << " empty, parents equal siblings" << std::endl;
1142 std::vector< Node > conc;
1143 //parent equal siblings
1144 for( unsigned e=0; e<true_sib; e++ ){
1145 if( d_equalityEngine.hasTerm( sib[e] ) && !ee_areEqual( n[e], sib[e] ) ){
1146 conc.push_back( n[e].eqNode( sib[e] ) );
1147 }
1148 }
1149 assertInference( conc, n.eqNode( emp_set ), lemmas, "cg_emp" );
1150 flushLemmas( lemmas );
1151 if( hasProcessed() ){
1152 return;
1153 }else{
1154 //justify why there is no edge to parents (necessary?)
1155 for( unsigned e=0; e<n_parents; e++ ){
1156 Node p = (e==true_sib) ? u : n[e];
1157
1158 }
1159 }
1160 }else{
1161 std::vector< Node > card_parents;
1162 std::vector< int > card_parent_ids;
1163 //check if equal to a parent
1164 for( unsigned e=0; e<n_parents; e++ ){
1165 Trace("sets-debug") << " check parent " << e << "/" << n_parents << std::endl;
1166 bool is_union = e==true_sib;
1167 Node p = (e==true_sib) ? u : n[e];
1168 Trace("sets-debug") << " check relation to parent " << p << ", isu=" << is_union << "..." << std::endl;
1169 //if parent is empty
1170 if( ee_areEqual( p, emp_set ) ){
1171 Trace("sets-debug") << " it is empty..." << std::endl;
1172 Assert( !ee_areEqual( n, emp_set ) );
1173 assertInference( n.eqNode( emp_set ), p.eqNode( emp_set ), lemmas, "cg_emppar" );
1174 if( hasProcessed() ){
1175 return;
1176 }
1177 //if we are equal to a parent
1178 }else if( ee_areEqual( p, n ) ){
1179 Trace("sets-debug") << " it is equal to this..." << std::endl;
1180 std::vector< Node > conc;
1181 std::vector< int > sib_emp_indices;
1182 if( is_union ){
1183 for( unsigned s=0; s<sib.size(); s++ ){
1184 sib_emp_indices.push_back( s );
1185 }
1186 }else{
1187 sib_emp_indices.push_back( e );
1188 }
1189 //sibling(s) are empty
1190 for( unsigned s=0; s<sib_emp_indices.size(); s++ ){
1191 unsigned si = sib_emp_indices[s];
1192 if( !ee_areEqual( sib[si], emp_set ) ){
1193 conc.push_back( sib[si].eqNode( emp_set ) );
1194 }else{
1195 Trace("sets-debug") << "Sibling " << sib[si] << " is already empty." << std::endl;
1196 }
1197 }
1198 if( !is_union && n.getKind()==kind::INTERSECTION && !u.isNull() ){
1199 //union is equal to other parent
1200 if( !ee_areEqual( u, n[1-e] ) ){
1201 conc.push_back( u.eqNode( n[1-e] ) );
1202 }
1203 }
1204 Trace("sets-debug") << "...derived " << conc.size() << " conclusions" << std::endl;
1205 assertInference( conc, n.eqNode( p ), lemmas, "cg_eqpar" );
1206 flushLemmas( lemmas );
1207 if( hasProcessed() ){
1208 return;
1209 }
1210 }else{
1211 Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
1212 //otherwise, we a syntactic subset of p
1213 card_parents.push_back( p );
1214 card_parent_ids.push_back( is_union ? 2 : e );
1215 }
1216 }
1217 Assert( d_card_parent[n].empty() );
1218 Trace("sets-debug") << "get parent representatives..." << std::endl;
1219 //for each parent, take their representatives
1220 for( unsigned k=0; k<card_parents.size(); k++ ){
1221 Node eqcc = d_equalityEngine.getRepresentative( card_parents[k] );
1222 Trace("sets-debug") << "Check card parent " << k << "/" << card_parents.size() << std::endl;
1223
1224 //if parent is singleton, then we should either be empty to equal to it
1225 std::map< Node, Node >::iterator itps = d_eqc_singleton.find( eqcc );
1226 if( itps!=d_eqc_singleton.end() ){
1227 bool eq_parent = false;
1228 std::vector< Node > exp;
1229 addEqualityToExp( card_parents[k], itps->second, exp );
1230 if( ee_areDisequal( n, emp_set ) ){
1231 exp.push_back( n.eqNode( emp_set ).negate() );
1232 eq_parent = true;
1233 }else{
1234 std::map< Node, std::map< Node, Node > >::iterator itpm = d_pol_mems[0].find( eqc );
1235 if( itpm!=d_pol_mems[0].end() && !itpm->second.empty() ){
1236 Node pmem = itpm->second.begin()->second;
1237 exp.push_back( pmem );
1238 addEqualityToExp( n, pmem[1], exp );
1239 eq_parent = true;
1240 }
1241 }
1242 //must be equal to parent
1243 if( eq_parent ){
1244 Node conc = n.eqNode( card_parents[k] );
1245 assertInference( conc, exp, lemmas, "cg_par_sing" );
1246 flushLemmas( lemmas );
1247 }else{
1248 //split on empty
1249 Trace("sets-nf") << "Split empty : " << n << std::endl;
1250 split( n.eqNode( emp_set ), 1 );
1251 }
1252 Assert( hasProcessed() );
1253 return;
1254 }else{
1255 bool dup = false;
1256 for( unsigned l=0; l<d_card_parent[n].size(); l++ ){
1257 if( eqcc==d_card_parent[n][l] ){
1258 Trace("sets-debug") << " parents " << l << " and " << k << " are equal, ids = " << card_parent_ids[l] << " " << card_parent_ids[k] << std::endl;
1259 dup = true;
1260 if( n.getKind()==kind::INTERSECTION ){
1261 Assert( card_parent_ids[l]!=2 );
1262 std::vector< Node > conc;
1263 if( card_parent_ids[k]==2 ){
1264 //intersection is equal to other parent
1265 unsigned pid = 1-card_parent_ids[l];
1266 if( !ee_areEqual( n[pid], n ) ){
1267 Trace("sets-debug") << " one of them is union, make equal to other..." << std::endl;
1268 conc.push_back( n[pid].eqNode( n ) );
1269 }
1270 }else{
1271 if( !ee_areEqual( card_parents[k], n ) ){
1272 Trace("sets-debug") << " neither is union, make equal to one parent..." << std::endl;
1273 //intersection is equal to one of the parents
1274 conc.push_back( card_parents[k].eqNode( n ) );
1275 }
1276 }
1277 assertInference( conc, card_parents[k].eqNode( d_card_parent[n][l] ), lemmas, "cg_pareq" );
1278 flushLemmas( lemmas );
1279 if( hasProcessed() ){
1280 return;
1281 }
1282 }
1283 }
1284 }
1285 if( !dup ){
1286 d_card_parent[n].push_back( eqcc );
1287 }
1288 }
1289 }
1290 //now recurse on parents (to ensure their normal will be computed after this eqc)
1291 exp.push_back( eqc.eqNode( n ) );
1292 for( unsigned k=0; k<d_card_parent[n].size(); k++ ){
1293 checkCardCyclesRec( d_card_parent[n][k], curr, exp, lemmas );
1294 if( hasProcessed() ){
1295 return;
1296 }
1297 }
1298 exp.pop_back();
1299 }
1300 }
1301 }
1302 }
1303 curr.pop_back();
1304 //parents now processed, can add to ordered list
1305 d_set_eqc.push_back( eqc );
1306 }else{
1307 //already processed
1308 }
1309 }
1310
1311 void TheorySetsPrivate::checkNormalForms( std::vector< Node >& lemmas, std::vector< Node >& intro_sets ){
1312 Trace("sets") << "Check normal forms..." << std::endl;
1313 // now, build normal form for each equivalence class
1314 // d_set_eqc is now sorted such that for each d_set_eqc[i], d_set_eqc[j],
1315 // if d_set_eqc[i] is a strict syntactic subterm of d_set_eqc[j], then i<j.
1316 d_ff.clear();
1317 d_nf.clear();
1318 for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
1319 checkNormalForm( d_set_eqc[i], intro_sets );
1320 if( hasProcessed() || !intro_sets.empty() ){
1321 return;
1322 }
1323 }
1324 Trace("sets") << "Done check normal forms" << std::endl;
1325 }
1326
1327 void TheorySetsPrivate::checkNormalForm( Node eqc, std::vector< Node >& intro_sets ){
1328 TypeNode tn = eqc.getType();
1329 Trace("sets") << "Compute normal form for " << eqc << std::endl;
1330 Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
1331 if( eqc==d_eqc_emptyset[tn] ){
1332 d_nf[eqc].clear();
1333 Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
1334 }else{
1335 //flat/normal forms are sets of equivalence classes
1336 Node base;
1337 std::vector< Node > comps;
1338 std::map< Node, std::map< Node, std::vector< Node > > >::iterator it = d_ff.find( eqc );
1339 if( it!=d_ff.end() ){
1340 for( std::map< Node, std::vector< Node > >::iterator itf = it->second.begin(); itf != it->second.end(); ++itf ){
1341 std::sort( itf->second.begin(), itf->second.end() );
1342 if( base.isNull() ){
1343 base = itf->first;
1344 }else{
1345 comps.push_back( itf->first );
1346 }
1347 Trace("sets-nf") << " F " << itf->first << " : ";
1348 if( Trace.isOn("sets-nf") ){
1349 Trace("sets-nf") << "{ ";
1350 for( unsigned k=0; k<itf->second.size(); k++ ){
1351 if( k>0 ){ Trace("sets-nf") << ", "; }
1352 Trace("sets-nf") << "[" << itf->second[k] << "]";
1353 }
1354 Trace("sets-nf") << " }" << std::endl;
1355 }
1356 Trace("sets-nf-debug") << " ...";
1357 debugPrintSet( itf->first, "sets-nf-debug" );
1358 Trace("sets-nf-debug") << std::endl;
1359 }
1360 }else{
1361 Trace("sets-nf") << "(no flat forms)" << std::endl;
1362 }
1363
1364 Assert( d_nf.find( eqc )==d_nf.end() );
1365 bool success = true;
1366 if( !base.isNull() ){
1367 Node emp_set = getEmptySet( tn );
1368 for( unsigned j=0; j<comps.size(); j++ ){
1369 //compare if equal
1370 std::vector< Node > c;
1371 c.push_back( base );
1372 c.push_back( comps[j] );
1373 std::vector< Node > only[2];
1374 std::vector< Node > common;
1375 Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs " << comps[j] << std::endl;
1376 unsigned k[2] = { 0, 0 };
1377 while( k[0]<d_ff[eqc][c[0]].size() || k[1]<d_ff[eqc][c[1]].size() ){
1378 bool proc = true;
1379 for( unsigned e=0; e<2; e++ ){
1380 if( k[e]==d_ff[eqc][c[e]].size() ){
1381 for( ; k[1-e]<d_ff[eqc][c[1-e]].size(); ++k[1-e] ){
1382 only[1-e].push_back( d_ff[eqc][c[1-e]][k[1-e]] );
1383 }
1384 proc = false;
1385 }
1386 }
1387 if( proc ){
1388 if( d_ff[eqc][c[0]][k[0]]==d_ff[eqc][c[1]][k[1]] ){
1389 common.push_back( d_ff[eqc][c[0]][k[0]] );
1390 k[0]++;
1391 k[1]++;
1392 }else if( d_ff[eqc][c[0]][k[0]]<d_ff[eqc][c[1]][k[1]] ){
1393 only[0].push_back( d_ff[eqc][c[0]][k[0]] );
1394 k[0]++;
1395 }else{
1396 only[1].push_back( d_ff[eqc][c[1]][k[1]] );
1397 k[1]++;
1398 }
1399 }
1400 }
1401 if( !only[0].empty() || !only[1].empty() ){
1402 if( Trace.isOn("sets-nf-debug") ){
1403 Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
1404 for( unsigned e=0; e<2; e++ ){
1405 Trace("sets-nf-debug") << " " << c[e] << " : { ";
1406 for( unsigned l=0; l<only[e].size(); l++ ){
1407 if( l>0 ){ Trace("sets-nf-debug") << ", "; }
1408 Trace("sets-nf-debug") << "[" << only[e][l] << "]";
1409 }
1410 Trace("sets-nf-debug") << " }" << std::endl;
1411 }
1412 }
1413 //try to make one empty, prefer the unique ones first
1414 for( unsigned e=0; e<3; e++ ){
1415 unsigned sz = e==2 ? common.size() : only[e].size();
1416 for( unsigned l=0; l<sz; l++ ){
1417 Node r = e==2 ? common[l] : only[e][l];
1418 Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
1419 Trace("sets-nf-debug") << " actual : ";
1420 debugPrintSet( r, "sets-nf-debug" );
1421 Trace("sets-nf-debug") << std::endl;
1422 Assert( !ee_areEqual( r, emp_set ) );
1423 if( !ee_areDisequal( r, emp_set ) && ( d_pol_mems[0].find( r )==d_pol_mems[0].end() || d_pol_mems[0][r].empty() ) ){
1424 //guess that its equal empty if it has no explicit members
1425 Trace("sets-nf") << " Split empty : " << r << std::endl;
1426 Trace("sets-nf") << "Actual Split : ";
1427 debugPrintSet( r, "sets-nf" );
1428 Trace("sets-nf") << std::endl;
1429 split( r.eqNode( emp_set ), 1 );
1430 Assert( hasProcessed() );
1431 return;
1432 }
1433 }
1434 }
1435 for( unsigned l=0; l<only[0].size(); l++ ){
1436 for( unsigned m=0; m<only[1].size(); m++ ){
1437 bool disjoint = false;
1438 Trace("sets-nf-debug") << "Try split " << only[0][l] << " against " << only[1][m] << std::endl;
1439 //split them
1440 for( unsigned e=0; e<2; e++ ){
1441 Node r1 = e==0 ? only[0][l] : only[1][m];
1442 Node r2 = e==0 ? only[1][m] : only[0][l];
1443 //check if their intersection exists modulo equality
1444 std::map< Node, Node >::iterator itb = d_bop_index[kind::INTERSECTION][r1].find( r2 );
1445 if( itb!=d_bop_index[kind::INTERSECTION][r1].end() ){
1446 Trace("sets-nf-debug") << "Split term already exists, but not in cardinality graph : " << itb->second << ", should be empty." << std::endl;
1447 //their intersection is empty (probably?)
1448 // e.g. these are two disjoint venn regions, proceed to next pair
1449 Assert( ee_areEqual( emp_set, itb->second ) );
1450 disjoint = true;
1451 break;
1452 }
1453 }
1454 if( !disjoint ){
1455 //simply introduce their intersection
1456 Assert( only[0][l]!=only[1][m] );
1457 Node kca = getProxy( only[0][l] );
1458 Node kcb = getProxy( only[1][m] );
1459 Node intro = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, kca, kcb ) );
1460 Trace("sets-nf") << " Intro split : " << only[0][l] << " against " << only[1][m] << ", term is " << intro << std::endl;
1461 intro_sets.push_back( intro );
1462 Assert( !d_equalityEngine.hasTerm( intro ) );
1463 return;
1464 }
1465 }
1466 }
1467 //should never get here
1468 success = false;
1469 }
1470 }
1471 if( success ){
1472 //normal form is flat form of base
1473 d_nf[eqc].insert( d_nf[eqc].end(), d_ff[eqc][base].begin(), d_ff[eqc][base].end() );
1474 Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
1475 }else{
1476 Trace("sets-nf") << "failed to build N " << eqc << std::endl;
1477 Assert( false );
1478 }
1479 }else{
1480 //normal form is this equivalence class
1481 d_nf[eqc].push_back( eqc );
1482 Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }" << std::endl;
1483 }
1484 if( success ){
1485 //send to parents
1486 std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
1487 if( itn!=d_nvar_sets.end() ){
1488 std::map< Node, std::map< Node, bool > > parents_proc;
1489 for( unsigned j=0; j<itn->second.size(); j++ ){
1490 Node n = itn->second[j];
1491 Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
1492 if( !d_card_parent[n].empty() ){
1493 Assert( d_card_base.find( n )!=d_card_base.end() );
1494 Node cbase = d_card_base[n];
1495 Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
1496 for( unsigned k=0; k<d_card_parent[n].size(); k++ ){
1497 Node p = d_card_parent[n][k];
1498 Trace("sets-nf-debug") << "Check parent " << p << std::endl;
1499 if( parents_proc[cbase].find( p )==parents_proc[cbase].end() ){
1500 parents_proc[cbase][p] = true;
1501 Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p << "] ), from " << n << "..." << std::endl;
1502 //for( unsigned i=0; i<d_nf[eqc].size(); i++ ){
1503 // Assert( std::find( d_ff[p][cbase].begin(), d_ff[p][cbase].end(), d_nf[eqc][i] )==d_ff[p][cbase].end() );
1504 //}
1505 for( unsigned i=0; i<d_nf[eqc].size(); i++ ){
1506 if( std::find( d_ff[p][cbase].begin(), d_ff[p][cbase].end(), d_nf[eqc][i] )==d_ff[p][cbase].end() ){
1507 d_ff[p][cbase].insert( d_ff[p][cbase].end(), d_nf[eqc].begin(), d_nf[eqc].end() );
1508 }else{
1509 //if it is a duplicate venn region, it must be empty since it is coming from syntactically disjoint siblings TODO?
1510 }
1511 }
1512 }else{
1513 Trace("sets-nf-debug") << "..already processed parent " << p << " for " << cbase << std::endl;
1514 }
1515 }
1516 }
1517 }
1518 }
1519 }else{
1520 Assert( hasProcessed() );
1521 }
1522 }
1523 }
1524
1525 void TheorySetsPrivate::checkMinCard( std::vector< Node >& lemmas ) {
1526
1527 for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
1528 Node eqc = d_set_eqc[i];
1529 //get members in class
1530 std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc );
1531 if( itm!=d_pol_mems[0].end() ){
1532 std::vector< Node > exp;
1533 std::vector< Node > members;
1534 Node cardTerm;
1535 std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc );
1536 if( it!=d_eqc_to_card_term.end() ){
1537 cardTerm = it->second;
1538 }else{
1539 cardTerm = NodeManager::currentNM()->mkNode( kind::CARD, eqc );
1540 }
1541 for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){
1542 /*
1543 for( unsigned j=0; j<members.size(); j++ ){
1544 if( !ee_areDisequal( members[j], itmm->second ) ){
1545 Assert( !ee_areEqual( members[j], itmm->second ) );
1546
1547 }
1548 }
1549 */
1550 members.push_back( itmm->first );
1551 exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, itmm->first, cardTerm[0] ) );
1552 }
1553 if( members.size()>1 ){
1554 exp.push_back( NodeManager::currentNM()->mkNode( kind::DISTINCT, members ) );
1555 }
1556 if( !members.empty() ){
1557 Node conc = NodeManager::currentNM()->mkNode( kind::GEQ, cardTerm, NodeManager::currentNM()->mkConst( Rational( members.size() ) ) );
1558 Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ), conc );
1559 Trace("sets-lemma") << "Sets::Lemma : " << lem << " by mincard" << std::endl;
1560 lemmas.push_back( lem );
1561 }
1562 }
1563 }
1564 }
1565
1566 void TheorySetsPrivate::flushLemmas( std::vector< Node >& lemmas, bool preprocess ) {
1567 for( unsigned i=0; i<lemmas.size(); i++ ){
1568 flushLemma( lemmas[i], preprocess );
1569 }
1570 lemmas.clear();
1571 }
1572
1573 void TheorySetsPrivate::flushLemma( Node lem, bool preprocess ) {
1574 if( d_lemmas_produced.find(lem)==d_lemmas_produced.end() ){
1575 Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
1576 d_lemmas_produced.insert(lem);
1577 d_external.d_out->lemma(lem, false, preprocess);
1578 d_sentLemma = true;
1579 }else{
1580 Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
1581 }
1582 }
1583
1584 Node TheorySetsPrivate::getProxy( Node n ) {
1585 if( n.getKind()==kind::EMPTYSET || n.getKind()==kind::SINGLETON || n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS || n.getKind()==kind::UNION ){
1586 NodeMap::const_iterator it = d_proxy.find( n );
1587 if( it==d_proxy.end() ){
1588 Node k = NodeManager::currentNM()->mkSkolem( "sp", n.getType(), "proxy for set" );
1589 d_proxy[n] = k;
1590 d_proxy_to_term[k] = n;
1591 Node eq = k.eqNode( n );
1592 Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
1593 d_external.d_out->lemma( eq );
1594 if( n.getKind()==kind::SINGLETON ){
1595 Node slem = NodeManager::currentNM()->mkNode( kind::MEMBER, n[0], k );
1596 Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton" << std::endl;
1597 d_external.d_out->lemma( slem );
1598 d_sentLemma = true;
1599 }
1600 return k;
1601 }else{
1602 return (*it).second;
1603 }
1604 }else{
1605 return n;
1606 }
1607 }
1608
1609 Node TheorySetsPrivate::getCongruent( Node n ) {
1610 Assert( d_equalityEngine.hasTerm( n ) );
1611 std::map< Node, Node >::iterator it = d_congruent.find( n );
1612 if( it==d_congruent.end() ){
1613 return n;
1614 }else{
1615 return it->second;
1616 }
1617 }
1618
1619 Node TheorySetsPrivate::getEmptySet( TypeNode tn ) {
1620 std::map< TypeNode, Node >::iterator it = d_emptyset.find( tn );
1621 if( it==d_emptyset.end() ){
1622 Node n = NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
1623 d_emptyset[tn] = n;
1624 return n;
1625 }else{
1626 return it->second;
1627 }
1628 }
1629 Node TheorySetsPrivate::getUnivSet( TypeNode tn ) {
1630 std::map< TypeNode, Node >::iterator it = d_univset.find( tn );
1631 if( it==d_univset.end() ){
1632 Node n = NodeManager::currentNM()->mkNullaryOperator(tn, kind::UNIVERSE_SET);
1633 for( it = d_univset.begin(); it != d_univset.end(); ++it ){
1634 Node n1;
1635 Node n2;
1636 if( tn.isSubtypeOf( it->first ) ){
1637 n1 = n;
1638 n2 = it->second;
1639 }else if( it->first.isSubtypeOf( tn ) ){
1640 n1 = it->second;
1641 n2 = n;
1642 }
1643 if( !n1.isNull() ){
1644 Node ulem = NodeManager::currentNM()->mkNode( kind::SUBSET, n1, n2 );
1645 Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" << std::endl;
1646 d_external.d_out->lemma( ulem );
1647 d_sentLemma = true;
1648 }
1649 }
1650 d_univset[tn] = n;
1651 return n;
1652 }else{
1653 return it->second;
1654 }
1655 }
1656
1657 bool TheorySetsPrivate::hasLemmaCached( Node lem ) {
1658 return d_lemmas_produced.find(lem)!=d_lemmas_produced.end();
1659 }
1660
1661 bool TheorySetsPrivate::hasProcessed() {
1662 return d_conflict || d_sentLemma || d_addedFact;
1663 }
1664
1665 void TheorySetsPrivate::debugPrintSet( Node s, const char * c ) {
1666 if( s.getNumChildren()==0 ){
1667 NodeMap::const_iterator it = d_proxy_to_term.find( s );
1668 if( it!=d_proxy_to_term.end() ){
1669 debugPrintSet( (*it).second, c );
1670 }else{
1671 Trace(c) << s;
1672 }
1673 }else{
1674 Trace(c) << "(" << s.getOperator();
1675 for( unsigned i=0; i<s.getNumChildren(); i++ ){
1676 Trace(c) << " ";
1677 debugPrintSet( s[i], c );
1678 }
1679 Trace(c) << ")";
1680 }
1681 }
1682
1683 void TheorySetsPrivate::lastCallEffortCheck() {
1684 Trace("sets") << "----- Last call effort check ------" << std::endl;
1685
1686 }
1687
1688 Node TheorySetsPrivate::getTypeConstraintSkolem(Node n, TypeNode tn)
1689 {
1690 std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
1691 if (it == d_tc_skolem[n].end())
1692 {
1693 Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn);
1694 d_tc_skolem[n][tn] = k;
1695 return k;
1696 }
1697 return it->second;
1698 }
1699
1700 /**************************** TheorySetsPrivate *****************************/
1701 /**************************** TheorySetsPrivate *****************************/
1702 /**************************** TheorySetsPrivate *****************************/
1703
1704 void TheorySetsPrivate::check(Theory::Effort level) {
1705 Trace("sets-check") << "Sets check effort " << level << std::endl;
1706 if( level == Theory::EFFORT_LAST_CALL ){
1707 lastCallEffortCheck();
1708 return;
1709 }
1710 while(!d_external.done() && !d_conflict) {
1711 // Get all the assertions
1712 Assertion assertion = d_external.get();
1713 TNode fact = assertion.assertion;
1714 Trace("sets-assert") << "Assert from input " << fact << std::endl;
1715 //assert the fact
1716 assertFact( fact, fact );
1717 }
1718 d_sentLemma = false;
1719 Trace("sets-check") << "Sets finished assertions effort " << level << std::endl;
1720 //invoke full effort check, relations check
1721 if( !d_conflict ){
1722 if( level == Theory::EFFORT_FULL ){
1723 if( !d_external.d_valuation.needCheck() ){
1724 fullEffortCheck();
1725 if( !d_conflict && !d_sentLemma ){
1726 //invoke relations solver
1727 d_rels->check(level);
1728 if( d_card_enabled && ( d_rels_enabled || options::setsExt() ) ){
1729 //if cardinality constraints are enabled,
1730 // then model construction may fail in there are relational operators, or universe set.
1731 // TODO: should internally check model, return unknown if fail
1732 d_full_check_incomplete = true;
1733 Trace("sets-incomplete") << "Sets : incomplete because of extended operators." << std::endl;
1734 }
1735 }
1736 if( d_full_check_incomplete ){
1737 d_external.d_out->setIncomplete();
1738 }
1739 }
1740 }else{
1741 if( options::setsRelEager() ){
1742 d_rels->check(level);
1743 }
1744 }
1745 }
1746 Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
1747 }/* TheorySetsPrivate::check() */
1748
1749 bool TheorySetsPrivate::needsCheckLastEffort() {
1750 if( !d_var_elim.empty() ){
1751 return true;
1752 }
1753 return false;
1754 }
1755
1756 /************************ Sharing ************************/
1757 /************************ Sharing ************************/
1758 /************************ Sharing ************************/
1759
1760 void TheorySetsPrivate::addSharedTerm(TNode n) {
1761 Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
1762 d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
1763 }
1764
1765 void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ){
1766 if( depth==arity ){
1767 if( t2!=NULL ){
1768 Node f1 = t1->getNodeData();
1769 Node f2 = t2->getNodeData();
1770 if( !ee_areEqual( f1, f2 ) ){
1771 Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
1772 vector< pair<TNode, TNode> > currentPairs;
1773 for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
1774 TNode x = f1[k];
1775 TNode y = f2[k];
1776 Assert( d_equalityEngine.hasTerm(x) );
1777 Assert( d_equalityEngine.hasTerm(y) );
1778 Assert( !ee_areDisequal( x, y ) );
1779 Assert( !ee_areCareDisequal( x, y ) );
1780 if( !d_equalityEngine.areEqual( x, y ) ){
1781 Trace("sets-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
1782 if( d_equalityEngine.isTriggerTerm(x, THEORY_SETS) && d_equalityEngine.isTriggerTerm(y, THEORY_SETS) ){
1783 TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_SETS);
1784 TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_SETS);
1785 currentPairs.push_back(make_pair(x_shared, y_shared));
1786 }else if( isCareArg( f1, k ) && isCareArg( f2, k ) ){
1787 //splitting on sets (necessary for handling set of sets properly)
1788 if( x.getType().isSet() ){
1789 Assert( y.getType().isSet() );
1790 if( !ee_areDisequal( x, y ) ){
1791 Trace("sets-cg-lemma") << "Should split on : " << x << "==" << y << std::endl;
1792 split( x.eqNode( y ) );
1793 }
1794 }
1795 }
1796 }
1797 }
1798 for (unsigned c = 0; c < currentPairs.size(); ++ c) {
1799 Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
1800 d_external.addCarePair(currentPairs[c].first, currentPairs[c].second);
1801 n_pairs++;
1802 }
1803 }
1804 }
1805 }else{
1806 if( t2==NULL ){
1807 if( depth<(arity-1) ){
1808 //add care pairs internal to each child
1809 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
1810 addCarePairs( &it->second, NULL, arity, depth+1, n_pairs );
1811 }
1812 }
1813 //add care pairs based on each pair of non-disequal arguments
1814 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
1815 std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
1816 ++it2;
1817 for( ; it2 != t1->d_data.end(); ++it2 ){
1818 if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
1819 if( !ee_areCareDisequal(it->first, it2->first) ){
1820 addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
1821 }
1822 }
1823 }
1824 }
1825 }else{
1826 //add care pairs based on product of indices, non-disequal arguments
1827 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
1828 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
1829 if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
1830 if( !ee_areCareDisequal(it->first, it2->first) ){
1831 addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
1832 }
1833 }
1834 }
1835 }
1836 }
1837 }
1838 }
1839
1840 void TheorySetsPrivate::computeCareGraph() {
1841 for( std::map< Kind, std::vector< Node > >::iterator it = d_op_list.begin(); it != d_op_list.end(); ++it ){
1842 if( it->first==kind::SINGLETON || it->first==kind::MEMBER ){
1843 unsigned n_pairs = 0;
1844 Trace("sets-cg-summary") << "Compute graph for sets, op=" << it->first << "..." << it->second.size() << std::endl;
1845 Trace("sets-cg") << "Build index for " << it->first << "..." << std::endl;
1846 std::map< TypeNode, quantifiers::TermArgTrie > index;
1847 unsigned arity = 0;
1848 //populate indices
1849 for( unsigned i=0; i<it->second.size(); i++ ){
1850 TNode f1 = it->second[i];
1851 Assert(d_equalityEngine.hasTerm(f1));
1852 Trace("sets-cg-debug") << "...build for " << f1 << std::endl;
1853 //break into index based on operator, and type of first argument (since some operators are parametric)
1854 TypeNode tn = f1[0].getType();
1855 std::vector< TNode > reps;
1856 bool hasCareArg = false;
1857 for( unsigned j=0; j<f1.getNumChildren(); j++ ){
1858 reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
1859 if( isCareArg( f1, j ) ){
1860 hasCareArg = true;
1861 }
1862 }
1863 if( hasCareArg ){
1864 Trace("sets-cg-debug") << "......adding." << std::endl;
1865 index[tn].addTerm( f1, reps );
1866 arity = reps.size();
1867 }else{
1868 Trace("sets-cg-debug") << "......skip." << std::endl;
1869 }
1870 }
1871 if( arity>0 ){
1872 //for each index
1873 for( std::map< TypeNode, quantifiers::TermArgTrie >::iterator iti = index.begin(); iti != index.end(); ++iti ){
1874 Trace("sets-cg") << "Process index " << iti->first << "..." << std::endl;
1875 addCarePairs( &iti->second, NULL, arity, 0, n_pairs );
1876 }
1877 }
1878 Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
1879 }
1880 }
1881 }
1882
1883 bool TheorySetsPrivate::isCareArg( Node n, unsigned a ) {
1884 if( d_equalityEngine.isTriggerTerm( n[a], THEORY_SETS ) ){
1885 return true;
1886 }else if( ( n.getKind()==kind::MEMBER || n.getKind()==kind::SINGLETON ) && a==0 && n[0].getType().isSet() ){
1887 return true;
1888 }else{
1889 return false;
1890 }
1891 }
1892
1893 EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
1894 Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
1895 if (d_equalityEngine.areEqual(a, b)) {
1896 // The terms are implied to be equal
1897 return EQUALITY_TRUE;
1898 }
1899 if (d_equalityEngine.areDisequal(a, b, false)) {
1900 // The terms are implied to be dis-equal
1901 return EQUALITY_FALSE;
1902 }
1903 return EQUALITY_UNKNOWN;
1904 /*
1905 Node aModelValue = d_external.d_valuation.getModelValue(a);
1906 if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; }
1907 Node bModelValue = d_external.d_valuation.getModelValue(b);
1908 if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; }
1909 if( aModelValue == bModelValue ) {
1910 // The term are true in current model
1911 return EQUALITY_TRUE_IN_MODEL;
1912 } else {
1913 return EQUALITY_FALSE_IN_MODEL;
1914 }
1915 */
1916 // }
1917 // //TODO: can we be more precise sometimes?
1918 // return EQUALITY_UNKNOWN;
1919 }
1920
1921 /******************** Model generation ********************/
1922 /******************** Model generation ********************/
1923 /******************** Model generation ********************/
1924
1925 bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
1926 {
1927 Trace("sets-model") << "Set collect model info" << std::endl;
1928 set<Node> termSet;
1929 // Compute terms appearing in assertions and shared terms
1930 d_external.computeRelevantTerms(termSet);
1931
1932 // Assert equalities and disequalities to the model
1933 if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
1934 {
1935 return false;
1936 }
1937
1938 std::map< Node, Node > mvals;
1939 for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
1940 Node eqc = d_set_eqc[i];
1941 if( termSet.find( eqc )==termSet.end() ){
1942 Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl;
1943 }else{
1944 std::vector< Node > els;
1945 bool is_base = !d_card_enabled || ( d_nf[eqc].size()==1 && d_nf[eqc][0]==eqc );
1946 if( is_base ){
1947 Trace("sets-model") << "Collect elements of base eqc " << eqc << std::endl;
1948 // members that must be in eqc
1949 std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc );
1950 if( itm!=d_pol_mems[0].end() ){
1951 for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){
1952 Node t = NodeManager::currentNM()->mkNode( kind::SINGLETON, itmm->first );
1953 els.push_back( t );
1954 }
1955 }
1956 }
1957 if( d_card_enabled ){
1958 TypeNode elementType = eqc.getType().getSetElementType();
1959 if( is_base ){
1960 std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc );
1961 if( it!=d_eqc_to_card_term.end() ){
1962 //slack elements from cardinality value
1963 Node v = d_external.d_valuation.getModelValue(it->second);
1964 Trace("sets-model") << "Cardinality of " << eqc << " is " << v << std::endl;
1965 Assert(v.getConst<Rational>() <= LONG_MAX, "Exceeded LONG_MAX in sets model");
1966 unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
1967 Assert( els.size()<=vu );
1968 while( els.size()<vu ){
1969 els.push_back( NodeManager::currentNM()->mkNode( kind::SINGLETON, NodeManager::currentNM()->mkSkolem( "msde", elementType ) ) );
1970 }
1971 }else{
1972 Trace("sets-model") << "No slack elements for " << eqc << std::endl;
1973 }
1974 }else{
1975 Trace("sets-model") << "Build value for " << eqc << " based on normal form, size = " << d_nf[eqc].size() << std::endl;
1976 //it is union of venn regions
1977 for( unsigned j=0; j<d_nf[eqc].size(); j++ ){
1978 Assert( mvals.find( d_nf[eqc][j] )!=mvals.end() );
1979 els.push_back( mvals[d_nf[eqc][j]] );
1980 }
1981 }
1982 }
1983 Node rep = NormalForm::mkBop( kind::UNION, els, eqc.getType() );
1984 rep = Rewriter::rewrite( rep );
1985 Trace("sets-model") << "* Assign representative of " << eqc << " to " << rep << std::endl;
1986 mvals[eqc] = rep;
1987 if (!m->assertEquality(eqc, rep, true))
1988 {
1989 return false;
1990 }
1991 m->assertSkeleton(rep);
1992 }
1993 }
1994 return true;
1995 }
1996
1997 /********************** Helper functions ***************************/
1998 /********************** Helper functions ***************************/
1999 /********************** Helper functions ***************************/
2000
2001 void TheorySetsPrivate::addEqualityToExp( Node a, Node b, std::vector< Node >& exp ) {
2002 if( a!=b ){
2003 Assert( ee_areEqual( a, b ) );
2004 exp.push_back( a.eqNode( b ) );
2005 }
2006 }
2007
2008 Node mkAnd(const std::vector<TNode>& conjunctions) {
2009 Assert(conjunctions.size() > 0);
2010
2011 std::set<TNode> all;
2012 for (unsigned i = 0; i < conjunctions.size(); ++i) {
2013 TNode t = conjunctions[i];
2014 if (t.getKind() == kind::AND) {
2015 for(TNode::iterator child_it = t.begin();
2016 child_it != t.end(); ++child_it) {
2017 Assert((*child_it).getKind() != kind::AND);
2018 all.insert(*child_it);
2019 }
2020 }
2021 else {
2022 all.insert(t);
2023 }
2024 }
2025
2026 Assert(all.size() > 0);
2027 if (all.size() == 1) {
2028 // All the same, or just one
2029 return conjunctions[0];
2030 }
2031
2032 NodeBuilder<> conjunction(kind::AND);
2033 std::set<TNode>::const_iterator it = all.begin();
2034 std::set<TNode>::const_iterator it_end = all.end();
2035 while (it != it_end) {
2036 conjunction << *it;
2037 ++ it;
2038 }
2039
2040 return conjunction;
2041 }/* mkAnd() */
2042
2043
2044 TheorySetsPrivate::Statistics::Statistics() :
2045 d_getModelValueTime("theory::sets::getModelValueTime")
2046 , d_mergeTime("theory::sets::merge_nodes::time")
2047 , d_processCard2Time("theory::sets::processCard2::time")
2048 , d_memberLemmas("theory::sets::lemmas::member", 0)
2049 , d_disequalityLemmas("theory::sets::lemmas::disequality", 0)
2050 , d_numVertices("theory::sets::vertices", 0)
2051 , d_numVerticesMax("theory::sets::vertices-max", 0)
2052 , d_numMergeEq1or2("theory::sets::merge1or2", 0)
2053 , d_numMergeEq3("theory::sets::merge3", 0)
2054 , d_numLeaves("theory::sets::leaves", 0)
2055 , d_numLeavesMax("theory::sets::leaves-max", 0)
2056 {
2057 smtStatisticsRegistry()->registerStat(&d_getModelValueTime);
2058 smtStatisticsRegistry()->registerStat(&d_mergeTime);
2059 smtStatisticsRegistry()->registerStat(&d_processCard2Time);
2060 smtStatisticsRegistry()->registerStat(&d_memberLemmas);
2061 smtStatisticsRegistry()->registerStat(&d_disequalityLemmas);
2062 smtStatisticsRegistry()->registerStat(&d_numVertices);
2063 smtStatisticsRegistry()->registerStat(&d_numVerticesMax);
2064 smtStatisticsRegistry()->registerStat(&d_numMergeEq1or2);
2065 smtStatisticsRegistry()->registerStat(&d_numMergeEq3);
2066 smtStatisticsRegistry()->registerStat(&d_numLeaves);
2067 smtStatisticsRegistry()->registerStat(&d_numLeavesMax);
2068 }
2069
2070
2071 TheorySetsPrivate::Statistics::~Statistics() {
2072 smtStatisticsRegistry()->unregisterStat(&d_getModelValueTime);
2073 smtStatisticsRegistry()->unregisterStat(&d_mergeTime);
2074 smtStatisticsRegistry()->unregisterStat(&d_processCard2Time);
2075 smtStatisticsRegistry()->unregisterStat(&d_memberLemmas);
2076 smtStatisticsRegistry()->unregisterStat(&d_disequalityLemmas);
2077 smtStatisticsRegistry()->unregisterStat(&d_numVertices);
2078 smtStatisticsRegistry()->unregisterStat(&d_numVerticesMax);
2079 smtStatisticsRegistry()->unregisterStat(&d_numMergeEq1or2);
2080 smtStatisticsRegistry()->unregisterStat(&d_numMergeEq3);
2081 smtStatisticsRegistry()->unregisterStat(&d_numLeaves);
2082 smtStatisticsRegistry()->unregisterStat(&d_numLeavesMax);
2083 }
2084
2085 void TheorySetsPrivate::propagate(Theory::Effort effort) {
2086
2087 }
2088
2089 bool TheorySetsPrivate::propagate(TNode literal) {
2090 Debug("sets-prop") << " propagate(" << literal << ")" << std::endl;
2091
2092 // If already in conflict, no more propagation
2093 if (d_conflict) {
2094 Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
2095 return false;
2096 }
2097
2098 // Propagate out
2099 bool ok = d_external.d_out->propagate(literal);
2100 if (!ok) {
2101 d_conflict = true;
2102 }
2103
2104 return ok;
2105 }/* TheorySetsPrivate::propagate(TNode) */
2106
2107
2108 void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
2109 d_equalityEngine.setMasterEqualityEngine(eq);
2110 }
2111
2112
2113 void TheorySetsPrivate::conflict(TNode a, TNode b)
2114 {
2115 d_conflictNode = explain(a.eqNode(b));
2116 d_external.d_out->conflict(d_conflictNode);
2117 Debug("sets") << "[sets] conflict: " << a << " iff " << b
2118 << ", explaination " << d_conflictNode << std::endl;
2119 Trace("sets-lemma") << "Equality Conflict : " << d_conflictNode << std::endl;
2120 d_conflict = true;
2121 }
2122
2123 Node TheorySetsPrivate::explain(TNode literal)
2124 {
2125 Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
2126 << std::endl;
2127
2128 bool polarity = literal.getKind() != kind::NOT;
2129 TNode atom = polarity ? literal : literal[0];
2130 std::vector<TNode> assumptions;
2131
2132 if(atom.getKind() == kind::EQUAL) {
2133 d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
2134 } else if(atom.getKind() == kind::MEMBER) {
2135 d_equalityEngine.explainPredicate(atom, polarity, assumptions);
2136 } else {
2137 Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
2138 << polarity << "); kind" << atom.getKind() << std::endl;
2139 Unhandled();
2140 }
2141
2142 return mkAnd(assumptions);
2143 }
2144
2145 void TheorySetsPrivate::preRegisterTerm(TNode node)
2146 {
2147 Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
2148 << std::endl;
2149 switch(node.getKind()) {
2150 case kind::EQUAL:
2151 // TODO: what's the point of this
2152 d_equalityEngine.addTriggerEquality(node);
2153 break;
2154 case kind::MEMBER:
2155 // TODO: what's the point of this
2156 d_equalityEngine.addTriggerPredicate(node);
2157 break;
2158 case kind::CARD:
2159 d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
2160 break;
2161 default:
2162 //if( node.getType().isSet() ){
2163 // d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
2164 //}else{
2165 d_equalityEngine.addTerm(node);
2166 //}
2167 break;
2168 }
2169 }
2170
2171 Node TheorySetsPrivate::expandDefinition(LogicRequest &logicRequest, Node n) {
2172 Debug("sets-proc") << "expandDefinition : " << n << std::endl;
2173 if( n.getKind()==kind::UNIVERSE_SET || n.getKind()==kind::COMPLEMENT || n.getKind()==kind::JOIN_IMAGE ){
2174 if( !options::setsExt() ){
2175 std::stringstream ss;
2176 ss << "Extended set operators are not supported in default mode, try --sets-ext.";
2177 throw LogicException(ss.str());
2178 }
2179 }
2180 return n;
2181 }
2182
2183 Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
2184 Debug("sets-proc") << "ppAssert : " << in << std::endl;
2185 Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
2186
2187 //TODO: allow variable elimination for sets when setsExt = true
2188
2189 //this is based off of Theory::ppAssert
2190 Node var;
2191 if (in.getKind() == kind::EQUAL) {
2192 if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
2193 (in[1].getType()).isSubtypeOf(in[0].getType()) ){
2194 if( !in[0].getType().isSet() || !options::setsExt() ){
2195 outSubstitutions.addSubstitution(in[0], in[1]);
2196 var = in[0];
2197 status = Theory::PP_ASSERT_STATUS_SOLVED;
2198 }
2199 }else if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
2200 (in[0].getType()).isSubtypeOf(in[1].getType())){
2201 if( !in[1].getType().isSet() || !options::setsExt() ){
2202 outSubstitutions.addSubstitution(in[1], in[0]);
2203 var = in[1];
2204 status = Theory::PP_ASSERT_STATUS_SOLVED;
2205 }
2206 }else if (in[0].isConst() && in[1].isConst()) {
2207 if (in[0] != in[1]) {
2208 status = Theory::PP_ASSERT_STATUS_CONFLICT;
2209 }
2210 }
2211 }
2212
2213 if( status==Theory::PP_ASSERT_STATUS_SOLVED ){
2214 Trace("sets-var-elim") << "Sets : ppAssert variable eliminated : " << in << ", var = " << var << std::endl;
2215 /*
2216 if( var.getType().isSet() ){
2217 //we must ensure that subs is included in the universe set
2218 d_var_elim[var] = true;
2219 }
2220 */
2221 if( options::setsExt() ){
2222 Assert( !var.getType().isSet() );
2223 }
2224 }
2225 return status;
2226 }
2227
2228 void TheorySetsPrivate::presolve() {
2229
2230 }
2231
2232 /**************************** eq::NotifyClass *****************************/
2233 /**************************** eq::NotifyClass *****************************/
2234 /**************************** eq::NotifyClass *****************************/
2235
2236
2237 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
2238 {
2239 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
2240 << " value = " << value << std::endl;
2241 if (value) {
2242 return d_theory.propagate(equality);
2243 } else {
2244 // We use only literal triggers so taking not is safe
2245 return d_theory.propagate(equality.notNode());
2246 }
2247 }
2248
2249 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
2250 {
2251 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
2252 << " value = " << value << std::endl;
2253 if (value) {
2254 return d_theory.propagate(predicate);
2255 } else {
2256 return d_theory.propagate(predicate.notNode());
2257 }
2258 }
2259
2260 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
2261 {
2262 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
2263 << " t1 = " << t1 << " t2 = " << t2 << " value = " << value << std::endl;
2264 d_theory.propagate( value ? t1.eqNode( t2 ) : t1.eqNode( t2 ).negate() );
2265 return true;
2266 }
2267
2268 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
2269 {
2270 Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
2271 d_theory.conflict(t1, t2);
2272 }
2273
2274 void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
2275 {
2276 Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
2277 d_theory.eqNotifyNewClass(t);
2278 }
2279
2280 void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
2281 {
2282 Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
2283 d_theory.eqNotifyPreMerge(t1, t2);
2284 }
2285
2286 void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
2287 {
2288 Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
2289 d_theory.eqNotifyPostMerge(t1, t2);
2290 }
2291
2292 void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
2293 {
2294 Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
2295 d_theory.eqNotifyDisequal(t1, t2, reason);
2296 }
2297
2298 }/* CVC4::theory::sets namespace */
2299 }/* CVC4::theory namespace */
2300 }/* CVC4 namespace */