GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/theory_sets_rels.cpp Lines: 755 790 95.6 %
Date: 2021-03-23 Branches: 1709 3285 52.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sets_rels.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Paul Meng, Gereon Kremer
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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 "theory/sets/theory_sets_private.h"
19
#include "theory/sets/theory_sets.h"
20
21
using namespace std;
22
using namespace CVC4::kind;
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::unordered_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::unordered_set< Node, NodeHashFunction > > >::iterator   TC_IT;
33
34
8997
TheorySetsRels::TheorySetsRels(SolverState& s,
35
                               InferenceManager& im,
36
                               SkolemCache& skc,
37
8997
                               TermRegistry& treg)
38
    : d_state(s),
39
      d_im(im),
40
      d_skCache(skc),
41
      d_treg(treg),
42
8997
      d_shared_terms(s.getUserContext())
43
{
44
8997
  d_trueNode = NodeManager::currentNM()->mkConst(true);
45
8997
  d_falseNode = NodeManager::currentNM()->mkConst(false);
46
8997
}
47
48
8994
TheorySetsRels::~TheorySetsRels() {}
49
50
689
void TheorySetsRels::check(Theory::Effort level)
51
{
52
1378
  Trace("rels") << "\n[sets-rels] ******************************* Start the "
53
689
                   "relational solver, effort = "
54
689
                << level << " *******************************\n"
55
689
                << std::endl;
56
689
  if (Theory::fullEffort(level))
57
  {
58
689
    collectRelsInfo();
59
689
    check();
60
689
    doPendingInfers();
61
  }
62
689
  Assert(d_pending.empty());
63
1378
  Trace("rels") << "\n[sets-rels] ******************************* Done with "
64
689
                   "the relational solver *******************************\n"
65
689
                << std::endl;
66
689
}
67
68
689
  void TheorySetsRels::check() {
69
689
    MEM_IT m_it = d_rReps_memberReps_cache.begin();
70
71
5597
    while(m_it != d_rReps_memberReps_cache.end()) {
72
4908
      Node rel_rep = m_it->first;
73
74
11066
      for(unsigned int i = 0; i < m_it->second.size(); i++) {
75
17224
        Node    mem     = d_rReps_memberReps_cache[rel_rep][i];
76
17224
        Node    exp     = d_rReps_memberReps_exp_cache[rel_rep][i];
77
        std::map<kind::Kind_t, std::vector<Node> >& kind_terms =
78
8612
            d_terms_cache[rel_rep];
79
80
8612
        if( kind_terms.find(kind::TRANSPOSE) != kind_terms.end() ) {
81
1270
          std::vector<Node>& tp_terms = kind_terms[TRANSPOSE];
82
1270
          if( tp_terms.size() > 0 ) {
83
1270
            applyTransposeRule( tp_terms );
84
1270
            applyTransposeRule( tp_terms[0], rel_rep, exp );
85
          }
86
        }
87
8612
        if( kind_terms.find(kind::JOIN) != kind_terms.end() ) {
88
1144
          std::vector<Node>& join_terms = kind_terms[JOIN];
89
2456
          for( unsigned int j = 0; j < join_terms.size(); j++ ) {
90
1312
            applyJoinRule( join_terms[j], rel_rep, exp );
91
          }
92
        }
93
8612
        if( kind_terms.find(kind::PRODUCT) != kind_terms.end() ) {
94
135
          std::vector<Node>& product_terms = kind_terms[PRODUCT];
95
270
          for( unsigned int j = 0; j < product_terms.size(); j++ ) {
96
135
            applyProductRule( product_terms[j], rel_rep, exp );
97
          }
98
        }
99
8612
        if( kind_terms.find(kind::TCLOSURE) != kind_terms.end() ) {
100
252
          std::vector<Node>& tc_terms = kind_terms[TCLOSURE];
101
504
          for( unsigned int j = 0; j < tc_terms.size(); j++ ) {
102
252
            applyTCRule( mem, tc_terms[j], rel_rep, exp );
103
          }
104
        }
105
8612
        if( kind_terms.find(kind::JOIN_IMAGE) != kind_terms.end() ) {
106
139
          std::vector<Node>& join_image_terms = kind_terms[JOIN_IMAGE];
107
278
          for( unsigned int j = 0; j < join_image_terms.size(); j++ ) {
108
139
            applyJoinImageRule( mem, join_image_terms[j], exp );
109
          }
110
        }
111
8612
        if( kind_terms.find(kind::IDEN) != kind_terms.end() ) {
112
15
          std::vector<Node>& iden_terms = kind_terms[IDEN];
113
30
          for( unsigned int j = 0; j < iden_terms.size(); j++ ) {
114
15
            applyIdenRule( mem, iden_terms[j], exp );
115
          }
116
        }
117
      }
118
2454
      ++m_it;
119
    }
120
121
689
    TERM_IT t_it = d_terms_cache.begin();
122
6865
    while( t_it != d_terms_cache.end() ) {
123
3088
      if( d_rReps_memberReps_cache.find(t_it->first) == d_rReps_memberReps_cache.end() ) {
124
634
        Trace("rels-debug") << "[sets-rels] A term does not have membership constraints: " << t_it->first << std::endl;
125
634
        KIND_TERM_IT k_t_it = t_it->second.begin();
126
127
1902
        while( k_t_it != t_it->second.end() ) {
128
634
          if( k_t_it->first == kind::JOIN || k_t_it->first == kind::PRODUCT ) {
129
413
            std::vector<Node>::iterator term_it = k_t_it->second.begin();
130
1247
            while(term_it != k_t_it->second.end()) {
131
417
              computeMembersForBinOpRel( *term_it );
132
417
              ++term_it;
133
            }
134
221
          } else if( k_t_it->first == kind::TRANSPOSE ) {
135
180
            std::vector<Node>::iterator term_it = k_t_it->second.begin();
136
540
            while( term_it != k_t_it->second.end() ) {
137
180
              computeMembersForUnaryOpRel( *term_it );
138
180
              ++term_it;
139
            }
140
41
          } else if ( k_t_it->first == kind::TCLOSURE ) {
141
31
            std::vector<Node>::iterator term_it = k_t_it->second.begin();
142
93
            while( term_it != k_t_it->second.end() ) {
143
31
              buildTCGraphForRel( *term_it );
144
31
              ++term_it;
145
            }
146
10
          } else if( k_t_it->first == kind::JOIN_IMAGE ) {
147
2
            std::vector<Node>::iterator term_it = k_t_it->second.begin();
148
6
            while( term_it != k_t_it->second.end() ) {
149
2
              computeMembersForJoinImageTerm( *term_it );
150
2
              ++term_it;
151
            }
152
8
          } else if( k_t_it->first == kind::IDEN ) {
153
8
            std::vector<Node>::iterator term_it = k_t_it->second.begin();
154
24
            while( term_it != k_t_it->second.end() ) {
155
8
              computeMembersForIdenTerm( *term_it );
156
8
              ++term_it;
157
            }
158
          }
159
634
          ++k_t_it;
160
        }
161
      }
162
3088
      ++t_it;
163
    }
164
689
    doTCInference();
165
166
    // clean up
167
689
    d_tuple_reps.clear();
168
689
    d_rReps_memberReps_exp_cache.clear();
169
689
    d_terms_cache.clear();
170
689
    d_membership_trie.clear();
171
689
    d_rel_nodes.clear();
172
689
    d_rReps_memberReps_cache.clear();
173
689
    d_rRep_tcGraph.clear();
174
689
    d_tcr_tcGraph_exps.clear();
175
689
    d_tcr_tcGraph.clear();
176
689
  }
177
178
  /*
179
   * Populate relational terms data structure
180
   */
181
182
689
  void TheorySetsRels::collectRelsInfo() {
183
689
    Trace("rels") << "[sets-rels] Start collecting relational terms..." << std::endl;
184
689
    eq::EqualityEngine* ee = d_state.getEqualityEngine();
185
689
    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
186
41697
    while( !eqcs_i.isFinished() ){
187
41008
      Node                      eqc_rep  = (*eqcs_i);
188
20504
      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc_rep, ee);
189
190
41008
      TypeNode erType = eqc_rep.getType();
191
20504
      Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << " with type " << eqc_rep.getType() << std::endl;
192
193
128364
      while( !eqc_i.isFinished() ){
194
107860
        Node eqc_node = (*eqc_i);
195
196
53930
        Trace("rels-ee") << "  term : " << eqc_node << std::endl;
197
198
53930
        if (erType.isBoolean() && eqc_rep.isConst())
199
        {
200
          // collect membership info
201
22009
          if( eqc_node.getKind() == kind::MEMBER && eqc_node[1].getType().getSetElementType().isTuple()) {
202
25956
            Node tup_rep = getRepresentative( eqc_node[0] );
203
25956
            Node rel_rep = getRepresentative( eqc_node[1] );
204
205
12978
            if( eqc_node[0].isVar() ){
206
1817
              reduceTupleVar( eqc_node );
207
            }
208
209
12978
            bool is_true_eq = eqc_rep.getConst<bool>();
210
25956
            Node reason        = is_true_eq ? eqc_node : eqc_node.negate();
211
212
12978
            if( is_true_eq ) {
213
11761
              if( safelyAddToMap(d_rReps_memberReps_cache, rel_rep, tup_rep) ) {
214
8612
                d_rReps_memberReps_exp_cache[rel_rep].push_back(reason);
215
8612
                computeTupleReps(tup_rep);
216
8612
                d_membership_trie[rel_rep].addTerm(tup_rep, d_tuple_reps[tup_rep]);
217
              }
218
            }
219
          }
220
        // collect relational terms info
221
        }
222
31921
        else if (erType.isSet() && erType.getSetElementType().isTuple())
223
        {
224
15226
          if( eqc_node.getKind() == kind::TRANSPOSE || eqc_node.getKind() == kind::JOIN ||
225
8933
              eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE ||
226
9836
              eqc_node.getKind() == kind::JOIN_IMAGE || eqc_node.getKind() == kind::IDEN ) {
227
2776
            std::vector<Node> terms;
228
2776
            std::map< kind::Kind_t, std::vector<Node> >  rel_terms;
229
1388
            TERM_IT terms_it = d_terms_cache.find(eqc_rep);
230
231
1388
            if( terms_it == d_terms_cache.end() ) {
232
1306
              terms.push_back(eqc_node);
233
1306
              rel_terms[eqc_node.getKind()]      = terms;
234
1306
              d_terms_cache[eqc_rep]             = rel_terms;
235
            } else {
236
82
              KIND_TERM_IT kind_term_it = terms_it->second.find(eqc_node.getKind());
237
238
82
              if( kind_term_it == terms_it->second.end() ) {
239
28
                terms.push_back(eqc_node);
240
28
                d_terms_cache[eqc_rep][eqc_node.getKind()] = terms;
241
              } else {
242
54
                kind_term_it->second.push_back(eqc_node);
243
              }
244
            }
245
          }
246
        // need to add all tuple elements as shared terms
247
        }
248
27750
        else if (erType.isTuple() && !eqc_node.isConst() && !eqc_node.isVar())
249
        {
250
11008
          std::vector<TypeNode> tupleTypes = erType.getTupleTypes();
251
16569
          for (unsigned i = 0, tlen = erType.getTupleLength(); i < tlen; i++)
252
          {
253
22130
            Node element = RelsUtils::nthElementOfTuple(eqc_node, i);
254
11065
            if (!element.isConst())
255
            {
256
10059
              makeSharedTerm(element, tupleTypes[i]);
257
            }
258
          }
259
        }
260
53930
        ++eqc_i;
261
      }
262
20504
      ++eqcs_i;
263
    }
264
689
    Trace("rels-debug") << "[Theory::Rels] Done with collecting relational terms!" << std::endl;
265
689
  }
266
267
  /* JOIN-IMAGE UP  :   (x, x1) IS_IN R, ..., (x, xn) IS_IN R  (R JOIN_IMAGE n)
268
  *                     -------------------------------------------------------
269
  *                     x IS_IN (R JOIN_IMAGE n) || NOT DISTINCT(x1, ... , xn)
270
  *
271
  */
272
273
71
  void TheorySetsRels::computeMembersForJoinImageTerm( Node join_image_term ) {
274
71
    Trace("rels-debug") << "\n[Theory::Rels] *********** Compute members for JoinImage Term = " << join_image_term << std::endl;
275
71
    MEM_IT rel_mem_it = d_rReps_memberReps_cache.find( getRepresentative( join_image_term[0] ) );
276
277
71
    if( rel_mem_it == d_rReps_memberReps_cache.end() ) {
278
      return;
279
    }
280
71
    NodeManager* nm = NodeManager::currentNM();
281
282
142
    Node join_image_rel = join_image_term[0];
283
142
    std::unordered_set< Node, NodeHashFunction > hasChecked;
284
142
    Node join_image_rel_rep = getRepresentative( join_image_rel );
285
71
    std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin();
286
71
    MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep );
287
71
    std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin();
288
71
    unsigned int min_card = join_image_term[1].getConst<Rational>().getNumerator().getUnsignedInt();
289
290
721
    while( mem_rep_it != (*rel_mem_it).second.end() ) {
291
431
      Node fst_mem_rep = RelsUtils::nthElementOfTuple( *mem_rep_it, 0 );
292
293
430
      if( hasChecked.find( fst_mem_rep ) != hasChecked.end() ) {
294
105
        ++mem_rep_it;
295
105
        ++mem_rep_exp_it;
296
105
        continue;
297
      }
298
220
      hasChecked.insert( fst_mem_rep );
299
300
      const DType& dt =
301
220
          join_image_term.getType().getSetElementType().getDType();
302
      Node new_membership = nm->mkNode(
303
          MEMBER,
304
440
          nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem_rep),
305
766
          join_image_term);
306
334
      if (d_state.isEntailed(new_membership, true))
307
      {
308
114
        ++mem_rep_it;
309
114
        ++mem_rep_exp_it;
310
114
        continue;
311
      }
312
313
212
      std::vector< Node > reasons;
314
212
      std::vector< Node > existing_members;
315
106
      std::vector< Node >::iterator mem_rep_exp_it_snd = (*rel_mem_exp_it).second.begin();
316
317
814
      while( mem_rep_exp_it_snd != (*rel_mem_exp_it).second.end() ) {
318
746
        Node fst_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 0 );
319
320
392
        if( areEqual( fst_mem_rep,  fst_element_snd_mem ) ) {
321
118
          bool notExist = true;
322
118
          std::vector< Node >::iterator existing_mem_it = existing_members.begin();
323
198
          Node snd_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 1 );
324
325
160
          while( existing_mem_it != existing_members.end() ) {
326
21
            if( areEqual( (*existing_mem_it), snd_element_snd_mem ) ) {
327
              notExist = false;
328
              break;
329
            }
330
21
            ++existing_mem_it;
331
          }
332
333
118
          if( notExist ) {
334
118
            existing_members.push_back( snd_element_snd_mem );
335
118
            reasons.push_back( *mem_rep_exp_it_snd );
336
118
            if( fst_mem_rep != fst_element_snd_mem ) {
337
6
              reasons.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, fst_mem_rep, fst_element_snd_mem ) );
338
            }
339
118
            if( join_image_rel != (*mem_rep_exp_it_snd)[1] ) {
340
70
              reasons.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it_snd)[1], join_image_rel ));
341
            }
342
118
            if( existing_members.size() == min_card ) {
343
38
              if( min_card >= 2) {
344
16
                new_membership = NodeManager::currentNM()->mkNode( kind::OR, new_membership, NodeManager::currentNM()->mkNode( kind::NOT, NodeManager::currentNM()->mkNode( kind::DISTINCT, existing_members ) ));
345
              }
346
38
              Assert(reasons.size() >= 1);
347
38
              sendInfer(
348
                  new_membership,
349
                  InferenceId::UNKNOWN,
350
76
                  reasons.size() > 1 ? nm->mkNode(AND, reasons) : reasons[0]);
351
38
              break;
352
            }
353
          }
354
        }
355
354
        ++mem_rep_exp_it_snd;
356
      }
357
106
      ++mem_rep_it;
358
106
      ++mem_rep_exp_it;
359
    }
360
71
    Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for JoinImage Term" << join_image_term << "*********** " << std::endl;
361
  }
362
363
  /* JOIN-IMAGE DOWN  : (x) IS_IN (R JOIN_IMAGE n)
364
  *                     -------------------------------------------------------
365
  *                     (x, x1) IS_IN R .... (x, xn) IS_IN R  DISTINCT(x1, ... , xn)
366
  *
367
  */
368
369
139
  void TheorySetsRels::applyJoinImageRule( Node mem_rep, Node join_image_term, Node exp ) {
370
278
    Trace("rels-debug") << "\n[Theory::Rels] *********** applyJoinImageRule on " << join_image_term
371
139
                        << " with mem_rep = " << mem_rep  << " and exp = " << exp << std::endl;
372
139
    if( d_rel_nodes.find( join_image_term ) == d_rel_nodes.end() ) {
373
69
      computeMembersForJoinImageTerm( join_image_term );
374
69
      d_rel_nodes.insert( join_image_term );
375
    }
376
377
176
    Node join_image_rel = join_image_term[0];
378
176
    Node join_image_rel_rep = getRepresentative( join_image_rel );
379
139
    MEM_IT rel_mem_it = d_rReps_memberReps_cache.find( join_image_rel_rep );
380
139
    unsigned int min_card = join_image_term[1].getConst<Rational>().getNumerator().getUnsignedInt();
381
382
139
    if( rel_mem_it != d_rReps_memberReps_cache.end() ) {
383
139
      if( d_membership_trie.find( join_image_rel_rep ) != d_membership_trie.end() ) {
384
139
        computeTupleReps( mem_rep );
385
139
        if( d_membership_trie[join_image_rel_rep].findSuccessors(d_tuple_reps[mem_rep]).size() >= min_card ) {
386
102
          return;
387
        }
388
      }
389
    }
390
391
74
    Node reason = exp;
392
74
    Node conclusion = d_trueNode;
393
74
    std::vector< Node > distinct_skolems;
394
74
    Node fst_mem_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
395
396
37
    if( exp[1] != join_image_term ) {
397
4
      reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], join_image_term ) );
398
    }
399
108
    for( unsigned int i = 0; i < min_card; i++ ) {
400
142
      Node skolem = NodeManager::currentNM()->mkSkolem( "jig", join_image_rel.getType()[0].getTupleTypes()[0] );
401
71
      distinct_skolems.push_back( skolem );
402
71
      conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( join_image_rel, fst_mem_element, skolem ), join_image_rel ) );
403
    }
404
37
    if( distinct_skolems.size() >= 2 ) {
405
31
      conclusion =  NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) );
406
    }
407
37
    sendInfer(conclusion, InferenceId::SETS_RELS_JOIN_IMAGE_DOWN, reason);
408
37
    Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl;
409
410
  }
411
412
413
  /* IDENTITY-DOWN  : (x, y) IS_IN IDEN(R)
414
  *               -------------------------------------------------------
415
  *                   x = y,  (x IS_IN R)
416
  *
417
  */
418
419
15
  void TheorySetsRels::applyIdenRule( Node mem_rep, Node iden_term, Node exp) {
420
30
    Trace("rels-debug") << "\n[Theory::Rels] *********** applyIdenRule on " << iden_term
421
15
                        << " with mem_rep = " << mem_rep  << " and exp = " << exp << std::endl;
422
15
    NodeManager* nm = NodeManager::currentNM();
423
15
    if( d_rel_nodes.find( iden_term ) == d_rel_nodes.end() ) {
424
6
      computeMembersForIdenTerm( iden_term );
425
6
      d_rel_nodes.insert( iden_term );
426
    }
427
30
    Node reason = exp;
428
30
    Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 );
429
30
    Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 );
430
15
    const DType& dt = iden_term[0].getType().getSetElementType().getDType();
431
    Node fact = nm->mkNode(
432
        MEMBER,
433
30
        nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem),
434
60
        iden_term[0]);
435
436
15
    if( exp[1] != iden_term ) {
437
7
      reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], iden_term ) );
438
    }
439
15
    sendInfer(nm->mkNode(AND, fact, nm->mkNode(EQUAL, fst_mem, snd_mem)),
440
              InferenceId::SETS_RELS_IDENTITY_DOWN,
441
              reason);
442
15
    Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyIdenRule on " << iden_term << std::endl;
443
15
  }
444
445
  /* IDEN UP  : (x) IS_IN R        IDEN(R) IN T
446
  *             --------------------------------
447
  *                   (x, x) IS_IN IDEN(R)
448
  *
449
  */
450
451
14
  void TheorySetsRels::computeMembersForIdenTerm( Node iden_term ) {
452
14
    Trace("rels-debug") << "\n[Theory::Rels] *********** Compute members for Iden Term = " << iden_term << std::endl;
453
22
    Node iden_term_rel = iden_term[0];
454
22
    Node iden_term_rel_rep = getRepresentative( iden_term_rel );
455
456
14
    if( d_rReps_memberReps_cache.find( iden_term_rel_rep ) == d_rReps_memberReps_cache.end() ) {
457
6
      return;
458
    }
459
8
    NodeManager* nm = NodeManager::currentNM();
460
461
8
    MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( iden_term_rel_rep );
462
8
    std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin();
463
464
54
    while( mem_rep_exp_it != (*rel_mem_exp_it).second.end() ) {
465
46
      Node reason = *mem_rep_exp_it;
466
46
      Node fst_exp_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it)[0], 0 );
467
46
      Node new_mem = RelsUtils::constructPair( iden_term, fst_exp_mem, fst_exp_mem );
468
469
23
      if( (*mem_rep_exp_it)[1] != iden_term_rel ) {
470
        reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it)[1], iden_term_rel ) );
471
      }
472
69
      sendInfer(
473
46
          nm->mkNode(MEMBER, new_mem, iden_term), InferenceId::SETS_RELS_IDENTITY_UP, reason);
474
23
      ++mem_rep_exp_it;
475
    }
476
8
    Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for Iden Term = " << iden_term << std::endl;
477
  }
478
479
480
  /*
481
   * Construct transitive closure graph for tc_rep based on the members of tc_r_rep
482
   */
483
484
  /*
485
   * TCLOSURE TCLOSURE(x) = x | x.x | x.x.x | ... (| is union)
486
   *
487
   * TCLOSURE-UP I:   (a, b) IS_IN x            TCLOSURE(x) in T
488
   *              ---------------------------------------------
489
   *                              (a, b) IS_IN TCLOSURE(x)
490
   *
491
   *
492
   *
493
   * TCLOSURE-UP II : (a, b) IS_IN TCLOSURE(x)  (b, c) IS_IN TCLOSURE(x)
494
   *              -----------------------------------------------------------
495
   *                            (a, c) IS_IN TCLOSURE(x)
496
   *
497
   */
498
252
  void TheorySetsRels::applyTCRule( Node mem_rep, Node tc_rel, Node tc_rel_rep, Node exp ) {
499
504
    Trace("rels-debug") << "[Theory::Rels] *********** Applying TCLOSURE rule on a tc term = " << tc_rel
500
252
                            << ", its representative = " << tc_rel_rep
501
252
                            << " with member rep = " << mem_rep << " and explanation = " << exp << std::endl;
502
252
    MEM_IT mem_it = d_rReps_memberReps_cache.find( tc_rel[0] );
503
504
748
    if( mem_it != d_rReps_memberReps_cache.end() && d_rel_nodes.find( tc_rel ) == d_rel_nodes.end()
505
591
        && d_rRep_tcGraph.find( getRepresentative( tc_rel[0] ) ) ==  d_rRep_tcGraph.end() ) {
506
87
      buildTCGraphForRel( tc_rel );
507
87
      d_rel_nodes.insert( tc_rel );
508
    }
509
510
    // mem_rep is a member of tc_rel[0] or mem_rep can be infered by TC_Graph of tc_rel[0], thus skip
511
252
    if( isTCReachable( mem_rep, tc_rel) ) {
512
454
      Trace("rels-debug") << "[Theory::Rels] mem_rep is a member of tc_rel[0] = " << tc_rel[0]
513
227
                              << " or can be infered by TC_Graph of tc_rel[0]! " << std::endl;
514
227
      return;
515
    }
516
25
    NodeManager* nm = NodeManager::currentNM();
517
518
    // add mem_rep to d_tcrRep_tcGraph
519
25
    TC_IT tc_it = d_tcr_tcGraph.find( tc_rel );
520
50
    Node mem_rep_fst = getRepresentative( RelsUtils::nthElementOfTuple( mem_rep, 0 ) );
521
50
    Node mem_rep_snd = getRepresentative( RelsUtils::nthElementOfTuple( mem_rep, 1 ) );
522
50
    Node mem_rep_tup = RelsUtils::constructPair( tc_rel, mem_rep_fst, mem_rep_snd );
523
524
25
    if( tc_it != d_tcr_tcGraph.end() ) {
525
17
      std::map< Node, std::map< Node, Node > >::iterator tc_exp_it = d_tcr_tcGraph_exps.find( tc_rel );
526
527
17
      TC_GRAPH_IT tc_graph_it = (tc_it->second).find( mem_rep_fst );
528
17
      Assert(tc_exp_it != d_tcr_tcGraph_exps.end());
529
17
      std::map< Node, Node >::iterator exp_map_it = (tc_exp_it->second).find( mem_rep_tup );
530
531
17
      if( exp_map_it == (tc_exp_it->second).end() ) {
532
17
        (tc_exp_it->second)[mem_rep_tup] = exp;
533
      }
534
535
17
      if( tc_graph_it != (tc_it->second).end() ) {
536
8
        (tc_graph_it->second).insert( mem_rep_snd );
537
      } else {
538
18
        std::unordered_set< Node, NodeHashFunction > sets;
539
9
        sets.insert( mem_rep_snd );
540
9
        (tc_it->second)[mem_rep_fst] = sets;
541
      }
542
    } else {
543
16
      std::map< Node, Node > exp_map;
544
16
      std::unordered_set< Node, NodeHashFunction > sets;
545
16
      std::map< Node, std::unordered_set<Node, NodeHashFunction> > element_map;
546
8
      sets.insert( mem_rep_snd );
547
8
      element_map[mem_rep_fst] = sets;
548
8
      d_tcr_tcGraph[tc_rel] = element_map;
549
8
      exp_map[mem_rep_tup] = exp;
550
8
      d_tcr_tcGraph_exps[tc_rel] = exp_map;
551
    }
552
50
    Node fst_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
553
50
    Node snd_element = RelsUtils::nthElementOfTuple( exp[0], 1 );
554
75
    Node sk_1 = d_skCache.mkTypedSkolemCached(fst_element.getType(),
555
                                              exp[0],
556
                                              tc_rel[0],
557
                                              SkolemCache::SK_TCLOSURE_DOWN1,
558
100
                                              "stc1");
559
75
    Node sk_2 = d_skCache.mkTypedSkolemCached(fst_element.getType(),
560
                                              exp[0],
561
                                              tc_rel[0],
562
                                              SkolemCache::SK_TCLOSURE_DOWN2,
563
100
                                              "stc2");
564
50
    Node mem_of_r = nm->mkNode(MEMBER, exp[0], tc_rel[0]);
565
50
    Node sk_eq = nm->mkNode(EQUAL, sk_1, sk_2);
566
50
    Node reason   = exp;
567
568
25
    if( tc_rel != exp[1] ) {
569
3
      reason = nm->mkNode(AND, reason, nm->mkNode(EQUAL, tc_rel, exp[1]));
570
    }
571
572
    Node conc = nm->mkNode(
573
        OR,
574
        mem_of_r,
575
150
        nm->mkNode(
576
            AND,
577
100
            nm->mkNode(MEMBER,
578
50
                       RelsUtils::constructPair(tc_rel, fst_element, sk_1),
579
                       tc_rel[0]),
580
100
            nm->mkNode(MEMBER,
581
50
                       RelsUtils::constructPair(tc_rel, sk_2, snd_element),
582
                       tc_rel[0]),
583
50
            nm->mkNode(OR,
584
                       sk_eq,
585
100
                       nm->mkNode(MEMBER,
586
50
                                  RelsUtils::constructPair(tc_rel, sk_1, sk_2),
587
50
                                  tc_rel))));
588
589
50
    Node tc_lemma = nm->mkNode(IMPLIES, reason, conc);
590
25
    d_pending.push_back(tc_lemma);
591
  }
592
593
252
  bool TheorySetsRels::isTCReachable( Node mem_rep, Node tc_rel ) {
594
252
    MEM_IT mem_it = d_rReps_memberReps_cache.find( getRepresentative( tc_rel[0] ) );
595
596
252
    if( mem_it != d_rReps_memberReps_cache.end() && std::find( (mem_it->second).begin(), (mem_it->second).end(), mem_rep) != (mem_it->second).end() ) {
597
140
      return true;
598
    }
599
600
112
    TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) );
601
112
    if( tc_it != d_rRep_tcGraph.end() ) {
602
104
      bool isReachable = false;
603
208
      std::unordered_set<Node, NodeHashFunction> seen;
604
208
      isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ),
605
312
                     getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable );
606
104
      return isReachable;
607
    }
608
8
    return false;
609
  }
610
611
218
  void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
612
                                    std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) {
613
218
    if(hasSeen.find(start) == hasSeen.end()) {
614
218
      hasSeen.insert(start);
615
    }
616
617
218
    TC_GRAPH_IT pair_set_it = tc_graph.find(start);
618
619
218
    if(pair_set_it != tc_graph.end()) {
620
188
      if(pair_set_it->second.find(dest) != pair_set_it->second.end()) {
621
87
        isReachable = true;
622
174
        return;
623
      } else {
624
101
        std::unordered_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin();
625
626
329
        while( set_it != pair_set_it->second.end() ) {
627
          // need to check if *set_it has been looked already
628
114
          if( hasSeen.find(*set_it) == hasSeen.end() ) {
629
114
            isTCReachable( *set_it, dest, hasSeen, tc_graph, isReachable );
630
          }
631
114
          ++set_it;
632
        }
633
      }
634
    }
635
  }
636
637
118
  void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) {
638
236
    std::map< Node, Node > rel_tc_graph_exps;
639
236
    std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph;
640
641
236
    Node rel_rep = getRepresentative( tc_rel[0] );
642
236
    Node tc_rel_rep = getRepresentative( tc_rel );
643
236
    std::vector< Node > members = d_rReps_memberReps_cache[rel_rep];
644
236
    std::vector< Node > exps = d_rReps_memberReps_exp_cache[rel_rep];
645
646
349
    for( unsigned int i = 0; i < members.size(); i++ ) {
647
462
      Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 ));
648
462
      Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 ));
649
462
      Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep );
650
231
      std::map< Node, std::unordered_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep );
651
652
231
      if( rel_tc_graph_it == rel_tc_graph.end() ) {
653
392
        std::unordered_set< Node, NodeHashFunction > snd_elements;
654
196
        snd_elements.insert( snd_element_rep );
655
196
        rel_tc_graph[fst_element_rep] = snd_elements;
656
196
        rel_tc_graph_exps[tuple_rep] = exps[i];
657
35
      } else if( (rel_tc_graph_it->second).find( snd_element_rep ) ==  (rel_tc_graph_it->second).end() ) {
658
35
        (rel_tc_graph_it->second).insert( snd_element_rep );
659
35
        rel_tc_graph_exps[tuple_rep] = exps[i];
660
      }
661
    }
662
663
118
    if( members.size() > 0 ) {
664
101
      d_rRep_tcGraph[rel_rep] = rel_tc_graph;
665
101
      d_tcr_tcGraph_exps[tc_rel] = rel_tc_graph_exps;
666
101
      d_tcr_tcGraph[tc_rel] = rel_tc_graph;
667
    }
668
118
  }
669
670
109
  void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) {
671
109
    Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl;
672
322
    for (TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin();
673
322
         tc_graph_it != rel_tc_graph.end();
674
         ++tc_graph_it)
675
    {
676
256
      for (std::unordered_set<Node, NodeHashFunction>::iterator
677
213
               snd_elements_it = tc_graph_it->second.begin();
678
469
           snd_elements_it != tc_graph_it->second.end();
679
           ++snd_elements_it)
680
      {
681
512
        std::vector< Node > reasons;
682
512
        std::unordered_set<Node, NodeHashFunction> seen;
683
512
        Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) );
684
256
        Assert(rel_tc_graph_exps.find(tuple) != rel_tc_graph_exps.end());
685
512
        Node exp   = rel_tc_graph_exps.find( tuple )->second;
686
687
256
        reasons.push_back( exp );
688
256
        seen.insert( tc_graph_it->first );
689
256
        doTCInference( tc_rel, reasons, rel_tc_graph, rel_tc_graph_exps, tc_graph_it->first, *snd_elements_it, seen);
690
      }
691
    }
692
109
    Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl;
693
109
  }
694
695
491
  void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
696
                                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) {
697
491
    NodeManager* nm = NodeManager::currentNM();
698
892
    Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) );
699
892
    std::vector< Node > all_reasons( reasons );
700
701
820
    for( unsigned int i = 0 ; i < reasons.size()-1; i++ ) {
702
658
      Node fst_element_end = RelsUtils::nthElementOfTuple( reasons[i][0], 1 );
703
658
      Node snd_element_begin = RelsUtils::nthElementOfTuple( reasons[i+1][0], 0 );
704
329
      if( fst_element_end != snd_element_begin ) {
705
24
        all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, fst_element_end, snd_element_begin) );
706
      }
707
329
      if( tc_rel != reasons[i][1] && tc_rel[0] != reasons[i][1] ) {
708
        all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel[0], reasons[i][1]) );
709
      }
710
    }
711
491
    if( tc_rel != reasons.back()[1] && tc_rel[0] != reasons.back()[1] ) {
712
8
      all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel[0], reasons.back()[1]) );
713
    }
714
491
    if( all_reasons.size() > 1) {
715
238
      sendInfer(nm->mkNode(MEMBER, tc_mem, tc_rel),
716
                InferenceId::SETS_RELS_TCLOSURE_FWD,
717
476
                nm->mkNode(AND, all_reasons));
718
    } else {
719
253
      sendInfer(nm->mkNode(MEMBER, tc_mem, tc_rel),
720
                InferenceId::SETS_RELS_TCLOSURE_FWD,
721
253
                all_reasons.front());
722
    }
723
724
    // check if cur_node has been traversed or not
725
491
    if( seen.find( cur_node_rep ) != seen.end() ) {
726
90
      return;
727
    }
728
401
    seen.insert( cur_node_rep );
729
401
    TC_GRAPH_IT  cur_set = tc_graph.find( cur_node_rep );
730
401
    if( cur_set != tc_graph.end() ) {
731
235
      for (std::unordered_set<Node, NodeHashFunction>::iterator set_it =
732
161
               cur_set->second.begin();
733
396
           set_it != cur_set->second.end();
734
           ++set_it)
735
      {
736
470
        Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it );
737
470
        std::vector< Node > new_reasons( reasons );
738
235
        new_reasons.push_back( rel_tc_graph_exps.find( new_pair )->second );
739
235
        doTCInference( tc_rel, new_reasons, tc_graph, rel_tc_graph_exps, start_node_rep, *set_it, seen );
740
      }
741
    }
742
  }
743
744
 /*  product-split rule:  (a, b) IS_IN (X PRODUCT Y)
745
  *                     ----------------------------------
746
  *                       a IS_IN X  && b IS_IN Y
747
  *
748
  *  product-compose rule: (a, b) IS_IN X    (c, d) IS_IN Y
749
  *                        ---------------------------------
750
  *                        (a, b, c, d) IS_IN (X PRODUCT Y)
751
  */
752
753
754
135
  void TheorySetsRels::applyProductRule( Node pt_rel, Node pt_rel_rep, Node exp ) {
755
270
    Trace("rels-debug") << "\n[Theory::Rels] *********** Applying PRODUCT rule on producted term = " << pt_rel
756
135
                            << ", its representative = " << pt_rel_rep
757
135
                            << " with explanation = " << exp << std::endl;
758
759
135
    if(d_rel_nodes.find( pt_rel ) == d_rel_nodes.end()) {
760
102
      Trace("rels-debug") <<  "\n[Theory::Rels] Apply PRODUCT-COMPOSE rule on term: " << pt_rel
761
51
                          << " with explanation: " << exp << std::endl;
762
763
51
      computeMembersForBinOpRel( pt_rel );
764
51
      d_rel_nodes.insert( pt_rel );
765
    }
766
767
270
    Node mem = exp[0];
768
270
    std::vector<Node>   r1_element;
769
270
    std::vector<Node>   r2_element;
770
135
    const DType& dt1 = pt_rel[0].getType().getSetElementType().getDType();
771
135
    unsigned int s1_len  = pt_rel[0].getType().getSetElementType().getTupleLength();
772
135
    unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength();
773
774
135
    r1_element.push_back(dt1[0].getConstructor());
775
776
135
    unsigned int i = 0;
777
609
    for(; i < s1_len; ++i) {
778
237
      r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
779
    }
780
135
    const DType& dt2 = pt_rel[1].getType().getSetElementType().getDType();
781
135
    r2_element.push_back(dt2[0].getConstructor());
782
609
    for(; i < tup_len; ++i) {
783
237
      r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
784
    }
785
270
    Node reason   = exp;
786
270
    Node mem1     = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
787
270
    Node mem2     = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r2_element);
788
270
    Node fact_1   = NodeManager::currentNM()->mkNode(kind::MEMBER, mem1, pt_rel[0]);
789
270
    Node fact_2   = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, pt_rel[1]);
790
791
135
    if( pt_rel != exp[1] ) {
792
16
      reason = NodeManager::currentNM()->mkNode(kind::AND, exp, NodeManager::currentNM()->mkNode(kind::EQUAL, pt_rel, exp[1]));
793
    }
794
135
    sendInfer(fact_1, InferenceId::SETS_RELS_PRODUCT_SPLIT, reason);
795
135
    sendInfer(fact_2, InferenceId::SETS_RELS_PRODUCT_SPLIT, reason);
796
135
  }
797
798
  /* join-split rule:           (a, b) IS_IN (X JOIN Y)
799
   *                  --------------------------------------------
800
   *                  exists z | (a, z) IS_IN X  && (z, b) IS_IN Y
801
   *
802
   *
803
   * join-compose rule: (a, b) IS_IN X    (b, c) IS_IN Y  NOT (t, u) IS_IN (X JOIN Y)
804
   *                    -------------------------------------------------------------
805
   *                                      (a, c) IS_IN (X JOIN Y)
806
   */
807
808
1312
  void TheorySetsRels::applyJoinRule( Node join_rel, Node join_rel_rep, Node exp ) {
809
2624
    Trace("rels-debug") << "\n[Theory::Rels] *********** Applying JOIN rule on joined term = " << join_rel
810
1312
                            << ", its representative = " << join_rel_rep
811
1312
                            << " with explanation = " << exp << std::endl;
812
1312
    if(d_rel_nodes.find( join_rel ) == d_rel_nodes.end()) {
813
702
      Trace("rels-debug") <<  "\n[Theory::Rels] Apply JOIN-COMPOSE rule on term: " << join_rel
814
351
                          << " with explanation: " << exp << std::endl;
815
816
351
      computeMembersForBinOpRel( join_rel );
817
351
      d_rel_nodes.insert( join_rel );
818
    }
819
820
1517
    Node mem = exp[0];
821
1517
    std::vector<Node> r1_element;
822
1517
    std::vector<Node> r2_element;
823
1517
    Node r1_rep = getRepresentative(join_rel[0]);
824
1517
    Node r2_rep = getRepresentative(join_rel[1]);
825
1517
    TypeNode     shared_type    = r2_rep.getType().getSetElementType().getTupleTypes()[0];
826
1312
    Node shared_x = d_skCache.mkTypedSkolemCached(
827
1517
        shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj");
828
1312
    const DType& dt1 = join_rel[0].getType().getSetElementType().getDType();
829
1312
    unsigned int s1_len         = join_rel[0].getType().getSetElementType().getTupleLength();
830
1312
    unsigned int tup_len        = join_rel.getType().getSetElementType().getTupleLength();
831
832
1312
    unsigned int i = 0;
833
1312
    r1_element.push_back(dt1[0].getConstructor());
834
3896
    for(; i < s1_len-1; ++i) {
835
1292
      r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
836
    }
837
1312
    r1_element.push_back(shared_x);
838
1312
    const DType& dt2 = join_rel[1].getType().getSetElementType().getDType();
839
1312
    r2_element.push_back(dt2[0].getConstructor());
840
1312
    r2_element.push_back(shared_x);
841
3980
    for(; i < tup_len; ++i) {
842
1334
      r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
843
    }
844
1517
    Node mem1 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
845
1517
    Node mem2 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r2_element);
846
847
1312
    computeTupleReps(mem1);
848
1312
    computeTupleReps(mem2);
849
850
1517
    std::vector<Node> elements = d_membership_trie[r1_rep].findTerms(d_tuple_reps[mem1]);
851
852
1499
    for(unsigned int j = 0; j < elements.size(); j++) {
853
1481
      std::vector<Node> new_tup;
854
1294
      new_tup.push_back(elements[j]);
855
1294
      new_tup.insert(new_tup.end(), d_tuple_reps[mem2].begin()+1, d_tuple_reps[mem2].end());
856
1294
      if(d_membership_trie[r2_rep].existsTerm(new_tup) != Node::null()) {
857
1107
        return;
858
      }
859
    }
860
410
    Node reason = exp;
861
205
    if( join_rel != exp[1] ) {
862
95
      reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, join_rel, exp[1]));
863
    }
864
410
    Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem1, join_rel[0]);
865
205
    sendInfer(fact, InferenceId::SETS_RELS_JOIN_SPLIT_1, reason);
866
205
    fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, join_rel[1]);
867
205
    sendInfer(fact, InferenceId::SETS_RELS_JOIN_SPLIT_2, reason);
868
205
    makeSharedTerm(shared_x, shared_type);
869
  }
870
871
  /*
872
   * transpose-occur rule:    (a, b) IS_IN X   (TRANSPOSE X) in T
873
   *                         ---------------------------------------
874
   *                            (b, a) IS_IN (TRANSPOSE X)
875
   *
876
   * transpose-reverse rule:    (a, b) IS_IN (TRANSPOSE X)
877
   *                         ---------------------------------------
878
   *                            (b, a) IS_IN X
879
   *
880
   */
881
1270
  void TheorySetsRels::applyTransposeRule( std::vector<Node> tp_terms ) {
882
1270
    if( tp_terms.size() < 1) {
883
      return;
884
    }
885
1270
    NodeManager* nm = NodeManager::currentNM();
886
1270
    for( unsigned int i = 1; i < tp_terms.size(); i++ ) {
887
      Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE-Equal rule on transposed term = " << tp_terms[0] << " and " << tp_terms[i] << std::endl;
888
      sendInfer(nm->mkNode(EQUAL, tp_terms[0][0], tp_terms[i][0]),
889
                InferenceId::SETS_RELS_TRANSPOSE_EQ,
890
                nm->mkNode(EQUAL, tp_terms[0], tp_terms[i]));
891
    }
892
  }
893
894
1270
  void TheorySetsRels::applyTransposeRule( Node tp_rel, Node tp_rel_rep, Node exp ) {
895
2540
    Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE rule on transposed term = " << tp_rel
896
1270
                        << ", its representative = " << tp_rel_rep
897
1270
                        << " with explanation = " << exp << std::endl;
898
1270
    NodeManager* nm = NodeManager::currentNM();
899
900
1270
    if(d_rel_nodes.find( tp_rel ) == d_rel_nodes.end()) {
901
356
      Trace("rels-debug") <<  "\n[Theory::Rels] Apply TRANSPOSE-Compose rule on term: " << tp_rel
902
178
                          << " with explanation: " << exp << std::endl;
903
904
178
      computeMembersForUnaryOpRel( tp_rel );
905
178
      d_rel_nodes.insert( tp_rel );
906
    }
907
908
2540
    Node reason = exp;
909
2540
    Node reversed_mem = RelsUtils::reverseTuple( exp[0] );
910
911
1270
    if( tp_rel != exp[1] ) {
912
174
      reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tp_rel, exp[1]));
913
    }
914
1270
    sendInfer(nm->mkNode(MEMBER, reversed_mem, tp_rel[0]),
915
              InferenceId::SETS_RELS_TRANSPOSE_REV,
916
              reason);
917
1270
  }
918
919
689
  void TheorySetsRels::doTCInference() {
920
689
    Trace("rels-debug") << "[Theory::Rels] ****** Finalizing transitive closure inferences!" << std::endl;
921
689
    TC_IT tc_graph_it = d_tcr_tcGraph.begin();
922
907
    while( tc_graph_it != d_tcr_tcGraph.end() ) {
923
109
      Assert(d_tcr_tcGraph_exps.find(tc_graph_it->first)
924
             != d_tcr_tcGraph_exps.end());
925
109
      doTCInference( tc_graph_it->second, d_tcr_tcGraph_exps.find(tc_graph_it->first)->second, tc_graph_it->first );
926
109
      ++tc_graph_it;
927
    }
928
689
    Trace("rels-debug") << "[Theory::Rels] ****** Done with finalizing transitive closure inferences!" << std::endl;
929
689
  }
930
931
932
  // Bottom-up fashion to compute relations with more than 1 arity
933
1131
  void TheorySetsRels::computeMembersForBinOpRel(Node rel) {
934
1131
    Trace("rels-debug") << "\n[Theory::Rels] computeMembersForBinOpRel for relation  " << rel << std::endl;
935
936
1131
    switch(rel[0].getKind()) {
937
224
      case kind::TRANSPOSE:
938
      case kind::TCLOSURE: {
939
224
        computeMembersForUnaryOpRel(rel[0]);
940
224
        break;
941
      }
942
198
      case kind::JOIN:
943
      case kind::PRODUCT: {
944
198
        computeMembersForBinOpRel(rel[0]);
945
198
        break;
946
      }
947
709
      default:
948
709
        break;
949
    }
950
1131
    switch(rel[1].getKind()) {
951
      case kind::TRANSPOSE: {
952
        computeMembersForUnaryOpRel(rel[1]);
953
        break;
954
      }
955
12
      case kind::JOIN:
956
      case kind::PRODUCT: {
957
12
        computeMembersForBinOpRel(rel[1]);
958
12
        break;
959
      }
960
1119
      default:
961
1119
        break;
962
    }
963
3203
    if(d_rReps_memberReps_cache.find(getRepresentative(rel[0])) == d_rReps_memberReps_cache.end() ||
964
2072
       d_rReps_memberReps_cache.find(getRepresentative(rel[1])) == d_rReps_memberReps_cache.end()) {
965
247
      return;
966
    }
967
884
    composeMembersForRels(rel);
968
  }
969
970
  // Bottom-up fashion to compute unary relation
971
582
  void TheorySetsRels::computeMembersForUnaryOpRel(Node rel) {
972
582
    Trace("rels-debug") << "\n[Theory::Rels] computeMembersForUnaryOpRel for relation  " << rel << std::endl;
973
974
582
    switch(rel[0].getKind()) {
975
      case kind::TRANSPOSE:
976
      case kind::TCLOSURE:
977
        computeMembersForUnaryOpRel(rel[0]);
978
        break;
979
102
      case kind::JOIN:
980
      case kind::PRODUCT:
981
102
        computeMembersForBinOpRel(rel[0]);
982
102
        break;
983
480
      default:
984
480
        break;
985
    }
986
987
1034
    Node rel0_rep  = getRepresentative(rel[0]);
988
1746
    if (d_rReps_memberReps_cache.find(rel0_rep)
989
1746
        == d_rReps_memberReps_cache.end())
990
    {
991
130
      return;
992
    }
993
452
    NodeManager* nm = NodeManager::currentNM();
994
995
904
    std::vector<Node>   members = d_rReps_memberReps_cache[rel0_rep];
996
904
    std::vector<Node>   exps    = d_rReps_memberReps_exp_cache[rel0_rep];
997
998
452
    Assert(members.size() == exps.size());
999
1000
5653
    for(unsigned int i = 0; i < members.size(); i++) {
1001
10402
      Node reason = exps[i];
1002
5201
      if( rel.getKind() == kind::TRANSPOSE) {
1003
5170
        if( rel[0] != exps[i][1] ) {
1004
78
          reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, rel[0], exps[i][1]));
1005
        }
1006
5170
        sendInfer(nm->mkNode(MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel),
1007
                  InferenceId::SETS_RELS_TRANSPOSE_REV,
1008
                  reason);
1009
      }
1010
    }
1011
  }
1012
1013
  /*
1014
   * Explicitly compose the join or product relations of r1 and r2
1015
   * e.g. If (a, b) in X and (b, c) in Y, (a, c) in (X JOIN Y)
1016
   *
1017
   */
1018
884
  void TheorySetsRels::composeMembersForRels( Node rel ) {
1019
884
    Trace("rels-debug") << "[Theory::Rels] Start composing members for relation = " << rel << std::endl;
1020
1768
    Node r1 = rel[0];
1021
1768
    Node r2 = rel[1];
1022
1768
    Node r1_rep = getRepresentative( r1 );
1023
1768
    Node r2_rep = getRepresentative( r2 );
1024
1025
2652
    if(d_rReps_memberReps_cache.find( r1_rep ) == d_rReps_memberReps_cache.end() ||
1026
1768
       d_rReps_memberReps_cache.find( r2_rep ) == d_rReps_memberReps_cache.end() ) {
1027
      return;
1028
    }
1029
884
    NodeManager* nm = NodeManager::currentNM();
1030
1031
1768
    std::vector<Node> r1_rep_exps = d_rReps_memberReps_exp_cache[r1_rep];
1032
1768
    std::vector<Node> r2_rep_exps = d_rReps_memberReps_exp_cache[r2_rep];
1033
884
    unsigned int r1_tuple_len = r1.getType().getSetElementType().getTupleLength();
1034
884
    unsigned int r2_tuple_len = r2.getType().getSetElementType().getTupleLength();
1035
1036
5964
    for( unsigned int i = 0; i < r1_rep_exps.size(); i++ ) {
1037
250863
      for( unsigned int j = 0; j < r2_rep_exps.size(); j++ ) {
1038
491566
        std::vector<Node> tuple_elements;
1039
491566
        TypeNode tn = rel.getType().getSetElementType();
1040
491566
        Node r1_rmost = RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], r1_tuple_len-1 );
1041
491566
        Node r2_lmost = RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 );
1042
245783
        tuple_elements.push_back(tn.getDType()[0].getConstructor());
1043
1044
491566
        Trace("rels-debug") << "[Theory::Rels] r1_rmost: " << r1_rmost
1045
245783
                            << " of type " << r1_rmost.getType() << std::endl;
1046
491566
        Trace("rels-debug") << "[Theory::Rels] r2_lmost: " << r2_lmost
1047
245783
                            << " of type " << r2_lmost.getType() << std::endl;
1048
1049
491566
        if (rel.getKind() == kind::PRODUCT
1050
491566
            || (rel.getKind() == kind::JOIN && areEqual(r1_rmost, r2_lmost)))
1051
        {
1052
25765
          bool isProduct = rel.getKind() == kind::PRODUCT;
1053
25765
          unsigned int k = 0;
1054
25765
          unsigned int l = 1;
1055
1056
77189
          for( ; k < r1_tuple_len - 1; ++k ) {
1057
25712
            tuple_elements.push_back( RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], k ) );
1058
          }
1059
25765
          if(isProduct) {
1060
314
            tuple_elements.push_back( RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], k ) );
1061
314
            tuple_elements.push_back( RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 ) );
1062
          }
1063
77257
          for( ; l < r2_tuple_len; ++l ) {
1064
25746
            tuple_elements.push_back( RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], l ) );
1065
          }
1066
1067
51530
          Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
1068
51530
          Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, composed_tuple, rel);
1069
51530
          std::vector<Node> reasons;
1070
25765
          reasons.push_back( r1_rep_exps[i] );
1071
25765
          reasons.push_back( r2_rep_exps[j] );
1072
1073
25765
          if( r1 != r1_rep_exps[i][1] ) {
1074
93
            reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1, r1_rep_exps[i][1]) );
1075
          }
1076
25765
          if( r2 != r2_rep_exps[j][1] ) {
1077
70
            reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r2, r2_rep_exps[j][1]) );
1078
          }
1079
25765
          if( isProduct ) {
1080
314
            sendInfer(
1081
628
                fact, InferenceId::SETS_RELS_PRODUCE_COMPOSE, nm->mkNode(kind::AND, reasons));
1082
          } else {
1083
25451
            if( r1_rmost != r2_lmost ) {
1084
6473
              reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1_rmost, r2_lmost) );
1085
            }
1086
25451
            sendInfer(
1087
50902
                fact, InferenceId::SETS_RELS_JOIN_COMPOSE, nm->mkNode(kind::AND, reasons));
1088
          }
1089
        }
1090
      }
1091
    }
1092
1093
  }
1094
1095
689
  void TheorySetsRels::doPendingInfers()
1096
  {
1097
    // process the inferences in d_pending
1098
689
    if (!d_state.isInConflict())
1099
    {
1100
34785
      for (const Node& p : d_pending)
1101
      {
1102
34096
        if (p.getKind() == IMPLIES)
1103
        {
1104
34096
          processInference(p[1], InferenceId::UNKNOWN, p[0]);
1105
        }
1106
        else
1107
        {
1108
          processInference(p, InferenceId::UNKNOWN, d_trueNode);
1109
        }
1110
34096
        if (d_state.isInConflict())
1111
        {
1112
          break;
1113
        }
1114
      }
1115
      // if we are still not in conflict, send lemmas
1116
689
      if (!d_state.isInConflict())
1117
      {
1118
689
        d_im.doPendingLemmas();
1119
      }
1120
    }
1121
689
    d_pending.clear();
1122
689
  }
1123
1124
34096
  void TheorySetsRels::processInference(Node conc, InferenceId id, Node exp)
1125
  {
1126
68192
    Trace("sets-pinfer") << "Process inference: " << exp << " => " << conc
1127
34096
                         << std::endl;
1128
34096
    if (!d_state.isEntailed(exp, true))
1129
    {
1130
8
      Trace("sets-pinfer") << "  must assert as lemma" << std::endl;
1131
      // we wrap the spurious explanation into a splitting lemma
1132
16
      Node lem = NodeManager::currentNM()->mkNode(OR, exp.negate(), conc);
1133
8
      d_im.assertInference(lem, id, d_trueNode, 1);
1134
8
      return;
1135
    }
1136
    // try to assert it as a fact
1137
34088
    d_im.assertInference(conc, id, exp);
1138
  }
1139
1140
481445
  bool TheorySetsRels::isRelationKind( Kind k ) {
1141
480989
    return k == TRANSPOSE || k == PRODUCT || k == JOIN || k == TCLOSURE
1142
960956
           || k == IDEN || k == JOIN_IMAGE;
1143
  }
1144
1145
49054
  Node TheorySetsRels::getRepresentative( Node t ) {
1146
49054
    return d_state.getRepresentative(t);
1147
  }
1148
1149
1088934
  bool TheorySetsRels::hasTerm(Node a) { return d_state.hasTerm(a); }
1150
566706
  bool TheorySetsRels::areEqual( Node a, Node b ){
1151
566706
    Assert(a.getType() == b.getType());
1152
566706
    Trace("rels-eq") << "[sets-rels]**** checking equality between " << a << " and " << b << std::endl;
1153
566706
    if(a == b) {
1154
22239
      return true;
1155
544467
    } else if( hasTerm( a ) && hasTerm( b ) ){
1156
544467
      return d_state.areEqual(a, b);
1157
    } else if(a.getType().isTuple()) {
1158
      bool equal = true;
1159
      for(unsigned int i = 0; i < a.getType().getTupleLength(); i++) {
1160
        equal = equal && areEqual(RelsUtils::nthElementOfTuple(a, i), RelsUtils::nthElementOfTuple(b, i));
1161
      }
1162
      return equal;
1163
    } else if(!a.getType().isBoolean()){
1164
      // TODO(project##230): Find a safe type for the singleton operator
1165
      makeSharedTerm(a, a.getType());
1166
      makeSharedTerm(b, b.getType());
1167
    }
1168
    return false;
1169
  }
1170
1171
  /*
1172
   * Make sure duplicate members are not added in map
1173
   */
1174
11761
  bool TheorySetsRels::safelyAddToMap(std::map< Node, std::vector<Node> >& map, Node rel_rep, Node member) {
1175
11761
    std::map< Node, std::vector< Node > >::iterator mem_it = map.find(rel_rep);
1176
11761
    if(mem_it == map.end()) {
1177
4908
      std::vector<Node> members;
1178
2454
      members.push_back(member);
1179
2454
      map[rel_rep] = members;
1180
2454
      return true;
1181
    } else {
1182
9307
      std::vector<Node>::iterator mems = mem_it->second.begin();
1183
644657
      while(mems != mem_it->second.end()) {
1184
320824
        if(areEqual(*mems, member)) {
1185
3149
          return false;
1186
        }
1187
317675
        ++mems;
1188
      }
1189
6158
      map[rel_rep].push_back(member);
1190
6158
      return true;
1191
    }
1192
    return false;
1193
  }
1194
1195
11448
  void TheorySetsRels::makeSharedTerm(Node n, TypeNode t)
1196
  {
1197
11448
    if (d_shared_terms.find(n) != d_shared_terms.end())
1198
    {
1199
10088
      return;
1200
    }
1201
1360
    Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl;
1202
    // force a proxy lemma to be sent for the singleton containing n
1203
2720
    Node ss = NodeManager::currentNM()->mkSingleton(t, n);
1204
1360
    d_treg.getProxy(ss);
1205
1360
    d_shared_terms.insert(n);
1206
  }
1207
1208
  /*
1209
   * For each tuple n, we store a mapping between n and a list of its elements representatives
1210
   * in d_tuple_reps. This would later be used for applying JOIN operator.
1211
   */
1212
11375
  void TheorySetsRels::computeTupleReps( Node n ) {
1213
11375
    if( d_tuple_reps.find( n ) == d_tuple_reps.end() ){
1214
20697
      for( unsigned i = 0; i < n.getType().getTupleLength(); i++ ){
1215
13838
        d_tuple_reps[n].push_back( getRepresentative( RelsUtils::nthElementOfTuple(n, i) ) );
1216
      }
1217
    }
1218
11375
  }
1219
1220
  /*
1221
   * Node n[0] is a tuple variable, reduce n[0] to a concrete representation,
1222
   * which is (e1, ..., en) where e1, ... ,en are concrete elements of tuple n[0].
1223
   */
1224
1817
  void TheorySetsRels::reduceTupleVar(Node n) {
1225
1817
    if(d_symbolic_tuples.find(n) == d_symbolic_tuples.end()) {
1226
582
      Trace("rels-debug") << "[Theory::Rels] Reduce tuple var: " << n[0] << " to a concrete one " << " node = " << n << std::endl;
1227
1164
      std::vector<Node> tuple_elements;
1228
582
      tuple_elements.push_back((n[0].getType().getDType())[0].getConstructor());
1229
1164
      std::vector<TypeNode> tupleTypes = n[0].getType().getTupleTypes();
1230
1766
      for (unsigned int i = 0; i < n[0].getType().getTupleLength(); i++)
1231
      {
1232
2368
        Node element = RelsUtils::nthElementOfTuple(n[0], i);
1233
1184
        makeSharedTerm(element, tupleTypes[i]);
1234
1184
        tuple_elements.push_back(element);
1235
      }
1236
1164
      Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
1237
582
      tuple_reduct = NodeManager::currentNM()->mkNode(kind::MEMBER,tuple_reduct, n[1]);
1238
1164
      Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::EQUAL, n, tuple_reduct);
1239
582
      sendInfer(tuple_reduction_lemma, InferenceId::SETS_RELS_TUPLE_REDUCTION, d_trueNode);
1240
582
      d_symbolic_tuples.insert(n);
1241
    }
1242
1817
  }
1243
1244
2526
  std::vector<Node> TupleTrie::findTerms( std::vector< Node >& reps, int argIndex ) {
1245
5052
    std::vector<Node>                           nodes;
1246
2526
    std::map< Node, TupleTrie >::iterator       it;
1247
1248
2526
    if( argIndex==(int)reps.size()-1 ){
1249
1234
      if(reps[argIndex].getKind() == kind::SKOLEM) {
1250
1149
        it = d_data.begin();
1251
15229
        while(it != d_data.end()) {
1252
7040
          nodes.push_back(it->first);
1253
7040
          ++it;
1254
        }
1255
      }
1256
1234
      return nodes;
1257
    }else{
1258
1292
      it = d_data.find( reps[argIndex] );
1259
1292
      if( it==d_data.end() ){
1260
78
        return nodes;
1261
      }else{
1262
1214
        return it->second.findTerms( reps, argIndex+1 );
1263
      }
1264
    }
1265
  }
1266
1267
243
  std::vector<Node> TupleTrie::findSuccessors( std::vector< Node >& reps, int argIndex ) {
1268
486
    std::vector<Node>   nodes;
1269
243
    std::map< Node, TupleTrie >::iterator it;
1270
1271
243
    if( argIndex==(int)reps.size() ){
1272
104
      it = d_data.begin();
1273
476
      while(it != d_data.end()) {
1274
186
        nodes.push_back(it->first);
1275
186
        ++it;
1276
      }
1277
104
      return nodes;
1278
    }else{
1279
139
      it = d_data.find( reps[argIndex] );
1280
139
      if( it==d_data.end() ){
1281
35
        return nodes;
1282
      }else{
1283
104
        return it->second.findSuccessors( reps, argIndex+1 );
1284
      }
1285
    }
1286
  }
1287
1288
3640
  Node TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) {
1289
3640
    if( argIndex==(int)reps.size() ){
1290
1107
      if( d_data.empty() ){
1291
        return Node::null();
1292
      }else{
1293
1107
        return d_data.begin()->first;
1294
      }
1295
    }else{
1296
2533
      std::map< Node, TupleTrie >::iterator it = d_data.find( reps[argIndex] );
1297
2533
      if( it==d_data.end() ){
1298
187
        return Node::null();
1299
      }else{
1300
2346
        return it->second.existsTerm( reps, argIndex+1 );
1301
      }
1302
    }
1303
  }
1304
1305
25853
  bool TupleTrie::addTerm( Node n, std::vector< Node >& reps, int argIndex ){
1306
25853
    if( argIndex==(int)reps.size() ){
1307
8612
      if( d_data.empty() ){
1308
        //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
1309
8612
        d_data[n].clear();
1310
8612
        return true;
1311
      }else{
1312
        return false;
1313
      }
1314
    }else{
1315
17241
      return d_data[reps[argIndex]].addTerm( n, reps, argIndex+1 );
1316
    }
1317
  }
1318
1319
  void TupleTrie::debugPrint( const char * c, Node n, unsigned depth ) {
1320
    for( std::map< Node, TupleTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
1321
      for( unsigned i=0; i<depth; i++ ){ Debug(c) << "  "; }
1322
      Debug(c) << it->first << std::endl;
1323
      it->second.debugPrint( c, n, depth+1 );
1324
    }
1325
  }
1326
1327
34071
  void TheorySetsRels::sendInfer(Node fact, InferenceId id, Node reason)
1328
  {
1329
68142
    Trace("rels-lemma") << "Rels::lemma " << fact << " from " << reason
1330
34071
                        << " by " << id << std::endl;
1331
68142
    Node lemma = NodeManager::currentNM()->mkNode(IMPLIES, reason, fact);
1332
34071
    d_pending.push_back(lemma);
1333
34071
  }
1334
}
1335
}
1336
26685
}