GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_model_builder.cpp Lines: 626 664 94.3 %
Date: 2021-03-22 Branches: 1224 2789 43.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_model_builder.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Clark Barrett, Andres Noetzli
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 theory model buidler class
13
 **/
14
#include "theory/theory_model_builder.h"
15
16
#include "expr/dtype.h"
17
#include "expr/dtype_cons.h"
18
#include "options/quantifiers_options.h"
19
#include "options/smt_options.h"
20
#include "options/theory_options.h"
21
#include "options/uf_options.h"
22
#include "theory/rewriter.h"
23
#include "theory/uf/theory_uf_model.h"
24
25
using namespace std;
26
using namespace CVC4::kind;
27
using namespace CVC4::context;
28
29
namespace CVC4 {
30
namespace theory {
31
32
8
void TheoryEngineModelBuilder::Assigner::initialize(
33
    TypeNode tn, TypeEnumeratorProperties* tep, const std::vector<Node>& aes)
34
{
35
8
  d_te.reset(new TypeEnumerator(tn, tep));
36
8
  d_assignExcSet.insert(d_assignExcSet.end(), aes.begin(), aes.end());
37
8
}
38
39
43
Node TheoryEngineModelBuilder::Assigner::getNextAssignment()
40
{
41
43
  Assert(d_te != nullptr);
42
86
  Node n;
43
43
  bool success = false;
44
43
  TypeEnumerator& te = *d_te;
45
  // Check if we have run out of elements. This should never happen; if it
46
  // does we assert false and return null.
47
43
  if (te.isFinished())
48
  {
49
    Assert(false);
50
    return Node::null();
51
  }
52
  // must increment until we find one that is not in the assignment
53
  // exclusion set
54
17
  do
55
  {
56
60
    n = *te;
57
60
    success = std::find(d_assignExcSet.begin(), d_assignExcSet.end(), n)
58
120
              == d_assignExcSet.end();
59
    // increment regardless of fail or succeed, to set up the next value
60
60
    ++te;
61
60
  } while (!success);
62
43
  return n;
63
}
64
65
8995
TheoryEngineModelBuilder::TheoryEngineModelBuilder() {}
66
67
266235
Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
68
{
69
266235
  eq::EqClassIterator eqc_i = eq::EqClassIterator(r, m->d_equalityEngine);
70
282085
  for (; !eqc_i.isFinished(); ++eqc_i)
71
  {
72
276772
    Node n = *eqc_i;
73
268847
    Trace("model-builder-debug") << "Look at term : " << n << std::endl;
74
268847
    if (!isAssignable(n))
75
    {
76
267679
      Trace("model-builder-debug") << "...try to normalize" << std::endl;
77
274436
      Node normalized = normalize(m, n, true);
78
267679
      if (normalized.isConst())
79
      {
80
260922
        return normalized;
81
      }
82
    }
83
  }
84
5313
  return Node::null();
85
}
86
87
43
bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
88
{
89
43
  if (a.d_isActive)
90
  {
91
35
    return true;
92
  }
93
8
  std::vector<Node>& eset = a.d_assignExcSet;
94
8
  std::map<Node, Node>::iterator it;
95
26
  for (unsigned i = 0, size = eset.size(); i < size; i++)
96
  {
97
    // Members of exclusion set must have values, otherwise we are not yet
98
    // assignable.
99
23
    Node er = eset[i];
100
18
    if (er.isConst())
101
    {
102
      // already processed
103
13
      continue;
104
    }
105
    // Assignable members of assignment exclusion set should be representatives
106
    // of their equivalence classes. This ensures we look up the constant
107
    // representatives for assignable members of assignment exclusion sets.
108
5
    Assert(er == tm->getRepresentative(er));
109
5
    it = d_constantReps.find(er);
110
5
    if (it == d_constantReps.end())
111
    {
112
      Trace("model-build-aes")
113
          << "isAssignerActive: not active due to " << er << std::endl;
114
      return false;
115
    }
116
    // update
117
5
    eset[i] = it->second;
118
  }
119
8
  Trace("model-build-aes") << "isAssignerActive: active!" << std::endl;
120
8
  a.d_isActive = true;
121
8
  return true;
122
}
123
124
3048991
bool TheoryEngineModelBuilder::isAssignable(TNode n)
125
{
126
3048991
  if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL)
127
  {
128
    // selectors are always assignable (where we guarantee that they are not
129
    // evaluatable here)
130
360113
    if (!options::ufHo())
131
    {
132
340785
      Assert(!n.getType().isFunction());
133
340785
      return true;
134
    }
135
    else
136
    {
137
      // might be a function field
138
19328
      return !n.getType().isFunction();
139
    }
140
  }
141
2688878
  else if (n.getKind() == kind::FLOATINGPOINT_COMPONENT_SIGN)
142
  {
143
    // Extracting the sign of a floating-point number acts similar to a
144
    // selector on a datatype, i.e. if `(sign x)` wasn't assigned a value, we
145
    // can pick an arbitrary one. Note that the other components of a
146
    // floating-point number should always be assigned a value.
147
1410
    return true;
148
  }
149
  else
150
  {
151
    // non-function variables, and fully applied functions
152
2687468
    if (!options::ufHo())
153
    {
154
      // no functions exist, all functions are fully applied
155
2622523
      Assert(n.getKind() != kind::HO_APPLY);
156
2622523
      Assert(!n.getType().isFunction());
157
2622523
      return n.isVar() || n.getKind() == kind::APPLY_UF;
158
    }
159
    else
160
    {
161
      // Assert( n.getKind() != kind::APPLY_UF );
162
144360
      return (n.isVar() && !n.getType().isFunction())
163
57837
             || n.getKind() == kind::APPLY_UF
164
199179
             || (n.getKind() == kind::HO_APPLY
165
70075
                 && n[0].getType().getNumChildren() == 2);
166
    }
167
  }
168
}
169
170
3897062
void TheoryEngineModelBuilder::addAssignableSubterms(TNode n,
171
                                                     TheoryModel* tm,
172
                                                     NodeSet& cache)
173
{
174
3897062
  if (n.isClosure())
175
  {
176
34084
    return;
177
  }
178
3862978
  if (cache.find(n) != cache.end())
179
  {
180
2269886
    return;
181
  }
182
1593092
  if (isAssignable(n))
183
  {
184
499359
    tm->d_equalityEngine->addTerm(n);
185
  }
186
3927743
  for (TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it)
187
  {
188
2334651
    addAssignableSubterms(*child_it, tm, cache);
189
  }
190
1593092
  cache.insert(n);
191
}
192
193
685103
void TheoryEngineModelBuilder::assignConstantRep(TheoryModel* tm,
194
                                                 Node eqc,
195
                                                 Node constRep)
196
{
197
685103
  d_constantReps[eqc] = constRep;
198
1370206
  Trace("model-builder") << "    Assign: Setting constant rep of " << eqc
199
685103
                         << " to " << constRep << endl;
200
685103
  tm->d_rep_set.setTermForRepresentative(constRep, eqc);
201
685103
}
202
203
51
bool TheoryEngineModelBuilder::isExcludedCdtValue(
204
    Node val,
205
    std::set<Node>* repSet,
206
    std::map<Node, Node>& assertedReps,
207
    Node eqc)
208
{
209
102
  Trace("model-builder-debug")
210
51
      << "Is " << val << " and excluded codatatype value for " << eqc << "? "
211
51
      << std::endl;
212
111
  for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i)
213
  {
214
68
    Assert(assertedReps.find(*i) != assertedReps.end());
215
128
    Node rep = assertedReps[*i];
216
68
    Trace("model-builder-debug") << "  Rep : " << rep << std::endl;
217
    // check matching val to rep with eqc as a free variable
218
128
    Node eqc_m;
219
68
    if (isCdtValueMatch(val, rep, eqc, eqc_m))
220
    {
221
40
      Trace("model-builder-debug") << "  ...matches with " << eqc << " -> "
222
20
                                   << eqc_m << std::endl;
223
20
      if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT)
224
      {
225
16
        Trace("model-builder-debug") << "*** " << val
226
8
                                     << " is excluded datatype for " << eqc
227
8
                                     << std::endl;
228
8
        return true;
229
      }
230
    }
231
  }
232
43
  return false;
233
}
234
235
184
bool TheoryEngineModelBuilder::isCdtValueMatch(Node v,
236
                                               Node r,
237
                                               Node eqc,
238
                                               Node& eqc_m)
239
{
240
184
  if (r == v)
241
  {
242
52
    return true;
243
  }
244
132
  else if (r == eqc)
245
  {
246
20
    if (eqc_m.isNull())
247
    {
248
      // only if an uninterpreted constant?
249
20
      eqc_m = v;
250
20
      return true;
251
    }
252
    else
253
    {
254
      return v == eqc_m;
255
    }
256
  }
257
224
  else if (v.getKind() == kind::APPLY_CONSTRUCTOR
258
112
           && r.getKind() == kind::APPLY_CONSTRUCTOR)
259
  {
260
74
    if (v.getOperator() == r.getOperator())
261
    {
262
136
      for (unsigned i = 0; i < v.getNumChildren(); i++)
263
      {
264
116
        if (!isCdtValueMatch(v[i], r[i], eqc, eqc_m))
265
        {
266
44
          return false;
267
        }
268
      }
269
20
      return true;
270
    }
271
  }
272
48
  return false;
273
}
274
275
21149
bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn)
276
{
277
21149
  if (tn.isSort())
278
  {
279
4
    return true;
280
  }
281
21145
  else if (tn.isArray())
282
  {
283
6
    return involvesUSort(tn.getArrayIndexType())
284
6
           || involvesUSort(tn.getArrayConstituentType());
285
  }
286
21143
  else if (tn.isSet())
287
  {
288
4
    return involvesUSort(tn.getSetElementType());
289
  }
290
21139
  else if (tn.isDatatype())
291
  {
292
20967
    const DType& dt = tn.getDType();
293
20967
    return dt.involvesUninterpretedType();
294
  }
295
  else
296
  {
297
172
    return false;
298
  }
299
}
300
301
89972
bool TheoryEngineModelBuilder::isExcludedUSortValue(
302
    std::map<TypeNode, unsigned>& eqc_usort_count,
303
    Node v,
304
    std::map<Node, bool>& visited)
305
{
306
89972
  Assert(v.isConst());
307
89972
  if (visited.find(v) == visited.end())
308
  {
309
66036
    visited[v] = true;
310
131886
    TypeNode tn = v.getType();
311
66036
    if (tn.isSort())
312
    {
313
372
      Trace("model-builder-debug") << "Is excluded usort value : " << v << " "
314
186
                                   << tn << std::endl;
315
186
      unsigned card = eqc_usort_count[tn];
316
186
      Trace("model-builder-debug") << "  Cardinality is " << card << std::endl;
317
      unsigned index =
318
186
          v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
319
186
      Trace("model-builder-debug") << "  Index is " << index << std::endl;
320
186
      return index > 0 && index >= card;
321
    }
322
142301
    for (unsigned i = 0; i < v.getNumChildren(); i++)
323
    {
324
76451
      if (isExcludedUSortValue(eqc_usort_count, v[i], visited))
325
      {
326
        return true;
327
      }
328
    }
329
  }
330
89786
  return false;
331
}
332
333
433541
void TheoryEngineModelBuilder::addToTypeList(
334
    TypeNode tn,
335
    std::vector<TypeNode>& type_list,
336
    std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting)
337
{
338
433541
  if (std::find(type_list.begin(), type_list.end(), tn) == type_list.end())
339
  {
340
136113
    if (visiting.find(tn) == visiting.end())
341
    {
342
40954
      visiting.insert(tn);
343
      /* This must make a recursive call on all types that are subterms of
344
       * values of the current type.
345
       * Note that recursive traversal here is over enumerated expressions
346
       * (very low expression depth). */
347
40954
      if (tn.isArray())
348
      {
349
414
        addToTypeList(tn.getArrayIndexType(), type_list, visiting);
350
414
        addToTypeList(tn.getArrayConstituentType(), type_list, visiting);
351
      }
352
40540
      else if (tn.isSet())
353
      {
354
391
        addToTypeList(tn.getSetElementType(), type_list, visiting);
355
      }
356
40149
      else if (tn.isDatatype())
357
      {
358
21691
        const DType& dt = tn.getDType();
359
180525
        for (unsigned i = 0; i < dt.getNumConstructors(); i++)
360
        {
361
280285
          for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
362
          {
363
242902
            TypeNode ctn = dt[i][j].getRangeType();
364
121451
            addToTypeList(ctn, type_list, visiting);
365
          }
366
        }
367
      }
368
40954
      Assert(std::find(type_list.begin(), type_list.end(), tn)
369
             == type_list.end());
370
40954
      type_list.push_back(tn);
371
    }
372
  }
373
433541
}
374
375
18942
bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
376
{
377
18942
  Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
378
379
37884
  Trace("model-builder")
380
18942
      << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl;
381
  // model-builder specific initialization
382
18942
  if (!preProcessBuildModel(tm))
383
  {
384
    Trace("model-builder")
385
        << "TheoryEngineModelBuilder: fail preprocess build model."
386
        << std::endl;
387
    return false;
388
  }
389
390
37884
  Trace("model-builder")
391
      << "TheoryEngineModelBuilder: Add assignable subterms "
392
18942
         ", collect representatives and compute assignable information..."
393
18942
      << std::endl;
394
395
  // type enumerator properties
396
37884
  TypeEnumeratorProperties tep;
397
398
  // In the first step of model building, we do a traversal of the
399
  // equality engine and record the information in the following:
400
401
  // The constant representatives, per equivalence class
402
18942
  d_constantReps.clear();
403
  // The representatives that have been asserted by theories. This includes
404
  // non-constant "skeletons" that have been specified by parametric theories.
405
37884
  std::map<Node, Node> assertedReps;
406
  // A parition of the set of equivalence classes that have:
407
  // (1) constant representatives,
408
  // (2) an assigned representative specified by a theory in collectModelInfo,
409
  // (3) no assigned representative.
410
37884
  TypeSet typeConstSet, typeRepSet, typeNoRepSet;
411
  // An ordered list of types, such that T1 comes before T2 if T1 is a
412
  // "component type" of T2, e.g. U comes before (Set U). This is only strictly
413
  // necessary for finite model finding + parametric types instantiated with
414
  // uninterpreted sorts, but is probably a good idea to do in general since it
415
  // leads to models with smaller term sizes. -AJR
416
37884
  std::vector<TypeNode> type_list;
417
  // The count of equivalence classes per sort (for finite model finding).
418
37884
  std::map<TypeNode, unsigned> eqc_usort_count;
419
420
  // the set of equivalence classes that are "assignable", i.e. those that have
421
  // an assignable expression in them (see isAssignable), and have not already
422
  // been assigned a constant.
423
37884
  std::unordered_set<Node, NodeHashFunction> assignableEqc;
424
  // The set of equivalence classes that are "evaluable", i.e. those that have
425
  // an expression in them that is not assignable, and have not already been
426
  // assigned a constant.
427
37884
  std::unordered_set<Node, NodeHashFunction> evaluableEqc;
428
  // Assigner objects for relevant equivalence classes that require special
429
  // ways of assigning values, e.g. those that take into account assignment
430
  // exclusion sets.
431
37884
  std::map<Node, Assigner> eqcToAssigner;
432
  // A map from equivalence classes to the equivalence class that it shares an
433
  // assigner object with (all elements in the range of this map are in the
434
  // domain of eqcToAssigner).
435
37884
  std::map<Node, Node> eqcToAssignerMaster;
436
437
  // Loop through equivalence classes of the equality engine of the model.
438
18942
  eq::EqualityEngine* ee = tm->d_equalityEngine;
439
37884
  NodeSet assignableCache;
440
18942
  std::map<Node, Node>::iterator itm;
441
18942
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
442
  // should we compute assigner objects?
443
18942
  bool computeAssigners = tm->hasAssignmentExclusionSets();
444
  // the set of exclusion sets we have processed
445
37884
  std::unordered_set<Node, NodeHashFunction> processedExcSet;
446
1391534
  for (; !eqcs_i.isFinished(); ++eqcs_i)
447
  {
448
997167
    Node eqc = *eqcs_i;
449
450
    // Information computed for each equivalence class
451
452
    // The assigned represenative and constant representative
453
997167
    Node rep, constRep;
454
    // A flag set to true if the current equivalence class is assignable (see
455
    // assignableEqc).
456
686296
    bool assignable = false;
457
    // Set to true if the current equivalence class is evaluatable (see
458
    // evaluableEqc).
459
686296
    bool evaluable = false;
460
    // Set to true if a term in the current equivalence class has been given an
461
    // assignment exclusion set.
462
686296
    bool hasESet CVC4_UNUSED = false;
463
    // Set to true if we found that a term in the current equivalence class has
464
    // been given an assignment exclusion set, and we have not seen this term
465
    // as part of a previous assignment exclusion group. In other words, when
466
    // this flag is true we construct a new assigner object with the current
467
    // equivalence class as its master.
468
686296
    bool foundESet = false;
469
    // The assignment exclusion set for the current equivalence class.
470
997167
    std::vector<Node> eset;
471
    // The group to which this equivalence class belongs when exclusion sets
472
    // were assigned (see the argument group of
473
    // TheoryModel::getAssignmentExclusionSet).
474
997167
    std::vector<Node> esetGroup;
475
476
    // Loop through terms in this EC
477
686296
    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
478
3811118
    for (; !eqc_i.isFinished(); ++eqc_i)
479
    {
480
1562589
      Node n = *eqc_i;
481
1562411
      Trace("model-builder") << "  Processing Term: " << n << endl;
482
483
      // For each term n in this equivalence class, below we register its
484
      // assignable subterms, compute whether it is a constant or assigned
485
      // representative, then if we don't have a constant representative,
486
      // compute information regarding how we will assign values.
487
488
      // (1) Add assignable subterms, which ensures that e.g. models for
489
      // uninterpreted functions take into account all subterms in the
490
      // equality engine of the model
491
1562411
      addAssignableSubterms(n, tm, assignableCache);
492
      // model-specific processing of the term
493
1562411
      tm->addTermInternal(n);
494
495
      // (2) Record constant representative or assign representative, if
496
      // applicable
497
1937836
      if (n.isConst())
498
      {
499
375425
        Assert(constRep.isNull());
500
375425
        constRep = n;
501
750850
        Trace("model-builder")
502
375425
            << "  ConstRep( " << eqc << " ) = " << constRep << std::endl;
503
        // if we have a constant representative, nothing else matters
504
375425
        continue;
505
      }
506
507
      // If we don't have a constant rep, check if this is an assigned rep.
508
1186986
      itm = tm->d_reps.find(n);
509
1186986
      if (itm != tm->d_reps.end())
510
      {
511
        // Notice that this equivalence class may contain multiple terms that
512
        // were specified as being a representative, since e.g. datatypes may
513
        // assert representative for two constructor terms that are not in the
514
        // care graph and are merged during collectModeInfo due to equality
515
        // information from another theory. We overwrite the value of rep in
516
        // these cases here.
517
25222
        rep = itm->second;
518
50444
        Trace("model-builder")
519
25222
            << "  Rep( " << eqc << " ) = " << rep << std::endl;
520
      }
521
522
      // (3) Finally, process assignable information
523
1874613
      if (!isAssignable(n))
524
      {
525
687627
        evaluable = true;
526
        // expressions that are not assignable should not be given assignment
527
        // exclusion sets
528
687627
        Assert(!tm->getAssignmentExclusionSet(n, esetGroup, eset));
529
687627
        continue;
530
      }
531
499359
      assignable = true;
532
499359
      if (!computeAssigners)
533
      {
534
        // we don't compute assigners, skip
535
499146
        continue;
536
      }
537
      // process the assignment exclusion set for term n
538
      // was it processed based on a master exclusion group (see
539
      // eqcToAssignerMaster)?
540
248
      if (processedExcSet.find(n) != processedExcSet.end())
541
      {
542
        // Should not have two assignment exclusion sets for the same
543
        // equivalence class
544
35
        Assert(!hasESet);
545
35
        Assert(eqcToAssignerMaster.find(eqc) != eqcToAssignerMaster.end());
546
        // already processed as a slave term
547
35
        hasESet = true;
548
35
        continue;
549
      }
550
      // was it assigned one?
551
178
      if (tm->getAssignmentExclusionSet(n, esetGroup, eset))
552
      {
553
        // Should not have two assignment exclusion sets for the same
554
        // equivalence class
555
8
        Assert(!hasESet);
556
8
        foundESet = true;
557
8
        hasESet = true;
558
      }
559
    }
560
561
    // finished traversing the equality engine
562
997167
    TypeNode eqct = eqc.getType();
563
    // count the number of equivalence classes of sorts in finite model finding
564
686296
    if (options::finiteModelFind())
565
    {
566
33068
      if (eqct.isSort())
567
      {
568
4460
        eqc_usort_count[eqct]++;
569
      }
570
    }
571
    // Assign representative for this equivalence class
572
1061721
    if (!constRep.isNull())
573
    {
574
      // Theories should not specify a rep if there is already a constant in the
575
      // equivalence class. However, it may be the case that the representative
576
      // specified by a theory may be merged with a constant based on equality
577
      // information from another class. Thus, rep may be non-null here.
578
      // Regardless, we assign constRep as the representative here.
579
375425
      assignConstantRep(tm, eqc, constRep);
580
375425
      typeConstSet.add(eqct.getBaseType(), constRep);
581
375425
      continue;
582
    }
583
310871
    else if (!rep.isNull())
584
    {
585
25149
      assertedReps[eqc] = rep;
586
25149
      typeRepSet.add(eqct.getBaseType(), eqc);
587
50298
      std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
588
25149
      addToTypeList(eqct.getBaseType(), type_list, visiting);
589
    }
590
    else
591
    {
592
285722
      typeNoRepSet.add(eqct, eqc);
593
571444
      std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
594
285722
      addToTypeList(eqct, type_list, visiting);
595
    }
596
597
310871
    if (assignable)
598
    {
599
44595
      assignableEqc.insert(eqc);
600
    }
601
310871
    if (evaluable)
602
    {
603
287292
      evaluableEqc.insert(eqc);
604
    }
605
    // If we found an assignment exclusion set, we construct a new assigner
606
    // object.
607
310871
    if (foundESet)
608
    {
609
      // we don't accept assignment exclusion sets for evaluable eqc
610
8
      Assert(!evaluable);
611
      // construct the assigner
612
8
      Assigner& a = eqcToAssigner[eqc];
613
      // Take the representatives of each term in the assignment exclusion
614
      // set, which ensures we can look up their value in d_constReps later.
615
16
      std::vector<Node> aes;
616
26
      for (const Node& e : eset)
617
      {
618
        // Should only supply terms that occur in the model or constants
619
        // in assignment exclusion sets.
620
18
        Assert(tm->hasTerm(e) || e.isConst());
621
36
        Node er = tm->hasTerm(e) ? tm->getRepresentative(e) : e;
622
18
        aes.push_back(er);
623
      }
624
      // initialize
625
8
      a.initialize(eqc.getType(), &tep, aes);
626
      // all others in the group are slaves of this
627
51
      for (const Node& g : esetGroup)
628
      {
629
43
        Assert(isAssignable(g));
630
43
        if (!tm->hasTerm(g))
631
        {
632
          // Ignore those that aren't in the model, in the case the user
633
          // has supplied an assignment exclusion set to a variable not in
634
          // the model.
635
          continue;
636
        }
637
86
        Node gr = tm->getRepresentative(g);
638
43
        if (gr != eqc)
639
        {
640
35
          eqcToAssignerMaster[gr] = eqc;
641
          // remember that this term has been processed
642
35
          processedExcSet.insert(g);
643
        }
644
      }
645
    }
646
  }
647
648
  // Now finished initialization
649
650
  // Compute type enumerator properties. This code ensures we do not
651
  // enumerate terms that have uninterpreted constants that violate the
652
  // bounds imposed by finite model finding. For example, if finite
653
  // model finding insists that there are only 2 values { U1, U2 } of type U,
654
  // then the type enumerator for list of U should enumerate:
655
  //   nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ...
656
  // instead of enumerating (cons U3 nil).
657
18942
  if (options::finiteModelFind())
658
  {
659
941
    tep.d_fixed_usort_card = true;
660
3408
    for (std::map<TypeNode, unsigned>::iterator it = eqc_usort_count.begin();
661
3408
         it != eqc_usort_count.end();
662
         ++it)
663
    {
664
4934
      Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : "
665
2467
                             << it->second << std::endl;
666
2467
      tep.d_fixed_card[it->first] = Integer(it->second);
667
    }
668
941
    typeConstSet.setTypeEnumeratorProperties(&tep);
669
  }
670
671
  // Need to ensure that each EC has a constant representative.
672
673
18942
  Trace("model-builder") << "Processing EC's..." << std::endl;
674
675
18942
  TypeSet::iterator it;
676
18942
  vector<TypeNode>::iterator type_it;
677
18942
  set<Node>::iterator i, i2;
678
18942
  bool changed, unassignedAssignable, assignOne = false;
679
37884
  set<TypeNode> evaluableSet;
680
681
  // Double-fixed-point loop
682
  // Outer loop handles a special corner case (see code at end of loop for
683
  // details)
684
  for (;;)
685
  {
686
    // Inner fixed-point loop: we are trying to learn constant values for every
687
    // EC.  Each time through this loop, we process all of the
688
    // types by type and may learn some new EC values.  EC's in one type may
689
    // depend on EC's in another type, so we need a fixed-point loop
690
    // to ensure that we learn as many EC values as possible
691
56149
    do
692
    {
693
56149
      changed = false;
694
56149
      unassignedAssignable = false;
695
56149
      evaluableSet.clear();
696
697
      // Iterate over all types we've seen
698
316311
      for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
699
      {
700
520324
        TypeNode t = *type_it;
701
520324
        TypeNode tb = t.getBaseType();
702
260162
        set<Node>* noRepSet = typeNoRepSet.getSet(t);
703
704
        // 1. Try to evaluate the EC's in this type
705
260162
        if (noRepSet != NULL && !noRepSet->empty())
706
        {
707
100168
          Trace("model-builder") << "  Eval phase, working on type: " << t
708
50084
                                 << endl;
709
          bool evaluable;
710
50084
          d_normalizedCache.clear();
711
1504921
          for (i = noRepSet->begin(); i != noRepSet->end();)
712
          {
713
1454837
            i2 = i;
714
1454837
            ++i;
715
2909674
            Trace("model-builder-debug") << "Look at eqc : " << (*i2)
716
1454837
                                         << std::endl;
717
2909674
            Node normalized;
718
            // only possible to normalize if we are evaluable
719
1454837
            evaluable = evaluableEqc.find(*i2) != evaluableEqc.end();
720
1454837
            if (evaluable)
721
            {
722
266235
              normalized = evaluateEqc(tm, *i2);
723
            }
724
1454837
            if (!normalized.isNull())
725
            {
726
260922
              Assert(normalized.isConst());
727
260922
              typeConstSet.add(tb, normalized);
728
260922
              assignConstantRep(tm, *i2, normalized);
729
521844
              Trace("model-builder") << "    Eval: Setting constant rep of "
730
260922
                                     << (*i2) << " to " << normalized << endl;
731
260922
              changed = true;
732
260922
              noRepSet->erase(i2);
733
            }
734
            else
735
            {
736
1193915
              if (evaluable)
737
              {
738
5313
                evaluableSet.insert(tb);
739
              }
740
              // If assignable, remember there is an equivalence class that is
741
              // not assigned and assignable.
742
1193915
              if (assignableEqc.find(*i2) != assignableEqc.end())
743
              {
744
1188857
                unassignedAssignable = true;
745
              }
746
            }
747
          }
748
        }
749
750
        // 2. Normalize any non-const representative terms for this type
751
260162
        set<Node>* repSet = typeRepSet.getSet(t);
752
260162
        if (repSet != NULL && !repSet->empty())
753
        {
754
116504
          Trace("model-builder")
755
58252
              << "  Normalization phase, working on type: " << t << endl;
756
58252
          d_normalizedCache.clear();
757
548145
          for (i = repSet->begin(); i != repSet->end();)
758
          {
759
489893
            Assert(assertedReps.find(*i) != assertedReps.end());
760
979786
            Node rep = assertedReps[*i];
761
979786
            Node normalized = normalize(tm, rep, false);
762
979786
            Trace("model-builder") << "    Normalizing rep (" << rep
763
489893
                                   << "), normalized to (" << normalized << ")"
764
489893
                                   << endl;
765
489893
            if (normalized.isConst())
766
            {
767
25149
              changed = true;
768
25149
              typeConstSet.add(tb, normalized);
769
25149
              assignConstantRep(tm, *i, normalized);
770
25149
              assertedReps.erase(*i);
771
25149
              i2 = i;
772
25149
              ++i;
773
25149
              repSet->erase(i2);
774
            }
775
            else
776
            {
777
464744
              if (normalized != rep)
778
              {
779
7563
                assertedReps[*i] = normalized;
780
7563
                changed = true;
781
              }
782
464744
              ++i;
783
            }
784
          }
785
        }
786
      }
787
    } while (changed);
788
789
37182
    if (!unassignedAssignable)
790
    {
791
18942
      break;
792
    }
793
794
    // 3. Assign unassigned assignable EC's using type enumeration - assign a
795
    // value *different* from all other EC's if the type is infinite
796
    // Assign first value from type enumerator otherwise - for finite types, we
797
    // rely on polite framework to ensure that EC's that have to be
798
    // different are different.
799
800
    // Only make assignments on a type if:
801
    // 1. there are no terms that share the same base type with un-normalized
802
    // representatives
803
    // 2. there are no terms that share teh same base type that are unevaluated
804
    // evaluable terms
805
    // Alternatively, if 2 or 3 don't hold but we are in a special
806
    // deadlock-breaking mode where assignOne is true, go ahead and make one
807
    // assignment
808
18240
    changed = false;
809
    // must iterate over the ordered type list to ensure that we do not
810
    // enumerate values with subterms
811
    //  having types that we are currently enumerating (when possible)
812
    //  for example, this ensures we enumerate uninterpreted sort U before (List
813
    //  of U) and (Array U U)
814
    //  however, it does not break cyclic type dependencies for mutually
815
    //  recursive datatypes, but this is handled
816
    //  by recording all subterms of enumerated values in TypeSet::addSubTerms.
817
154307
    for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
818
    {
819
148617
      TypeNode t = *type_it;
820
      // continue if there are no more equivalence classes of this type to
821
      // assign
822
136067
      std::set<Node>* noRepSetPtr = typeNoRepSet.getSet(t);
823
136067
      if (noRepSetPtr == NULL)
824
      {
825
20517
        continue;
826
      }
827
115550
      set<Node>& noRepSet = *noRepSetPtr;
828
115550
      if (noRepSet.empty())
829
      {
830
89386
        continue;
831
      }
832
833
      // get properties of this type
834
26164
      bool isCorecursive = false;
835
26164
      if (t.isDatatype())
836
      {
837
21284
        const DType& dt = t.getDType();
838
42568
        isCorecursive = dt.isCodatatype()
839
63852
                        && (!dt.isFinite(t) || dt.isRecursiveSingleton(t));
840
      }
841
#ifdef CVC4_ASSERTIONS
842
26164
      bool isUSortFiniteRestricted = false;
843
26164
      if (options::finiteModelFind())
844
      {
845
23614
        isUSortFiniteRestricted = !t.isSort() && involvesUSort(t);
846
      }
847
#endif
848
849
38714
      TypeNode tb = t.getBaseType();
850
26164
      if (!assignOne)
851
      {
852
18283
        set<Node>* repSet = typeRepSet.getSet(tb);
853
18283
        if (repSet != NULL && !repSet->empty())
854
        {
855
13025
          continue;
856
        }
857
5258
        if (evaluableSet.find(tb) != evaluableSet.end())
858
        {
859
589
          continue;
860
        }
861
      }
862
25100
      Trace("model-builder") << "  Assign phase, working on type: " << t
863
12550
                             << endl;
864
      bool assignable, evaluable CVC4_UNUSED;
865
12550
      std::map<Node, Assigner>::iterator itAssigner;
866
12550
      std::map<Node, Node>::iterator itAssignerM;
867
12550
      set<Node>* repSet = typeRepSet.getSet(t);
868
28351
      for (i = noRepSet.begin(); i != noRepSet.end();)
869
      {
870
23672
        i2 = i;
871
23672
        ++i;
872
        // check whether it has an assigner object
873
23672
        itAssignerM = eqcToAssignerMaster.find(*i2);
874
23672
        if (itAssignerM != eqcToAssignerMaster.end())
875
        {
876
          // Take the master's assigner. Notice we don't care which order
877
          // equivalence classes are assigned. For instance, the master can
878
          // be assigned after one of its slaves.
879
35
          itAssigner = eqcToAssigner.find(itAssignerM->second);
880
        }
881
        else
882
        {
883
23637
          itAssigner = eqcToAssigner.find(*i2);
884
        }
885
23672
        if (itAssigner != eqcToAssigner.end())
886
        {
887
43
          assignable = isAssignerActive(tm, itAssigner->second);
888
        }
889
        else
890
        {
891
23629
          assignable = assignableEqc.find(*i2) != assignableEqc.end();
892
        }
893
23672
        evaluable = evaluableEqc.find(*i2) != evaluableEqc.end();
894
47344
        Trace("model-builder-debug")
895
23672
            << "    eqc " << *i2 << " is assignable=" << assignable
896
23672
            << ", evaluable=" << evaluable << std::endl;
897
23672
        if (assignable)
898
        {
899
23607
          Assert(!evaluable || assignOne);
900
          // this assertion ensures that if we are assigning to a term of
901
          // Boolean type, then the term must be assignable.
902
          // Note we only assign to terms of Boolean type if the term occurs in
903
          // a singleton equivalence class; otherwise the term would have been
904
          // in the equivalence class of true or false and would not need
905
          // assigning.
906
23607
          Assert(!t.isBoolean() || isAssignable(*i2));
907
39343
          Node n;
908
23607
          if (itAssigner != eqcToAssigner.end())
909
          {
910
86
            Trace("model-builder-debug")
911
43
                << "Get value from assigner for finite type..." << std::endl;
912
            // if it has an assigner, get the value from the assigner.
913
43
            n = itAssigner->second.getNextAssignment();
914
43
            Assert(!n.isNull());
915
          }
916
23564
          else if (t.isSort() || !t.isInterpretedFinite())
917
          {
918
            // If its interpreted as infinite, we get a fresh value that does
919
            // not occur in the model.
920
            // Note we also consider uninterpreted sorts to be infinite here
921
            // regardless of whether isInterpretedFinite is true (which is true
922
            // for uninterpreted sorts iff finite model finding is enabled).
923
            // This is required because the UF solver does not explicitly
924
            // assign uninterpreted constants to equivalence classes in its
925
            // collectModelValues method. Doing so would have the same effect
926
            // as running the code in this case.
927
            bool success;
928
8
            do
929
            {
930
46986
              Trace("model-builder-debug") << "Enumerate term of type " << t
931
23493
                                           << std::endl;
932
23493
              n = typeConstSet.nextTypeEnum(t, true);
933
              //--- AJR: this code checks whether n is a legal value
934
23493
              Assert(!n.isNull());
935
23493
              success = true;
936
46986
              Trace("model-builder-debug") << "Check if excluded : " << n
937
23493
                                           << std::endl;
938
#ifdef CVC4_ASSERTIONS
939
23493
              if (isUSortFiniteRestricted)
940
              {
941
                // must not involve uninterpreted constants beyond cardinality
942
                // bound (which assumed to coincide with #eqc)
943
                // this is just an assertion now, since TypeEnumeratorProperties
944
                // should ensure that only legal values are enumerated wrt this
945
                // constraint.
946
27042
                std::map<Node, bool> visited;
947
13521
                success = !isExcludedUSortValue(eqc_usort_count, n, visited);
948
13521
                if (!success)
949
                {
950
                  Trace("model-builder")
951
                      << "Excluded value for " << t << " : " << n
952
                      << " due to out of range uninterpreted constant."
953
                      << std::endl;
954
                }
955
13521
                Assert(success);
956
              }
957
#endif
958
23493
              if (success && isCorecursive)
959
              {
960
59
                if (repSet != NULL && !repSet->empty())
961
                {
962
                  // in the case of codatatypes, check if it is in the set of
963
                  // values that we cannot assign
964
51
                  success = !isExcludedCdtValue(n, repSet, assertedReps, *i2);
965
51
                  if (!success)
966
                  {
967
16
                    Trace("model-builder")
968
8
                        << "Excluded value : " << n
969
8
                        << " due to alpha-equivalent codatatype expression."
970
8
                        << std::endl;
971
                  }
972
                }
973
              }
974
              //---
975
23493
            } while (!success);
976
23485
            Assert(!n.isNull());
977
          }
978
          else
979
          {
980
158
            Trace("model-builder-debug")
981
79
                << "Get first value from finite type..." << std::endl;
982
            // Otherwise, we get the first value from the type enumerator.
983
158
            TypeEnumerator te(t);
984
79
            n = *te;
985
          }
986
23607
          Trace("model-builder-debug") << "...got " << n << std::endl;
987
23607
          assignConstantRep(tm, *i2, n);
988
23607
          changed = true;
989
23607
          noRepSet.erase(i2);
990
23607
          if (assignOne)
991
          {
992
7871
            assignOne = false;
993
7871
            break;
994
          }
995
        }
996
      }
997
    }
998
999
    // Corner case - I'm not sure this can even happen - but it's theoretically
1000
    // possible to have a cyclical dependency
1001
    // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}.  In
1002
    // this case, neither one will get assigned because we are waiting
1003
    // to be able to evaluate.  But we will never be able to evaluate because
1004
    // the variables that need to be assigned are in
1005
    // these same EC's.  In this case, repeat the whole fixed-point computation
1006
    // with the difference that the first EC
1007
    // that has both assignable and evaluable expressions will get assigned.
1008
18240
    if (!changed)
1009
    {
1010
7871
      Assert(!assignOne);  // check for infinite loop!
1011
7871
      assignOne = true;
1012
    }
1013
18240
  }
1014
1015
#ifdef CVC4_ASSERTIONS
1016
  // Assert that all representatives have been converted to constants
1017
32860
  for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it)
1018
  {
1019
13918
    set<Node>& repSet = TypeSet::getSet(it);
1020
13918
    if (!repSet.empty())
1021
    {
1022
      Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size()
1023
                             << ", first = " << *(repSet.begin()) << endl;
1024
      Assert(false);
1025
    }
1026
  }
1027
#endif /* CVC4_ASSERTIONS */
1028
1029
18942
  Trace("model-builder") << "Copy representatives to model..." << std::endl;
1030
18942
  tm->d_reps.clear();
1031
18942
  std::map<Node, Node>::iterator itMap;
1032
704045
  for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap)
1033
  {
1034
685103
    tm->d_reps[itMap->first] = itMap->second;
1035
685103
    tm->d_rep_set.add(itMap->second.getType(), itMap->second);
1036
  }
1037
1038
18942
  Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
1039
  // Make sure every EC has a rep
1040
18942
  for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap)
1041
  {
1042
    tm->d_reps[itMap->first] = itMap->second;
1043
    tm->d_rep_set.add(itMap->second.getType(), itMap->second);
1044
  }
1045
37251
  for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it)
1046
  {
1047
18309
    set<Node>& noRepSet = TypeSet::getSet(it);
1048
19502
    for (const Node& node : noRepSet)
1049
    {
1050
1193
      tm->d_reps[node] = node;
1051
1193
      tm->d_rep_set.add(node.getType(), node);
1052
    }
1053
  }
1054
1055
  // modelBuilder-specific initialization
1056
18942
  if (!processBuildModel(tm))
1057
  {
1058
    Trace("model-builder")
1059
        << "TheoryEngineModelBuilder: fail process build model." << std::endl;
1060
    return false;
1061
  }
1062
18942
  Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl;
1063
18942
  return true;
1064
}
1065
1066
948
void TheoryEngineModelBuilder::postProcessModel(bool incomplete, TheoryModel* m)
1067
{
1068
  // if we are incomplete, there is no guarantee on the model.
1069
  // thus, we do not check the model here.
1070
948
  if (incomplete)
1071
  {
1072
50
    return;
1073
  }
1074
898
  Assert(m != nullptr);
1075
  // debug-check the model if the checkModels() is enabled.
1076
898
  if (options::debugCheckModels())
1077
  {
1078
218
    debugCheckModel(m);
1079
  }
1080
}
1081
1082
218
void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
1083
{
1084
#ifdef CVC4_ASSERTIONS
1085
218
  if (tm->hasApproximations())
1086
  {
1087
    // models with approximations may fail the assertions below
1088
    return;
1089
  }
1090
218
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
1091
218
  std::map<Node, Node>::iterator itMap;
1092
  // Check that every term evaluates to its representative in the model
1093
4139
  for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
1094
4139
       !eqcs_i.isFinished();
1095
       ++eqcs_i)
1096
  {
1097
    // eqc is the equivalence class representative
1098
7842
    Node eqc = (*eqcs_i);
1099
    // get the representative
1100
7842
    Node rep = tm->getRepresentative(eqc);
1101
3921
    if (!rep.isConst() && eqc.getType().isBoolean())
1102
    {
1103
      // if Boolean, it does not necessarily have a constant representative, use
1104
      // get value instead
1105
      rep = tm->getValue(eqc);
1106
      Assert(rep.isConst());
1107
    }
1108
3921
    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
1109
31453
    for (; !eqc_i.isFinished(); ++eqc_i)
1110
    {
1111
27532
      Node n = *eqc_i;
1112
      static int repCheckInstance = 0;
1113
13766
      ++repCheckInstance;
1114
1115
      // non-linear mult is not necessarily accurate wrt getValue
1116
13766
      if (n.getKind() != kind::NONLINEAR_MULT)
1117
      {
1118
27502
        Debug("check-model::rep-checking") << "( " << repCheckInstance << ") "
1119
13751
                                           << "n: " << n << endl
1120
27502
                                           << "getValue(n): " << tm->getValue(n)
1121
13751
                                           << endl
1122
13751
                                           << "rep: " << rep << endl;
1123
13751
        Assert(tm->getValue(*eqc_i) == rep)
1124
            << "run with -d check-model::rep-checking for details";
1125
      }
1126
    }
1127
  }
1128
#endif /* CVC4_ASSERTIONS */
1129
1130
  // builder-specific debugging
1131
218
  debugModel(tm);
1132
}
1133
1134
840840
Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
1135
{
1136
840840
  std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
1137
840840
  if (itMap != d_constantReps.end())
1138
  {
1139
    return (*itMap).second;
1140
  }
1141
840840
  NodeMap::iterator it = d_normalizedCache.find(r);
1142
840840
  if (it != d_normalizedCache.end())
1143
  {
1144
22006
    return (*it).second;
1145
  }
1146
818834
  Trace("model-builder-debug") << "do normalize on " << r << std::endl;
1147
1637668
  Node retNode = r;
1148
818834
  if (r.getNumChildren() > 0)
1149
  {
1150
1625954
    std::vector<Node> children;
1151
812977
    if (r.getMetaKind() == kind::metakind::PARAMETERIZED)
1152
    {
1153
512158
      children.push_back(r.getOperator());
1154
    }
1155
812977
    bool childrenConst = true;
1156
2452227
    for (size_t i = 0; i < r.getNumChildren(); ++i)
1157
    {
1158
3278500
      Node ri = r[i];
1159
1639250
      bool recurse = true;
1160
1639250
      if (!ri.isConst())
1161
      {
1162
1151477
        if (m->d_equalityEngine->hasTerm(ri))
1163
        {
1164
1123285
          itMap =
1165
2246570
              d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
1166
1123285
          if (itMap != d_constantReps.end())
1167
          {
1168
459321
            ri = (*itMap).second;
1169
459321
            Trace("model-builder-debug") << i << ": const child " << ri << std::endl;
1170
459321
            recurse = false;
1171
          }
1172
663964
          else if (!evalOnly)
1173
          {
1174
608888
            recurse = false;
1175
608888
            Trace("model-builder-debug") << i << ": keep " << ri << std::endl;
1176
          }
1177
        }
1178
        else
1179
        {
1180
28192
          Trace("model-builder-debug") << i << ": no hasTerm " << ri << std::endl;
1181
        }
1182
1151477
        if (recurse)
1183
        {
1184
83268
          ri = normalize(m, ri, evalOnly);
1185
        }
1186
1151477
        if (!ri.isConst())
1187
        {
1188
615052
          childrenConst = false;
1189
        }
1190
      }
1191
1639250
      children.push_back(ri);
1192
    }
1193
812977
    retNode = NodeManager::currentNM()->mkNode(r.getKind(), children);
1194
812977
    if (childrenConst)
1195
    {
1196
342589
      retNode = Rewriter::rewrite(retNode);
1197
    }
1198
  }
1199
818834
  d_normalizedCache[r] = retNode;
1200
818834
  return retNode;
1201
}
1202
1203
17326
bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m)
1204
{
1205
17326
  return true;
1206
}
1207
1208
18942
bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m)
1209
{
1210
18942
  if (m->areFunctionValuesEnabled())
1211
  {
1212
18942
    assignFunctions(m);
1213
  }
1214
18942
  return true;
1215
}
1216
1217
4785
void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
1218
{
1219
4785
  Assert(!options::ufHo());
1220
9570
  uf::UfModelTree ufmt(f);
1221
9570
  Node default_v;
1222
27963
  for (size_t i = 0; i < m->d_uf_terms[f].size(); i++)
1223
  {
1224
46356
    Node un = m->d_uf_terms[f][i];
1225
46356
    vector<TNode> children;
1226
23178
    children.push_back(f);
1227
23178
    Trace("model-builder-debug") << "  process term : " << un << std::endl;
1228
96401
    for (size_t j = 0; j < un.getNumChildren(); ++j)
1229
    {
1230
146446
      Node rc = m->getRepresentative(un[j]);
1231
146446
      Trace("model-builder-debug2") << "    get rep : " << un[j] << " returned "
1232
73223
                                    << rc << std::endl;
1233
73223
      Assert(rc.isConst());
1234
73223
      children.push_back(rc);
1235
    }
1236
46356
    Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
1237
46356
    Node v = m->getRepresentative(un);
1238
46356
    Trace("model-builder") << "  Setting (" << simp << ") to (" << v << ")"
1239
23178
                           << endl;
1240
23178
    ufmt.setValue(m, simp, v);
1241
23178
    default_v = v;
1242
  }
1243
4785
  if (default_v.isNull())
1244
  {
1245
    // choose default value from model if none exists
1246
    TypeEnumerator te(f.getType().getRangeType());
1247
    default_v = (*te);
1248
  }
1249
4785
  ufmt.setDefaultValue(m, default_v);
1250
4785
  bool condenseFuncValues = options::condenseFunctionValues();
1251
4785
  if (condenseFuncValues)
1252
  {
1253
4785
    ufmt.simplify();
1254
  }
1255
9570
  std::stringstream ss;
1256
4785
  ss << "_arg_";
1257
9570
  Node val = ufmt.getFunctionValue(ss.str().c_str(), condenseFuncValues);
1258
4785
  m->assignFunctionDefinition(f, val);
1259
  // ufmt.debugPrint( std::cout, m );
1260
4785
}
1261
1262
1147
void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
1263
{
1264
1147
  Assert(options::ufHo());
1265
2294
  TypeNode type = f.getType();
1266
2294
  std::vector<TypeNode> argTypes = type.getArgTypes();
1267
2294
  std::vector<Node> args;
1268
2294
  std::vector<TNode> apply_args;
1269
2386
  for (unsigned i = 0; i < argTypes.size(); i++)
1270
  {
1271
2478
    Node v = NodeManager::currentNM()->mkBoundVar(argTypes[i]);
1272
1239
    args.push_back(v);
1273
1239
    if (i > 0)
1274
    {
1275
92
      apply_args.push_back(v);
1276
    }
1277
  }
1278
  // start with the base return value (currently we use the same default value
1279
  // for all functions)
1280
2294
  TypeEnumerator te(type.getRangeType());
1281
2294
  Node curr = (*te);
1282
1147
  std::map<Node, std::vector<Node> >::iterator itht = m->d_ho_uf_terms.find(f);
1283
1147
  if (itht != m->d_ho_uf_terms.end())
1284
  {
1285
3516
    for (size_t i = 0; i < itht->second.size(); i++)
1286
    {
1287
4738
      Node hn = itht->second[i];
1288
2369
      Trace("model-builder-debug") << "    process : " << hn << std::endl;
1289
2369
      Assert(hn.getKind() == kind::HO_APPLY);
1290
2369
      Assert(m->areEqual(hn[0], f));
1291
4738
      Node hni = m->getRepresentative(hn[1]);
1292
4738
      Trace("model-builder-debug2") << "      get rep : " << hn[0]
1293
2369
                                    << " returned " << hni << std::endl;
1294
2369
      Assert(hni.isConst());
1295
2369
      Assert(hni.getType().isSubtypeOf(args[0].getType()));
1296
2369
      hni = Rewriter::rewrite(args[0].eqNode(hni));
1297
4738
      Node hnv = m->getRepresentative(hn);
1298
4738
      Trace("model-builder-debug2") << "      get rep val : " << hn
1299
2369
                                    << " returned " << hnv << std::endl;
1300
2369
      Assert(hnv.isConst());
1301
2369
      if (!apply_args.empty())
1302
      {
1303
197
        Assert(hnv.getKind() == kind::LAMBDA
1304
               && hnv[0].getNumChildren() + 1 == args.size());
1305
394
        std::vector<TNode> largs;
1306
422
        for (unsigned j = 0; j < hnv[0].getNumChildren(); j++)
1307
        {
1308
225
          largs.push_back(hnv[0][j]);
1309
        }
1310
197
        Assert(largs.size() == apply_args.size());
1311
197
        hnv = hnv[1].substitute(
1312
            largs.begin(), largs.end(), apply_args.begin(), apply_args.end());
1313
197
        hnv = Rewriter::rewrite(hnv);
1314
      }
1315
2369
      Assert(!TypeNode::leastCommonTypeNode(hnv.getType(), curr.getType())
1316
                  .isNull());
1317
2369
      curr = NodeManager::currentNM()->mkNode(kind::ITE, hni, hnv, curr);
1318
    }
1319
  }
1320
  Node val = NodeManager::currentNM()->mkNode(
1321
      kind::LAMBDA,
1322
2294
      NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args),
1323
4588
      curr);
1324
1147
  m->assignFunctionDefinition(f, val);
1325
1147
}
1326
1327
// This struct is used to sort terms by the "size" of their type
1328
//   The size of the type is the number of nodes in the type, for example
1329
//  size of Int is 1
1330
//  size of Function( Int, Int ) is 3
1331
//  size of Function( Function( Bool, Int ), Int ) is 5
1332
10354
struct sortTypeSize
1333
{
1334
  // stores the size of the type
1335
  std::map<TypeNode, unsigned> d_type_size;
1336
  // get the size of type tn
1337
6085
  unsigned getTypeSize(TypeNode tn)
1338
  {
1339
6085
    std::map<TypeNode, unsigned>::iterator it = d_type_size.find(tn);
1340
6085
    if (it != d_type_size.end())
1341
    {
1342
4729
      return it->second;
1343
    }
1344
    else
1345
    {
1346
1356
      unsigned sum = 1;
1347
3065
      for (unsigned i = 0; i < tn.getNumChildren(); i++)
1348
      {
1349
1709
        sum += getTypeSize(tn[i]);
1350
      }
1351
1356
      d_type_size[tn] = sum;
1352
1356
      return sum;
1353
    }
1354
  }
1355
1356
 public:
1357
  // compares the type size of i and j
1358
  // returns true iff the size of i is less than that of j
1359
  // tiebreaks are determined by node value
1360
2188
  bool operator()(Node i, Node j)
1361
  {
1362
2188
    int si = getTypeSize(i.getType());
1363
2188
    int sj = getTypeSize(j.getType());
1364
2188
    if (si < sj)
1365
    {
1366
234
      return true;
1367
    }
1368
1954
    else if (si == sj)
1369
    {
1370
1840
      return i < j;
1371
    }
1372
    else
1373
    {
1374
114
      return false;
1375
    }
1376
  }
1377
};
1378
1379
18942
void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
1380
{
1381
18942
  if (!options::assignFunctionValues())
1382
  {
1383
    return;
1384
  }
1385
18942
  Trace("model-builder") << "Assigning function values..." << std::endl;
1386
37884
  std::vector<Node> funcs_to_assign = m->getFunctionsToAssign();
1387
1388
18942
  if (options::ufHo())
1389
  {
1390
    // sort based on type size if higher-order
1391
504
    Trace("model-builder") << "Sort functions by type..." << std::endl;
1392
1008
    sortTypeSize sts;
1393
504
    std::sort(funcs_to_assign.begin(), funcs_to_assign.end(), sts);
1394
  }
1395
1396
18942
  if (Trace.isOn("model-builder"))
1397
  {
1398
    Trace("model-builder") << "...have " << funcs_to_assign.size()
1399
                           << " functions to assign:" << std::endl;
1400
    for (unsigned k = 0; k < funcs_to_assign.size(); k++)
1401
    {
1402
      Node f = funcs_to_assign[k];
1403
      Trace("model-builder") << "  [" << k << "] : " << f << " : "
1404
                             << f.getType() << std::endl;
1405
    }
1406
  }
1407
1408
  // construct function values
1409
24874
  for (unsigned k = 0; k < funcs_to_assign.size(); k++)
1410
  {
1411
11864
    Node f = funcs_to_assign[k];
1412
5932
    Trace("model-builder") << "  Function #" << k << " is " << f << std::endl;
1413
    // std::map< Node, std::vector< Node > >::iterator itht =
1414
    // m->d_ho_uf_terms.find( f );
1415
5932
    if (!options::ufHo())
1416
    {
1417
9570
      Trace("model-builder") << "  Assign function value for " << f
1418
4785
                             << " based on APPLY_UF" << std::endl;
1419
4785
      assignFunction(m, f);
1420
    }
1421
    else
1422
    {
1423
2294
      Trace("model-builder") << "  Assign function value for " << f
1424
1147
                             << " based on curried HO_APPLY" << std::endl;
1425
1147
      assignHoFunction(m, f);
1426
    }
1427
  }
1428
18942
  Trace("model-builder") << "Finished assigning function values." << std::endl;
1429
}
1430
1431
} /* namespace CVC4::theory */
1432
26676
} /* namespace CVC4 */