projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Make statistics output consistent. (#1647)
[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 Node mctt = d_most_common_type_term[s];
743 std::vector< Node > exp;
744 exp.push_back( it2->second );
745 Assert( ee_areEqual( mctt, it2->second[1] ) );
746 exp.push_back( mctt.eqNode( it2->second[1] ) );
747 Node etc = TypeNode::getEnsureTypeCondition( it2->first, mct );
748 if( !etc.isNull() ){
749 assertInference( etc, exp, lemmas, "subtype-clash" );
750 if( d_conflict ){
751 return;
752 }
753 }else{
754 // very strange situation : we have a member in a set that is not a subtype, and we do not have a type condition for it
755 d_full_check_incomplete = true;
756 Trace("sets-incomplete") << "Sets : incomplete because of unknown type constraint." << std::endl;
757 }
758 }
759 }
760 }
761 }
762 }
763
764 void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) {
765 Trace("sets") << "Downwards closure..." << std::endl;
766 //downwards closure
767 for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){
768 std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( it->first );
769 if( itn!=d_nvar_sets.end() ){
770 for( unsigned j=0; j<itn->second.size(); j++ ){
771 if( d_congruent.find( itn->second[j] )==d_congruent.end() ){
772 for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
773 Node mem = it2->second;
774 Node eq_set = itn->second[j];
775 Assert( d_equalityEngine.areEqual( mem[1], eq_set ) );
776 if( mem[1]!=eq_set ){
777 Trace("sets-debug") << "Downwards closure based on " << mem << ", eq_set = " << eq_set << std::endl;
778 if( !options::setsProxyLemmas() ){
779 Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
780 nmem = Rewriter::rewrite( nmem );
781 std::vector< Node > exp;
782 exp.push_back( mem );
783 exp.push_back( mem[1].eqNode( eq_set ) );
784 assertInference( nmem, exp, lemmas, "downc" );
785 if( d_conflict ){
786 return;
787 }
788 }else{
789 //use proxy set
790 Node k = getProxy( eq_set );
791 Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k );
792 Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
793 nmem = Rewriter::rewrite( nmem );
794 std::vector< Node > exp;
795 if( ee_areEqual( mem, pmem ) ){
796 exp.push_back( pmem );
797 }else{
798 nmem = NodeManager::currentNM()->mkNode( kind::OR, pmem.negate(), nmem );
799 }
800 assertInference( nmem, exp, lemmas, "downc" );
801 }
802 }
803 }
804 }
805 }
806 }
807 }
808 }
809
810 void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) {
811 //upwards closure
812 for( std::map< Kind, std::map< Node, std::map< Node, Node > > >::iterator itb = d_bop_index.begin(); itb != d_bop_index.end(); ++itb ){
813 Kind k = itb->first;
814 Trace("sets") << "Upwards closure " << k << "..." << std::endl;
815 for( std::map< Node, std::map< Node, Node > >::iterator it = itb->second.begin(); it != itb->second.end(); ++it ){
816 Node r1 = it->first;
817 //see if there are members in first argument r1
818 std::map< Node, std::map< Node, Node > >::iterator itm1 = d_pol_mems[0].find( r1 );
819 if( itm1!=d_pol_mems[0].end() || k==kind::UNION ){
820 for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
821 Node r2 = it2->first;
822 //see if there are members in second argument
823 std::map< Node, std::map< Node, Node > >::iterator itm2 = d_pol_mems[0].find( r2 );
824 std::map< Node, std::map< Node, Node > >::iterator itm2n = d_pol_mems[1].find( r2 );
825 if( itm2!=d_pol_mems[0].end() || k!=kind::INTERSECTION ){
826 Trace("sets-debug") << "Checking " << it2->second << ", members = " << (itm1!=d_pol_mems[0].end()) << ", " << (itm2!=d_pol_mems[0].end()) << std::endl;
827 //for all members of r1
828 if( itm1!=d_pol_mems[0].end() ){
829 for( std::map< Node, Node >::iterator itm1m = itm1->second.begin(); itm1m != itm1->second.end(); ++itm1m ){
830 Node xr = itm1m->first;
831 Node x = itm1m->second[0];
832 Trace("sets-debug") << "checking membership " << xr << " " << itm1m->second << std::endl;
833 std::vector< Node > exp;
834 exp.push_back( itm1m->second );
835 addEqualityToExp( it2->second[0], itm1m->second[1], exp );
836 bool valid = false;
837 int inferType = 0;
838 if( k==kind::UNION ){
839 valid = true;
840 }else if( k==kind::INTERSECTION ){
841 //conclude x is in it2->second
842 //if also existing in members of r2
843 bool in_r2 = itm2!=d_pol_mems[0].end() && itm2->second.find( xr )!=itm2->second.end();
844 if( in_r2 ){
845 exp.push_back( itm2->second[xr] );
846 addEqualityToExp( it2->second[1], itm2->second[xr][1], exp );
847 addEqualityToExp( x, itm2->second[xr][0], exp );
848 valid = true;
849 }else{
850 // if not, check whether it is definitely not a member, if unknown, split
851 bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2n->second.end();
852 if( !not_in_r2 ){
853 exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ) );
854 valid = true;
855 inferType = 1;
856 }
857 }
858 }else{
859 Assert( k==kind::SETMINUS );
860 /*
861 std::map< Node, std::map< Node, Node > >::iterator itnm2 = d_pol_mems[1].find( r2 );
862 if( itnm2!=d_pol_mems[1].end() ){
863 bool not_in_r2 = itnm2->second.find( xr )!=itnm2->second.end();
864 if( not_in_r2 ){
865 exp.push_back( itnm2->second[xr] );
866 if( it2->second[1]!=itnm2->second[xr][1] ){
867 Assert( d_equalityEngine.areEqual( it2->second[1], itnm2->second[xr][1] ) );
868 exp.push_back( it2->second[1].eqNode( itnm2->second[xr][1] ) );
869 }
870 if( x!=itnm2->second[xr][0] ){
871 Assert( d_equalityEngine.areEqual( x, itnm2->second[xr][0] ) );
872 exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, x, itnm2->second[xr][0] ) );
873 }
874 valid = true;
875 }
876 }
877 */
878 if( !valid ){
879 bool in_r2 = itm2!=d_pol_mems[0].end() && itm2->second.find( xr )!=itm2->second.end();
880 if( !in_r2 ){
881 // must add lemma for set minus since non-membership in this case is not explained
882 exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ).negate() );
883 valid = true;
884 inferType = 1;
885 }
886 }
887 }
888 if( valid ){
889 Node rr = d_equalityEngine.getRepresentative( it2->second );
890 if( !isMember( x, rr ) ){
891 Node kk = getProxy( it2->second );
892 Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, x, kk );
893 assertInference( fact, exp, lemmas, "upc", inferType );
894 if( d_conflict ){
895 return;
896 }
897 }
898 }
899 Trace("sets-debug") << "done checking membership " << xr << " " << itm1m->second << std::endl;
900 }
901 }
902 if( k==kind::UNION ){
903 if( itm2!=d_pol_mems[0].end() ){
904 //for all members of r2
905 for( std::map< Node, Node >::iterator itm2m = itm2->second.begin(); itm2m != itm2->second.end(); ++itm2m ){
906 Node x = itm2m->second[0];
907 Node rr = d_equalityEngine.getRepresentative( it2->second );
908 if( !isMember( x, rr ) ){
909 std::vector< Node > exp;
910 exp.push_back( itm2m->second );
911 addEqualityToExp( it2->second[1], itm2m->second[1], exp );
912 Node k = getProxy( it2->second );
913 Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, x, k );
914 assertInference( fact, exp, lemmas, "upc2" );
915 if( d_conflict ){
916 return;
917 }
918 }
919 }
920 }
921 }
922 }
923 }
924 }
925 }
926 }
927 if( !hasProcessed() ){
928 if( options::setsExt() ){
929 //universal sets
930 Trace("sets-debug") << "Check universe sets..." << std::endl;
931 //all elements must be in universal set
932 for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){
933 //if equivalence class contains a variable
934 std::map< Node, Node >::iterator itv = d_var_set.find( it->first );
935 if( itv!=d_var_set.end() ){
936 //the variable in the equivalence class
937 Node v = itv->second;
938 std::map< TypeNode, Node > univ_set;
939 for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
940 Node e = it2->second[0];
941 TypeNode tn = NodeManager::currentNM()->mkSetType( e.getType() );
942 Node u;
943 std::map< TypeNode, Node >::iterator itu = univ_set.find( tn );
944 if( itu==univ_set.end() ){
945 std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn );
946 // if the universe does not yet exist, or is not in this equivalence class
947 if( itu==d_eqc_univset.end() || itu->second!=it->first ){
948 u = getUnivSet( tn );
949 }
950 univ_set[tn] = u;
951 }else{
952 u = itu->second;
953 }
954 if( !u.isNull() ){
955 Assert( it2->second.getKind()==kind::MEMBER );
956 std::vector< Node > exp;
957 exp.push_back( it2->second );
958 if( v!=it2->second[1] ){
959 exp.push_back( v.eqNode( it2->second[1] ) );
960 }
961 Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, it2->second[0], u );
962 assertInference( fact, exp, lemmas, "upuniv" );
963 if( d_conflict ){
964 return;
965 }
966 }
967 }
968 }
969 }
970 }
971 }
972 }
973
974 void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) {
975 //disequalities
976 Trace("sets") << "Disequalities..." << std::endl;
977 for(NodeBoolMap::const_iterator it=d_deq.begin(); it !=d_deq.end(); ++it) {
978 if( (*it).second ){
979 Node deq = (*it).first;
980 //check if it is already satisfied
981 Assert( d_equalityEngine.hasTerm( deq[0] ) && d_equalityEngine.hasTerm( deq[1] ) );
982 Node r1 = d_equalityEngine.getRepresentative( deq[0] );
983 Node r2 = d_equalityEngine.getRepresentative( deq[1] );
984 bool is_sat = isSetDisequalityEntailed( r1, r2 );
985 /*
986 if( !is_sat ){
987 //try to make one of them empty
988 for( unsigned e=0; e<2; e++ ){
989 }
990 }
991 */
992 Trace("sets-debug") << "Check disequality " << deq << ", is_sat = " << is_sat << std::endl;
993 //will process regardless of sat/processed/unprocessed
994 d_deq[deq] = false;
995
996 if( !is_sat ){
997 if( d_deq_processed.find( deq )==d_deq_processed.end() ){
998 d_deq_processed.insert( deq );
999 d_deq_processed.insert( deq[1].eqNode( deq[0] ) );
1000 Trace("sets") << "Process Disequality : " << deq.negate() << std::endl;
1001 TypeNode elementType = deq[0].getType().getSetElementType();
1002 Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType);
1003 Node mem1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[0] );
1004 Node mem2 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[1] );
1005 Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::EQUAL, mem1, mem2 ).negate() );
1006 lem = Rewriter::rewrite( lem );
1007 assertInference( lem, d_emp_exp, lemmas, "diseq", 1 );
1008 flushLemmas( lemmas );
1009 if( hasProcessed() ){
1010 return;
1011 }
1012 }
1013 }
1014 }
1015 }
1016 }
1017
1018 void TheorySetsPrivate::checkCardBuildGraph( std::vector< Node >& lemmas ) {
1019 Trace("sets") << "Cardinality graph..." << std::endl;
1020 //first, ensure cardinality relationships are added as lemmas for all non-basic set terms
1021 for( unsigned i=0; i<d_set_eqc.size(); i++ ){
1022 Node eqc = d_set_eqc[i];
1023 std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
1024 if( itn!=d_nvar_sets.end() ){
1025 for( unsigned j=0; j<itn->second.size(); j++ ){
1026 Node n = itn->second[j];
1027 if( d_congruent.find( n )==d_congruent.end() ){
1028 //if setminus, do for intersection instead
1029 if( n.getKind()==kind::SETMINUS ){
1030 n = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, n[0], n[1] ) );
1031 }
1032 registerCardinalityTerm( n, lemmas );
1033 }
1034 }
1035 }
1036 }
1037 Trace("sets") << "Done cardinality graph" << std::endl;
1038 }
1039
1040 void TheorySetsPrivate::registerCardinalityTerm( Node n, std::vector< Node >& lemmas ){
1041 if( d_card_processed.find( n )==d_card_processed.end() ){
1042 d_card_processed.insert( n );
1043 Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
1044 std::vector< Node > cterms;
1045 if( n.getKind()==kind::INTERSECTION ){
1046 for( unsigned e=0; e<2; e++ ){
1047 Node s = NodeManager::currentNM()->mkNode( kind::SETMINUS, n[e], n[1-e] );
1048 cterms.push_back( s );
1049 }
1050 Node pos_lem = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::CARD, n ), d_zero );
1051 assertInference( pos_lem, d_emp_exp, lemmas, "pcard", 1 );
1052 }else{
1053 cterms.push_back( n );
1054 }
1055 for( unsigned k=0; k<cterms.size(); k++ ){
1056 Node nn = cterms[k];
1057 Node nk = getProxy( nn );
1058 Node pos_lem = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::CARD, nk ), d_zero );
1059 assertInference( pos_lem, d_emp_exp, lemmas, "pcard", 1 );
1060 if( nn!=nk ){
1061 Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::CARD, nk ),
1062 NodeManager::currentNM()->mkNode( kind::CARD, nn ) );
1063 lem = Rewriter::rewrite( lem );
1064 Trace("sets-card") << " " << k << " : " << lem << std::endl;
1065 assertInference( lem, d_emp_exp, lemmas, "card", 1 );
1066 }
1067 }
1068 }
1069 }
1070
1071 void TheorySetsPrivate::checkCardCycles( std::vector< Node >& lemmas ) {
1072 Trace("sets") << "Check cardinality cycles..." << std::endl;
1073 //build order of equivalence classes, also build cardinality graph
1074 std::vector< Node > set_eqc_tmp;
1075 set_eqc_tmp.insert( set_eqc_tmp.end(), d_set_eqc.begin(), d_set_eqc.end() );
1076 d_set_eqc.clear();
1077 d_card_parent.clear();
1078 for( unsigned i=0; i<set_eqc_tmp.size(); i++ ){
1079 std::vector< Node > curr;
1080 std::vector< Node > exp;
1081 checkCardCyclesRec( set_eqc_tmp[i], curr, exp, lemmas );
1082 flushLemmas( lemmas );
1083 if( hasProcessed() ){
1084 return;
1085 }
1086 }
1087 Trace("sets") << "Done check cardinality cycles" << std::endl;
1088 }
1089
1090 void TheorySetsPrivate::checkCardCyclesRec( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp, std::vector< Node >& lemmas ) {
1091 if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
1092 Trace("sets-debug") << "Found venn region loop..." << std::endl;
1093 if( curr.size()>1 ){
1094 //all regions must be equal
1095 std::vector< Node > conc;
1096 for( unsigned i=1; i<curr.size(); i++ ){
1097 conc.push_back( curr[0].eqNode( curr[i] ) );
1098 }
1099 Node fact = conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::AND, conc );
1100 assertInference( fact, exp, lemmas, "card_cycle" );
1101 flushLemmas( lemmas );
1102 }else{
1103 //should be guaranteed based on not exploring equal parents
1104 Assert( false );
1105 }
1106 }else if( std::find( d_set_eqc.begin(), d_set_eqc.end(), eqc )==d_set_eqc.end() ){
1107 curr.push_back( eqc );
1108 TypeNode tn = eqc.getType();
1109 bool is_empty = eqc==d_eqc_emptyset[tn];
1110 Node emp_set = getEmptySet( tn );
1111 std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
1112 if( itn!=d_nvar_sets.end() ){
1113 for( unsigned j=0; j<itn->second.size(); j++ ){
1114 Node n = itn->second[j];
1115 if( n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS ){
1116 Trace("sets-debug") << "Build cardinality parents for " << n << "..." << std::endl;
1117 std::vector< Node > sib;
1118 unsigned true_sib = 0;
1119 if( n.getKind()==kind::INTERSECTION ){
1120 d_card_base[n] = n;
1121 for( unsigned e=0; e<2; e++ ){
1122 Node sm = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::SETMINUS, n[e], n[1-e] ) );
1123 sib.push_back( sm );
1124 }
1125 true_sib = 2;
1126 }else{
1127 Node si = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, n[0], n[1] ) );
1128 sib.push_back( si );
1129 d_card_base[n] = si;
1130 Node osm = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::SETMINUS, n[1], n[0] ) );
1131 sib.push_back( osm );
1132 true_sib = 1;
1133 }
1134 Node u = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::UNION, n[0], n[1] ) );
1135 if( !d_equalityEngine.hasTerm( u ) ){
1136 u = Node::null();
1137 }
1138 unsigned n_parents = true_sib + ( u.isNull() ? 0 : 1 );
1139 //if this set is empty
1140 if( is_empty ){
1141 Assert( ee_areEqual( n, emp_set ) );
1142 Trace("sets-debug") << " empty, parents equal siblings" << std::endl;
1143 std::vector< Node > conc;
1144 //parent equal siblings
1145 for( unsigned e=0; e<true_sib; e++ ){
1146 if( d_equalityEngine.hasTerm( sib[e] ) && !ee_areEqual( n[e], sib[e] ) ){
1147 conc.push_back( n[e].eqNode( sib[e] ) );
1148 }
1149 }
1150 assertInference( conc, n.eqNode( emp_set ), lemmas, "cg_emp" );
1151 flushLemmas( lemmas );
1152 if( hasProcessed() ){
1153 return;
1154 }else{
1155 //justify why there is no edge to parents (necessary?)
1156 for( unsigned e=0; e<n_parents; e++ ){
1157 Node p = (e==true_sib) ? u : n[e];
1158
1159 }
1160 }
1161 }else{
1162 std::vector< Node > card_parents;
1163 std::vector< int > card_parent_ids;
1164 //check if equal to a parent
1165 for( unsigned e=0; e<n_parents; e++ ){
1166 Trace("sets-debug") << " check parent " << e << "/" << n_parents << std::endl;
1167 bool is_union = e==true_sib;
1168 Node p = (e==true_sib) ? u : n[e];
1169 Trace("sets-debug") << " check relation to parent " << p << ", isu=" << is_union << "..." << std::endl;
1170 //if parent is empty
1171 if( ee_areEqual( p, emp_set ) ){
1172 Trace("sets-debug") << " it is empty..." << std::endl;
1173 Assert( !ee_areEqual( n, emp_set ) );
1174 assertInference( n.eqNode( emp_set ), p.eqNode( emp_set ), lemmas, "cg_emppar" );
1175 if( hasProcessed() ){
1176 return;
1177 }
1178 //if we are equal to a parent
1179 }else if( ee_areEqual( p, n ) ){
1180 Trace("sets-debug") << " it is equal to this..." << std::endl;
1181 std::vector< Node > conc;
1182 std::vector< int > sib_emp_indices;
1183 if( is_union ){
1184 for( unsigned s=0; s<sib.size(); s++ ){
1185 sib_emp_indices.push_back( s );
1186 }
1187 }else{
1188 sib_emp_indices.push_back( e );
1189 }
1190 //sibling(s) are empty
1191 for( unsigned s=0; s<sib_emp_indices.size(); s++ ){
1192 unsigned si = sib_emp_indices[s];
1193 if( !ee_areEqual( sib[si], emp_set ) ){
1194 conc.push_back( sib[si].eqNode( emp_set ) );
1195 }else{
1196 Trace("sets-debug") << "Sibling " << sib[si] << " is already empty." << std::endl;
1197 }
1198 }
1199 if( !is_union && n.getKind()==kind::INTERSECTION && !u.isNull() ){
1200 //union is equal to other parent
1201 if( !ee_areEqual( u, n[1-e] ) ){
1202 conc.push_back( u.eqNode( n[1-e] ) );
1203 }
1204 }
1205 Trace("sets-debug") << "...derived " << conc.size() << " conclusions" << std::endl;
1206 assertInference( conc, n.eqNode( p ), lemmas, "cg_eqpar" );
1207 flushLemmas( lemmas );
1208 if( hasProcessed() ){
1209 return;
1210 }
1211 }else{
1212 Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
1213 //otherwise, we a syntactic subset of p
1214 card_parents.push_back( p );
1215 card_parent_ids.push_back( is_union ? 2 : e );
1216 }
1217 }
1218 Assert( d_card_parent[n].empty() );
1219 Trace("sets-debug") << "get parent representatives..." << std::endl;
1220 //for each parent, take their representatives
1221 for( unsigned k=0; k<card_parents.size(); k++ ){
1222 Node eqcc = d_equalityEngine.getRepresentative( card_parents[k] );
1223 Trace("sets-debug") << "Check card parent " << k << "/" << card_parents.size() << std::endl;
1224
1225 //if parent is singleton, then we should either be empty to equal to it
1226 std::map< Node, Node >::iterator itps = d_eqc_singleton.find( eqcc );
1227 if( itps!=d_eqc_singleton.end() ){
1228 bool eq_parent = false;
1229 std::vector< Node > exp;
1230 addEqualityToExp( card_parents[k], itps->second, exp );
1231 if( ee_areDisequal( n, emp_set ) ){
1232 exp.push_back( n.eqNode( emp_set ).negate() );
1233 eq_parent = true;
1234 }else{
1235 std::map< Node, std::map< Node, Node > >::iterator itpm = d_pol_mems[0].find( eqc );
1236 if( itpm!=d_pol_mems[0].end() && !itpm->second.empty() ){
1237 Node pmem = itpm->second.begin()->second;
1238 exp.push_back( pmem );
1239 addEqualityToExp( n, pmem[1], exp );
1240 eq_parent = true;
1241 }
1242 }
1243 //must be equal to parent
1244 if( eq_parent ){
1245 Node conc = n.eqNode( card_parents[k] );
1246 assertInference( conc, exp, lemmas, "cg_par_sing" );
1247 flushLemmas( lemmas );
1248 }else{
1249 //split on empty
1250 Trace("sets-nf") << "Split empty : " << n << std::endl;
1251 split( n.eqNode( emp_set ), 1 );
1252 }
1253 Assert( hasProcessed() );
1254 return;
1255 }else{
1256 bool dup = false;
1257 for( unsigned l=0; l<d_card_parent[n].size(); l++ ){
1258 if( eqcc==d_card_parent[n][l] ){
1259 Trace("sets-debug") << " parents " << l << " and " << k << " are equal, ids = " << card_parent_ids[l] << " " << card_parent_ids[k] << std::endl;
1260 dup = true;
1261 if( n.getKind()==kind::INTERSECTION ){
1262 Assert( card_parent_ids[l]!=2 );
1263 std::vector< Node > conc;
1264 if( card_parent_ids[k]==2 ){
1265 //intersection is equal to other parent
1266 unsigned pid = 1-card_parent_ids[l];
1267 if( !ee_areEqual( n[pid], n ) ){
1268 Trace("sets-debug") << " one of them is union, make equal to other..." << std::endl;
1269 conc.push_back( n[pid].eqNode( n ) );
1270 }
1271 }else{
1272 if( !ee_areEqual( card_parents[k], n ) ){
1273 Trace("sets-debug") << " neither is union, make equal to one parent..." << std::endl;
1274 //intersection is equal to one of the parents
1275 conc.push_back( card_parents[k].eqNode( n ) );
1276 }
1277 }
1278 assertInference( conc, card_parents[k].eqNode( d_card_parent[n][l] ), lemmas, "cg_pareq" );
1279 flushLemmas( lemmas );
1280 if( hasProcessed() ){
1281 return;
1282 }
1283 }
1284 }
1285 }
1286 if( !dup ){
1287 d_card_parent[n].push_back( eqcc );
1288 }
1289 }
1290 }
1291 //now recurse on parents (to ensure their normal will be computed after this eqc)
1292 exp.push_back( eqc.eqNode( n ) );
1293 for( unsigned k=0; k<d_card_parent[n].size(); k++ ){
1294 checkCardCyclesRec( d_card_parent[n][k], curr, exp, lemmas );
1295 if( hasProcessed() ){
1296 return;
1297 }
1298 }
1299 exp.pop_back();
1300 }
1301 }
1302 }
1303 }
1304 curr.pop_back();
1305 //parents now processed, can add to ordered list
1306 d_set_eqc.push_back( eqc );
1307 }else{
1308 //already processed
1309 }
1310 }
1311
1312 void TheorySetsPrivate::checkNormalForms( std::vector< Node >& lemmas, std::vector< Node >& intro_sets ){
1313 Trace("sets") << "Check normal forms..." << std::endl;
1314 // now, build normal form for each equivalence class
1315 // d_set_eqc is now sorted such that for each d_set_eqc[i], d_set_eqc[j],
1316 // if d_set_eqc[i] is a strict syntactic subterm of d_set_eqc[j], then i<j.
1317 d_ff.clear();
1318 d_nf.clear();
1319 for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
1320 checkNormalForm( d_set_eqc[i], intro_sets );
1321 if( hasProcessed() || !intro_sets.empty() ){
1322 return;
1323 }
1324 }
1325 Trace("sets") << "Done check normal forms" << std::endl;
1326 }
1327
1328 void TheorySetsPrivate::checkNormalForm( Node eqc, std::vector< Node >& intro_sets ){
1329 TypeNode tn = eqc.getType();
1330 Trace("sets") << "Compute normal form for " << eqc << std::endl;
1331 Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
1332 if( eqc==d_eqc_emptyset[tn] ){
1333 d_nf[eqc].clear();
1334 Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
1335 }else{
1336 //flat/normal forms are sets of equivalence classes
1337 Node base;
1338 std::vector< Node > comps;
1339 std::map< Node, std::map< Node, std::vector< Node > > >::iterator it = d_ff.find( eqc );
1340 if( it!=d_ff.end() ){
1341 for( std::map< Node, std::vector< Node > >::iterator itf = it->second.begin(); itf != it->second.end(); ++itf ){
1342 std::sort( itf->second.begin(), itf->second.end() );
1343 if( base.isNull() ){
1344 base = itf->first;
1345 }else{
1346 comps.push_back( itf->first );
1347 }
1348 Trace("sets-nf") << " F " << itf->first << " : ";
1349 if( Trace.isOn("sets-nf") ){
1350 Trace("sets-nf") << "{ ";
1351 for( unsigned k=0; k<itf->second.size(); k++ ){
1352 if( k>0 ){ Trace("sets-nf") << ", "; }
1353 Trace("sets-nf") << "[" << itf->second[k] << "]";
1354 }
1355 Trace("sets-nf") << " }" << std::endl;
1356 }
1357 Trace("sets-nf-debug") << " ...";
1358 debugPrintSet( itf->first, "sets-nf-debug" );
1359 Trace("sets-nf-debug") << std::endl;
1360 }
1361 }else{
1362 Trace("sets-nf") << "(no flat forms)" << std::endl;
1363 }
1364
1365 Assert( d_nf.find( eqc )==d_nf.end() );
1366 bool success = true;
1367 if( !base.isNull() ){
1368 Node emp_set = getEmptySet( tn );
1369 for( unsigned j=0; j<comps.size(); j++ ){
1370 //compare if equal
1371 std::vector< Node > c;
1372 c.push_back( base );
1373 c.push_back( comps[j] );
1374 std::vector< Node > only[2];
1375 std::vector< Node > common;
1376 Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs " << comps[j] << std::endl;
1377 unsigned k[2] = { 0, 0 };
1378 while( k[0]<d_ff[eqc][c[0]].size() || k[1]<d_ff[eqc][c[1]].size() ){
1379 bool proc = true;
1380 for( unsigned e=0; e<2; e++ ){
1381 if( k[e]==d_ff[eqc][c[e]].size() ){
1382 for( ; k[1-e]<d_ff[eqc][c[1-e]].size(); ++k[1-e] ){
1383 only[1-e].push_back( d_ff[eqc][c[1-e]][k[1-e]] );
1384 }
1385 proc = false;
1386 }
1387 }
1388 if( proc ){
1389 if( d_ff[eqc][c[0]][k[0]]==d_ff[eqc][c[1]][k[1]] ){
1390 common.push_back( d_ff[eqc][c[0]][k[0]] );
1391 k[0]++;
1392 k[1]++;
1393 }else if( d_ff[eqc][c[0]][k[0]]<d_ff[eqc][c[1]][k[1]] ){
1394 only[0].push_back( d_ff[eqc][c[0]][k[0]] );
1395 k[0]++;
1396 }else{
1397 only[1].push_back( d_ff[eqc][c[1]][k[1]] );
1398 k[1]++;
1399 }
1400 }
1401 }
1402 if( !only[0].empty() || !only[1].empty() ){
1403 if( Trace.isOn("sets-nf-debug") ){
1404 Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
1405 for( unsigned e=0; e<2; e++ ){
1406 Trace("sets-nf-debug") << " " << c[e] << " : { ";
1407 for( unsigned l=0; l<only[e].size(); l++ ){
1408 if( l>0 ){ Trace("sets-nf-debug") << ", "; }
1409 Trace("sets-nf-debug") << "[" << only[e][l] << "]";
1410 }
1411 Trace("sets-nf-debug") << " }" << std::endl;
1412 }
1413 }
1414 //try to make one empty, prefer the unique ones first
1415 for( unsigned e=0; e<3; e++ ){
1416 unsigned sz = e==2 ? common.size() : only[e].size();
1417 for( unsigned l=0; l<sz; l++ ){
1418 Node r = e==2 ? common[l] : only[e][l];
1419 Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
1420 Trace("sets-nf-debug") << " actual : ";
1421 debugPrintSet( r, "sets-nf-debug" );
1422 Trace("sets-nf-debug") << std::endl;
1423 Assert( !ee_areEqual( r, emp_set ) );
1424 if( !ee_areDisequal( r, emp_set ) && ( d_pol_mems[0].find( r )==d_pol_mems[0].end() || d_pol_mems[0][r].empty() ) ){
1425 //guess that its equal empty if it has no explicit members
1426 Trace("sets-nf") << " Split empty : " << r << std::endl;
1427 Trace("sets-nf") << "Actual Split : ";
1428 debugPrintSet( r, "sets-nf" );
1429 Trace("sets-nf") << std::endl;
1430 split( r.eqNode( emp_set ), 1 );
1431 Assert( hasProcessed() );
1432 return;
1433 }
1434 }
1435 }
1436 for( unsigned l=0; l<only[0].size(); l++ ){
1437 for( unsigned m=0; m<only[1].size(); m++ ){
1438 bool disjoint = false;
1439 Trace("sets-nf-debug") << "Try split " << only[0][l] << " against " << only[1][m] << std::endl;
1440 //split them
1441 for( unsigned e=0; e<2; e++ ){
1442 Node r1 = e==0 ? only[0][l] : only[1][m];
1443 Node r2 = e==0 ? only[1][m] : only[0][l];
1444 //check if their intersection exists modulo equality
1445 std::map< Node, Node >::iterator itb = d_bop_index[kind::INTERSECTION][r1].find( r2 );
1446 if( itb!=d_bop_index[kind::INTERSECTION][r1].end() ){
1447 Trace("sets-nf-debug") << "Split term already exists, but not in cardinality graph : " << itb->second << ", should be empty." << std::endl;
1448 //their intersection is empty (probably?)
1449 // e.g. these are two disjoint venn regions, proceed to next pair
1450 Assert( ee_areEqual( emp_set, itb->second ) );
1451 disjoint = true;
1452 break;
1453 }
1454 }
1455 if( !disjoint ){
1456 //simply introduce their intersection
1457 Assert( only[0][l]!=only[1][m] );
1458 Node kca = getProxy( only[0][l] );
1459 Node kcb = getProxy( only[1][m] );
1460 Node intro = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, kca, kcb ) );
1461 Trace("sets-nf") << " Intro split : " << only[0][l] << " against " << only[1][m] << ", term is " << intro << std::endl;
1462 intro_sets.push_back( intro );
1463 Assert( !d_equalityEngine.hasTerm( intro ) );
1464 return;
1465 }
1466 }
1467 }
1468 //should never get here
1469 success = false;
1470 }
1471 }
1472 if( success ){
1473 //normal form is flat form of base
1474 d_nf[eqc].insert( d_nf[eqc].end(), d_ff[eqc][base].begin(), d_ff[eqc][base].end() );
1475 Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
1476 }else{
1477 Trace("sets-nf") << "failed to build N " << eqc << std::endl;
1478 Assert( false );
1479 }
1480 }else{
1481 //normal form is this equivalence class
1482 d_nf[eqc].push_back( eqc );
1483 Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }" << std::endl;
1484 }
1485 if( success ){
1486 //send to parents
1487 std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
1488 if( itn!=d_nvar_sets.end() ){
1489 std::map< Node, std::map< Node, bool > > parents_proc;
1490 for( unsigned j=0; j<itn->second.size(); j++ ){
1491 Node n = itn->second[j];
1492 Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
1493 if( !d_card_parent[n].empty() ){
1494 Assert( d_card_base.find( n )!=d_card_base.end() );
1495 Node cbase = d_card_base[n];
1496 Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
1497 for( unsigned k=0; k<d_card_parent[n].size(); k++ ){
1498 Node p = d_card_parent[n][k];
1499 Trace("sets-nf-debug") << "Check parent " << p << std::endl;
1500 if( parents_proc[cbase].find( p )==parents_proc[cbase].end() ){
1501 parents_proc[cbase][p] = true;
1502 Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p << "] ), from " << n << "..." << std::endl;
1503 //for( unsigned i=0; i<d_nf[eqc].size(); i++ ){
1504 // Assert( std::find( d_ff[p][cbase].begin(), d_ff[p][cbase].end(), d_nf[eqc][i] )==d_ff[p][cbase].end() );
1505 //}
1506 for( unsigned i=0; i<d_nf[eqc].size(); i++ ){
1507 if( std::find( d_ff[p][cbase].begin(), d_ff[p][cbase].end(), d_nf[eqc][i] )==d_ff[p][cbase].end() ){
1508 d_ff[p][cbase].insert( d_ff[p][cbase].end(), d_nf[eqc].begin(), d_nf[eqc].end() );
1509 }else{
1510 //if it is a duplicate venn region, it must be empty since it is coming from syntactically disjoint siblings TODO?
1511 }
1512 }
1513 }else{
1514 Trace("sets-nf-debug") << "..already processed parent " << p << " for " << cbase << std::endl;
1515 }
1516 }
1517 }
1518 }
1519 }
1520 }else{
1521 Assert( hasProcessed() );
1522 }
1523 }
1524 }
1525
1526 void TheorySetsPrivate::checkMinCard( std::vector< Node >& lemmas ) {
1527
1528 for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
1529 Node eqc = d_set_eqc[i];
1530 //get members in class
1531 std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc );
1532 if( itm!=d_pol_mems[0].end() ){
1533 std::vector< Node > exp;
1534 std::vector< Node > members;
1535 Node cardTerm;
1536 std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc );
1537 if( it!=d_eqc_to_card_term.end() ){
1538 cardTerm = it->second;
1539 }else{
1540 cardTerm = NodeManager::currentNM()->mkNode( kind::CARD, eqc );
1541 }
1542 for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){
1543 /*
1544 for( unsigned j=0; j<members.size(); j++ ){
1545 if( !ee_areDisequal( members[j], itmm->second ) ){
1546 Assert( !ee_areEqual( members[j], itmm->second ) );
1547
1548 }
1549 }
1550 */
1551 members.push_back( itmm->first );
1552 exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, itmm->first, cardTerm[0] ) );
1553 }
1554 if( members.size()>1 ){
1555 exp.push_back( NodeManager::currentNM()->mkNode( kind::DISTINCT, members ) );
1556 }
1557 if( !members.empty() ){
1558 Node conc = NodeManager::currentNM()->mkNode( kind::GEQ, cardTerm, NodeManager::currentNM()->mkConst( Rational( members.size() ) ) );
1559 Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ), conc );
1560 Trace("sets-lemma") << "Sets::Lemma : " << lem << " by mincard" << std::endl;
1561 lemmas.push_back( lem );
1562 }
1563 }
1564 }
1565 }
1566
1567 void TheorySetsPrivate::flushLemmas( std::vector< Node >& lemmas, bool preprocess ) {
1568 for( unsigned i=0; i<lemmas.size(); i++ ){
1569 flushLemma( lemmas[i], preprocess );
1570 }
1571 lemmas.clear();
1572 }
1573
1574 void TheorySetsPrivate::flushLemma( Node lem, bool preprocess ) {
1575 if( d_lemmas_produced.find(lem)==d_lemmas_produced.end() ){
1576 Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
1577 d_lemmas_produced.insert(lem);
1578 d_external.d_out->lemma(lem, false, preprocess);
1579 d_sentLemma = true;
1580 }else{
1581 Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
1582 }
1583 }
1584
1585 Node TheorySetsPrivate::getProxy( Node n ) {
1586 if( n.getKind()==kind::EMPTYSET || n.getKind()==kind::SINGLETON || n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS || n.getKind()==kind::UNION ){
1587 NodeMap::const_iterator it = d_proxy.find( n );
1588 if( it==d_proxy.end() ){
1589 Node k = NodeManager::currentNM()->mkSkolem( "sp", n.getType(), "proxy for set" );
1590 d_proxy[n] = k;
1591 d_proxy_to_term[k] = n;
1592 Node eq = k.eqNode( n );
1593 Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
1594 d_external.d_out->lemma( eq );
1595 if( n.getKind()==kind::SINGLETON ){
1596 Node slem = NodeManager::currentNM()->mkNode( kind::MEMBER, n[0], k );
1597 Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton" << std::endl;
1598 d_external.d_out->lemma( slem );
1599 d_sentLemma = true;
1600 }
1601 return k;
1602 }else{
1603 return (*it).second;
1604 }
1605 }else{
1606 return n;
1607 }
1608 }
1609
1610 Node TheorySetsPrivate::getCongruent( Node n ) {
1611 Assert( d_equalityEngine.hasTerm( n ) );
1612 std::map< Node, Node >::iterator it = d_congruent.find( n );
1613 if( it==d_congruent.end() ){
1614 return n;
1615 }else{
1616 return it->second;
1617 }
1618 }
1619
1620 Node TheorySetsPrivate::getEmptySet( TypeNode tn ) {
1621 std::map< TypeNode, Node >::iterator it = d_emptyset.find( tn );
1622 if( it==d_emptyset.end() ){
1623 Node n = NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
1624 d_emptyset[tn] = n;
1625 return n;
1626 }else{
1627 return it->second;
1628 }
1629 }
1630 Node TheorySetsPrivate::getUnivSet( TypeNode tn ) {
1631 std::map< TypeNode, Node >::iterator it = d_univset.find( tn );
1632 if( it==d_univset.end() ){
1633 Node n = NodeManager::currentNM()->mkNullaryOperator(tn, kind::UNIVERSE_SET);
1634 for( it = d_univset.begin(); it != d_univset.end(); ++it ){
1635 Node n1;
1636 Node n2;
1637 if( tn.isSubtypeOf( it->first ) ){
1638 n1 = n;
1639 n2 = it->second;
1640 }else if( it->first.isSubtypeOf( tn ) ){
1641 n1 = it->second;
1642 n2 = n;
1643 }
1644 if( !n1.isNull() ){
1645 Node ulem = NodeManager::currentNM()->mkNode( kind::SUBSET, n1, n2 );
1646 Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" << std::endl;
1647 d_external.d_out->lemma( ulem );
1648 d_sentLemma = true;
1649 }
1650 }
1651 d_univset[tn] = n;
1652 return n;
1653 }else{
1654 return it->second;
1655 }
1656 }
1657
1658 bool TheorySetsPrivate::hasLemmaCached( Node lem ) {
1659 return d_lemmas_produced.find(lem)!=d_lemmas_produced.end();
1660 }
1661
1662 bool TheorySetsPrivate::hasProcessed() {
1663 return d_conflict || d_sentLemma || d_addedFact;
1664 }
1665
1666 void TheorySetsPrivate::debugPrintSet( Node s, const char * c ) {
1667 if( s.getNumChildren()==0 ){
1668 NodeMap::const_iterator it = d_proxy_to_term.find( s );
1669 if( it!=d_proxy_to_term.end() ){
1670 debugPrintSet( (*it).second, c );
1671 }else{
1672 Trace(c) << s;
1673 }
1674 }else{
1675 Trace(c) << "(" << s.getOperator();
1676 for( unsigned i=0; i<s.getNumChildren(); i++ ){
1677 Trace(c) << " ";
1678 debugPrintSet( s[i], c );
1679 }
1680 Trace(c) << ")";
1681 }
1682 }
1683
1684 void TheorySetsPrivate::lastCallEffortCheck() {
1685 Trace("sets") << "----- Last call effort check ------" << std::endl;
1686
1687 }
1688
1689 /**************************** TheorySetsPrivate *****************************/
1690 /**************************** TheorySetsPrivate *****************************/
1691 /**************************** TheorySetsPrivate *****************************/
1692
1693 void TheorySetsPrivate::check(Theory::Effort level) {
1694 Trace("sets-check") << "Sets check effort " << level << std::endl;
1695 if( level == Theory::EFFORT_LAST_CALL ){
1696 lastCallEffortCheck();
1697 return;
1698 }
1699 while(!d_external.done() && !d_conflict) {
1700 // Get all the assertions
1701 Assertion assertion = d_external.get();
1702 TNode fact = assertion.assertion;
1703 Trace("sets-assert") << "Assert from input " << fact << std::endl;
1704 //assert the fact
1705 assertFact( fact, fact );
1706 }
1707 d_sentLemma = false;
1708 Trace("sets-check") << "Sets finished assertions effort " << level << std::endl;
1709 //invoke full effort check, relations check
1710 if( !d_conflict ){
1711 if( level == Theory::EFFORT_FULL ){
1712 if( !d_external.d_valuation.needCheck() ){
1713 fullEffortCheck();
1714 if( !d_conflict && !d_sentLemma ){
1715 //invoke relations solver
1716 d_rels->check(level);
1717 if( d_card_enabled && ( d_rels_enabled || options::setsExt() ) ){
1718 //if cardinality constraints are enabled,
1719 // then model construction may fail in there are relational operators, or universe set.
1720 // TODO: should internally check model, return unknown if fail
1721 d_full_check_incomplete = true;
1722 Trace("sets-incomplete") << "Sets : incomplete because of extended operators." << std::endl;
1723 }
1724 }
1725 if( d_full_check_incomplete ){
1726 d_external.d_out->setIncomplete();
1727 }
1728 }
1729 }else{
1730 if( options::setsRelEager() ){
1731 d_rels->check(level);
1732 }
1733 }
1734 }
1735 Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
1736 }/* TheorySetsPrivate::check() */
1737
1738 bool TheorySetsPrivate::needsCheckLastEffort() {
1739 if( !d_var_elim.empty() ){
1740 return true;
1741 }
1742 return false;
1743 }
1744
1745 /************************ Sharing ************************/
1746 /************************ Sharing ************************/
1747 /************************ Sharing ************************/
1748
1749 void TheorySetsPrivate::addSharedTerm(TNode n) {
1750 Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
1751 d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
1752 }
1753
1754 void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ){
1755 if( depth==arity ){
1756 if( t2!=NULL ){
1757 Node f1 = t1->getNodeData();
1758 Node f2 = t2->getNodeData();
1759 if( !ee_areEqual( f1, f2 ) ){
1760 Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
1761 vector< pair<TNode, TNode> > currentPairs;
1762 for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
1763 TNode x = f1[k];
1764 TNode y = f2[k];
1765 Assert( d_equalityEngine.hasTerm(x) );
1766 Assert( d_equalityEngine.hasTerm(y) );
1767 Assert( !ee_areDisequal( x, y ) );
1768 Assert( !ee_areCareDisequal( x, y ) );
1769 if( !d_equalityEngine.areEqual( x, y ) ){
1770 Trace("sets-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
1771 if( d_equalityEngine.isTriggerTerm(x, THEORY_SETS) && d_equalityEngine.isTriggerTerm(y, THEORY_SETS) ){
1772 TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_SETS);
1773 TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_SETS);
1774 currentPairs.push_back(make_pair(x_shared, y_shared));
1775 }else if( isCareArg( f1, k ) && isCareArg( f2, k ) ){
1776 //splitting on sets (necessary for handling set of sets properly)
1777 if( x.getType().isSet() ){
1778 Assert( y.getType().isSet() );
1779 if( !ee_areDisequal( x, y ) ){
1780 Trace("sets-cg-lemma") << "Should split on : " << x << "==" << y << std::endl;
1781 split( x.eqNode( y ) );
1782 }
1783 }
1784 }
1785 }
1786 }
1787 for (unsigned c = 0; c < currentPairs.size(); ++ c) {
1788 Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
1789 d_external.addCarePair(currentPairs[c].first, currentPairs[c].second);
1790 n_pairs++;
1791 }
1792 }
1793 }
1794 }else{
1795 if( t2==NULL ){
1796 if( depth<(arity-1) ){
1797 //add care pairs internal to each child
1798 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
1799 addCarePairs( &it->second, NULL, arity, depth+1, n_pairs );
1800 }
1801 }
1802 //add care pairs based on each pair of non-disequal arguments
1803 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
1804 std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
1805 ++it2;
1806 for( ; it2 != t1->d_data.end(); ++it2 ){
1807 if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
1808 if( !ee_areCareDisequal(it->first, it2->first) ){
1809 addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
1810 }
1811 }
1812 }
1813 }
1814 }else{
1815 //add care pairs based on product of indices, non-disequal arguments
1816 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
1817 for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->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 }
1826 }
1827 }
1828
1829 void TheorySetsPrivate::computeCareGraph() {
1830 for( std::map< Kind, std::vector< Node > >::iterator it = d_op_list.begin(); it != d_op_list.end(); ++it ){
1831 if( it->first==kind::SINGLETON || it->first==kind::MEMBER ){
1832 unsigned n_pairs = 0;
1833 Trace("sets-cg-summary") << "Compute graph for sets, op=" << it->first << "..." << it->second.size() << std::endl;
1834 Trace("sets-cg") << "Build index for " << it->first << "..." << std::endl;
1835 std::map< TypeNode, quantifiers::TermArgTrie > index;
1836 unsigned arity = 0;
1837 //populate indices
1838 for( unsigned i=0; i<it->second.size(); i++ ){
1839 TNode f1 = it->second[i];
1840 Assert(d_equalityEngine.hasTerm(f1));
1841 Trace("sets-cg-debug") << "...build for " << f1 << std::endl;
1842 //break into index based on operator, and type of first argument (since some operators are parametric)
1843 TypeNode tn = f1[0].getType();
1844 std::vector< TNode > reps;
1845 bool hasCareArg = false;
1846 for( unsigned j=0; j<f1.getNumChildren(); j++ ){
1847 reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
1848 if( isCareArg( f1, j ) ){
1849 hasCareArg = true;
1850 }
1851 }
1852 if( hasCareArg ){
1853 Trace("sets-cg-debug") << "......adding." << std::endl;
1854 index[tn].addTerm( f1, reps );
1855 arity = reps.size();
1856 }else{
1857 Trace("sets-cg-debug") << "......skip." << std::endl;
1858 }
1859 }
1860 if( arity>0 ){
1861 //for each index
1862 for( std::map< TypeNode, quantifiers::TermArgTrie >::iterator iti = index.begin(); iti != index.end(); ++iti ){
1863 Trace("sets-cg") << "Process index " << iti->first << "..." << std::endl;
1864 addCarePairs( &iti->second, NULL, arity, 0, n_pairs );
1865 }
1866 }
1867 Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
1868 }
1869 }
1870 }
1871
1872 bool TheorySetsPrivate::isCareArg( Node n, unsigned a ) {
1873 if( d_equalityEngine.isTriggerTerm( n[a], THEORY_SETS ) ){
1874 return true;
1875 }else if( ( n.getKind()==kind::MEMBER || n.getKind()==kind::SINGLETON ) && a==0 && n[0].getType().isSet() ){
1876 return true;
1877 }else{
1878 return false;
1879 }
1880 }
1881
1882 EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
1883 Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
1884 if (d_equalityEngine.areEqual(a, b)) {
1885 // The terms are implied to be equal
1886 return EQUALITY_TRUE;
1887 }
1888 if (d_equalityEngine.areDisequal(a, b, false)) {
1889 // The terms are implied to be dis-equal
1890 return EQUALITY_FALSE;
1891 }
1892 return EQUALITY_UNKNOWN;
1893 /*
1894 Node aModelValue = d_external.d_valuation.getModelValue(a);
1895 if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; }
1896 Node bModelValue = d_external.d_valuation.getModelValue(b);
1897 if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; }
1898 if( aModelValue == bModelValue ) {
1899 // The term are true in current model
1900 return EQUALITY_TRUE_IN_MODEL;
1901 } else {
1902 return EQUALITY_FALSE_IN_MODEL;
1903 }
1904 */
1905 // }
1906 // //TODO: can we be more precise sometimes?
1907 // return EQUALITY_UNKNOWN;
1908 }
1909
1910 /******************** Model generation ********************/
1911 /******************** Model generation ********************/
1912 /******************** Model generation ********************/
1913
1914 bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
1915 {
1916 Trace("sets-model") << "Set collect model info" << std::endl;
1917 set<Node> termSet;
1918 // Compute terms appearing in assertions and shared terms
1919 d_external.computeRelevantTerms(termSet);
1920
1921 // Assert equalities and disequalities to the model
1922 if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
1923 {
1924 return false;
1925 }
1926
1927 std::map< Node, Node > mvals;
1928 for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
1929 Node eqc = d_set_eqc[i];
1930 if( termSet.find( eqc )==termSet.end() ){
1931 Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl;
1932 }else{
1933 std::vector< Node > els;
1934 bool is_base = !d_card_enabled || ( d_nf[eqc].size()==1 && d_nf[eqc][0]==eqc );
1935 if( is_base ){
1936 Trace("sets-model") << "Collect elements of base eqc " << eqc << std::endl;
1937 // members that must be in eqc
1938 std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc );
1939 if( itm!=d_pol_mems[0].end() ){
1940 for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){
1941 Node t = NodeManager::currentNM()->mkNode( kind::SINGLETON, itmm->first );
1942 els.push_back( t );
1943 }
1944 }
1945 }
1946 if( d_card_enabled ){
1947 TypeNode elementType = eqc.getType().getSetElementType();
1948 if( is_base ){
1949 std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc );
1950 if( it!=d_eqc_to_card_term.end() ){
1951 //slack elements from cardinality value
1952 Node v = d_external.d_valuation.getModelValue(it->second);
1953 Trace("sets-model") << "Cardinality of " << eqc << " is " << v << std::endl;
1954 Assert(v.getConst<Rational>() <= LONG_MAX, "Exceeded LONG_MAX in sets model");
1955 unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
1956 Assert( els.size()<=vu );
1957 while( els.size()<vu ){
1958 els.push_back( NodeManager::currentNM()->mkNode( kind::SINGLETON, NodeManager::currentNM()->mkSkolem( "msde", elementType ) ) );
1959 }
1960 }else{
1961 Trace("sets-model") << "No slack elements for " << eqc << std::endl;
1962 }
1963 }else{
1964 Trace("sets-model") << "Build value for " << eqc << " based on normal form, size = " << d_nf[eqc].size() << std::endl;
1965 //it is union of venn regions
1966 for( unsigned j=0; j<d_nf[eqc].size(); j++ ){
1967 Assert( mvals.find( d_nf[eqc][j] )!=mvals.end() );
1968 els.push_back( mvals[d_nf[eqc][j]] );
1969 }
1970 }
1971 }
1972 Node rep = NormalForm::mkBop( kind::UNION, els, eqc.getType() );
1973 rep = Rewriter::rewrite( rep );
1974 Trace("sets-model") << "* Assign representative of " << eqc << " to " << rep << std::endl;
1975 mvals[eqc] = rep;
1976 if (!m->assertEquality(eqc, rep, true))
1977 {
1978 return false;
1979 }
1980 m->assertSkeleton(rep);
1981 }
1982 }
1983 return true;
1984 }
1985
1986 /********************** Helper functions ***************************/
1987 /********************** Helper functions ***************************/
1988 /********************** Helper functions ***************************/
1989
1990 void TheorySetsPrivate::addEqualityToExp( Node a, Node b, std::vector< Node >& exp ) {
1991 if( a!=b ){
1992 Assert( ee_areEqual( a, b ) );
1993 exp.push_back( a.eqNode( b ) );
1994 }
1995 }
1996
1997 Node mkAnd(const std::vector<TNode>& conjunctions) {
1998 Assert(conjunctions.size() > 0);
1999
2000 std::set<TNode> all;
2001 for (unsigned i = 0; i < conjunctions.size(); ++i) {
2002 TNode t = conjunctions[i];
2003 if (t.getKind() == kind::AND) {
2004 for(TNode::iterator child_it = t.begin();
2005 child_it != t.end(); ++child_it) {
2006 Assert((*child_it).getKind() != kind::AND);
2007 all.insert(*child_it);
2008 }
2009 }
2010 else {
2011 all.insert(t);
2012 }
2013 }
2014
2015 Assert(all.size() > 0);
2016 if (all.size() == 1) {
2017 // All the same, or just one
2018 return conjunctions[0];
2019 }
2020
2021 NodeBuilder<> conjunction(kind::AND);
2022 std::set<TNode>::const_iterator it = all.begin();
2023 std::set<TNode>::const_iterator it_end = all.end();
2024 while (it != it_end) {
2025 conjunction << *it;
2026 ++ it;
2027 }
2028
2029 return conjunction;
2030 }/* mkAnd() */
2031
2032
2033 TheorySetsPrivate::Statistics::Statistics() :
2034 d_getModelValueTime("theory::sets::getModelValueTime")
2035 , d_mergeTime("theory::sets::merge_nodes::time")
2036 , d_processCard2Time("theory::sets::processCard2::time")
2037 , d_memberLemmas("theory::sets::lemmas::member", 0)
2038 , d_disequalityLemmas("theory::sets::lemmas::disequality", 0)
2039 , d_numVertices("theory::sets::vertices", 0)
2040 , d_numVerticesMax("theory::sets::vertices-max", 0)
2041 , d_numMergeEq1or2("theory::sets::merge1or2", 0)
2042 , d_numMergeEq3("theory::sets::merge3", 0)
2043 , d_numLeaves("theory::sets::leaves", 0)
2044 , d_numLeavesMax("theory::sets::leaves-max", 0)
2045 {
2046 smtStatisticsRegistry()->registerStat(&d_getModelValueTime);
2047 smtStatisticsRegistry()->registerStat(&d_mergeTime);
2048 smtStatisticsRegistry()->registerStat(&d_processCard2Time);
2049 smtStatisticsRegistry()->registerStat(&d_memberLemmas);
2050 smtStatisticsRegistry()->registerStat(&d_disequalityLemmas);
2051 smtStatisticsRegistry()->registerStat(&d_numVertices);
2052 smtStatisticsRegistry()->registerStat(&d_numVerticesMax);
2053 smtStatisticsRegistry()->registerStat(&d_numMergeEq1or2);
2054 smtStatisticsRegistry()->registerStat(&d_numMergeEq3);
2055 smtStatisticsRegistry()->registerStat(&d_numLeaves);
2056 smtStatisticsRegistry()->registerStat(&d_numLeavesMax);
2057 }
2058
2059
2060 TheorySetsPrivate::Statistics::~Statistics() {
2061 smtStatisticsRegistry()->unregisterStat(&d_getModelValueTime);
2062 smtStatisticsRegistry()->unregisterStat(&d_mergeTime);
2063 smtStatisticsRegistry()->unregisterStat(&d_processCard2Time);
2064 smtStatisticsRegistry()->unregisterStat(&d_memberLemmas);
2065 smtStatisticsRegistry()->unregisterStat(&d_disequalityLemmas);
2066 smtStatisticsRegistry()->unregisterStat(&d_numVertices);
2067 smtStatisticsRegistry()->unregisterStat(&d_numVerticesMax);
2068 smtStatisticsRegistry()->unregisterStat(&d_numMergeEq1or2);
2069 smtStatisticsRegistry()->unregisterStat(&d_numMergeEq3);
2070 smtStatisticsRegistry()->unregisterStat(&d_numLeaves);
2071 smtStatisticsRegistry()->unregisterStat(&d_numLeavesMax);
2072 }
2073
2074 void TheorySetsPrivate::propagate(Theory::Effort effort) {
2075
2076 }
2077
2078 bool TheorySetsPrivate::propagate(TNode literal) {
2079 Debug("sets-prop") << " propagate(" << literal << ")" << std::endl;
2080
2081 // If already in conflict, no more propagation
2082 if (d_conflict) {
2083 Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
2084 return false;
2085 }
2086
2087 // Propagate out
2088 bool ok = d_external.d_out->propagate(literal);
2089 if (!ok) {
2090 d_conflict = true;
2091 }
2092
2093 return ok;
2094 }/* TheorySetsPrivate::propagate(TNode) */
2095
2096
2097 void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
2098 d_equalityEngine.setMasterEqualityEngine(eq);
2099 }
2100
2101
2102 void TheorySetsPrivate::conflict(TNode a, TNode b)
2103 {
2104 d_conflictNode = explain(a.eqNode(b));
2105 d_external.d_out->conflict(d_conflictNode);
2106 Debug("sets") << "[sets] conflict: " << a << " iff " << b
2107 << ", explaination " << d_conflictNode << std::endl;
2108 Trace("sets-lemma") << "Equality Conflict : " << d_conflictNode << std::endl;
2109 d_conflict = true;
2110 }
2111
2112 Node TheorySetsPrivate::explain(TNode literal)
2113 {
2114 Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
2115 << std::endl;
2116
2117 bool polarity = literal.getKind() != kind::NOT;
2118 TNode atom = polarity ? literal : literal[0];
2119 std::vector<TNode> assumptions;
2120
2121 if(atom.getKind() == kind::EQUAL) {
2122 d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
2123 } else if(atom.getKind() == kind::MEMBER) {
2124 d_equalityEngine.explainPredicate(atom, polarity, assumptions);
2125 } else {
2126 Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
2127 << polarity << "); kind" << atom.getKind() << std::endl;
2128 Unhandled();
2129 }
2130
2131 return mkAnd(assumptions);
2132 }
2133
2134 void TheorySetsPrivate::preRegisterTerm(TNode node)
2135 {
2136 Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
2137 << std::endl;
2138 switch(node.getKind()) {
2139 case kind::EQUAL:
2140 // TODO: what's the point of this
2141 d_equalityEngine.addTriggerEquality(node);
2142 break;
2143 case kind::MEMBER:
2144 // TODO: what's the point of this
2145 d_equalityEngine.addTriggerPredicate(node);
2146 break;
2147 case kind::CARD:
2148 d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
2149 break;
2150 default:
2151 //if( node.getType().isSet() ){
2152 // d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
2153 //}else{
2154 d_equalityEngine.addTerm(node);
2155 //}
2156 break;
2157 }
2158 }
2159
2160 Node TheorySetsPrivate::expandDefinition(LogicRequest &logicRequest, Node n) {
2161 Debug("sets-proc") << "expandDefinition : " << n << std::endl;
2162 if( n.getKind()==kind::UNIVERSE_SET || n.getKind()==kind::COMPLEMENT || n.getKind()==kind::JOIN_IMAGE ){
2163 if( !options::setsExt() ){
2164 std::stringstream ss;
2165 ss << "Extended set operators are not supported in default mode, try --sets-ext.";
2166 throw LogicException(ss.str());
2167 }
2168 }
2169 return n;
2170 }
2171
2172 Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
2173 Debug("sets-proc") << "ppAssert : " << in << std::endl;
2174 Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
2175
2176 //TODO: allow variable elimination for sets when setsExt = true
2177
2178 //this is based off of Theory::ppAssert
2179 Node var;
2180 if (in.getKind() == kind::EQUAL) {
2181 if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
2182 (in[1].getType()).isSubtypeOf(in[0].getType()) ){
2183 if( !in[0].getType().isSet() || !options::setsExt() ){
2184 outSubstitutions.addSubstitution(in[0], in[1]);
2185 var = in[0];
2186 status = Theory::PP_ASSERT_STATUS_SOLVED;
2187 }
2188 }else if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
2189 (in[0].getType()).isSubtypeOf(in[1].getType())){
2190 if( !in[1].getType().isSet() || !options::setsExt() ){
2191 outSubstitutions.addSubstitution(in[1], in[0]);
2192 var = in[1];
2193 status = Theory::PP_ASSERT_STATUS_SOLVED;
2194 }
2195 }else if (in[0].isConst() && in[1].isConst()) {
2196 if (in[0] != in[1]) {
2197 status = Theory::PP_ASSERT_STATUS_CONFLICT;
2198 }
2199 }
2200 }
2201
2202 if( status==Theory::PP_ASSERT_STATUS_SOLVED ){
2203 Trace("sets-var-elim") << "Sets : ppAssert variable eliminated : " << in << ", var = " << var << std::endl;
2204 /*
2205 if( var.getType().isSet() ){
2206 //we must ensure that subs is included in the universe set
2207 d_var_elim[var] = true;
2208 }
2209 */
2210 if( options::setsExt() ){
2211 Assert( !var.getType().isSet() );
2212 }
2213 }
2214 return status;
2215 }
2216
2217 void TheorySetsPrivate::presolve() {
2218
2219 }
2220
2221 /**************************** eq::NotifyClass *****************************/
2222 /**************************** eq::NotifyClass *****************************/
2223 /**************************** eq::NotifyClass *****************************/
2224
2225
2226 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
2227 {
2228 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
2229 << " value = " << value << std::endl;
2230 if (value) {
2231 return d_theory.propagate(equality);
2232 } else {
2233 // We use only literal triggers so taking not is safe
2234 return d_theory.propagate(equality.notNode());
2235 }
2236 }
2237
2238 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
2239 {
2240 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
2241 << " value = " << value << std::endl;
2242 if (value) {
2243 return d_theory.propagate(predicate);
2244 } else {
2245 return d_theory.propagate(predicate.notNode());
2246 }
2247 }
2248
2249 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
2250 {
2251 Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
2252 << " t1 = " << t1 << " t2 = " << t2 << " value = " << value << std::endl;
2253 d_theory.propagate( value ? t1.eqNode( t2 ) : t1.eqNode( t2 ).negate() );
2254 return true;
2255 }
2256
2257 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
2258 {
2259 Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
2260 d_theory.conflict(t1, t2);
2261 }
2262
2263 void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
2264 {
2265 Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
2266 d_theory.eqNotifyNewClass(t);
2267 }
2268
2269 void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
2270 {
2271 Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
2272 d_theory.eqNotifyPreMerge(t1, t2);
2273 }
2274
2275 void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
2276 {
2277 Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
2278 d_theory.eqNotifyPostMerge(t1, t2);
2279 }
2280
2281 void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
2282 {
2283 Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
2284 d_theory.eqNotifyDisequal(t1, t2, reason);
2285 }
2286
2287 }/* CVC4::theory::sets namespace */
2288 }/* CVC4::theory namespace */
2289 }/* CVC4 namespace */