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