GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/rep_set.cpp Lines: 186 251 74.1 %
Date: 2021-03-22 Branches: 276 792 34.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file rep_set.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Morgan Deters
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 Implementation of representative set
13
 **/
14
15
#include <unordered_set>
16
17
#include "theory/rep_set.h"
18
#include "theory/type_enumerator.h"
19
20
using namespace std;
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
26
22352
void RepSet::clear(){
27
22352
  d_type_reps.clear();
28
22352
  d_type_complete.clear();
29
22352
  d_tmap.clear();
30
22352
  d_values_to_terms.clear();
31
22352
}
32
33
bool RepSet::hasRep(TypeNode tn, Node n) const
34
{
35
  std::map<TypeNode, std::vector<Node> >::const_iterator it =
36
      d_type_reps.find(tn);
37
  if( it==d_type_reps.end() ){
38
    return false;
39
  }else{
40
    return std::find( it->second.begin(), it->second.end(), n )!=it->second.end();
41
  }
42
}
43
44
176526
size_t RepSet::getNumRepresentatives(TypeNode tn) const
45
{
46
176526
  const std::vector<Node>* reps = getTypeRepsOrNull(tn);
47
176526
  return (reps != nullptr) ? reps->size() : 0;
48
}
49
50
588
Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
51
{
52
  std::map<TypeNode, std::vector<Node> >::const_iterator it =
53
588
      d_type_reps.find(tn);
54
588
  Assert(it != d_type_reps.end());
55
588
  Assert(i < it->second.size());
56
588
  return it->second[i];
57
}
58
59
180530
const std::vector<Node>* RepSet::getTypeRepsOrNull(TypeNode tn) const
60
{
61
180530
  auto it = d_type_reps.find(tn);
62
180530
  if (it == d_type_reps.end())
63
  {
64
4
    return nullptr;
65
  }
66
180526
  return &(it->second);
67
}
68
69
namespace {
70
71
2283
bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
72
{
73
2283
  if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
74
2283
    cache.insert(n);
75
2283
    if( n.getKind()==STORE_ALL ){
76
1015
      return true;
77
    }else{
78
1268
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
79
1264
        if( containsStoreAll( n[i], cache ) ){
80
1264
          return true;
81
        }
82
      }
83
    }
84
  }
85
4
  return false;
86
}
87
88
}  // namespace
89
90
687027
void RepSet::add( TypeNode tn, Node n ){
91
  //for now, do not add array constants FIXME
92
687027
  if( tn.isArray() ){
93
1023
    std::unordered_set<Node, NodeHashFunction> cache;
94
1019
    if( containsStoreAll( n, cache ) ){
95
1015
      return;
96
    }
97
  }
98
686012
  Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
99
686012
  Assert(n.getType().isSubtypeOf(tn));
100
686012
  d_tmap[ n ] = (int)d_type_reps[tn].size();
101
686012
  d_type_reps[tn].push_back( n );
102
}
103
104
int RepSet::getIndexFor( Node n ) const {
105
  std::map< Node, int >::const_iterator it = d_tmap.find( n );
106
  if( it!=d_tmap.end() ){
107
    return it->second;
108
  }else{
109
    return -1;
110
  }
111
}
112
113
2126
bool RepSet::complete( TypeNode t ){
114
2126
  std::map< TypeNode, bool >::iterator it = d_type_complete.find( t );
115
2126
  if( it==d_type_complete.end() ){
116
    //remove all previous
117
766
    for( unsigned i=0; i<d_type_reps[t].size(); i++ ){
118
579
      d_tmap.erase( d_type_reps[t][i] );
119
    }
120
187
    d_type_reps[t].clear();
121
    //now complete the type
122
187
    d_type_complete[t] = true;
123
374
    TypeEnumerator te(t);
124
1375
    while( !te.isFinished() ){
125
1188
      Node n = *te;
126
594
      if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){
127
594
        add( t, n );
128
      }
129
594
      ++te;
130
    }
131
781
    for( size_t i=0; i<d_type_reps[t].size(); i++ ){
132
594
      Trace("reps-complete") << d_type_reps[t][i] << " ";
133
    }
134
187
    Trace("reps-complete") << std::endl;
135
187
    return true;
136
  }else{
137
1939
    return it->second;
138
  }
139
}
140
141
42647
Node RepSet::getTermForRepresentative(Node n) const
142
{
143
42647
  std::map<Node, Node>::const_iterator it = d_values_to_terms.find(n);
144
42647
  if (it != d_values_to_terms.end())
145
  {
146
41436
    return it->second;
147
  }
148
  else
149
  {
150
1211
    return Node::null();
151
  }
152
}
153
154
685103
void RepSet::setTermForRepresentative(Node n, Node t)
155
{
156
685103
  d_values_to_terms[n] = t;
157
685103
}
158
159
Node RepSet::getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const
160
{
161
  std::map<TypeNode, std::vector<Node> >::const_iterator it =
162
      d_type_reps.find(tn);
163
  if (it != d_type_reps.end())
164
  {
165
    // try to find a pre-existing arbitrary element
166
    for (size_t i = 0; i < it->second.size(); i++)
167
    {
168
      if (std::find(exclude.begin(), exclude.end(), it->second[i])
169
          == exclude.end())
170
      {
171
        return it->second[i];
172
      }
173
    }
174
  }
175
  return Node::null();
176
}
177
178
void RepSet::toStream(std::ostream& out){
179
  for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
180
    if( !it->first.isFunction() && !it->first.isPredicate() ){
181
      out << "(" << it->first << " " << it->second.size();
182
      out << " (";
183
      for( unsigned i=0; i<it->second.size(); i++ ){
184
        if( i>0 ){ out << " "; }
185
        out << it->second[i];
186
      }
187
      out << ")";
188
      out << ")" << std::endl;
189
    }
190
  }
191
}
192
193
4377
RepSetIterator::RepSetIterator(const RepSet* rs, RepBoundExt* rext)
194
4377
    : d_rs(rs), d_rext(rext), d_incomplete(false)
195
{
196
4377
}
197
198
76740
unsigned RepSetIterator::domainSize(unsigned i)
199
{
200
76740
  unsigned v = d_var_order[i];
201
76740
  return d_domain_elements[v].size();
202
}
203
204
72690
TypeNode RepSetIterator::getTypeOf(unsigned i) const { return d_types[i]; }
205
206
4377
bool RepSetIterator::setQuantifier(Node q)
207
{
208
4377
  Trace("rsi") << "Make rsi for quantified formula " << q << std::endl;
209
4377
  Assert(d_types.empty());
210
  //store indicies
211
10452
  for (size_t i = 0; i < q[0].getNumChildren(); i++)
212
  {
213
6075
    d_types.push_back(q[0][i].getType());
214
  }
215
4377
  d_owner = q;
216
4377
  return initialize();
217
}
218
219
bool RepSetIterator::setFunctionDomain(Node op)
220
{
221
  Trace("rsi") << "Make rsi for function " << op << std::endl;
222
  Assert(d_types.empty());
223
  TypeNode tn = op.getType();
224
  for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
225
    d_types.push_back( tn[i] );
226
  }
227
  d_owner = op;
228
  return initialize();
229
}
230
231
4377
bool RepSetIterator::initialize()
232
{
233
4377
  Trace("rsi") << "Initialize rep set iterator..." << std::endl;
234
10452
  for( unsigned v=0; v<d_types.size(); v++ ){
235
6075
    d_index.push_back( 0 );
236
    //store default index order
237
6075
    d_index_order.push_back( v );
238
6075
    d_var_order[v] = v;
239
    //store default domain
240
    //d_domain.push_back( RepDomain() );
241
6075
    d_domain_elements.push_back( std::vector< Node >() );
242
12150
    TypeNode tn = d_types[v];
243
6075
    Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl;
244
6075
    bool inc = true;
245
6075
    bool setEnum = false;
246
    //check if it is externally bound
247
6075
    if (d_rext)
248
    {
249
6075
      inc = !d_rext->initializeRepresentativesForType(tn);
250
6075
      RsiEnumType rsiet = d_rext->setBound(d_owner, v, d_domain_elements[v]);
251
6075
      if (rsiet != ENUM_INVALID)
252
      {
253
2075
        d_enum_type.push_back(rsiet);
254
2075
        inc = false;
255
2075
        setEnum = true;
256
      }
257
    }
258
6075
    if (inc)
259
    {
260
      Trace("fmf-incomplete") << "Incomplete because of quantification of type "
261
                              << tn << std::endl;
262
      d_incomplete = true;
263
    }
264
265
    //if we have yet to determine the type of enumeration
266
6075
    if (!setEnum)
267
    {
268
4000
      if (d_rs->hasType(tn))
269
      {
270
4000
        d_enum_type.push_back( ENUM_DEFAULT );
271
4000
        if (const auto* type_reps = d_rs->getTypeRepsOrNull(tn))
272
        {
273
4000
          std::vector<Node>& v_domain_elements = d_domain_elements[v];
274
12000
          v_domain_elements.insert(v_domain_elements.end(),
275
12000
                                   type_reps->begin(), type_reps->end());
276
        }
277
      }else{
278
        Assert(d_incomplete);
279
        return false;
280
      }
281
    }
282
  }
283
284
4377
  if (d_rext)
285
  {
286
8754
    std::vector<unsigned> varOrder;
287
4377
    if (d_rext->getVariableOrder(d_owner, varOrder))
288
    {
289
4377
      if (Trace.isOn("bound-int-rsi"))
290
      {
291
        Trace("bound-int-rsi") << "Variable order : ";
292
        for (unsigned i = 0; i < varOrder.size(); i++)
293
        {
294
          Trace("bound-int-rsi") << varOrder[i] << " ";
295
        }
296
        Trace("bound-int-rsi") << std::endl;
297
      }
298
8754
      std::vector<unsigned> indexOrder;
299
4377
      indexOrder.resize(varOrder.size());
300
10452
      for (unsigned i = 0; i < varOrder.size(); i++)
301
      {
302
6075
        Assert(varOrder[i] < indexOrder.size());
303
6075
        indexOrder[varOrder[i]] = i;
304
      }
305
4377
      if (Trace.isOn("bound-int-rsi"))
306
      {
307
        Trace("bound-int-rsi") << "Will use index order : ";
308
        for (unsigned i = 0; i < indexOrder.size(); i++)
309
        {
310
          Trace("bound-int-rsi") << indexOrder[i] << " ";
311
        }
312
        Trace("bound-int-rsi") << std::endl;
313
      }
314
4377
      setIndexOrder(indexOrder);
315
    }
316
  }
317
  //now reset the indices
318
4377
  do_reset_increment( -1, true );
319
4377
  return true;
320
}
321
322
4377
void RepSetIterator::setIndexOrder(std::vector<unsigned>& indexOrder)
323
{
324
4377
  d_index_order.clear();
325
4377
  d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
326
  //make the d_var_order mapping
327
10452
  for( unsigned i=0; i<d_index_order.size(); i++ ){
328
6075
    d_var_order[d_index_order[i]] = i;
329
  }
330
4377
}
331
332
13019
int RepSetIterator::resetIndex(unsigned i, bool initial)
333
{
334
13019
  d_index[i] = 0;
335
13019
  unsigned v = d_var_order[i];
336
13019
  Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl;
337
13019
  if (d_rext)
338
  {
339
13019
    if (!d_rext->resetIndex(this, d_owner, v, initial, d_domain_elements[v]))
340
    {
341
68
      return -1;
342
    }
343
  }
344
12951
  return d_domain_elements[v].empty() ? 0 : 1;
345
}
346
347
31273
int RepSetIterator::incrementAtIndex(int i)
348
{
349
31273
  Assert(!isFinished());
350
#ifdef DISABLE_EVAL_SKIP_MULTIPLE
351
  i = (int)d_index.size()-1;
352
#endif
353
31273
  Trace("rsi-debug") << "RepSetIterator::incrementAtIndex: " << i << std::endl;
354
  //increment d_index
355
31273
  if( i>=0){
356
30822
    Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
357
  }
358
53825
  while( i>=0 && d_index[i]>=(int)(domainSize(i)-1) ){
359
11276
    i--;
360
11276
    if( i>=0){
361
7548
      Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
362
    }
363
  }
364
31273
  if( i==-1 ){
365
4179
    Trace("rsi-debug") << "increment failed" << std::endl;
366
4179
    d_index.clear();
367
4179
    return -1;
368
  }else{
369
27094
    Trace("rsi-debug") << "increment " << i << std::endl;
370
27094
    d_index[i]++;
371
27094
    return do_reset_increment( i );
372
  }
373
}
374
375
31471
int RepSetIterator::do_reset_increment( int i, bool initial ) {
376
62942
  Trace("rsi-debug") << "RepSetIterator::do_reset_increment: " << i
377
31471
                     << ", initial=" << initial << std::endl;
378
44250
  for( unsigned ii=(i+1); ii<d_index.size(); ii++ ){
379
13019
    bool emptyDomain = false;
380
13019
    int ri_res = resetIndex( ii, initial );
381
13019
    if( ri_res==-1 ){
382
      //failed
383
68
      d_index.clear();
384
68
      d_incomplete = true;
385
68
      break;
386
12951
    }else if( ri_res==0 ){
387
172
      emptyDomain = true;
388
    }
389
    //force next iteration if currently an empty domain
390
12951
    if (emptyDomain)
391
    {
392
344
      Trace("rsi-debug") << "This is an empty domain (index " << ii << ")."
393
172
                         << std::endl;
394
172
      if (ii > 0)
395
      {
396
        // increment at the previous index
397
214
        return incrementAtIndex(ii - 1);
398
      }
399
      else
400
      {
401
        // this is the first index, we are done
402
130
        d_index.clear();
403
130
        return -1;
404
      }
405
    }
406
  }
407
62598
  Trace("rsi-debug") << "Finished, return " << i << std::endl;
408
31299
  return i;
409
}
410
411
29818
int RepSetIterator::increment(){
412
29818
  if( !isFinished() ){
413
29818
    return incrementAtIndex(d_index.size() - 1);
414
  }else{
415
    return -1;
416
  }
417
}
418
419
124491
bool RepSetIterator::isFinished() const { return d_index.empty(); }
420
421
75404
Node RepSetIterator::getCurrentTerm(unsigned i, bool valTerm) const
422
{
423
75404
  unsigned ii = d_index_order[i];
424
75404
  unsigned curr = d_index[ii];
425
150808
  Trace("rsi-debug") << "rsi : get term " << i
426
75404
                     << ", index order = " << d_index_order[i] << std::endl;
427
150808
  Trace("rsi-debug") << "rsi : curr = " << curr << " / "
428
75404
                     << d_domain_elements[i].size() << std::endl;
429
75404
  Assert(0 <= curr && curr < d_domain_elements[i].size());
430
150808
  Node t = d_domain_elements[i][curr];
431
75404
  if (valTerm)
432
  {
433
37820
    Node tt = d_rs->getTermForRepresentative(t);
434
36609
    if (!tt.isNull())
435
    {
436
35398
      return tt;
437
    }
438
  }
439
40006
  return t;
440
}
441
442
void RepSetIterator::getCurrentTerms(std::vector<Node>& terms) const
443
{
444
  for (unsigned i = 0, size = d_index_order.size(); i < size; i++)
445
  {
446
    terms.push_back(getCurrentTerm(i));
447
  }
448
}
449
450
void RepSetIterator::debugPrint( const char* c ){
451
  for( unsigned v=0; v<d_index.size(); v++ ){
452
    Debug( c ) << v << " : " << getCurrentTerm( v ) << std::endl;
453
  }
454
}
455
456
void RepSetIterator::debugPrintSmall( const char* c ){
457
  Debug( c ) << "RI: ";
458
  for( unsigned v=0; v<d_index.size(); v++ ){
459
    Debug( c ) << v << ": " << getCurrentTerm( v ) << " ";
460
  }
461
  Debug( c ) << std::endl;
462
}
463
464
} /* CVC4::theory namespace */
465
26676
} /* CVC4 namespace */