projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Use new copyright header format.
[cvc5.git] / src / theory / sets / theory_sets_rels.cpp
1 /********************* */
2 /*! \file theory_sets_rels.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** none
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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 ** Extension to Sets theory.
15 **/
16
17 #include "theory/sets/theory_sets_rels.h"
18 #include "expr/datatype.h"
19 #include "theory/sets/theory_sets_private.h"
20 #include "theory/sets/theory_sets.h"
21
22 using namespace std;
23
24 namespace CVC4 {
25 namespace theory {
26 namespace sets {
27
28 typedef std::map< Node, std::vector< Node > >::iterator MEM_IT;
29 typedef std::map< kind::Kind_t, std::vector< Node > >::iterator KIND_TERM_IT;
30 typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_GRAPH_IT;
31 typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT;
32 typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > > >::iterator TC_IT;
33
34 void TheorySetsRels::check(Theory::Effort level) {
35 Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver, effort = " << level << " *******************************\n" << std::endl;
36 if(Theory::fullEffort(level)) {
37 collectRelsInfo();
38 check();
39 doPendingLemmas();
40 Assert( d_lemmas_out.empty() );
41 Assert( d_pending_facts.empty() );
42 } else {
43 doPendingMerge();
44 }
45 Trace("rels") << "\n[sets-rels] ******************************* Done with the relational solver *******************************\n" << std::endl;
46 }
47
48 void TheorySetsRels::check() {
49 MEM_IT m_it = d_rReps_memberReps_cache.begin();
50
51 while(m_it != d_rReps_memberReps_cache.end()) {
52 Node rel_rep = m_it->first;
53
54 for(unsigned int i = 0; i < m_it->second.size(); i++) {
55 Node mem = d_rReps_memberReps_cache[rel_rep][i];
56 Node exp = d_rReps_memberReps_exp_cache[rel_rep][i];
57 std::map<kind::Kind_t, std::vector<Node> > kind_terms = d_terms_cache[rel_rep];
58
59 if( kind_terms.find(kind::TRANSPOSE) != kind_terms.end() ) {
60 std::vector<Node> tp_terms = kind_terms[kind::TRANSPOSE];
61 if( tp_terms.size() > 0 ) {
62 applyTransposeRule( tp_terms );
63 applyTransposeRule( tp_terms[0], rel_rep, exp );
64 }
65 }
66 if( kind_terms.find(kind::JOIN) != kind_terms.end() ) {
67 std::vector<Node> join_terms = kind_terms[kind::JOIN];
68 for( unsigned int j = 0; j < join_terms.size(); j++ ) {
69 applyJoinRule( join_terms[j], rel_rep, exp );
70 }
71 }
72 if( kind_terms.find(kind::PRODUCT) != kind_terms.end() ) {
73 std::vector<Node> product_terms = kind_terms[kind::PRODUCT];
74 for( unsigned int j = 0; j < product_terms.size(); j++ ) {
75 applyProductRule( product_terms[j], rel_rep, exp );
76 }
77 }
78 if( kind_terms.find(kind::TCLOSURE) != kind_terms.end() ) {
79 std::vector<Node> tc_terms = kind_terms[kind::TCLOSURE];
80 for( unsigned int j = 0; j < tc_terms.size(); j++ ) {
81 applyTCRule( mem, tc_terms[j], rel_rep, exp );
82 }
83 }
84 if( kind_terms.find(kind::JOIN_IMAGE) != kind_terms.end() ) {
85 std::vector<Node> join_image_terms = kind_terms[kind::JOIN_IMAGE];
86 for( unsigned int j = 0; j < join_image_terms.size(); j++ ) {
87 applyJoinImageRule( mem, join_image_terms[j], exp );
88 }
89 }
90 if( kind_terms.find(kind::IDEN) != kind_terms.end() ) {
91 std::vector<Node> iden_terms = kind_terms[kind::IDEN];
92 for( unsigned int j = 0; j < iden_terms.size(); j++ ) {
93 applyIdenRule( mem, iden_terms[j], exp );
94 }
95 }
96 }
97 m_it++;
98 }
99
100 TERM_IT t_it = d_terms_cache.begin();
101 while( t_it != d_terms_cache.end() ) {
102 if( d_rReps_memberReps_cache.find(t_it->first) == d_rReps_memberReps_cache.end() ) {
103 Trace("rels-debug") << "[sets-rels] A term does not have membership constraints: " << t_it->first << std::endl;
104 KIND_TERM_IT k_t_it = t_it->second.begin();
105
106 while( k_t_it != t_it->second.end() ) {
107 if( k_t_it->first == kind::JOIN || k_t_it->first == kind::PRODUCT ) {
108 std::vector<Node>::iterator term_it = k_t_it->second.begin();
109 while(term_it != k_t_it->second.end()) {
110 computeMembersForBinOpRel( *term_it );
111 term_it++;
112 }
113 } else if( k_t_it->first == kind::TRANSPOSE ) {
114 std::vector<Node>::iterator term_it = k_t_it->second.begin();
115 while( term_it != k_t_it->second.end() ) {
116 computeMembersForUnaryOpRel( *term_it );
117 term_it++;
118 }
119 } else if ( k_t_it->first == kind::TCLOSURE ) {
120 std::vector<Node>::iterator term_it = k_t_it->second.begin();
121 while( term_it != k_t_it->second.end() ) {
122 buildTCGraphForRel( *term_it );
123 term_it++;
124 }
125 } else if( k_t_it->first == kind::JOIN_IMAGE ) {
126 std::vector<Node>::iterator term_it = k_t_it->second.begin();
127 while( term_it != k_t_it->second.end() ) {
128 computeMembersForJoinImageTerm( *term_it );
129 term_it++;
130 }
131 } else if( k_t_it->first == kind::IDEN ) {
132 std::vector<Node>::iterator term_it = k_t_it->second.begin();
133 while( term_it != k_t_it->second.end() ) {
134 computeMembersForIdenTerm( *term_it );
135 term_it++;
136 }
137 }
138 k_t_it++;
139 }
140 }
141 t_it++;
142 }
143 doTCInference();
144 }
145
146 /*
147 * Populate relational terms data structure
148 */
149
150 void TheorySetsRels::collectRelsInfo() {
151 Trace("rels") << "[sets-rels] Start collecting relational terms..." << std::endl;
152 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine );
153 while( !eqcs_i.isFinished() ){
154 Node eqc_rep = (*eqcs_i);
155 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc_rep, d_eqEngine );
156
157 Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << " with type " << eqc_rep.getType() << std::endl;
158
159 while( !eqc_i.isFinished() ){
160 Node eqc_node = (*eqc_i);
161
162 Trace("rels-ee") << " term : " << eqc_node << std::endl;
163
164 if( getRepresentative(eqc_rep) == getRepresentative(d_trueNode) ||
165 getRepresentative(eqc_rep) == getRepresentative(d_falseNode) ) {
166
167 // collect membership info
168 if( eqc_node.getKind() == kind::MEMBER && eqc_node[1].getType().getSetElementType().isTuple()) {
169 Node tup_rep = getRepresentative( eqc_node[0] );
170 Node rel_rep = getRepresentative( eqc_node[1] );
171
172 if( eqc_node[0].isVar() ){
173 reduceTupleVar( eqc_node );
174 }
175
176 bool is_true_eq = areEqual( eqc_rep, d_trueNode );
177 Node reason = is_true_eq ? eqc_node : eqc_node.negate();
178
179 if( is_true_eq ) {
180 if( safelyAddToMap(d_rReps_memberReps_cache, rel_rep, tup_rep) ) {
181 addToMap(d_rReps_memberReps_exp_cache, rel_rep, reason);
182 computeTupleReps(tup_rep);
183 d_membership_trie[rel_rep].addTerm(tup_rep, d_tuple_reps[tup_rep]);
184 }
185 }
186 }
187 // collect relational terms info
188 } else if( eqc_rep.getType().isSet() && eqc_rep.getType().getSetElementType().isTuple() ) {
189 if( eqc_node.getKind() == kind::TRANSPOSE || eqc_node.getKind() == kind::JOIN ||
190 eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE ||
191 eqc_node.getKind() == kind::JOIN_IMAGE || eqc_node.getKind() == kind::IDEN ) {
192 std::vector<Node> terms;
193 std::map< kind::Kind_t, std::vector<Node> > rel_terms;
194 TERM_IT terms_it = d_terms_cache.find(eqc_rep);
195
196 if( terms_it == d_terms_cache.end() ) {
197 terms.push_back(eqc_node);
198 rel_terms[eqc_node.getKind()] = terms;
199 d_terms_cache[eqc_rep] = rel_terms;
200 } else {
201 KIND_TERM_IT kind_term_it = terms_it->second.find(eqc_node.getKind());
202
203 if( kind_term_it == terms_it->second.end() ) {
204 terms.push_back(eqc_node);
205 d_terms_cache[eqc_rep][eqc_node.getKind()] = terms;
206 } else {
207 kind_term_it->second.push_back(eqc_node);
208 }
209 }
210 }
211 // need to add all tuple elements as shared terms
212 } else if( eqc_node.getType().isTuple() && !eqc_node.isConst() && !eqc_node.isVar() ) {
213 for( unsigned int i = 0; i < eqc_node.getType().getTupleLength(); i++ ) {
214 Node element = RelsUtils::nthElementOfTuple( eqc_node, i );
215
216 if( !element.isConst() ) {
217 makeSharedTerm( element );
218 }
219 }
220 }
221 ++eqc_i;
222 }
223 ++eqcs_i;
224 }
225 Trace("rels-debug") << "[Theory::Rels] Done with collecting relational terms!" << std::endl;
226 }
227
228 /* JOIN-IMAGE UP : (x, x1) IS_IN R, ..., (x, xn) IS_IN R (R JOIN_IMAGE n)
229 * -------------------------------------------------------
230 * x IS_IN (R JOIN_IMAGE n) || NOT DISTINCT(x1, ... , xn)
231 *
232 */
233
234 void TheorySetsRels::computeMembersForJoinImageTerm( Node join_image_term ) {
235 Trace("rels-debug") << "\n[Theory::Rels] *********** Compute members for JoinImage Term = " << join_image_term << std::endl;
236 MEM_IT rel_mem_it = d_rReps_memberReps_cache.find( getRepresentative( join_image_term[0] ) );
237
238 if( rel_mem_it == d_rReps_memberReps_cache.end() ) {
239 return;
240 }
241
242 Node join_image_rel = join_image_term[0];
243 std::hash_set< Node, NodeHashFunction > hasChecked;
244 Node join_image_rel_rep = getRepresentative( join_image_rel );
245 std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin();
246 MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep );
247 std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin();
248 unsigned int min_card = join_image_term[1].getConst<Rational>().getNumerator().getUnsignedInt();
249
250 while( mem_rep_it != (*rel_mem_it).second.end() ) {
251 Node fst_mem_rep = RelsUtils::nthElementOfTuple( *mem_rep_it, 0 );
252
253 if( hasChecked.find( fst_mem_rep ) != hasChecked.end() ) {
254 ++mem_rep_it;
255 ++mem_rep_exp_it;
256 continue;
257 }
258 hasChecked.insert( fst_mem_rep );
259
260 Datatype dt = join_image_term.getType().getSetElementType().getDatatype();
261 Node new_membership = NodeManager::currentNM()->mkNode(kind::MEMBER,
262 NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR,
263 Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ),
264 join_image_term);
265 if( holds( new_membership ) ) {
266 ++mem_rep_it;
267 ++mem_rep_exp_it;
268 continue;
269 }
270
271 std::vector< Node > reasons;
272 std::vector< Node > existing_members;
273 std::vector< Node >::iterator mem_rep_exp_it_snd = (*rel_mem_exp_it).second.begin();
274
275 while( mem_rep_exp_it_snd != (*rel_mem_exp_it).second.end() ) {
276 Node fst_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 0 );
277
278 if( areEqual( fst_mem_rep, fst_element_snd_mem ) ) {
279 bool notExist = true;
280 std::vector< Node >::iterator existing_mem_it = existing_members.begin();
281 Node snd_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 1 );
282
283 while( existing_mem_it != existing_members.end() ) {
284 if( areEqual( (*existing_mem_it), snd_element_snd_mem ) ) {
285 notExist = false;
286 break;
287 }
288 ++existing_mem_it;
289 }
290
291 if( notExist ) {
292 existing_members.push_back( snd_element_snd_mem );
293 reasons.push_back( *mem_rep_exp_it_snd );
294 if( fst_mem_rep != fst_element_snd_mem ) {
295 reasons.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, fst_mem_rep, fst_element_snd_mem ) );
296 }
297 if( join_image_rel != (*mem_rep_exp_it_snd)[1] ) {
298 reasons.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it_snd)[1], join_image_rel ));
299 }
300 if( existing_members.size() == min_card ) {
301 if( min_card >= 2) {
302 new_membership = NodeManager::currentNM()->mkNode( kind::OR, new_membership, NodeManager::currentNM()->mkNode( kind::NOT, NodeManager::currentNM()->mkNode( kind::DISTINCT, existing_members ) ));
303 }
304 Assert(reasons.size() >= 1);
305 sendInfer( new_membership, reasons.size() > 1 ? NodeManager::currentNM()->mkNode( kind::AND, reasons) : reasons[0], "JOIN-IMAGE UP" );
306 break;
307 }
308 }
309 }
310 ++mem_rep_exp_it_snd;
311 }
312 ++mem_rep_it;
313 ++mem_rep_exp_it;
314 }
315 Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for JoinImage Term" << join_image_term << "*********** " << std::endl;
316 }
317
318 /* JOIN-IMAGE DOWN : (x) IS_IN (R JOIN_IMAGE n)
319 * -------------------------------------------------------
320 * (x, x1) IS_IN R .... (x, xn) IS_IN R DISTINCT(x1, ... , xn)
321 *
322 */
323
324 void TheorySetsRels::applyJoinImageRule( Node mem_rep, Node join_image_term, Node exp ) {
325 Trace("rels-debug") << "\n[Theory::Rels] *********** applyJoinImageRule on " << join_image_term
326 << " with mem_rep = " << mem_rep << " and exp = " << exp << std::endl;
327 if( d_rel_nodes.find( join_image_term ) == d_rel_nodes.end() ) {
328 computeMembersForJoinImageTerm( join_image_term );
329 d_rel_nodes.insert( join_image_term );
330 }
331
332 Node join_image_rel = join_image_term[0];
333 Node join_image_rel_rep = getRepresentative( join_image_rel );
334 MEM_IT rel_mem_it = d_rReps_memberReps_cache.find( join_image_rel_rep );
335 unsigned int min_card = join_image_term[1].getConst<Rational>().getNumerator().getUnsignedInt();
336
337 if( rel_mem_it != d_rReps_memberReps_cache.end() ) {
338 if( d_membership_trie.find( join_image_rel_rep ) != d_membership_trie.end() ) {
339 computeTupleReps( mem_rep );
340 if( d_membership_trie[join_image_rel_rep].findSuccessors(d_tuple_reps[mem_rep]).size() >= min_card ) {
341 return;
342 }
343 }
344 }
345
346 Node reason = exp;
347 Node conclusion = d_trueNode;
348 std::vector< Node > distinct_skolems;
349 Node fst_mem_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
350
351 if( exp[1] != join_image_term ) {
352 reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], join_image_term ) );
353 }
354 for( unsigned int i = 0; i < min_card; i++ ) {
355 Node skolem = NodeManager::currentNM()->mkSkolem( "jig", join_image_rel.getType()[0].getTupleTypes()[0] );
356 distinct_skolems.push_back( skolem );
357 conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( join_image_rel, fst_mem_element, skolem ), join_image_rel ) );
358 }
359 if( distinct_skolems.size() >= 2 ) {
360 conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) );
361 }
362 sendInfer( conclusion, reason, "JOIN-IMAGE DOWN" );
363 Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl;
364
365 }
366
367
368 /* IDENTITY-DOWN : (x, y) IS_IN IDEN(R)
369 * -------------------------------------------------------
370 * x = y, (x IS_IN R)
371 *
372 */
373
374 void TheorySetsRels::applyIdenRule( Node mem_rep, Node iden_term, Node exp) {
375 Trace("rels-debug") << "\n[Theory::Rels] *********** applyIdenRule on " << iden_term
376 << " with mem_rep = " << mem_rep << " and exp = " << exp << std::endl;
377 if( d_rel_nodes.find( iden_term ) == d_rel_nodes.end() ) {
378 computeMembersForIdenTerm( iden_term );
379 d_rel_nodes.insert( iden_term );
380 }
381 Node reason = exp;
382 Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 );
383 Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 );
384 Datatype dt = iden_term[0].getType().getSetElementType().getDatatype();
385 Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ), iden_term[0] );
386
387 if( exp[1] != iden_term ) {
388 reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], iden_term ) );
389 }
390 sendInfer( NodeManager::currentNM()->mkNode( kind::AND, fact, NodeManager::currentNM()->mkNode( kind::EQUAL, fst_mem, snd_mem ) ), reason, "IDENTITY-DOWN" );
391 Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyIdenRule on " << iden_term << std::endl;
392 }
393
394 /* IDEN UP : (x) IS_IN R IDEN(R) IN T
395 * --------------------------------
396 * (x, x) IS_IN IDEN(R)
397 *
398 */
399
400 void TheorySetsRels::computeMembersForIdenTerm( Node iden_term ) {
401 Trace("rels-debug") << "\n[Theory::Rels] *********** Compute members for Iden Term = " << iden_term << std::endl;
402 Node iden_term_rel = iden_term[0];
403 Node iden_term_rel_rep = getRepresentative( iden_term_rel );
404
405 if( d_rReps_memberReps_cache.find( iden_term_rel_rep ) == d_rReps_memberReps_cache.end() ) {
406 return;
407 }
408
409 MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( iden_term_rel_rep );
410 std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin();
411
412 while( mem_rep_exp_it != (*rel_mem_exp_it).second.end() ) {
413 Node reason = *mem_rep_exp_it;
414 Node fst_exp_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it)[0], 0 );
415 Node new_mem = RelsUtils::constructPair( iden_term, fst_exp_mem, fst_exp_mem );
416
417 if( (*mem_rep_exp_it)[1] != iden_term_rel ) {
418 reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it)[1], iden_term_rel ) );
419 }
420 sendInfer( NodeManager::currentNM()->mkNode( kind::MEMBER, new_mem, iden_term ), reason, "IDENTITY-UP" );
421 ++mem_rep_exp_it;
422 }
423 Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for Iden Term = " << iden_term << std::endl;
424 }
425
426
427 /*
428 * Construct transitive closure graph for tc_rep based on the members of tc_r_rep
429 */
430
431 /*
432 * TCLOSURE TCLOSURE(x) = x | x.x | x.x.x | ... (| is union)
433 *
434 * TCLOSURE-UP I: (a, b) IS_IN x TCLOSURE(x) in T
435 * ---------------------------------------------
436 * (a, b) IS_IN TCLOSURE(x)
437 *
438 *
439 *
440 * TCLOSURE-UP II : (a, b) IS_IN TCLOSURE(x) (b, c) IS_IN TCLOSURE(x)
441 * -----------------------------------------------------------
442 * (a, c) IS_IN TCLOSURE(x)
443 *
444 */
445 void TheorySetsRels::applyTCRule( Node mem_rep, Node tc_rel, Node tc_rel_rep, Node exp ) {
446 Trace("rels-debug") << "[Theory::Rels] *********** Applying TCLOSURE rule on a tc term = " << tc_rel
447 << ", its representative = " << tc_rel_rep
448 << " with member rep = " << mem_rep << " and explanation = " << exp << std::endl;
449 MEM_IT mem_it = d_rReps_memberReps_cache.find( tc_rel[0] );
450
451 if( mem_it != d_rReps_memberReps_cache.end() && d_rel_nodes.find( tc_rel ) == d_rel_nodes.end()
452 && d_rRep_tcGraph.find( getRepresentative( tc_rel[0] ) ) == d_rRep_tcGraph.end() ) {
453 buildTCGraphForRel( tc_rel );
454 d_rel_nodes.insert( tc_rel );
455 }
456
457 // mem_rep is a member of tc_rel[0] or mem_rep can be infered by TC_Graph of tc_rel[0], thus skip
458 if( isTCReachable( mem_rep, tc_rel) ) {
459 Trace("rels-debug") << "[Theory::Rels] mem_rep is a member of tc_rel[0] = " << tc_rel[0]
460 << " or can be infered by TC_Graph of tc_rel[0]! " << std::endl;
461 return;
462 }
463 // add mem_rep to d_tcrRep_tcGraph
464 TC_IT tc_it = d_tcr_tcGraph.find( tc_rel );
465 Node mem_rep_fst = getRepresentative( RelsUtils::nthElementOfTuple( mem_rep, 0 ) );
466 Node mem_rep_snd = getRepresentative( RelsUtils::nthElementOfTuple( mem_rep, 1 ) );
467 Node mem_rep_tup = RelsUtils::constructPair( tc_rel, mem_rep_fst, mem_rep_snd );
468
469 if( tc_it != d_tcr_tcGraph.end() ) {
470 std::map< Node, std::map< Node, Node > >::iterator tc_exp_it = d_tcr_tcGraph_exps.find( tc_rel );
471
472 TC_GRAPH_IT tc_graph_it = (tc_it->second).find( mem_rep_fst );
473 Assert( tc_exp_it != d_tcr_tcGraph_exps.end() );
474 std::map< Node, Node >::iterator exp_map_it = (tc_exp_it->second).find( mem_rep_tup );
475
476 if( exp_map_it == (tc_exp_it->second).end() ) {
477 (tc_exp_it->second)[mem_rep_tup] = exp;
478 }
479
480 if( tc_graph_it != (tc_it->second).end() ) {
481 (tc_graph_it->second).insert( mem_rep_snd );
482 } else {
483 std::hash_set< Node, NodeHashFunction > sets;
484 sets.insert( mem_rep_snd );
485 (tc_it->second)[mem_rep_fst] = sets;
486 }
487 } else {
488 std::map< Node, Node > exp_map;
489 std::hash_set< Node, NodeHashFunction > sets;
490 std::map< Node, std::hash_set<Node, NodeHashFunction> > element_map;
491 sets.insert( mem_rep_snd );
492 element_map[mem_rep_fst] = sets;
493 d_tcr_tcGraph[tc_rel] = element_map;
494 exp_map[mem_rep_tup] = exp;
495 d_tcr_tcGraph_exps[tc_rel] = exp_map;
496 }
497
498 Node fst_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
499 Node snd_element = RelsUtils::nthElementOfTuple( exp[0], 1 );
500 Node sk_1 = NodeManager::currentNM()->mkSkolem("stc", fst_element.getType());
501 Node sk_2 = NodeManager::currentNM()->mkSkolem("stc", snd_element.getType());
502 Node mem_of_r = NodeManager::currentNM()->mkNode(kind::MEMBER, exp[0], tc_rel[0]);
503 Node sk_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sk_1, sk_2);
504 Node reason = exp;
505
506 if( tc_rel != exp[1] ) {
507 reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel, exp[1]));
508 }
509
510 Node conclusion = NodeManager::currentNM()->mkNode(kind::OR, mem_of_r,
511 (NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, fst_element, sk_1), tc_rel[0]),
512 (NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, sk_2, snd_element), tc_rel[0]),
513 (NodeManager::currentNM()->mkNode(kind::OR, sk_eq, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, sk_1, sk_2), tc_rel))))))));
514
515 Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, conclusion );
516 std::vector< Node > require_phase;
517 require_phase.push_back(Rewriter::rewrite(mem_of_r));
518 require_phase.push_back(Rewriter::rewrite(sk_eq));
519 d_tc_lemmas_last[tc_lemma] = require_phase;
520 }
521
522 bool TheorySetsRels::isTCReachable( Node mem_rep, Node tc_rel ) {
523 MEM_IT mem_it = d_rReps_memberReps_cache.find( getRepresentative( tc_rel[0] ) );
524
525 if( mem_it != d_rReps_memberReps_cache.end() && std::find( (mem_it->second).begin(), (mem_it->second).end(), mem_rep) != (mem_it->second).end() ) {
526 return true;
527 }
528
529 TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) );
530 if( tc_it != d_rRep_tcGraph.end() ) {
531 bool isReachable = false;
532 std::hash_set<Node, NodeHashFunction> seen;
533 isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ),
534 getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable );
535 return isReachable;
536 }
537 return false;
538 }
539
540 void TheorySetsRels::isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen,
541 std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) {
542 if(hasSeen.find(start) == hasSeen.end()) {
543 hasSeen.insert(start);
544 }
545
546 TC_GRAPH_IT pair_set_it = tc_graph.find(start);
547
548 if(pair_set_it != tc_graph.end()) {
549 if(pair_set_it->second.find(dest) != pair_set_it->second.end()) {
550 isReachable = true;
551 return;
552 } else {
553 std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin();
554
555 while( set_it != pair_set_it->second.end() ) {
556 // need to check if *set_it has been looked already
557 if( hasSeen.find(*set_it) == hasSeen.end() ) {
558 isTCReachable( *set_it, dest, hasSeen, tc_graph, isReachable );
559 }
560 set_it++;
561 }
562 }
563 }
564 }
565
566 void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) {
567 std::map< Node, Node > rel_tc_graph_exps;
568 std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph;
569
570 Node rel_rep = getRepresentative( tc_rel[0] );
571 Node tc_rel_rep = getRepresentative( tc_rel );
572 std::vector< Node > members = d_rReps_memberReps_cache[rel_rep];
573 std::vector< Node > exps = d_rReps_memberReps_exp_cache[rel_rep];
574
575 for( unsigned int i = 0; i < members.size(); i++ ) {
576 Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 ));
577 Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 ));
578 Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep );
579 std::map< Node, std::hash_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep );
580
581 if( rel_tc_graph_it == rel_tc_graph.end() ) {
582 std::hash_set< Node, NodeHashFunction > snd_elements;
583 snd_elements.insert( snd_element_rep );
584 rel_tc_graph[fst_element_rep] = snd_elements;
585 rel_tc_graph_exps[tuple_rep] = exps[i];
586 } else if( (rel_tc_graph_it->second).find( snd_element_rep ) == (rel_tc_graph_it->second).end() ) {
587 (rel_tc_graph_it->second).insert( snd_element_rep );
588 rel_tc_graph_exps[tuple_rep] = exps[i];
589 }
590 }
591
592 if( members.size() > 0 ) {
593 d_rRep_tcGraph[rel_rep] = rel_tc_graph;
594 d_tcr_tcGraph_exps[tc_rel] = rel_tc_graph_exps;
595 d_tcr_tcGraph[tc_rel] = rel_tc_graph;
596 }
597 }
598
599 void TheorySetsRels::doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) {
600 Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl;
601 for( TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); tc_graph_it != rel_tc_graph.end(); tc_graph_it++ ) {
602 for( std::hash_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin();
603 snd_elements_it != tc_graph_it->second.end(); snd_elements_it++ ) {
604 std::vector< Node > reasons;
605 std::hash_set<Node, NodeHashFunction> seen;
606 Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) );
607 Assert( rel_tc_graph_exps.find( tuple ) != rel_tc_graph_exps.end() );
608 Node exp = rel_tc_graph_exps.find( tuple )->second;
609
610 reasons.push_back( exp );
611 seen.insert( tc_graph_it->first );
612 doTCInference( tc_rel, reasons, rel_tc_graph, rel_tc_graph_exps, tc_graph_it->first, *snd_elements_it, seen);
613 }
614 }
615 Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl;
616 }
617
618 void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph,
619 std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ) {
620 Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) );
621 std::vector< Node > all_reasons( reasons );
622
623 for( unsigned int i = 0 ; i < reasons.size()-1; i++ ) {
624 Node fst_element_end = RelsUtils::nthElementOfTuple( reasons[i][0], 1 );
625 Node snd_element_begin = RelsUtils::nthElementOfTuple( reasons[i+1][0], 0 );
626 if( fst_element_end != snd_element_begin ) {
627 all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, fst_element_end, snd_element_begin) );
628 }
629 if( tc_rel != reasons[i][1] && tc_rel[0] != reasons[i][1] ) {
630 all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel[0], reasons[i][1]) );
631 }
632 }
633 if( tc_rel != reasons.back()[1] && tc_rel[0] != reasons.back()[1] ) {
634 all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel[0], reasons.back()[1]) );
635 }
636 if( all_reasons.size() > 1) {
637 sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tc_mem, tc_rel), NodeManager::currentNM()->mkNode(kind::AND, all_reasons), "TCLOSURE-Forward");
638 } else {
639 sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tc_mem, tc_rel), all_reasons.front(), "TCLOSURE-Forward");
640 }
641
642 // check if cur_node has been traversed or not
643 if( seen.find( cur_node_rep ) != seen.end() ) {
644 return;
645 }
646 seen.insert( cur_node_rep );
647 TC_GRAPH_IT cur_set = tc_graph.find( cur_node_rep );
648 if( cur_set != tc_graph.end() ) {
649 for( std::hash_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin();
650 set_it != cur_set->second.end(); set_it++ ) {
651 Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it );
652 std::vector< Node > new_reasons( reasons );
653 new_reasons.push_back( rel_tc_graph_exps.find( new_pair )->second );
654 doTCInference( tc_rel, new_reasons, tc_graph, rel_tc_graph_exps, start_node_rep, *set_it, seen );
655 }
656 }
657 }
658
659 /* product-split rule: (a, b) IS_IN (X PRODUCT Y)
660 * ----------------------------------
661 * a IS_IN X && b IS_IN Y
662 *
663 * product-compose rule: (a, b) IS_IN X (c, d) IS_IN Y
664 * ---------------------------------
665 * (a, b, c, d) IS_IN (X PRODUCT Y)
666 */
667
668
669 void TheorySetsRels::applyProductRule( Node pt_rel, Node pt_rel_rep, Node exp ) {
670 Trace("rels-debug") << "\n[Theory::Rels] *********** Applying PRODUCT rule on producted term = " << pt_rel
671 << ", its representative = " << pt_rel_rep
672 << " with explanation = " << exp << std::endl;
673
674 if(d_rel_nodes.find( pt_rel ) == d_rel_nodes.end()) {
675 Trace("rels-debug") << "\n[Theory::Rels] Apply PRODUCT-COMPOSE rule on term: " << pt_rel
676 << " with explanation: " << exp << std::endl;
677
678 computeMembersForBinOpRel( pt_rel );
679 d_rel_nodes.insert( pt_rel );
680 }
681
682 Node mem = exp[0];
683 std::vector<Node> r1_element;
684 std::vector<Node> r2_element;
685 Datatype dt = pt_rel[0].getType().getSetElementType().getDatatype();
686 unsigned int s1_len = pt_rel[0].getType().getSetElementType().getTupleLength();
687 unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength();
688
689 r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
690
691 unsigned int i = 0;
692 for(; i < s1_len; ++i) {
693 r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
694 }
695 dt = pt_rel[1].getType().getSetElementType().getDatatype();
696 r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
697 for(; i < tup_len; ++i) {
698 r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
699 }
700 Node reason = exp;
701 Node mem1 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
702 Node mem2 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r2_element);
703 Node fact_1 = NodeManager::currentNM()->mkNode(kind::MEMBER, mem1, pt_rel[0]);
704 Node fact_2 = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, pt_rel[1]);
705
706 if( pt_rel != exp[1] ) {
707 reason = NodeManager::currentNM()->mkNode(kind::AND, exp, NodeManager::currentNM()->mkNode(kind::EQUAL, pt_rel, exp[1]));
708 }
709 sendInfer( fact_1, reason, "product-split" );
710 sendInfer( fact_2, reason, "product-split" );
711 }
712
713 /* join-split rule: (a, b) IS_IN (X JOIN Y)
714 * --------------------------------------------
715 * exists z | (a, z) IS_IN X && (z, b) IS_IN Y
716 *
717 *
718 * join-compose rule: (a, b) IS_IN X (b, c) IS_IN Y NOT (t, u) IS_IN (X JOIN Y)
719 * -------------------------------------------------------------
720 * (a, c) IS_IN (X JOIN Y)
721 */
722
723 void TheorySetsRels::applyJoinRule( Node join_rel, Node join_rel_rep, Node exp ) {
724 Trace("rels-debug") << "\n[Theory::Rels] *********** Applying JOIN rule on joined term = " << join_rel
725 << ", its representative = " << join_rel_rep
726 << " with explanation = " << exp << std::endl;
727 if(d_rel_nodes.find( join_rel ) == d_rel_nodes.end()) {
728 Trace("rels-debug") << "\n[Theory::Rels] Apply JOIN-COMPOSE rule on term: " << join_rel
729 << " with explanation: " << exp << std::endl;
730
731 computeMembersForBinOpRel( join_rel );
732 d_rel_nodes.insert( join_rel );
733 }
734
735 Node mem = exp[0];
736 std::vector<Node> r1_element;
737 std::vector<Node> r2_element;
738 Node r1_rep = getRepresentative(join_rel[0]);
739 Node r2_rep = getRepresentative(join_rel[1]);
740 TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0];
741 Node shared_x = NodeManager::currentNM()->mkSkolem("srj_", shared_type);
742 Datatype dt = join_rel[0].getType().getSetElementType().getDatatype();
743 unsigned int s1_len = join_rel[0].getType().getSetElementType().getTupleLength();
744 unsigned int tup_len = join_rel.getType().getSetElementType().getTupleLength();
745
746 unsigned int i = 0;
747 r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
748 for(; i < s1_len-1; ++i) {
749 r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
750 }
751 r1_element.push_back(shared_x);
752 dt = join_rel[1].getType().getSetElementType().getDatatype();
753 r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
754 r2_element.push_back(shared_x);
755 for(; i < tup_len; ++i) {
756 r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
757 }
758 Node mem1 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
759 Node mem2 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r2_element);
760
761 computeTupleReps(mem1);
762 computeTupleReps(mem2);
763
764 std::vector<Node> elements = d_membership_trie[r1_rep].findTerms(d_tuple_reps[mem1]);
765
766 for(unsigned int j = 0; j < elements.size(); j++) {
767 std::vector<Node> new_tup;
768 new_tup.push_back(elements[j]);
769 new_tup.insert(new_tup.end(), d_tuple_reps[mem2].begin()+1, d_tuple_reps[mem2].end());
770 if(d_membership_trie[r2_rep].existsTerm(new_tup) != Node::null()) {
771 return;
772 }
773 }
774 Node reason = exp;
775 if( join_rel != exp[1] ) {
776 reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, join_rel, exp[1]));
777 }
778 Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem1, join_rel[0]);
779 sendInfer( fact, reason, "JOIN-Split" );
780 fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, join_rel[1]);
781 sendInfer( fact, reason, "JOIN-Split" );
782 makeSharedTerm( shared_x );
783 }
784
785 /*
786 * transpose-occur rule: (a, b) IS_IN X (TRANSPOSE X) in T
787 * ---------------------------------------
788 * (b, a) IS_IN (TRANSPOSE X)
789 *
790 * transpose-reverse rule: (a, b) IS_IN (TRANSPOSE X)
791 * ---------------------------------------
792 * (b, a) IS_IN X
793 *
794 */
795 void TheorySetsRels::applyTransposeRule( std::vector<Node> tp_terms ) {
796 if( tp_terms.size() < 1) {
797 return;
798 }
799 for( unsigned int i = 1; i < tp_terms.size(); i++ ) {
800 Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE-Equal rule on transposed term = " << tp_terms[0] << " and " << tp_terms[i] << std::endl;
801 sendInfer(NodeManager::currentNM()->mkNode(kind::EQUAL, tp_terms[0][0], tp_terms[i][0]), NodeManager::currentNM()->mkNode(kind::EQUAL, tp_terms[0], tp_terms[i]), "TRANSPOSE-Equal");
802 }
803 }
804
805 void TheorySetsRels::applyTransposeRule( Node tp_rel, Node tp_rel_rep, Node exp ) {
806 Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE rule on transposed term = " << tp_rel
807 << ", its representative = " << tp_rel_rep
808 << " with explanation = " << exp << std::endl;
809
810 if(d_rel_nodes.find( tp_rel ) == d_rel_nodes.end()) {
811 Trace("rels-debug") << "\n[Theory::Rels] Apply TRANSPOSE-Compose rule on term: " << tp_rel
812 << " with explanation: " << exp << std::endl;
813
814 computeMembersForUnaryOpRel( tp_rel );
815 d_rel_nodes.insert( tp_rel );
816 }
817
818 Node reason = exp;
819 Node reversed_mem = RelsUtils::reverseTuple( exp[0] );
820
821 if( tp_rel != exp[1] ) {
822 reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tp_rel, exp[1]));
823 }
824 sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, reversed_mem, tp_rel[0]), reason, "TRANSPOSE-Reverse" );
825 }
826
827 void TheorySetsRels::doTCInference() {
828 Trace("rels-debug") << "[Theory::Rels] ****** Finalizing transitive closure inferences!" << std::endl;
829 TC_IT tc_graph_it = d_tcr_tcGraph.begin();
830 while( tc_graph_it != d_tcr_tcGraph.end() ) {
831 Assert ( d_tcr_tcGraph_exps.find(tc_graph_it->first) != d_tcr_tcGraph_exps.end() );
832 doTCInference( tc_graph_it->second, d_tcr_tcGraph_exps.find(tc_graph_it->first)->second, tc_graph_it->first );
833 tc_graph_it++;
834 }
835 Trace("rels-debug") << "[Theory::Rels] ****** Done with finalizing transitive closure inferences!" << std::endl;
836 }
837
838
839 // Bottom-up fashion to compute relations with more than 1 arity
840 void TheorySetsRels::computeMembersForBinOpRel(Node rel) {
841 Trace("rels-debug") << "\n[Theory::Rels] computeMembersForBinOpRel for relation " << rel << std::endl;
842
843 switch(rel[0].getKind()) {
844 case kind::TRANSPOSE:
845 case kind::TCLOSURE: {
846 computeMembersForUnaryOpRel(rel[0]);
847 break;
848 }
849 case kind::JOIN:
850 case kind::PRODUCT: {
851 computeMembersForBinOpRel(rel[0]);
852 break;
853 }
854 default:
855 break;
856 }
857 switch(rel[1].getKind()) {
858 case kind::TRANSPOSE: {
859 computeMembersForUnaryOpRel(rel[1]);
860 break;
861 }
862 case kind::JOIN:
863 case kind::PRODUCT: {
864 computeMembersForBinOpRel(rel[1]);
865 break;
866 }
867 default:
868 break;
869 }
870 if(d_rReps_memberReps_cache.find(getRepresentative(rel[0])) == d_rReps_memberReps_cache.end() ||
871 d_rReps_memberReps_cache.find(getRepresentative(rel[1])) == d_rReps_memberReps_cache.end()) {
872 return;
873 }
874 composeMembersForRels(rel);
875 }
876
877 // Bottom-up fashion to compute unary relation
878 void TheorySetsRels::computeMembersForUnaryOpRel(Node rel) {
879 Trace("rels-debug") << "\n[Theory::Rels] computeMembersForUnaryOpRel for relation " << rel << std::endl;
880
881 switch(rel[0].getKind()) {
882 case kind::TRANSPOSE:
883 case kind::TCLOSURE:
884 computeMembersForUnaryOpRel(rel[0]);
885 break;
886 case kind::JOIN:
887 case kind::PRODUCT:
888 computeMembersForBinOpRel(rel[0]);
889 break;
890 default:
891 break;
892 }
893
894 Node rel0_rep = getRepresentative(rel[0]);
895 if(d_rReps_memberReps_cache.find( rel0_rep ) == d_rReps_memberReps_cache.end())
896 return;
897
898 std::vector<Node> members = d_rReps_memberReps_cache[rel0_rep];
899 std::vector<Node> exps = d_rReps_memberReps_exp_cache[rel0_rep];
900
901 Assert( members.size() == exps.size() );
902
903 for(unsigned int i = 0; i < members.size(); i++) {
904 Node reason = exps[i];
905 if( rel.getKind() == kind::TRANSPOSE) {
906 if( rel[0] != exps[i][1] ) {
907 reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, rel[0], exps[i][1]));
908 }
909 sendInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel), reason, "TRANSPOSE-reverse");
910 }
911 }
912 }
913
914 /*
915 * Explicitly compose the join or product relations of r1 and r2
916 * e.g. If (a, b) in X and (b, c) in Y, (a, c) in (X JOIN Y)
917 *
918 */
919 void TheorySetsRels::composeMembersForRels( Node rel ) {
920 Trace("rels-debug") << "[Theory::Rels] Start composing members for relation = " << rel << std::endl;
921 Node r1 = rel[0];
922 Node r2 = rel[1];
923 Node r1_rep = getRepresentative( r1 );
924 Node r2_rep = getRepresentative( r2 );
925
926 if(d_rReps_memberReps_cache.find( r1_rep ) == d_rReps_memberReps_cache.end() ||
927 d_rReps_memberReps_cache.find( r2_rep ) == d_rReps_memberReps_cache.end() ) {
928 return;
929 }
930
931 std::vector<Node> r1_rep_exps = d_rReps_memberReps_exp_cache[r1_rep];
932 std::vector<Node> r2_rep_exps = d_rReps_memberReps_exp_cache[r2_rep];
933 unsigned int r1_tuple_len = r1.getType().getSetElementType().getTupleLength();
934 unsigned int r2_tuple_len = r2.getType().getSetElementType().getTupleLength();
935
936 for( unsigned int i = 0; i < r1_rep_exps.size(); i++ ) {
937 for( unsigned int j = 0; j < r2_rep_exps.size(); j++ ) {
938 std::vector<Node> tuple_elements;
939 TypeNode tn = rel.getType().getSetElementType();
940 Node r1_rmost = RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], r1_tuple_len-1 );
941 Node r2_lmost = RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 );
942 tuple_elements.push_back( Node::fromExpr(tn.getDatatype()[0].getConstructor()) );
943
944 if( (areEqual(r1_rmost, r2_lmost) && rel.getKind() == kind::JOIN) ||
945 rel.getKind() == kind::PRODUCT ) {
946 bool isProduct = rel.getKind() == kind::PRODUCT;
947 unsigned int k = 0;
948 unsigned int l = 1;
949
950 for( ; k < r1_tuple_len - 1; ++k ) {
951 tuple_elements.push_back( RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], k ) );
952 }
953 if(isProduct) {
954 tuple_elements.push_back( RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], k ) );
955 tuple_elements.push_back( RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 ) );
956 }
957 for( ; l < r2_tuple_len; ++l ) {
958 tuple_elements.push_back( RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], l ) );
959 }
960
961 Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
962 Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, composed_tuple, rel);
963 std::vector<Node> reasons;
964 reasons.push_back( r1_rep_exps[i] );
965 reasons.push_back( r2_rep_exps[j] );
966
967 if( r1 != r1_rep_exps[i][1] ) {
968 reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1, r1_rep_exps[i][1]) );
969 }
970 if( r2 != r2_rep_exps[j][1] ) {
971 reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r2, r2_rep_exps[j][1]) );
972 }
973 if( isProduct ) {
974 sendInfer( fact, NodeManager::currentNM()->mkNode(kind::AND, reasons), "PRODUCT-Compose" );
975 } else {
976 if( r1_rmost != r2_lmost ) {
977 reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1_rmost, r2_lmost) );
978 }
979 sendInfer( fact, NodeManager::currentNM()->mkNode(kind::AND, reasons), "JOIN-Compose" );
980 }
981 }
982 }
983 }
984
985 }
986
987 void TheorySetsRels::doPendingLemmas() {
988 Trace("rels-debug") << "[Theory::Rels] **************** Start doPendingLemmas !" << std::endl;
989 if( !(*d_conflict) ){
990 if ( (!d_lemmas_out.empty() || !d_pending_facts.empty()) ) {
991 for( unsigned i=0; i < d_lemmas_out.size(); i++ ){
992 Assert(d_lemmas_out[i].getKind() == kind::IMPLIES);
993 if(holds( d_lemmas_out[i][1] )) {
994 Trace("rels-lemma-skip") << "[sets-rels-lemma-skip] Skip an already held lemma: "
995 << d_lemmas_out[i]<< std::endl;
996 continue;
997 }
998 d_sets_theory.d_out->lemma( d_lemmas_out[i] );
999 Trace("rels-lemma") << "[sets-rels-lemma] Send out a lemma : "
1000 << d_lemmas_out[i] << std::endl;
1001 }
1002 for( std::map<Node, Node>::iterator pending_it = d_pending_facts.begin();
1003 pending_it != d_pending_facts.end(); pending_it++ ) {
1004 if( holds( pending_it->first ) ) {
1005 Trace("rels-lemma-skip") << "[sets-rels-fact-lemma-skip] Skip an already held fact,: "
1006 << pending_it->first << std::endl;
1007 continue;
1008 }
1009 Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, pending_it->second, pending_it->first);
1010 if( d_lemmas_produced.find( lemma ) == d_lemmas_produced.end() ) {
1011 d_sets_theory.d_out->lemma(NodeManager::currentNM()->mkNode(kind::IMPLIES, pending_it->second, pending_it->first));
1012 Trace("rels-lemma") << "[sets-rels-fact-lemma] Send out a fact as lemma : "
1013 << pending_it->first << " with reason " << pending_it->second << std::endl;
1014 d_lemmas_produced.insert( lemma );
1015 }
1016 }
1017 }
1018 }
1019 doTCLemmas();
1020 Trace("rels-debug") << "[Theory::Rels] **************** Done with doPendingLemmas !" << std::endl;
1021 d_tuple_reps.clear();
1022 d_rReps_memberReps_exp_cache.clear();
1023 d_terms_cache.clear();
1024 d_lemmas_out.clear();
1025 d_membership_trie.clear();
1026 d_rel_nodes.clear();
1027 d_pending_facts.clear();
1028 d_rReps_memberReps_cache.clear();
1029 d_rRep_tcGraph.clear();
1030 d_tcr_tcGraph_exps.clear();
1031 d_tcr_tcGraph.clear();
1032 d_tc_lemmas_last.clear();
1033 }
1034
1035
1036 bool TheorySetsRels::isRelationKind( Kind k ) {
1037 return k == kind::TRANSPOSE || k == kind::PRODUCT || k == kind::JOIN || k == kind::TCLOSURE;
1038 }
1039
1040 void TheorySetsRels::doTCLemmas() {
1041 Trace("rels-debug") << "[Theory::Rels] **************** Start doTCLemmas !" << std::endl;
1042 std::map< Node, std::vector< Node > >::iterator tc_lemma_it = d_tc_lemmas_last.begin();
1043 while( tc_lemma_it != d_tc_lemmas_last.end() ) {
1044 if( !holds( tc_lemma_it->first[1] ) ) {
1045 if( d_lemmas_produced.find( tc_lemma_it->first ) == d_lemmas_produced.end() ) {
1046 d_sets_theory.d_out->lemma( tc_lemma_it->first );
1047 d_lemmas_produced.insert( tc_lemma_it->first );
1048
1049 for( unsigned int i = 0; i < (tc_lemma_it->second).size(); i++ ) {
1050 if( (tc_lemma_it->second)[i] == d_falseNode ) {
1051 d_sets_theory.d_out->requirePhase((tc_lemma_it->second)[i], true);
1052 }
1053 }
1054 Trace("rels-lemma") << "[Theory::Rels] **** Send out a TC lemma = " << tc_lemma_it->first << " by " << "TCLOSURE-Forward"<< std::endl;
1055 }
1056 }
1057 ++tc_lemma_it;
1058 }
1059 Trace("rels-debug") << "[Theory::Rels] **************** Done with doTCLemmas !" << std::endl;
1060 }
1061
1062 void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) {
1063 if( !holds( conc ) ) {
1064 Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
1065 if( d_lemmas_produced.find( lemma ) == d_lemmas_produced.end() ) {
1066 d_lemmas_out.push_back( lemma );
1067 d_lemmas_produced.insert( lemma );
1068 Trace("rels-send-lemma") << "[Theory::Rels] **** Generate a lemma conclusion = " << conc << " with reason = " << ant << " by " << c << std::endl;
1069 }
1070 }
1071 }
1072
1073 void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) {
1074 if( !holds( fact ) ) {
1075 Trace("rels-send-lemma") << "[Theory::Rels] **** Generate an infered fact "
1076 << fact << " with reason " << exp << " by "<< c << std::endl;
1077 d_pending_facts[fact] = exp;
1078 } else {
1079 Trace("rels-send-lemma-debug") << "[Theory::Rels] **** Generate an infered fact "
1080 << fact << " with reason " << exp << " by "<< c
1081 << ", but it holds already, thus skip it!" << std::endl;
1082 }
1083 }
1084
1085 Node TheorySetsRels::getRepresentative( Node t ) {
1086 if( d_eqEngine->hasTerm( t ) ){
1087 return d_eqEngine->getRepresentative( t );
1088 }else{
1089 return t;
1090 }
1091 }
1092
1093 bool TheorySetsRels::hasTerm( Node a ){
1094 return d_eqEngine->hasTerm( a );
1095 }
1096
1097 bool TheorySetsRels::areEqual( Node a, Node b ){
1098 Assert(a.getType() == b.getType());
1099 Trace("rels-eq") << "[sets-rels]**** checking equality between " << a << " and " << b << std::endl;
1100 if(a == b) {
1101 return true;
1102 } else if( hasTerm( a ) && hasTerm( b ) ){
1103 return d_eqEngine->areEqual( a, b );
1104 } else if(a.getType().isTuple()) {
1105 bool equal = true;
1106 for(unsigned int i = 0; i < a.getType().getTupleLength(); i++) {
1107 equal = equal && areEqual(RelsUtils::nthElementOfTuple(a, i), RelsUtils::nthElementOfTuple(b, i));
1108 }
1109 return equal;
1110 } else if(!a.getType().isBoolean()){
1111 makeSharedTerm(a);
1112 makeSharedTerm(b);
1113 }
1114 return false;
1115 }
1116
1117 /*
1118 * Make sure duplicate members are not added in map
1119 */
1120 bool TheorySetsRels::safelyAddToMap(std::map< Node, std::vector<Node> >& map, Node rel_rep, Node member) {
1121 std::map< Node, std::vector< Node > >::iterator mem_it = map.find(rel_rep);
1122 if(mem_it == map.end()) {
1123 std::vector<Node> members;
1124 members.push_back(member);
1125 map[rel_rep] = members;
1126 return true;
1127 } else {
1128 std::vector<Node>::iterator mems = mem_it->second.begin();
1129 while(mems != mem_it->second.end()) {
1130 if(areEqual(*mems, member)) {
1131 return false;
1132 }
1133 mems++;
1134 }
1135 map[rel_rep].push_back(member);
1136 return true;
1137 }
1138 return false;
1139 }
1140
1141 void TheorySetsRels::addToMap(std::map< Node, std::vector<Node> >& map, Node rel_rep, Node member) {
1142 if(map.find(rel_rep) == map.end()) {
1143 std::vector<Node> members;
1144 members.push_back(member);
1145 map[rel_rep] = members;
1146 } else {
1147 map[rel_rep].push_back(member);
1148 }
1149 }
1150
1151 void TheorySetsRels::addSharedTerm( TNode n ) {
1152 Trace("rels-debug") << "[sets-rels] Add a shared term: " << n << std::endl;
1153 d_sets_theory.addSharedTerm(n);
1154 d_eqEngine->addTriggerTerm(n, THEORY_SETS);
1155 }
1156
1157 void TheorySetsRels::makeSharedTerm( Node n ) {
1158 Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl;
1159 if(d_shared_terms.find(n) == d_shared_terms.end()) {
1160 Node skolem = NodeManager::currentNM()->mkSkolem( "sts", NodeManager::currentNM()->mkSetType( n.getType() ) );
1161 sendLemma(skolem.eqNode(NodeManager::currentNM()->mkNode(kind::SINGLETON,n)), d_trueNode, "share-term");
1162 d_shared_terms.insert(n);
1163 }
1164 }
1165
1166 bool TheorySetsRels::holds(Node node) {
1167 bool polarity = node.getKind() != kind::NOT;
1168 Node atom = polarity ? node : node[0];
1169 return d_sets_theory.isEntailed( atom, polarity );
1170 }
1171
1172 /*
1173 * For each tuple n, we store a mapping between n and a list of its elements representatives
1174 * in d_tuple_reps. This would later be used for applying JOIN operator.
1175 */
1176 void TheorySetsRels::computeTupleReps( Node n ) {
1177 if( d_tuple_reps.find( n ) == d_tuple_reps.end() ){
1178 for( unsigned i = 0; i < n.getType().getTupleLength(); i++ ){
1179 d_tuple_reps[n].push_back( getRepresentative( RelsUtils::nthElementOfTuple(n, i) ) );
1180 }
1181 }
1182 }
1183
1184 /*
1185 * Node n[0] is a tuple variable, reduce n[0] to a concrete representation,
1186 * which is (e1, ..., en) where e1, ... ,en are concrete elements of tuple n[0].
1187 */
1188 void TheorySetsRels::reduceTupleVar(Node n) {
1189 if(d_symbolic_tuples.find(n) == d_symbolic_tuples.end()) {
1190 Trace("rels-debug") << "[Theory::Rels] Reduce tuple var: " << n[0] << " to a concrete one " << " node = " << n << std::endl;
1191 std::vector<Node> tuple_elements;
1192 tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor()));
1193 for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) {
1194 Node element = RelsUtils::nthElementOfTuple(n[0], i);
1195 makeSharedTerm(element);
1196 tuple_elements.push_back(element);
1197 }
1198 Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
1199 tuple_reduct = NodeManager::currentNM()->mkNode(kind::MEMBER,tuple_reduct, n[1]);
1200 Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::EQUAL, n, tuple_reduct);
1201 sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction");
1202 d_symbolic_tuples.insert(n);
1203 }
1204 }
1205
1206 TheorySetsRels::TheorySetsRels( context::Context* c,
1207 context::UserContext* u,
1208 eq::EqualityEngine* eq,
1209 context::CDO<bool>* conflict,
1210 TheorySets& d_set ):
1211 d_eqEngine(eq),
1212 d_conflict(conflict),
1213 d_sets_theory(d_set),
1214 d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)),
1215 d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)),
1216 d_pending_merge(c),
1217 d_lemmas_produced(u),
1218 d_shared_terms(u)
1219 {
1220 d_eqEngine->addFunctionKind(kind::PRODUCT);
1221 d_eqEngine->addFunctionKind(kind::JOIN);
1222 d_eqEngine->addFunctionKind(kind::TRANSPOSE);
1223 d_eqEngine->addFunctionKind(kind::TCLOSURE);
1224 d_eqEngine->addFunctionKind(kind::JOIN_IMAGE);
1225 d_eqEngine->addFunctionKind(kind::IDEN);
1226 }
1227
1228 TheorySetsRels::~TheorySetsRels() {
1229 for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end();
1230 i != iend; ++i){
1231 EqcInfo* current = (*i).second;
1232 Assert(current != NULL);
1233 delete current;
1234 }
1235 }
1236
1237 std::vector<Node> TupleTrie::findTerms( std::vector< Node >& reps, int argIndex ) {
1238 std::vector<Node> nodes;
1239 std::map< Node, TupleTrie >::iterator it;
1240
1241 if( argIndex==(int)reps.size()-1 ){
1242 if(reps[argIndex].getKind() == kind::SKOLEM) {
1243 it = d_data.begin();
1244 while(it != d_data.end()) {
1245 nodes.push_back(it->first);
1246 it++;
1247 }
1248 }
1249 return nodes;
1250 }else{
1251 it = d_data.find( reps[argIndex] );
1252 if( it==d_data.end() ){
1253 return nodes;
1254 }else{
1255 return it->second.findTerms( reps, argIndex+1 );
1256 }
1257 }
1258 }
1259
1260 std::vector<Node> TupleTrie::findSuccessors( std::vector< Node >& reps, int argIndex ) {
1261 std::vector<Node> nodes;
1262 std::map< Node, TupleTrie >::iterator it;
1263
1264 if( argIndex==(int)reps.size() ){
1265 it = d_data.begin();
1266 while(it != d_data.end()) {
1267 nodes.push_back(it->first);
1268 it++;
1269 }
1270 return nodes;
1271 }else{
1272 it = d_data.find( reps[argIndex] );
1273 if( it==d_data.end() ){
1274 return nodes;
1275 }else{
1276 return it->second.findSuccessors( reps, argIndex+1 );
1277 }
1278 }
1279 }
1280
1281 Node TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) {
1282 if( argIndex==(int)reps.size() ){
1283 if( d_data.empty() ){
1284 return Node::null();
1285 }else{
1286 return d_data.begin()->first;
1287 }
1288 }else{
1289 std::map< Node, TupleTrie >::iterator it = d_data.find( reps[argIndex] );
1290 if( it==d_data.end() ){
1291 return Node::null();
1292 }else{
1293 return it->second.existsTerm( reps, argIndex+1 );
1294 }
1295 }
1296 }
1297
1298 bool TupleTrie::addTerm( Node n, std::vector< Node >& reps, int argIndex ){
1299 if( argIndex==(int)reps.size() ){
1300 if( d_data.empty() ){
1301 //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
1302 d_data[n].clear();
1303 return true;
1304 }else{
1305 return false;
1306 }
1307 }else{
1308 return d_data[reps[argIndex]].addTerm( n, reps, argIndex+1 );
1309 }
1310 }
1311
1312 void TupleTrie::debugPrint( const char * c, Node n, unsigned depth ) {
1313 for( std::map< Node, TupleTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
1314 for( unsigned i=0; i<depth; i++ ){ Debug(c) << " "; }
1315 Debug(c) << it->first << std::endl;
1316 it->second.debugPrint( c, n, depth+1 );
1317 }
1318 }
1319
1320 TheorySetsRels::EqcInfo::EqcInfo( context::Context* c ) :
1321 d_mem(c), d_mem_exp(c), d_tp(c), d_pt(c), d_tc(c), d_rel_tc(c) {}
1322
1323 void TheorySetsRels::eqNotifyNewClass( Node n ) {
1324 Trace("rels-std") << "[sets-rels] eqNotifyNewClass:" << " t = " << n << std::endl;
1325 if(n.getKind() == kind::TRANSPOSE || n.getKind() == kind::PRODUCT || n.getKind() == kind::TCLOSURE) {
1326 getOrMakeEqcInfo( n, true );
1327 if( n.getKind() == kind::TCLOSURE ) {
1328 Node relRep_of_tc = getRepresentative( n[0] );
1329 EqcInfo* rel_ei = getOrMakeEqcInfo( relRep_of_tc, true );
1330
1331 if( rel_ei->d_rel_tc.get().isNull() ) {
1332 rel_ei->d_rel_tc = n;
1333 Node exp = relRep_of_tc == n[0] ? d_trueNode : NodeManager::currentNM()->mkNode( kind::EQUAL, relRep_of_tc, n[0] );
1334 for( NodeSet::const_iterator mem_it = rel_ei->d_mem.begin(); mem_it != rel_ei->d_mem.end(); mem_it++ ) {
1335 Node mem_exp = (*rel_ei->d_mem_exp.find(*mem_it)).second;
1336 exp = NodeManager::currentNM()->mkNode( kind::AND, exp, mem_exp);
1337 if( mem_exp[1] != relRep_of_tc ) {
1338 exp = NodeManager::currentNM()->mkNode( kind::AND, exp, NodeManager::currentNM()->mkNode(kind::EQUAL, relRep_of_tc, mem_exp[1] ) );
1339 }
1340 sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, mem_exp[0], n), exp, "TCLOSURE-UP I" );
1341 }
1342 }
1343 }
1344 }
1345 }
1346
1347 // Merge t2 into t1, t1 will be the rep of the new eqc
1348 void TheorySetsRels::eqNotifyPostMerge( Node t1, Node t2 ) {
1349 Trace("rels-std") << "[sets-rels-std] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1350
1351 // Merge membership constraint with "true" eqc
1352 if( t1 == d_trueNode && t2.getKind() == kind::MEMBER && t2[0].getType().isTuple() ) {
1353 Node mem_rep = getRepresentative( t2[0] );
1354 Node t2_1rep = getRepresentative( t2[1] );
1355 EqcInfo* ei = getOrMakeEqcInfo( t2_1rep, true );
1356 if(ei->d_mem.contains(mem_rep)) {
1357 return;
1358 }
1359 Node exp = t2;
1360
1361 ei->d_mem.insert( mem_rep );
1362 ei->d_mem_exp.insert( mem_rep, exp );
1363
1364 // Process a membership constraint that a tuple is a member of transpose of rel
1365 if( !ei->d_tp.get().isNull() ) {
1366 if( ei->d_tp.get() != t2[1] ) {
1367 exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_tp.get(), t2[1]), t2 );
1368 }
1369 sendInferTranspose( t2[0], ei->d_tp.get(), exp );
1370 }
1371 // Process a membership constraint that a tuple is a member of product of rel
1372 if( !ei->d_pt.get().isNull() ) {
1373 if( ei->d_pt.get() != t2[1] ) {
1374 exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_pt.get(), t2[1]), t2 );
1375 }
1376 sendInferProduct( t2[0], ei->d_pt.get(), exp );
1377 }
1378
1379 if( !ei->d_rel_tc.get().isNull() ) {
1380 if( ei->d_rel_tc.get()[0] != t2[1] ) {
1381 exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_rel_tc.get()[0], t2[1]), t2 );
1382 }
1383 sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t2[0], ei->d_rel_tc.get()), exp, "TCLOSURE-UP I");
1384 }
1385 // Process a membership constraint that a tuple is a member of transitive closure of rel
1386 if( !ei->d_tc.get().isNull() ) {
1387 sendInferTClosure( t2, ei );
1388 }
1389
1390 // Merge two relation eqcs
1391 } else if( t1.getType().isSet() && t2.getType().isSet() && t1.getType().getSetElementType().isTuple() ) {
1392 EqcInfo* t1_ei = getOrMakeEqcInfo( t1 );
1393 EqcInfo* t2_ei = getOrMakeEqcInfo( t2 );
1394
1395 if( t1_ei != NULL && t2_ei != NULL ) {
1396 if( !t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) {
1397 sendInferTranspose(t1_ei->d_tp.get(), t2_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::EQUAL, t1_ei->d_tp.get(), t2_ei->d_tp.get() ) );
1398 }
1399 std::vector< Node > t2_new_mems;
1400 std::vector< Node > t2_new_exps;
1401 NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin();
1402 NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin();
1403
1404 for( ; t2_mem_it != t2_ei->d_mem.end(); t2_mem_it++ ) {
1405 if( !t1_ei->d_mem.contains( *t2_mem_it ) ) {
1406 Node t2_mem_exp = (*t2_ei->d_mem_exp.find(*t2_mem_it)).second;
1407
1408 if( t2_ei->d_tp.get().isNull() && !t1_ei->d_tp.get().isNull() ) {
1409 Node reason = t1_ei->d_tp.get() == (t2_mem_exp)[1]
1410 ? (t2_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t2_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_mem_exp)[1], t1_ei->d_tp.get()));
1411 sendInferTranspose( t2_mem_exp[0], t1_ei->d_tp.get(), reason );
1412 }
1413 if( t2_ei->d_pt.get().isNull() && !t1_ei->d_pt.get().isNull() ) {
1414 Node reason = t1_ei->d_pt.get() == (t2_mem_exp)[1]
1415 ? (t2_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t2_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_mem_exp)[1], t1_ei->d_pt.get()));
1416 sendInferProduct( t2_mem_exp[0], t1_ei->d_pt.get(), reason );
1417 }
1418 if( t2_ei->d_tc.get().isNull() && !t1_ei->d_tc.get().isNull() ) {
1419 sendInferTClosure( t2_mem_exp, t1_ei );
1420 }
1421 if( t2_ei->d_rel_tc.get().isNull() && !t1_ei->d_rel_tc.get().isNull() ) {
1422 Node reason = t1_ei->d_rel_tc.get()[0] == t2_mem_exp[1] ?
1423 t2_mem_exp : NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, t1_ei->d_rel_tc.get()[0], t2_mem_exp[1]), t2_mem_exp );
1424 sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t2_mem_exp[0], t1_ei->d_rel_tc.get()), reason, "TCLOSURE-UP I");
1425 }
1426 t2_new_mems.push_back( *t2_mem_it );
1427 t2_new_exps.push_back( t2_mem_exp );
1428 }
1429 }
1430 for( ; t1_mem_it != t1_ei->d_mem.end(); t1_mem_it++ ) {
1431 if( !t2_ei->d_mem.contains( *t1_mem_it ) ) {
1432 Node t1_mem_exp = (*t1_ei->d_mem_exp.find(*t1_mem_it)).second;
1433 if( t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) {
1434 Node reason = t2_ei->d_tp.get() == (t1_mem_exp)[1]
1435 ? (t1_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t1_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_mem_exp)[1], t2_ei->d_tp.get()));
1436 sendInferTranspose( (t1_mem_exp)[0], t2_ei->d_tp.get(), reason );
1437 }
1438 if( t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) {
1439 Node reason = t2_ei->d_pt.get() == (t1_mem_exp)[1]
1440 ? (t1_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t1_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_mem_exp)[1], t2_ei->d_pt.get()));
1441 sendInferProduct( (t1_mem_exp)[0], t2_ei->d_pt.get(), reason );
1442 }
1443 if( t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) {
1444 sendInferTClosure(t1_mem_exp, t2_ei );
1445 }
1446 if( t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) {
1447 Node reason = t2_ei->d_rel_tc.get()[0] == t1_mem_exp[1] ?
1448 t1_mem_exp : NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, t2_ei->d_rel_tc.get()[0], t1_mem_exp[1]), t1_mem_exp );
1449 sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t1_mem_exp[0], t2_ei->d_rel_tc.get()), reason, "TCLOSURE-UP I");
1450 }
1451 }
1452 }
1453 std::vector< Node >::iterator t2_new_mem_it = t2_new_mems.begin();
1454 std::vector< Node >::iterator t2_new_exp_it = t2_new_exps.begin();
1455 for( ; t2_new_mem_it != t2_new_mems.end(); t2_new_mem_it++, t2_new_exp_it++ ) {
1456 t1_ei->d_mem.insert( *t2_new_mem_it );
1457 t1_ei->d_mem_exp.insert( *t2_new_mem_it, *t2_new_exp_it );
1458 }
1459 if( t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) {
1460 t1_ei->d_tp.set(t2_ei->d_tp.get());
1461 }
1462 if( t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) {
1463 t1_ei->d_pt.set(t2_ei->d_pt.get());
1464 }
1465 if( t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) {
1466 t1_ei->d_tc.set(t2_ei->d_tc.get());
1467 }
1468 if( t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) {
1469 t1_ei->d_rel_tc.set(t2_ei->d_rel_tc.get());
1470 }
1471 } else if( t1_ei != NULL ) {
1472 if( (t2.getKind() == kind::TRANSPOSE && t1_ei->d_tp.get().isNull()) ||
1473 (t2.getKind() == kind::PRODUCT && t1_ei->d_pt.get().isNull()) ||
1474 (t2.getKind() == kind::TCLOSURE && t1_ei->d_tc.get().isNull()) ) {
1475 NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin();
1476
1477 if( t2.getKind() == kind::TRANSPOSE ) {
1478 t1_ei->d_tp = t2;
1479 } else if( t2.getKind() == kind::PRODUCT ) {
1480 t1_ei->d_pt = t2;
1481 } else if( t2.getKind() == kind::TCLOSURE ) {
1482 t1_ei->d_tc = t2;
1483 }
1484 for( ; t1_mem_it != t1_ei->d_mem.end(); t1_mem_it++ ) {
1485 Node t1_exp = (*t1_ei->d_mem_exp.find(*t1_mem_it)).second;
1486 if( t2.getKind() == kind::TRANSPOSE ) {
1487 Node reason = t2 == t1_exp[1]
1488 ? (t1_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t1_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_exp)[1], t2));
1489 sendInferTranspose( (t1_exp)[0], t2, reason );
1490 } else if( t2.getKind() == kind::PRODUCT ) {
1491 Node reason = t2 == (t1_exp)[1]
1492 ? (t1_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t1_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_exp)[1], t2));
1493 sendInferProduct( (t1_exp)[0], t2, reason );
1494 } else if( t2.getKind() == kind::TCLOSURE ) {
1495 sendInferTClosure( t1_exp, t1_ei );
1496 }
1497 }
1498 }
1499 } else if( t2_ei != NULL ) {
1500 EqcInfo* new_t1_ei = getOrMakeEqcInfo( t1, true );
1501 if( new_t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) {
1502 new_t1_ei->d_tp.set(t2_ei->d_tp.get());
1503 }
1504 if( new_t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) {
1505 new_t1_ei->d_pt.set(t2_ei->d_pt.get());
1506 }
1507 if( new_t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) {
1508 new_t1_ei->d_tc.set(t2_ei->d_tc.get());
1509 }
1510 if( new_t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) {
1511 new_t1_ei->d_rel_tc.set(t2_ei->d_rel_tc.get());
1512 }
1513 if( (t1.getKind() == kind::TRANSPOSE && t2_ei->d_tp.get().isNull()) ||
1514 (t1.getKind() == kind::PRODUCT && t2_ei->d_pt.get().isNull()) ||
1515 (t1.getKind() == kind::TCLOSURE && t2_ei->d_tc.get().isNull()) ) {
1516 NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin();
1517
1518 for( ; t2_mem_it != t2_ei->d_mem.end(); t2_mem_it++ ) {
1519 Node t2_exp = (*t1_ei->d_mem_exp.find(*t2_mem_it)).second;
1520
1521 if( t1.getKind() == kind::TRANSPOSE ) {
1522 Node reason = t1 == (t2_exp)[1]
1523 ? (t2_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t2_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_exp)[1], t1));
1524 sendInferTranspose( (t2_exp)[0], t1, reason );
1525 } else if( t1.getKind() == kind::PRODUCT ) {
1526 Node reason = t1 == (t2_exp)[1]
1527 ? (t2_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t2_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_exp)[1], t1));
1528 sendInferProduct( (t2_exp)[0], t1, reason );
1529 } else if( t1.getKind() == kind::TCLOSURE ) {
1530 sendInferTClosure( t2_exp, new_t1_ei );
1531 }
1532 }
1533 }
1534 }
1535 }
1536
1537 Trace("rels-std") << "[sets-rels] done with eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1538 }
1539
1540 void TheorySetsRels::sendInferTClosure( Node new_mem_exp, EqcInfo* ei ) {
1541 NodeSet::const_iterator mem_it = ei->d_mem.begin();
1542 Node mem_rep = getRepresentative( new_mem_exp[0] );
1543 Node new_mem_rel = new_mem_exp[1];
1544 Node new_mem_fst = RelsUtils::nthElementOfTuple( new_mem_exp[0], 0 );
1545 Node new_mem_snd = RelsUtils::nthElementOfTuple( new_mem_exp[0], 1 );
1546 for( ; mem_it != ei->d_mem.end(); mem_it++ ) {
1547 if( *mem_it == mem_rep ) {
1548 continue;
1549 }
1550 Node d_mem_exp = (*ei->d_mem_exp.find(*mem_it)).second;
1551 Node d_mem_fst = RelsUtils::nthElementOfTuple( d_mem_exp[0], 0 );
1552 Node d_mem_snd = RelsUtils::nthElementOfTuple( d_mem_exp[0], 1 );
1553 Node d_mem_rel = d_mem_exp[1];
1554 if( areEqual( new_mem_fst, d_mem_snd) ) {
1555 Node reason = NodeManager::currentNM()->mkNode( kind::AND, new_mem_exp, d_mem_exp );
1556 reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_fst, d_mem_snd ) );
1557 if( new_mem_rel != ei->d_tc.get() ) {
1558 reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_rel, ei->d_tc.get() ) );
1559 }
1560 if( d_mem_rel != ei->d_tc.get() ) {
1561 reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, d_mem_rel, ei->d_tc.get() ) );
1562 }
1563 Node new_membership = NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( d_mem_rel, d_mem_fst, new_mem_snd ), ei->d_tc.get() );
1564 sendMergeInfer( new_membership, reason, "TCLOSURE-UP II" );
1565 }
1566 if( areEqual( new_mem_snd, d_mem_fst ) ) {
1567 Node reason = NodeManager::currentNM()->mkNode( kind::AND, new_mem_exp, d_mem_exp );
1568 reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_snd, d_mem_fst ) );
1569 if( new_mem_rel != ei->d_tc.get() ) {
1570 reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_rel, ei->d_tc.get() ) );
1571 }
1572 if( d_mem_rel != ei->d_tc.get() ) {
1573 reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, d_mem_rel, ei->d_tc.get() ) );
1574 }
1575 Node new_membership = NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( d_mem_rel, new_mem_fst, d_mem_snd ), ei->d_tc.get() );
1576 sendMergeInfer( new_membership, reason, "TCLOSURE-UP II" );
1577 }
1578 }
1579 }
1580
1581
1582 void TheorySetsRels::doPendingMerge() {
1583 for( NodeList::const_iterator itr = d_pending_merge.begin(); itr != d_pending_merge.end(); itr++ ) {
1584 if( !holds(*itr) ) {
1585 if( d_lemmas_produced.find(*itr)==d_lemmas_produced.end() ) {
1586 Trace("rels-std-lemma") << "[std-sets-rels-lemma] Send out a merge fact as lemma: "
1587 << *itr << std::endl;
1588 d_sets_theory.d_out->lemma( *itr );
1589 d_lemmas_produced.insert(*itr);
1590 }
1591 }
1592 }
1593 }
1594
1595 // t1 and t2 can be both relations
1596 // or t1 is a tuple, t2 is a transposed relation
1597 void TheorySetsRels::sendInferTranspose( Node t1, Node t2, Node exp ) {
1598 Assert( t2.getKind() == kind::TRANSPOSE );
1599
1600 if( isRel(t1) && isRel(t2) ) {
1601 Assert(t1.getKind() == kind::TRANSPOSE);
1602 sendMergeInfer(NodeManager::currentNM()->mkNode(kind::EQUAL, t1[0], t2[0]), exp, "Transpose-Equal");
1603 return;
1604 }
1605 sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(t1), t2[0]), exp, "Transpose-Rule");
1606 }
1607
1608 void TheorySetsRels::sendMergeInfer( Node fact, Node reason, const char * c ) {
1609 if( !holds( fact ) ) {
1610 Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, reason, fact);
1611 d_pending_merge.push_back(lemma);
1612 Trace("rels-std") << "[std-rels-lemma] Generate a lemma by applying " << c
1613 << ": " << lemma << std::endl;
1614 }
1615 }
1616
1617 void TheorySetsRels::sendInferProduct( Node member, Node pt_rel, Node exp ) {
1618 Assert( pt_rel.getKind() == kind::PRODUCT );
1619
1620 std::vector<Node> r1_element;
1621 std::vector<Node> r2_element;
1622 Node r1 = pt_rel[0];
1623 Node r2 = pt_rel[1];
1624 Datatype dt = r1.getType().getSetElementType().getDatatype();
1625 unsigned int i = 0;
1626 unsigned int s1_len = r1.getType().getSetElementType().getTupleLength();
1627 unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength();
1628
1629 r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
1630 for( ; i < s1_len; ++i ) {
1631 r1_element.push_back( RelsUtils::nthElementOfTuple( member, i ) );
1632 }
1633
1634 dt = r2.getType().getSetElementType().getDatatype();
1635 r2_element.push_back( Node::fromExpr( dt[0].getConstructor() ) );
1636 for( ; i < tup_len; ++i ) {
1637 r2_element.push_back( RelsUtils::nthElementOfTuple(member, i) );
1638 }
1639
1640 Node tuple_1 = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, r1_element );
1641 Node tuple_2 = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, r2_element );
1642 sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_1, r1), exp, "Product-Split" );
1643 sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_2, r2), exp, "Product-Split" );
1644 }
1645
1646 TheorySetsRels::EqcInfo* TheorySetsRels::getOrMakeEqcInfo( Node n, bool doMake ){
1647 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
1648 if( eqc_i == d_eqc_info.end() ){
1649 if( doMake ){
1650 EqcInfo* ei;
1651 if( eqc_i!=d_eqc_info.end() ){
1652 ei = eqc_i->second;
1653 }else{
1654 ei = new EqcInfo(d_sets_theory.getSatContext());
1655 d_eqc_info[n] = ei;
1656 }
1657 if( n.getKind() == kind::TRANSPOSE ){
1658 ei->d_tp = n;
1659 } else if( n.getKind() == kind::PRODUCT ) {
1660 ei->d_pt = n;
1661 } else if( n.getKind() == kind::TCLOSURE ) {
1662 ei->d_tc = n;
1663 }
1664 return ei;
1665 }else{
1666 return NULL;
1667 }
1668 }else{
1669 return (*eqc_i).second;
1670 }
1671 }
1672
1673
1674 Node TheorySetsRels::mkAnd( std::vector<TNode>& conjunctions ) {
1675 Assert(conjunctions.size() > 0);
1676 std::set<TNode> all;
1677
1678 for (unsigned i = 0; i < conjunctions.size(); ++i) {
1679 TNode t = conjunctions[i];
1680 if (t.getKind() == kind::AND) {
1681 for(TNode::iterator child_it = t.begin();
1682 child_it != t.end(); ++child_it) {
1683 Assert((*child_it).getKind() != kind::AND);
1684 all.insert(*child_it);
1685 }
1686 }
1687 else {
1688 all.insert(t);
1689 }
1690 }
1691 Assert(all.size() > 0);
1692 if (all.size() == 1) {
1693 // All the same, or just one
1694 return conjunctions[0];
1695 }
1696
1697 NodeBuilder<> conjunction(kind::AND);
1698 std::set<TNode>::const_iterator it = all.begin();
1699 std::set<TNode>::const_iterator it_end = all.end();
1700 while (it != it_end) {
1701 conjunction << *it;
1702 ++ it;
1703 }
1704
1705 return conjunction;
1706 }/* mkAnd() */
1707
1708 void TheorySetsRels::printNodeMap(char* fst, char* snd, NodeMap map) {
1709 NodeMap::iterator map_it = map.begin();
1710 while(map_it != map.end()) {
1711 Trace("rels-debug") << fst << " "<< (*map_it).first << " " << snd << " " << (*map_it).second<< std::endl;
1712 map_it++;
1713 }
1714 }
1715
1716 }
1717 }
1718 }