GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_model.cpp Lines: 378 429 88.1 %
Date: 2021-03-22 Branches: 792 1895 41.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_model.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Clark Barrett, 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 model class
13
 **/
14
#include "theory/theory_model.h"
15
16
#include "expr/node_algorithm.h"
17
#include "options/quantifiers_options.h"
18
#include "options/smt_options.h"
19
#include "options/theory_options.h"
20
#include "options/uf_options.h"
21
#include "smt/smt_engine.h"
22
#include "theory/rewriter.h"
23
24
using namespace std;
25
using namespace CVC4::kind;
26
using namespace CVC4::context;
27
28
namespace CVC4 {
29
namespace theory {
30
31
11938
TheoryModel::TheoryModel(context::Context* c,
32
                         std::string name,
33
11938
                         bool enableFuncModels)
34
    : d_name(name),
35
      d_substitutions(c, false),
36
      d_equalityEngine(nullptr),
37
      d_using_model_core(false),
38
11938
      d_enableFuncModels(enableFuncModels)
39
{
40
  // must use function models when ufHo is enabled
41
11938
  Assert(d_enableFuncModels || !options::ufHo());
42
11938
  d_true = NodeManager::currentNM()->mkConst( true );
43
11938
  d_false = NodeManager::currentNM()->mkConst( false );
44
11938
}
45
46
14878
TheoryModel::~TheoryModel() {}
47
48
8995
void TheoryModel::finishInit(eq::EqualityEngine* ee)
49
{
50
8995
  Assert(ee != nullptr);
51
8995
  d_equalityEngine = ee;
52
  // The kinds we are treating as function application in congruence
53
8995
  d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
54
8995
  d_equalityEngine->addFunctionKind(kind::HO_APPLY);
55
8995
  d_equalityEngine->addFunctionKind(kind::SELECT);
56
  // d_equalityEngine->addFunctionKind(kind::STORE);
57
8995
  d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
58
8995
  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
59
8995
  d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
60
  // do not interpret APPLY_UF if we are not assigning function values
61
8995
  if (!d_enableFuncModels)
62
  {
63
    setSemiEvaluatedKind(kind::APPLY_UF);
64
  }
65
  // Equal and not terms are not relevant terms. In other words, asserted
66
  // equalities and negations of predicates (as terms) do not need to be sent
67
  // to the model. Regardless, theories should send information to the model
68
  // that ensures that all assertions are satisfied.
69
8995
  setIrrelevantKind(EQUAL);
70
8995
  setIrrelevantKind(NOT);
71
8995
}
72
73
22352
void TheoryModel::reset(){
74
22352
  d_modelCache.clear();
75
22352
  d_comment_str.clear();
76
22352
  d_sep_heap = Node::null();
77
22352
  d_sep_nil_eq = Node::null();
78
22352
  d_approximations.clear();
79
22352
  d_approx_list.clear();
80
22352
  d_reps.clear();
81
22352
  d_assignExcSet.clear();
82
22352
  d_aesMaster.clear();
83
22352
  d_aesSlaves.clear();
84
22352
  d_rep_set.clear();
85
22352
  d_uf_terms.clear();
86
22352
  d_ho_uf_terms.clear();
87
22352
  d_uf_models.clear();
88
22352
  d_using_model_core = false;
89
22352
  d_model_core.clear();
90
22352
}
91
92
25
void TheoryModel::getComments(std::ostream& out) const {
93
25
  Trace("model-builder") << "get comments..." << std::endl;
94
25
  out << d_comment_str.str();
95
25
}
96
97
7
void TheoryModel::setHeapModel( Node h, Node neq ) {
98
7
  d_sep_heap = h;
99
7
  d_sep_nil_eq = neq;
100
7
}
101
102
31
bool TheoryModel::getHeapModel(Node& h, Node& neq) const
103
{
104
31
  if (d_sep_heap.isNull() || d_sep_nil_eq.isNull())
105
  {
106
25
    return false;
107
  }
108
6
  h = d_sep_heap;
109
6
  neq = d_sep_nil_eq;
110
6
  return true;
111
}
112
113
5900
bool TheoryModel::hasApproximations() const { return !d_approx_list.empty(); }
114
115
std::vector<std::pair<Node, Node> > TheoryModel::getApproximations() const
116
{
117
  return d_approx_list;
118
}
119
120
4
std::vector<Node> TheoryModel::getDomainElements(TypeNode tn) const
121
{
122
  // must be an uninterpreted sort
123
4
  Assert(tn.isSort());
124
8
  std::vector<Node> elements;
125
4
  const std::vector<Node>* type_refs = d_rep_set.getTypeRepsOrNull(tn);
126
4
  if (type_refs == nullptr || type_refs->empty())
127
  {
128
    // This is called when t is a sort that does not occur in this model.
129
    // Sorts are always interpreted as non-empty, thus we add a single element.
130
4
    elements.push_back(tn.mkGroundTerm());
131
4
    return elements;
132
  }
133
  return *type_refs;
134
}
135
136
284275
Node TheoryModel::getValue(TNode n) const
137
{
138
  //apply substitutions
139
284275
  Node nn = d_substitutions.apply(n);
140
284275
  Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl;
141
  //get value in model
142
284275
  nn = getModelValue(nn);
143
284275
  if (nn.isNull()) return nn;
144
573335
  if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
145
    //normalize
146
284275
    nn = Rewriter::rewrite(nn);
147
  }
148
568550
  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): " << std::endl
149
284275
                          << "[model-getvalue] returning " << nn << std::endl;
150
284275
  return nn;
151
}
152
153
30
bool TheoryModel::isModelCoreSymbol(Node s) const
154
{
155
30
  if (!d_using_model_core)
156
  {
157
30
    return true;
158
  }
159
  Assert(s.isVar() && s.getKind() != BOUND_VARIABLE);
160
  return d_model_core.find(s) != d_model_core.end();
161
}
162
163
234
Cardinality TheoryModel::getCardinality(TypeNode tn) const
164
{
165
  //for now, we only handle cardinalities for uninterpreted sorts
166
234
  if (!tn.isSort())
167
  {
168
    Debug("model-getvalue-debug")
169
        << "Get cardinality other sort, unknown." << std::endl;
170
    return Cardinality( CardinalityUnknown() );
171
  }
172
234
  if (d_rep_set.hasType(tn))
173
  {
174
468
    Debug("model-getvalue-debug")
175
234
        << "Get cardinality sort, #rep : "
176
234
        << d_rep_set.getNumRepresentatives(tn) << std::endl;
177
234
    return Cardinality(d_rep_set.getNumRepresentatives(tn));
178
  }
179
  Debug("model-getvalue-debug")
180
      << "Get cardinality sort, unconstrained, return 1." << std::endl;
181
  return Cardinality(1);
182
}
183
184
1597017
Node TheoryModel::getModelValue(TNode n) const
185
{
186
1597017
  std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
187
1597017
  if (it != d_modelCache.end()) {
188
943754
    return (*it).second;
189
  }
190
653263
  Debug("model-getvalue-debug") << "Get model value " << n << " ... ";
191
653263
  Debug("model-getvalue-debug") << d_equalityEngine->hasTerm(n) << std::endl;
192
653263
  Kind nk = n.getKind();
193
653263
  if (n.isConst() || nk == BOUND_VARIABLE)
194
  {
195
30398
    d_modelCache[n] = n;
196
30398
    return n;
197
  }
198
199
1245730
  Node ret = n;
200
622865
  NodeManager* nm = NodeManager::currentNM();
201
202
  // if it is an evaluated kind, compute model values for children and evaluate
203
1245730
  if (n.getNumChildren() > 0
204
1119345
      && d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end()
205
1118564
      && d_semi_evaluated_kinds.find(nk) == d_semi_evaluated_kinds.end())
206
  {
207
991398
    Debug("model-getvalue-debug")
208
495699
        << "Get model value children " << n << std::endl;
209
991398
    std::vector<Node> children;
210
495699
    if (n.getKind() == APPLY_UF)
211
    {
212
17946
      Node op = getModelValue(n.getOperator());
213
8973
      Debug("model-getvalue-debug") << "  operator : " << op << std::endl;
214
8973
      children.push_back(op);
215
    }
216
486726
    else if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
217
    {
218
6045
      children.push_back(n.getOperator());
219
    }
220
    // evaluate the children
221
1799468
    for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
222
    {
223
1303769
      ret = getModelValue(n[i]);
224
2607538
      Debug("model-getvalue-debug")
225
1303769
          << "  " << n << "[" << i << "] is " << ret << std::endl;
226
1303769
      children.push_back(ret);
227
    }
228
495699
    ret = nm->mkNode(n.getKind(), children);
229
495699
    Debug("model-getvalue-debug") << "ret (pre-rewrite): " << ret << std::endl;
230
495699
    ret = Rewriter::rewrite(ret);
231
495699
    Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl;
232
    // special cases
233
495699
    if (ret.getKind() == kind::CARDINALITY_CONSTRAINT)
234
    {
235
468
      Debug("model-getvalue-debug")
236
234
          << "get cardinality constraint " << ret[0].getType() << std::endl;
237
702
      ret = nm->mkConst(getCardinality(ret[0].getType()).getFiniteCardinality()
238
936
                        <= ret[1].getConst<Rational>().getNumerator());
239
    }
240
495465
    else if (ret.getKind() == kind::CARDINALITY_VALUE)
241
    {
242
      Debug("model-getvalue-debug")
243
          << "get cardinality value " << ret[0].getType() << std::endl;
244
      ret = nm->mkConst(
245
          Rational(getCardinality(ret[0].getType()).getFiniteCardinality()));
246
    }
247
495699
    d_modelCache[n] = ret;
248
495699
    return ret;
249
  }
250
  // it might be approximate
251
127166
  std::map<Node, Node>::const_iterator ita = d_approximations.find(n);
252
127166
  if (ita != d_approximations.end())
253
  {
254
    // If the value of n is approximate based on predicate P(n), we return
255
    // witness z. P(z).
256
4
    Node v = nm->mkBoundVar(n.getType());
257
4
    Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
258
4
    Node answer = nm->mkNode(WITNESS, bvl, ita->second.substitute(n, v));
259
2
    d_modelCache[n] = answer;
260
2
    return answer;
261
  }
262
  // must rewrite the term at this point
263
127164
  ret = Rewriter::rewrite(n);
264
  // return the representative of the term in the equality engine, if it exists
265
254328
  TypeNode t = ret.getType();
266
  bool eeHasTerm;
267
127164
  if (!options::ufHo() && (t.isFunction() || t.isPredicate()))
268
  {
269
    // functions are in the equality engine, but *not* as first-class members
270
    // when higher-order is disabled. In this case, we cannot query
271
    // representatives for functions since they are "internal" nodes according
272
    // to the equality engine despite hasTerm returning true. However, they are
273
    // first class members when higher-order is enabled. Hence, the special
274
    // case here.
275
1696
    eeHasTerm = false;
276
  }
277
  else
278
  {
279
125468
    eeHasTerm = d_equalityEngine->hasTerm(ret);
280
  }
281
127164
  if (eeHasTerm)
282
  {
283
239656
    Debug("model-getvalue-debug")
284
119828
        << "get value from representative " << ret << "..." << std::endl;
285
119828
    ret = d_equalityEngine->getRepresentative(ret);
286
119828
    Assert(d_reps.find(ret) != d_reps.end());
287
119828
    std::map<Node, Node>::const_iterator it2 = d_reps.find(ret);
288
119828
    if (it2 != d_reps.end())
289
    {
290
119828
      ret = it2->second;
291
119828
      d_modelCache[n] = ret;
292
119828
      return ret;
293
    }
294
  }
295
296
  // if we are a evaluated or semi-evaluated kind, return an arbitrary value
297
  // if we are not in the d_unevaluated_kinds map, we are evaluated
298
7336
  if (d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end())
299
  {
300
7194
    if (t.isFunction() || t.isPredicate())
301
    {
302
1697
      if (d_enableFuncModels)
303
      {
304
1697
        std::map<Node, Node>::const_iterator entry = d_uf_models.find(n);
305
1697
        if (entry != d_uf_models.end())
306
        {
307
          // Existing function
308
1677
          ret = entry->second;
309
1677
          d_modelCache[n] = ret;
310
1677
          return ret;
311
        }
312
        // Unknown function symbol: return LAMBDA x. c, where c is the first
313
        // constant in the enumeration of the range type
314
40
        vector<TypeNode> argTypes = t.getArgTypes();
315
40
        vector<Node> args;
316
52
        for (unsigned i = 0, size = argTypes.size(); i < size; ++i)
317
        {
318
32
          args.push_back(nm->mkBoundVar(argTypes[i]));
319
        }
320
40
        Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
321
40
        TypeEnumerator te(t.getRangeType());
322
20
        ret = nm->mkNode(kind::LAMBDA, boundVarList, *te);
323
      }
324
      else
325
      {
326
        // if func models not enabled, throw an error
327
        Unreachable();
328
      }
329
    }
330
5497
    else if (!t.isFirstClass())
331
    {
332
      // this is the class for regular expressions
333
      // we simply invoke the rewriter on them
334
19
      ret = Rewriter::rewrite(ret);
335
    }
336
    else
337
    {
338
      // Unknown term - return first enumerated value for this type
339
10956
      TypeEnumerator te(n.getType());
340
5478
      ret = *te;
341
    }
342
5517
    d_modelCache[n] = ret;
343
5517
    return ret;
344
  }
345
346
142
  d_modelCache[n] = n;
347
142
  return n;
348
}
349
350
/** add substitution */
351
44635
void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
352
44635
  if( !d_substitutions.hasSubstitution( x ) ){
353
44574
    Debug("model") << "Add substitution in model " << x << " -> " << t << std::endl;
354
44574
    d_substitutions.addSubstitution( x, t, invalidateCache );
355
  } else {
356
#ifdef CVC4_ASSERTIONS
357
122
    Node oldX = d_substitutions.getSubstitution(x);
358
    // check that either the old substitution is the same, or it now maps to the new substitution
359
61
    if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) {
360
      InternalError()
361
          << "Two incompatible substitutions added to TheoryModel:\n"
362
          << "the term:    " << x << "\n"
363
          << "old mapping: " << d_substitutions.apply(oldX) << "\n"
364
          << "new mapping: " << d_substitutions.apply(t);
365
    }
366
#endif /* CVC4_ASSERTIONS */
367
  }
368
44635
}
369
370
/** add term */
371
1562411
void TheoryModel::addTermInternal(TNode n)
372
{
373
1562411
  Assert(d_equalityEngine->hasTerm(n));
374
1562411
  Trace("model-builder-debug2") << "TheoryModel::addTerm : " << n << std::endl;
375
  //must collect UF terms
376
1562411
  if (n.getKind()==APPLY_UF) {
377
127352
    Node op = n.getOperator();
378
63676
    if( std::find( d_uf_terms[ op ].begin(), d_uf_terms[ op ].end(), n )==d_uf_terms[ op ].end() ){
379
63676
      d_uf_terms[ op ].push_back( n );
380
63676
      Trace("model-builder-fun") << "Add apply term " << n << std::endl;
381
    }
382
1498735
  }else if( n.getKind()==HO_APPLY ){
383
4738
    Node op = n[0];
384
2369
    if( std::find( d_ho_uf_terms[ op ].begin(), d_ho_uf_terms[ op ].end(), n )==d_ho_uf_terms[ op ].end() ){
385
2369
      d_ho_uf_terms[ op ].push_back( n );
386
2369
      Trace("model-builder-fun") << "Add ho apply term " << n << std::endl;
387
    }
388
  }
389
  // all functions must be included, marked as higher-order
390
1562411
  if( n.getType().isFunction() ){
391
1491
    Trace("model-builder-fun") << "Add function variable (without term) " << n << std::endl;
392
1491
    if( d_uf_terms.find( n )==d_uf_terms.end() ){
393
1365
      d_uf_terms[n].clear();
394
    }
395
1491
    if( d_ho_uf_terms.find( n )==d_ho_uf_terms.end() ){
396
1261
      d_ho_uf_terms[n].clear();
397
    }
398
  }
399
1562411
}
400
401
/** assert equality */
402
890208
bool TheoryModel::assertEquality(TNode a, TNode b, bool polarity)
403
{
404
890208
  Assert(d_equalityEngine->consistent());
405
890208
  if (a == b && polarity) {
406
3949
    return true;
407
  }
408
886259
  Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl;
409
886259
  d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() );
410
886259
  return d_equalityEngine->consistent();
411
}
412
413
/** assert predicate */
414
342429
bool TheoryModel::assertPredicate(TNode a, bool polarity)
415
{
416
342429
  Assert(d_equalityEngine->consistent());
417
760440
  if ((a == d_true && polarity) ||
418
342429
      (a == d_false && (!polarity))) {
419
151164
    return true;
420
  }
421
191265
  if (a.getKind() == EQUAL) {
422
    Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl;
423
    d_equalityEngine->assertEquality( a, polarity, Node::null() );
424
  } else {
425
191265
    Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl;
426
191265
    d_equalityEngine->assertPredicate( a, polarity, Node::null() );
427
  }
428
191265
  return d_equalityEngine->consistent();
429
}
430
431
/** assert equality engine */
432
75582
bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee,
433
                                       const std::set<Node>* termSet)
434
{
435
75582
  Assert(d_equalityEngine->consistent());
436
75582
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
437
4061948
  for (; !eqcs_i.isFinished(); ++eqcs_i) {
438
3986366
    Node eqc = (*eqcs_i);
439
1993183
    bool predicate = false;
440
1993183
    bool predTrue = false;
441
1993183
    bool predFalse = false;
442
1993183
    Trace("model-builder-debug") << "...asserting terms in equivalence class " << eqc;
443
1993183
    if (eqc.getType().isBoolean()) {
444
361445
      predicate = true;
445
361445
      predTrue = ee->areEqual(eqc, d_true);
446
361445
      predFalse = ee->areEqual(eqc, d_false);
447
361445
      Trace("model-builder-debug") << ", pred = " << predTrue << "/" << predFalse;
448
    }
449
1993183
    Trace("model-builder-debug") << std::endl;
450
1993183
    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
451
1993183
    bool first = true;
452
3986366
    Node rep;
453
14426203
    for (; !eqc_i.isFinished(); ++eqc_i) {
454
8115506
      Node n = *eqc_i;
455
      // notice that constants are always relevant
456
16750534
      if (termSet != nullptr && termSet->find(n) == termSet->end()
457
10981971
          && !n.isConst())
458
      {
459
8635028
        Trace("model-builder-debug")
460
4317514
            << "...skip node " << n << " in eqc " << eqc << std::endl;
461
4317514
        continue;
462
      }
463
1898996
      if (predicate) {
464
246905
        if (predTrue || predFalse)
465
        {
466
480858
          if (!assertPredicate(n, predTrue))
467
          {
468
            return false;
469
          }
470
        }
471
        else {
472
6476
          if (first) {
473
6476
            rep = n;
474
6476
            first = false;
475
          }
476
          else {
477
            Node eq = (n).eqNode(rep);
478
            Trace("model-builder-assertions")
479
                << "(assert " << eq << ");" << std::endl;
480
            d_equalityEngine->assertEquality(eq, true, Node::null());
481
            if (!d_equalityEngine->consistent())
482
            {
483
              return false;
484
            }
485
          }
486
        }
487
      } else {
488
1652091
        if (first) {
489
1103611
          rep = n;
490
          //add the term (this is specifically for the case of singleton equivalence classes)
491
1103611
          if (rep.getType().isFirstClass())
492
          {
493
1102718
            d_equalityEngine->addTerm( rep );
494
1102718
            Trace("model-builder-debug") << "Add term to ee within assertEqualityEngine: " << rep << std::endl;
495
          }
496
1103611
          first = false;
497
        }
498
        else {
499
548480
          if (!assertEquality(n, rep, true))
500
          {
501
            return false;
502
          }
503
        }
504
      }
505
    }
506
  }
507
75582
  return true;
508
}
509
510
83163
void TheoryModel::assertSkeleton(TNode n)
511
{
512
83163
  Trace("model-builder-reps") << "Assert skeleton : " << n << std::endl;
513
166326
  Trace("model-builder-reps") << "...rep eqc is : " << getRepresentative(n)
514
83163
                              << std::endl;
515
83163
  d_reps[ n ] = n;
516
83163
}
517
518
8
void TheoryModel::setAssignmentExclusionSet(TNode n,
519
                                            const std::vector<Node>& eset)
520
{
521
  // should not be assigned yet
522
8
  Assert(d_assignExcSet.find(n) == d_assignExcSet.end());
523
16
  Trace("model-builder-debug")
524
8
      << "Exclude values of " << n << " : " << eset << std::endl;
525
8
  std::vector<Node>& aes = d_assignExcSet[n];
526
8
  aes.insert(aes.end(), eset.begin(), eset.end());
527
8
}
528
529
8
void TheoryModel::setAssignmentExclusionSetGroup(
530
    const std::vector<TNode>& group, const std::vector<Node>& eset)
531
{
532
8
  if (group.empty())
533
  {
534
    return;
535
  }
536
  // for efficiency, we store a single copy of eset and set a slave/master
537
  // relationship
538
8
  setAssignmentExclusionSet(group[0], eset);
539
8
  std::vector<Node>& gslaves = d_aesSlaves[group[0]];
540
43
  for (unsigned i = 1, gsize = group.size(); i < gsize; ++i)
541
  {
542
70
    Node gs = group[i];
543
    // set master
544
35
    d_aesMaster[gs] = group[0];
545
    // add to slaves
546
35
    gslaves.push_back(gs);
547
  }
548
}
549
550
687807
bool TheoryModel::getAssignmentExclusionSet(TNode n,
551
                                            std::vector<Node>& group,
552
                                            std::vector<Node>& eset)
553
{
554
  // does it have a master?
555
687807
  std::map<Node, Node>::iterator itm = d_aesMaster.find(n);
556
687807
  if (itm != d_aesMaster.end())
557
  {
558
2
    return getAssignmentExclusionSet(itm->second, group, eset);
559
  }
560
687805
  std::map<Node, std::vector<Node> >::iterator ita = d_assignExcSet.find(n);
561
687805
  if (ita == d_assignExcSet.end())
562
  {
563
687797
    return false;
564
  }
565
8
  eset.insert(eset.end(), ita->second.begin(), ita->second.end());
566
8
  group.push_back(n);
567
  // does it have slaves?
568
8
  ita = d_aesSlaves.find(n);
569
8
  if (ita != d_aesSlaves.end())
570
  {
571
8
    group.insert(group.end(), ita->second.begin(), ita->second.end());
572
  }
573
8
  return true;
574
}
575
576
18942
bool TheoryModel::hasAssignmentExclusionSets() const
577
{
578
18942
  return !d_assignExcSet.empty();
579
}
580
581
35
void TheoryModel::recordApproximation(TNode n, TNode pred)
582
{
583
70
  Trace("model-builder-debug")
584
35
      << "Record approximation : " << n << " satisfies the predicate " << pred
585
35
      << std::endl;
586
35
  Assert(d_approximations.find(n) == d_approximations.end());
587
35
  Assert(pred.getType().isBoolean());
588
35
  d_approximations[n] = pred;
589
35
  d_approx_list.push_back(std::pair<Node, Node>(n, pred));
590
  // model cache is invalid
591
35
  d_modelCache.clear();
592
35
}
593
1
void TheoryModel::recordApproximation(TNode n, TNode pred, Node witness)
594
{
595
2
  Node predDisj = NodeManager::currentNM()->mkNode(OR, n.eqNode(witness), pred);
596
1
  recordApproximation(n, predDisj);
597
1
}
598
void TheoryModel::setUsingModelCore()
599
{
600
  d_using_model_core = true;
601
  d_model_core.clear();
602
}
603
604
void TheoryModel::recordModelCoreSymbol(Node sym) { d_model_core.insert(sym); }
605
606
94783
void TheoryModel::setUnevaluatedKind(Kind k) { d_unevaluated_kinds.insert(k); }
607
608
17990
void TheoryModel::setSemiEvaluatedKind(Kind k)
609
{
610
17990
  d_semi_evaluated_kinds.insert(k);
611
17990
}
612
613
26985
void TheoryModel::setIrrelevantKind(Kind k) { d_irrKinds.insert(k); }
614
615
4074084
const std::set<Kind>& TheoryModel::getIrrelevantKinds() const
616
{
617
4074084
  return d_irrKinds;
618
}
619
620
2688
bool TheoryModel::isLegalElimination(TNode x, TNode val)
621
{
622
2688
  return !expr::hasSubtermKinds(d_unevaluated_kinds, val);
623
}
624
625
21266
bool TheoryModel::hasTerm(TNode a)
626
{
627
21266
  return d_equalityEngine->hasTerm( a );
628
}
629
630
563013
Node TheoryModel::getRepresentative(TNode a)
631
{
632
563013
  if( d_equalityEngine->hasTerm( a ) ){
633
1048768
    Node r = d_equalityEngine->getRepresentative( a );
634
524384
    if( d_reps.find( r )!=d_reps.end() ){
635
440785
      return d_reps[ r ];
636
    }else{
637
83599
      return r;
638
    }
639
  }else{
640
38629
    return a;
641
  }
642
}
643
644
2369
bool TheoryModel::areEqual(TNode a, TNode b)
645
{
646
2369
  if( a==b ){
647
2235
    return true;
648
134
  }else if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){
649
134
    return d_equalityEngine->areEqual( a, b );
650
  }else{
651
    return false;
652
  }
653
}
654
655
bool TheoryModel::areDisequal(TNode a, TNode b)
656
{
657
  if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){
658
    return d_equalityEngine->areDisequal( a, b, false );
659
  }else{
660
    return false;
661
  }
662
}
663
664
20530
bool TheoryModel::areFunctionValuesEnabled() const
665
{
666
20530
  return d_enableFuncModels;
667
}
668
669
14340
void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) {
670
14340
  Trace("model-builder") << "  Assigning function (" << f << ") to (" << f_def << ")" << endl;
671
14340
  Assert(d_uf_models.find(f) == d_uf_models.end());
672
673
14340
  if( options::ufHo() ){
674
    //we must rewrite the function value since the definition needs to be a constant value
675
1147
    f_def = Rewriter::rewrite( f_def );
676
2294
    Trace("model-builder-debug")
677
1147
        << "Model value (post-rewrite) : " << f_def << std::endl;
678
1147
    Assert(f_def.isConst()) << "Non-constant f_def: " << f_def;
679
  }
680
681
  // d_uf_models only stores models for variables
682
14340
  if( f.isVar() ){
683
14206
    d_uf_models[f] = f_def;
684
  }
685
686
14340
  if (options::ufHo() && d_equalityEngine->hasTerm(f))
687
  {
688
1147
    Trace("model-builder-debug") << "  ...function is first-class member of equality engine" << std::endl;
689
    // assign to representative if higher-order
690
2294
    Node r = d_equalityEngine->getRepresentative( f );
691
    //always replace the representative, since it is initially assigned to itself
692
1147
    Trace("model-builder") << "    Assign: Setting function rep " << r << " to " << f_def << endl;
693
1147
    d_reps[r] = f_def;
694
    // also assign to other assignable functions in the same equivalence class
695
1147
    eq::EqClassIterator eqc_i = eq::EqClassIterator(r,d_equalityEngine);
696
4129
    while( !eqc_i.isFinished() ) {
697
2982
      Node n = *eqc_i;
698
      // if an unassigned variable function
699
1491
      if( n.isVar() && d_uf_terms.find( n )!=d_uf_terms.end() && !hasAssignedFunctionDefinition( n ) ){
700
281
        d_uf_models[n] = f_def;
701
281
        Trace("model-builder") << "  Assigning function (" << n << ") to function definition of " << f << std::endl;
702
      }
703
1491
      ++eqc_i;
704
    }
705
1147
    Trace("model-builder-debug") << "  ...finished." << std::endl;
706
  }
707
14340
}
708
709
18942
std::vector< Node > TheoryModel::getFunctionsToAssign() {
710
18942
  std::vector< Node > funcs_to_assign;
711
37884
  std::map< Node, Node > func_to_rep;
712
713
  // collect functions
714
31552
  for( std::map< Node, std::vector< Node > >::iterator it = d_uf_terms.begin(); it != d_uf_terms.end(); ++it ){
715
25220
    Node n = it->first;
716
12610
    Assert(!n.isNull());
717
12610
    if( !hasAssignedFunctionDefinition( n ) ){
718
6276
      Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl;
719
6276
      if( options::ufHo() ){
720
        // if in higher-order mode, assign function definitions modulo equality
721
2982
        Node r = getRepresentative( n );
722
1491
        std::map< Node, Node >::iterator itf = func_to_rep.find( r );
723
1491
        if( itf==func_to_rep.end() ){
724
1147
          func_to_rep[r] = n;
725
1147
          funcs_to_assign.push_back( n );
726
1147
          Trace("model-builder-fun") << "Make function " << n;
727
1147
          Trace("model-builder-fun") << " the assignable function in its equivalence class." << std::endl;
728
        }else{
729
          // must combine uf terms
730
344
          Trace("model-builder-fun") << "Copy " << it->second.size() << " uf terms";
731
344
          d_uf_terms[itf->second].insert( d_uf_terms[itf->second].end(), it->second.begin(), it->second.end() );
732
344
          std::map< Node, std::vector< Node > >::iterator ith = d_ho_uf_terms.find( n );
733
344
          if( ith!=d_ho_uf_terms.end() ){
734
344
            d_ho_uf_terms[itf->second].insert( d_ho_uf_terms[itf->second].end(), ith->second.begin(), ith->second.end() );
735
344
            Trace("model-builder-fun") << " and " << ith->second.size() << " ho uf terms";
736
          }
737
344
          Trace("model-builder-fun") << " from " << n << " to its assignable representative function " << itf->second << std::endl;
738
344
          it->second.clear();
739
        }
740
      }else{
741
4785
        Trace("model-builder-fun") << "Function to assign : " << n << std::endl;
742
4785
        funcs_to_assign.push_back( n );
743
      }
744
    }
745
  }
746
747
18942
  Trace("model-builder-fun") << "return " << funcs_to_assign.size() << " functions to assign..." << std::endl;
748
37884
  return funcs_to_assign;
749
}
750
751
8995
const std::string& TheoryModel::getName() const { return d_name; }
752
753
std::string TheoryModel::debugPrintModelEqc() const
754
{
755
  std::stringstream ss;
756
  ss << "--- Equivalence classes:" << std::endl;
757
  ss << d_equalityEngine->debugPrintEqc() << std::endl;
758
  ss << "--- Representative map: " << std::endl;
759
  for (const std::pair<const Node, Node>& r : d_reps)
760
  {
761
    ss << r.first << " -> " << r.second << std::endl;
762
  }
763
  ss << "---" << std::endl;
764
  return ss.str();
765
}
766
767
} /* namespace CVC4::theory */
768
315736
} /* namespace CVC4 */