Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Clark Barrett, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of theory model buidler class.
14 : : */
15 : : #include "theory/theory_model_builder.h"
16 : :
17 : : #include "expr/dtype.h"
18 : : #include "expr/dtype_cons.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "expr/sort_to_term.h"
21 : : #include "expr/sort_type_size.h"
22 : : #include "options/quantifiers_options.h"
23 : : #include "options/smt_options.h"
24 : : #include "options/strings_options.h"
25 : : #include "options/theory_options.h"
26 : : #include "options/uf_options.h"
27 : : #include "smt/env.h"
28 : : #include "theory/rewriter.h"
29 : : #include "theory/uf/function_const.h"
30 : : #include "theory/uf/theory_uf_model.h"
31 : : #include "util/uninterpreted_sort_value.h"
32 : :
33 : : using namespace std;
34 : : using namespace cvc5::internal::kind;
35 : : using namespace cvc5::context;
36 : :
37 : : namespace cvc5::internal {
38 : : namespace theory {
39 : :
40 : 57151 : TheoryEngineModelBuilder::TheoryEngineModelBuilder(Env& env) : EnvObj(env) {}
41 : :
42 : 12 : void TheoryEngineModelBuilder::Assigner::initialize(
43 : : TypeNode tn, TypeEnumeratorProperties* tep, const std::vector<Node>& aes)
44 : : {
45 : 12 : d_te.reset(new TypeEnumerator(tn, tep));
46 : 12 : d_assignExcSet.insert(d_assignExcSet.end(), aes.begin(), aes.end());
47 : 12 : }
48 : :
49 : 47 : Node TheoryEngineModelBuilder::Assigner::getNextAssignment()
50 : : {
51 [ - + ][ - + ]: 47 : Assert(d_te != nullptr);
[ - - ]
52 : 94 : Node n;
53 : 47 : bool success = false;
54 : 47 : TypeEnumerator& te = *d_te;
55 : : // Check if we have run out of elements. This should never happen; if it
56 : : // does we assert false and return null.
57 [ - + ]: 47 : if (te.isFinished())
58 : : {
59 : 0 : Assert(false);
60 : : return Node::null();
61 : : }
62 : : // must increment until we find one that is not in the assignment
63 : : // exclusion set
64 : 10 : do
65 : : {
66 : 57 : n = *te;
67 : 57 : success = std::find(d_assignExcSet.begin(), d_assignExcSet.end(), n)
68 : 114 : == d_assignExcSet.end();
69 : : // increment regardless of fail or succeed, to set up the next value
70 : 57 : ++te;
71 [ + + ]: 57 : } while (!success);
72 : 47 : return n;
73 : : }
74 : :
75 : 411495 : Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
76 : : {
77 : 411495 : eq::EqClassIterator eqc_i = eq::EqClassIterator(r, m->d_equalityEngine);
78 [ + + ]: 427524 : for (; !eqc_i.isFinished(); ++eqc_i)
79 : : {
80 : 414796 : Node n = *eqc_i;
81 [ + - ]: 414796 : Trace("model-builder-debug") << "Look at term : " << n << std::endl;
82 [ + + ]: 414796 : if (!isAssignable(n))
83 : : {
84 [ + - ]: 413658 : Trace("model-builder-debug") << "...try to normalize" << std::endl;
85 : 413658 : Node normalized = normalize(m, n, true);
86 [ + - ]: 827316 : Trace("model-builder-debug")
87 : 0 : << "...return " << normalized
88 [ - + ][ - - ]: 413658 : << ", isValue=" << m->isValue(normalized) << std::endl;
89 [ + + ]: 413658 : if (m->isValue(normalized))
90 : : {
91 : 398767 : return normalized;
92 : : }
93 : : }
94 : : }
95 : 12728 : return Node::null();
96 : : }
97 : :
98 : 47 : bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
99 : : {
100 [ + + ]: 47 : if (a.d_isActive)
101 : : {
102 : 35 : return true;
103 : : }
104 : 12 : std::vector<Node>& eset = a.d_assignExcSet;
105 : 12 : std::map<Node, Node>::iterator it;
106 [ + + ]: 34 : for (unsigned i = 0, size = eset.size(); i < size; i++)
107 : : {
108 : : // Members of exclusion set must have values, otherwise we are not yet
109 : : // assignable.
110 : 22 : Node er = eset[i];
111 [ + + ]: 22 : if (tm->isValue(er))
112 : : {
113 : : // already processed
114 : 16 : continue;
115 : : }
116 : : // Assignable members of assignment exclusion set should be representatives
117 : : // of their equivalence classes. This ensures we look up the constant
118 : : // representatives for assignable members of assignment exclusion sets.
119 [ - + ][ - + ]: 6 : Assert(er == tm->getRepresentative(er));
[ - - ]
120 : 6 : it = d_constantReps.find(er);
121 [ - + ]: 6 : if (it == d_constantReps.end())
122 : : {
123 [ - - ]: 0 : Trace("model-build-aes")
124 : 0 : << "isAssignerActive: not active due to " << er << std::endl;
125 : 0 : return false;
126 : : }
127 : : // update
128 : 6 : eset[i] = it->second;
129 : : }
130 [ + - ]: 12 : Trace("model-build-aes") << "isAssignerActive: active!" << std::endl;
131 : 12 : a.d_isActive = true;
132 : 12 : return true;
133 : : }
134 : :
135 : 5260420 : bool TheoryEngineModelBuilder::isAssignable(TNode n)
136 : : {
137 : 5260420 : Kind k = n.getKind();
138 [ + + ][ + + ]: 5260420 : if (k == Kind::SELECT || k == Kind::APPLY_SELECTOR
139 [ + + ]: 4790810 : || k == Kind::SEQ_NTH)
140 : : {
141 : : // selectors are always assignable (where we guarantee that they are not
142 : : // evaluatable here)
143 [ + + ]: 470375 : if (!logicInfo().isHigherOrder())
144 : : {
145 [ - + ][ - + ]: 468841 : Assert(!n.getType().isFunction());
[ - - ]
146 : 468841 : return true;
147 : : }
148 : : else
149 : : {
150 : : // might be a function field
151 : 1534 : return !n.getType().isFunction();
152 : : }
153 : : }
154 [ + + ][ + + ]: 4790050 : else if (k == Kind::FLOATINGPOINT_COMPONENT_SIGN || k==Kind::SEP_NIL)
155 : : {
156 : : // - Extracting the sign of a floating-point number acts similar to a
157 : : // selector on a datatype, i.e. if `(sign x)` wasn't assigned a value, we
158 : : // can pick an arbitrary one. Note that the other components of a
159 : : // floating-point number should always be assigned a value.
160 : : // - sep.nil is a nullary constant that acts like a variable and thus is
161 : : // assignable.
162 : 2724 : return true;
163 : : }
164 : : else
165 : : {
166 : : // non-function variables, and fully applied functions
167 [ + + ]: 4787320 : if (!logicInfo().isHigherOrder())
168 : : {
169 : : // no functions exist, all functions are fully applied
170 [ - + ][ - + ]: 4642830 : Assert(k != Kind::HO_APPLY);
[ - - ]
171 [ - + ][ - + ]: 4642830 : Assert(!n.getType().isFunction());
[ - - ]
172 [ + + ][ + + ]: 4642830 : return n.isVar() || k == Kind::APPLY_UF;
173 : : }
174 : : else
175 : : {
176 [ + + ][ - - ]: 182435 : return (n.isVar() && !n.getType().isFunction())
177 [ + + ]: 114418 : || k == Kind::APPLY_UF
178 [ + + ][ + + ]: 330707 : || (k == Kind::HO_APPLY
179 : 186217 : && n[0].getType().getNumChildren() == 2);
180 : : }
181 : : }
182 : : }
183 : :
184 : 6623050 : void TheoryEngineModelBuilder::addAssignableSubterms(TNode n,
185 : : TheoryModel* tm,
186 : : NodeSet& cache)
187 : : {
188 [ + + ]: 6623050 : if (n.isClosure())
189 : : {
190 : 52608 : return;
191 : : }
192 [ + + ]: 6570440 : if (cache.find(n) != cache.end())
193 : : {
194 : 4141520 : return;
195 : : }
196 [ + + ]: 2428910 : if (isAssignable(n))
197 : : {
198 : 975846 : tm->d_equalityEngine->addTerm(n);
199 : : }
200 [ + + ]: 6635300 : for (TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it)
201 : : {
202 : 4206390 : addAssignableSubterms(*child_it, tm, cache);
203 : : }
204 : 2428910 : cache.insert(n);
205 : : }
206 : :
207 : 1162660 : void TheoryEngineModelBuilder::assignConstantRep(TheoryModel* tm,
208 : : Node eqc,
209 : : Node constRep)
210 : : {
211 : 1162660 : d_constantReps[eqc] = constRep;
212 [ + - ]: 2325320 : Trace("model-builder") << " Assign: Setting constant rep of " << eqc
213 : 1162660 : << " to " << constRep << endl;
214 : 1162660 : tm->d_rep_set.setTermForRepresentative(constRep, eqc);
215 : 1162660 : }
216 : :
217 : 48 : bool TheoryEngineModelBuilder::isExcludedCdtValue(
218 : : Node val,
219 : : std::set<Node>* repSet,
220 : : std::map<Node, Node>& assertedReps,
221 : : Node eqc)
222 : : {
223 [ + - ]: 96 : Trace("model-builder-debug")
224 : 0 : << "Is " << val << " and excluded codatatype value for " << eqc << "? "
225 : 48 : << std::endl;
226 [ + + ]: 98 : for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i)
227 : : {
228 [ - + ][ - + ]: 68 : Assert(assertedReps.find(*i) != assertedReps.end());
[ - - ]
229 : 68 : Node rep = assertedReps[*i];
230 [ + - ]: 68 : Trace("model-builder-debug") << " Rep : " << rep << std::endl;
231 : : // check whether it is possible that rep will be assigned the same value
232 : : // as val.
233 [ + + ]: 68 : if (isCdtValueMatch(val, rep))
234 : : {
235 : 18 : return true;
236 : : }
237 : : }
238 : 30 : return false;
239 : : }
240 : :
241 : 173 : bool TheoryEngineModelBuilder::isCdtValueMatch(Node v, Node r)
242 : : {
243 [ + + ]: 173 : if (r == v)
244 : : {
245 : : // values equal match trivially
246 : 45 : return true;
247 : : }
248 [ + - ][ + + ]: 128 : else if (v.isConst() && r.isConst())
[ + + ]
249 : : {
250 : : // distinct constant values do not match
251 : 10 : return false;
252 : : }
253 [ + + ]: 118 : else if (r.getKind() == Kind::APPLY_CONSTRUCTOR)
254 : : {
255 [ + + ]: 69 : if (v.getKind() != Kind::APPLY_CONSTRUCTOR)
256 : : {
257 [ - + ][ - + ]: 1 : Assert(v.getKind() == Kind::CODATATYPE_BOUND_VARIABLE);
[ - - ]
258 : : // v is the position of a loop. It may be possible to match, we return
259 : : // true, which is an over-approximation of when it is unsafe to use v.
260 : 1 : return true;
261 : : }
262 [ + + ]: 68 : if (v.getOperator() == r.getOperator())
263 : : {
264 [ + + ]: 123 : for (size_t i = 0, nchild = v.getNumChildren(); i < nchild; i++)
265 : : {
266 [ + + ]: 105 : if (!isCdtValueMatch(v[i], r[i]))
267 : : {
268 : : // if one child fails to match, we cannot match
269 : 42 : return false;
270 : : }
271 : : }
272 : 18 : return true;
273 : : }
274 : : // operators do not match
275 : 8 : return false;
276 : : }
277 [ + + ]: 49 : else if (v.getKind() == Kind::APPLY_CONSTRUCTOR)
278 : : {
279 : : // v has a constructor in a position that we have yet to fill in r.
280 : : // we are either a finite type in which case this subfield of r can be
281 : : // assigned a default value (or otherwise would have been split on).
282 : : // otherwise we are an infinite type and the subfield of r will be
283 : : // chosen not to clash with the subfield of v.
284 : 32 : return false;
285 : : }
286 : 17 : return true;
287 : : }
288 : :
289 : 7782 : bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) const
290 : : {
291 [ + + ]: 7782 : if (tn.isUninterpretedSort())
292 : : {
293 : 5 : return true;
294 : : }
295 [ + + ]: 7777 : else if (tn.isArray())
296 : : {
297 [ - - ]: 23 : return involvesUSort(tn.getArrayIndexType())
298 [ + - ][ + + ]: 23 : || involvesUSort(tn.getArrayConstituentType());
[ + - ][ + - ]
[ - - ]
299 : : }
300 [ + + ]: 7754 : else if (tn.isSet())
301 : : {
302 : 4 : return involvesUSort(tn.getSetElementType());
303 : : }
304 [ + + ]: 7750 : else if (tn.isDatatype())
305 : : {
306 : 7402 : const DType& dt = tn.getDType();
307 : 7402 : return dt.involvesUninterpretedType();
308 : : }
309 : : else
310 : : {
311 : 348 : return false;
312 : : }
313 : : }
314 : :
315 : 16498 : bool TheoryEngineModelBuilder::isExcludedUSortValue(
316 : : std::map<TypeNode, unsigned>& eqc_usort_count,
317 : : Node v,
318 : : std::map<Node, bool>& visited)
319 : : {
320 [ - + ][ - + ]: 16498 : Assert(v.isConst());
[ - - ]
321 [ + + ]: 16498 : if (visited.find(v) == visited.end())
322 : : {
323 : 12805 : visited[v] = true;
324 : 12805 : TypeNode tn = v.getType();
325 [ + + ]: 12805 : if (tn.isUninterpretedSort())
326 : : {
327 [ + - ]: 336 : Trace("model-builder-debug") << "Is excluded usort value : " << v << " "
328 : 168 : << tn << std::endl;
329 : 168 : unsigned card = eqc_usort_count[tn];
330 [ + - ]: 168 : Trace("model-builder-debug") << " Cardinality is " << card << std::endl;
331 : : unsigned index =
332 : 168 : v.getConst<UninterpretedSortValue>().getIndex().toUnsignedInt();
333 [ + - ]: 168 : Trace("model-builder-debug") << " Index is " << index << std::endl;
334 [ - + ][ - - ]: 168 : return index > 0 && index >= card;
335 : : }
336 [ + + ]: 25879 : for (unsigned i = 0; i < v.getNumChildren(); i++)
337 : : {
338 [ - + ]: 13242 : if (isExcludedUSortValue(eqc_usort_count, v[i], visited))
339 : : {
340 : 0 : return true;
341 : : }
342 : : }
343 : : }
344 : 16330 : return false;
345 : : }
346 : :
347 : 700403 : void TheoryEngineModelBuilder::addToTypeList(
348 : : TypeNode tn,
349 : : std::vector<TypeNode>& type_list,
350 : : std::unordered_set<TypeNode>& visiting)
351 : : {
352 [ + + ]: 700403 : if (std::find(type_list.begin(), type_list.end(), tn) == type_list.end())
353 : : {
354 [ + + ]: 158787 : if (visiting.find(tn) == visiting.end())
355 : : {
356 : 51852 : visiting.insert(tn);
357 : : /* This must make a recursive call on all types that are subterms of
358 : : * values of the current type.
359 : : * Note that recursive traversal here is over enumerated expressions
360 : : * (very low expression depth). */
361 [ + + ]: 51852 : if (tn.isArray())
362 : : {
363 : 461 : addToTypeList(tn.getArrayIndexType(), type_list, visiting);
364 : 461 : addToTypeList(tn.getArrayConstituentType(), type_list, visiting);
365 : : }
366 [ + + ]: 51391 : else if (tn.isSet())
367 : : {
368 : 1335 : addToTypeList(tn.getSetElementType(), type_list, visiting);
369 : : }
370 [ + + ]: 50056 : else if (tn.isDatatype())
371 : : {
372 : 22633 : const DType& dt = tn.getDType();
373 [ + + ]: 148116 : for (unsigned i = 0; i < dt.getNumConstructors(); i++)
374 : : {
375 [ + + ]: 257543 : for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
376 : : {
377 : 132060 : TypeNode ctn = dt[i][j].getRangeType();
378 : 132060 : addToTypeList(ctn, type_list, visiting);
379 : : }
380 : : }
381 : : }
382 [ - + ][ - + ]: 51852 : Assert(std::find(type_list.begin(), type_list.end(), tn)
[ - - ]
383 : : == type_list.end());
384 : 51852 : type_list.push_back(tn);
385 : : }
386 : : }
387 : 700403 : }
388 : :
389 : 35036 : bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
390 : : {
391 [ + - ]: 35036 : Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
392 : :
393 [ + - ]: 70072 : Trace("model-builder")
394 : 35036 : << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl;
395 : : // model-builder specific initialization
396 [ - + ]: 35036 : if (!preProcessBuildModel(tm))
397 : : {
398 [ - - ]: 0 : Trace("model-builder")
399 : 0 : << "TheoryEngineModelBuilder: fail preprocess build model."
400 : 0 : << std::endl;
401 : 0 : return false;
402 : : }
403 : :
404 [ + - ]: 70072 : Trace("model-builder")
405 : : << "TheoryEngineModelBuilder: Add assignable subterms "
406 : 0 : ", collect representatives and compute assignable information..."
407 : 35036 : << std::endl;
408 : :
409 : : // type enumerator properties
410 : 35036 : bool tepFixUSortCard = options().quantifiers.finiteModelFind;
411 : 35036 : uint32_t tepStrAlphaCard = options().strings.stringsAlphaCard;
412 : 70072 : TypeEnumeratorProperties tep(tepFixUSortCard, tepStrAlphaCard);
413 : :
414 : : // In the first step of model building, we do a traversal of the
415 : : // equality engine and record the information in the following:
416 : :
417 : : // The constant representatives, per equivalence class
418 : 35036 : d_constantReps.clear();
419 : : // The representatives that have been asserted by theories. This includes
420 : : // non-constant "skeletons" that have been specified by parametric theories.
421 : 70072 : std::map<Node, Node> assertedReps;
422 : : // A parition of the set of equivalence classes that have:
423 : : // (1) constant representatives,
424 : : // (2) an assigned representative specified by a theory in collectModelInfo,
425 : : // (3) no assigned representative.
426 : 70072 : TypeSet typeConstSet, typeRepSet, typeNoRepSet;
427 : : // An ordered list of types, such that T1 comes before T2 if T1 is a
428 : : // "component type" of T2, e.g. U comes before (Set U). This is only strictly
429 : : // necessary for finite model finding + parametric types instantiated with
430 : : // uninterpreted sorts, but is probably a good idea to do in general since it
431 : : // leads to models with smaller term sizes. -AJR
432 : 70072 : std::vector<TypeNode> type_list;
433 : : // The count of equivalence classes per sort (for finite model finding).
434 : 70072 : std::map<TypeNode, unsigned> eqc_usort_count;
435 : :
436 : : // the set of equivalence classes that are "assignable", i.e. those that have
437 : : // an assignable expression in them (see isAssignable), and have not already
438 : : // been assigned a constant.
439 : 70072 : std::unordered_set<Node> assignableEqc;
440 : : // The set of equivalence classes that are "evaluable", i.e. those that have
441 : : // an expression in them that is not assignable, and have not already been
442 : : // assigned a constant.
443 : 70072 : std::unordered_set<Node> evaluableEqc;
444 : : // Assigner objects for relevant equivalence classes that require special
445 : : // ways of assigning values, e.g. those that take into account assignment
446 : : // exclusion sets.
447 : 70072 : std::map<Node, Assigner> eqcToAssigner;
448 : : // A map from equivalence classes to the equivalence class that it shares an
449 : : // assigner object with (all elements in the range of this map are in the
450 : : // domain of eqcToAssigner).
451 : 70072 : std::map<Node, Node> eqcToAssignerMaster;
452 : :
453 : : // Loop through equivalence classes of the equality engine of the model.
454 : 35036 : eq::EqualityEngine* ee = tm->d_equalityEngine;
455 : 70072 : NodeSet assignableCache;
456 : 35036 : std::map<Node, Node>::iterator itm;
457 : 35036 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
458 : : // should we compute assigner objects?
459 : 35036 : bool computeAssigners = tm->hasAssignmentExclusionSets();
460 : : // the set of exclusion sets we have processed
461 : 70072 : std::unordered_set<Node> processedExcSet;
462 [ + + ]: 1199990 : for (; !eqcs_i.isFinished(); ++eqcs_i)
463 : : {
464 : 1164960 : Node eqc = *eqcs_i;
465 [ + - ]: 1164960 : Trace("model-builder") << " Processing EQC " << eqc << std::endl;
466 : : // Information computed for each equivalence class
467 : :
468 : : // The assigned represenative and constant representative
469 : 1164960 : Node rep, constRep;
470 : : // is constant rep a "base model value" (see TheoryModel::isBaseModelValue)
471 : 1164960 : bool constRepBaseModelValue = false;
472 : : // A flag set to true if the current equivalence class is assignable (see
473 : : // assignableEqc).
474 : 1164960 : bool assignable = false;
475 : : // Set to true if the current equivalence class is evaluatable (see
476 : : // evaluableEqc).
477 : 1164960 : bool evaluable = false;
478 : : // Set to true if a term in the current equivalence class has been given an
479 : : // assignment exclusion set.
480 : 1164960 : bool hasESet CVC5_UNUSED = false;
481 : : // Set to true if we found that a term in the current equivalence class has
482 : : // been given an assignment exclusion set, and we have not seen this term
483 : : // as part of a previous assignment exclusion group. In other words, when
484 : : // this flag is true we construct a new assigner object with the current
485 : : // equivalence class as its master.
486 : 1164960 : bool foundESet = false;
487 : : // The assignment exclusion set for the current equivalence class.
488 : 1164960 : std::vector<Node> eset;
489 : : // The group to which this equivalence class belongs when exclusion sets
490 : : // were assigned (see the argument group of
491 : : // TheoryModel::getAssignmentExclusionSet).
492 : 1164960 : std::vector<Node> esetGroup;
493 : :
494 : : // Loop through terms in this EC
495 : 1164960 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
496 [ + + ]: 3581610 : for (; !eqc_i.isFinished(); ++eqc_i)
497 : : {
498 : 2416660 : Node n = *eqc_i;
499 [ + - ]: 2416660 : Trace("model-builder") << " Processing Term: " << n << endl;
500 : :
501 : : // For each term n in this equivalence class, below we register its
502 : : // assignable subterms, compute whether it is a constant or assigned
503 : : // representative, then if we don't have a constant representative,
504 : : // compute information regarding how we will assign values.
505 : :
506 : : // (1) Add assignable subterms, which ensures that e.g. models for
507 : : // uninterpreted functions take into account all subterms in the
508 : : // equality engine of the model
509 : 2416660 : addAssignableSubterms(n, tm, assignableCache);
510 : : // model-specific processing of the term
511 : 2416660 : tm->addTermInternal(n);
512 : :
513 : : // compute whether n is assignable
514 [ + + ]: 2416660 : if (!isAssignable(n))
515 : : {
516 : : // (2) Record constant representative or assign representative, if
517 : : // applicable. We check if n is a value here, e.g. a term for which
518 : : // isConst returns true, or a lambda. The latter is required only for
519 : : // higher-order.
520 [ + + ]: 1440810 : if (tm->isValue(n))
521 : : {
522 : : // In some cases, there can be multiple terms in the same equivalence
523 : : // class are considered values, e.g., when real algebraic numbers did
524 : : // not simplify to rational values or real.pi was used as a model
525 : : // value. We distinguish three kinds of model values: constants,
526 : : // non-constant base values and non-base values, and we use them in
527 : : // this order of preference.
528 : : // We print a trace message if there is more than one model value in
529 : : // the same equivalence class. We throw a debug failure if there are
530 : : // at least two base model values in the same equivalence class that
531 : : // do not compare equal.
532 : 598880 : bool assignConstRep = false;
533 : 598880 : bool isBaseValue = tm->isBaseModelValue(n);
534 [ + + ]: 598880 : if (constRep.isNull())
535 : : {
536 : 598871 : assignConstRep = true;
537 : : }
538 : : else
539 : : {
540 : : // This is currently a trace message, as it often triggers for
541 : : // non-linear arithmetic before the model is refined enough to
542 : : // e.g. show transcendental function apps are not equal to rationals
543 [ + - ]: 18 : Trace("model-warn") << "Model values in the same equivalence class "
544 : 9 : << constRep << " " << n << std::endl;
545 [ - + ]: 9 : if (!constRepBaseModelValue)
546 : : {
547 : 0 : assignConstRep = isBaseValue;
548 : : }
549 [ + + ]: 9 : else if (isBaseValue)
550 : : {
551 : 3 : Node isEqual = rewrite(constRep.eqNode(n));
552 [ + - ][ + - ]: 1 : if (isEqual.isConst() && isEqual.getConst<bool>())
[ + - ]
553 : : {
554 : 1 : assignConstRep = n.isConst();
555 : : }
556 : : else
557 : : {
558 : 0 : Assert(false) << "Distinct base model values in the same "
559 : 0 : "equivalence class "
560 : 0 : << constRep << " " << n << std::endl;
561 : : }
562 : : }
563 : : }
564 [ + + ]: 598880 : if (assignConstRep)
565 : : {
566 : 598871 : constRep = n;
567 [ + - ]: 1197740 : Trace("model-builder") << " ..ConstRep( " << eqc
568 : 598871 : << " ) = " << constRep << std::endl;
569 : 598871 : constRepBaseModelValue = isBaseValue;
570 : : }
571 : : // if we have a constant representative, nothing else matters
572 : 598880 : continue;
573 : : }
574 : :
575 : : // If we don't have a constant rep, check if this is an assigned rep.
576 : 841931 : itm = tm->d_reps.find(n);
577 [ + + ]: 841931 : if (itm != tm->d_reps.end())
578 : : {
579 : : // Notice that this equivalence class may contain multiple terms that
580 : : // were specified as being a representative, since e.g. datatypes may
581 : : // assert representative for two constructor terms that are not in the
582 : : // care graph and are merged during collectModeInfo due to equality
583 : : // information from another theory. We overwrite the value of rep in
584 : : // these cases here.
585 : 75007 : rep = itm->second;
586 [ + - ]: 150014 : Trace("model-builder")
587 : 75007 : << " ..Rep( " << eqc << " ) = " << rep << std::endl;
588 : : }
589 : :
590 : : // (3) Finally, process assignable information
591 : 841931 : evaluable = true;
592 : : // expressions that are not assignable should not be given assignment
593 : : // exclusion sets
594 [ - + ][ - + ]: 841931 : Assert(!tm->getAssignmentExclusionSet(n, esetGroup, eset));
[ - - ]
595 : 841931 : continue;
596 : : }
597 : 975846 : assignable = true;
598 [ + + ]: 975846 : if (!computeAssigners)
599 : : {
600 : : // we don't compute assigners, skip
601 : 975599 : continue;
602 : : }
603 : : // process the assignment exclusion set for term n
604 : : // was it processed based on a master exclusion group (see
605 : : // eqcToAssignerMaster)?
606 [ + + ]: 247 : if (processedExcSet.find(n) != processedExcSet.end())
607 : : {
608 : : // Should not have two assignment exclusion sets for the same
609 : : // equivalence class
610 [ - + ][ - + ]: 35 : Assert(!hasESet);
[ - - ]
611 [ - + ][ - + ]: 35 : Assert(eqcToAssignerMaster.find(eqc) != eqcToAssignerMaster.end());
[ - - ]
612 : : // already processed as a slave term
613 : 35 : hasESet = true;
614 : 35 : continue;
615 : : }
616 : : // was it assigned one?
617 [ + + ]: 212 : if (tm->getAssignmentExclusionSet(n, esetGroup, eset))
618 : : {
619 : : // Should not have two assignment exclusion sets for the same
620 : : // equivalence class
621 [ - + ][ - + ]: 12 : Assert(!hasESet);
[ - - ]
622 : 12 : foundESet = true;
623 : 12 : hasESet = true;
624 : : }
625 : : }
626 : :
627 : : // finished traversing the equality engine
628 : 1164960 : TypeNode eqct = eqc.getType();
629 : : // count the number of equivalence classes of sorts in finite model finding
630 [ + + ]: 1164960 : if (options().quantifiers.finiteModelFind)
631 : : {
632 [ + + ]: 23206 : if (eqct.isUninterpretedSort())
633 : : {
634 : 5149 : eqc_usort_count[eqct]++;
635 : : }
636 : : }
637 : : // Assign representative for this equivalence class
638 [ + + ]: 1164960 : if (!constRep.isNull())
639 : : {
640 : : // Theories should not specify a rep if there is already a constant in the
641 : : // equivalence class. However, it may be the case that the representative
642 : : // specified by a theory may be merged with a constant based on equality
643 : : // information from another class. Thus, rep may be non-null here.
644 : : // Regardless, we assign constRep as the representative here.
645 : 598871 : assignConstantRep(tm, eqc, constRep);
646 : 598871 : typeConstSet.add(eqct, constRep);
647 : 598871 : continue;
648 : : }
649 [ + + ]: 566086 : else if (!rep.isNull())
650 : : {
651 : 72343 : assertedReps[eqc] = rep;
652 : 72343 : typeRepSet.add(eqct, eqc);
653 : 72343 : std::unordered_set<TypeNode> visiting;
654 : 72343 : addToTypeList(eqct, type_list, visiting);
655 : : }
656 : : else
657 : : {
658 : 493743 : typeNoRepSet.add(eqct, eqc);
659 : 493743 : std::unordered_set<TypeNode> visiting;
660 : 493743 : addToTypeList(eqct, type_list, visiting);
661 : : }
662 : :
663 [ + + ]: 566086 : if (assignable)
664 : : {
665 : 163468 : assignableEqc.insert(eqc);
666 : : }
667 [ + + ]: 566086 : if (evaluable)
668 : : {
669 : 473406 : evaluableEqc.insert(eqc);
670 : : }
671 : : // If we found an assignment exclusion set, we construct a new assigner
672 : : // object.
673 [ + + ]: 566086 : if (foundESet)
674 : : {
675 : : // we don't accept assignment exclusion sets for evaluable eqc
676 [ - + ][ - + ]: 12 : Assert(!evaluable);
[ - - ]
677 : : // construct the assigner
678 : 12 : Assigner& a = eqcToAssigner[eqc];
679 : : // Take the representatives of each term in the assignment exclusion
680 : : // set, which ensures we can look up their value in d_constReps later.
681 : 24 : std::vector<Node> aes;
682 [ + + ]: 34 : for (const Node& e : eset)
683 : : {
684 : : // Should only supply terms that occur in the model or constants
685 : : // in assignment exclusion sets.
686 : 22 : Assert(tm->hasTerm(e) || e.isConst());
687 [ + - ][ + - ]: 66 : Node er = tm->hasTerm(e) ? tm->getRepresentative(e) : e;
[ - - ]
688 : 22 : aes.push_back(er);
689 : : }
690 : : // initialize
691 : 12 : a.initialize(eqc.getType(), &tep, aes);
692 : : // all others in the group are slaves of this
693 [ + + ]: 59 : for (const Node& g : esetGroup)
694 : : {
695 [ - + ][ - + ]: 47 : Assert(isAssignable(g));
[ - - ]
696 [ - + ]: 47 : if (!tm->hasTerm(g))
697 : : {
698 : : // Ignore those that aren't in the model, in the case the user
699 : : // has supplied an assignment exclusion set to a variable not in
700 : : // the model.
701 : 0 : continue;
702 : : }
703 : 94 : Node gr = tm->getRepresentative(g);
704 [ + + ]: 47 : if (gr != eqc)
705 : : {
706 : 35 : eqcToAssignerMaster[gr] = eqc;
707 : : // remember that this term has been processed
708 : 35 : processedExcSet.insert(g);
709 : : }
710 : : }
711 : : }
712 : : }
713 : :
714 : : // Now finished initialization
715 : :
716 : : // Compute type enumerator properties. This code ensures we do not
717 : : // enumerate terms that have uninterpreted constants that violate the
718 : : // bounds imposed by finite model finding. For example, if finite
719 : : // model finding insists that there are only 2 values { U1, U2 } of type U,
720 : : // then the type enumerator for list of U should enumerate:
721 : : // nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ...
722 : : // instead of enumerating (cons U3 nil).
723 [ + + ]: 35036 : if (options().quantifiers.finiteModelFind)
724 : : {
725 : 1560 : tep.d_fixed_usort_card = true;
726 : 4386 : for (std::map<TypeNode, unsigned>::iterator it = eqc_usort_count.begin();
727 [ + + ]: 4386 : it != eqc_usort_count.end();
728 : 2826 : ++it)
729 : : {
730 [ + - ]: 5652 : Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : "
731 : 2826 : << it->second << std::endl;
732 : 2826 : tep.d_fixed_card[it->first] = Integer(it->second);
733 : : }
734 : 1560 : typeConstSet.setTypeEnumeratorProperties(&tep);
735 : : }
736 : :
737 : : // Need to ensure that each EC has a constant representative.
738 : :
739 [ + - ]: 35036 : Trace("model-builder") << "Processing EC's..." << std::endl;
740 : :
741 : 35036 : TypeSet::iterator it;
742 : 35036 : vector<TypeNode>::iterator type_it;
743 : 35036 : set<Node>::iterator i, i2;
744 : 35036 : bool changed, unassignedAssignable, assignOne = false;
745 : 70072 : set<TypeNode> evaluableSet;
746 : :
747 : : // Double-fixed-point loop
748 : : // Outer loop handles a special corner case (see code at end of loop for
749 : : // details)
750 : : for (;;)
751 : : {
752 : : // Inner fixed-point loop: we are trying to learn constant values for every
753 : : // EC. Each time through this loop, we process all of the
754 : : // types by type and may learn some new EC values. EC's in one type may
755 : : // depend on EC's in another type, so we need a fixed-point loop
756 : : // to ensure that we learn as many EC values as possible
757 [ + + ]: 220390 : do
758 : : {
759 : 220390 : changed = false;
760 : 220390 : unassignedAssignable = false;
761 : 220390 : evaluableSet.clear();
762 : :
763 : : // Iterate over all types we've seen
764 [ + + ]: 1007970 : for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
765 : : {
766 : 1575170 : TypeNode t = *type_it;
767 : 1575170 : TypeNode tb = t;
768 : 787583 : set<Node>* noRepSet = typeNoRepSet.getSet(t);
769 : :
770 : : // 1. Try to evaluate the EC's in this type
771 [ + + ][ + + ]: 787583 : if (noRepSet != NULL && !noRepSet->empty())
[ + + ]
772 : : {
773 [ + - ]: 579422 : Trace("model-builder") << " Eval phase, working on type: " << t
774 : 289711 : << endl;
775 : : bool evaluable;
776 : 289711 : d_normalizedCache.clear();
777 [ + + ]: 3410070 : for (i = noRepSet->begin(); i != noRepSet->end();)
778 : : {
779 : 3120360 : i2 = i;
780 : 3120360 : ++i;
781 [ + - ]: 6240730 : Trace("model-builder-debug") << "Look at eqc : " << (*i2)
782 : 3120360 : << std::endl;
783 : 6240730 : Node normalized;
784 : : // only possible to normalize if we are evaluable
785 : 3120360 : evaluable = evaluableEqc.find(*i2) != evaluableEqc.end();
786 [ + + ]: 3120360 : if (evaluable)
787 : : {
788 : 411495 : normalized = evaluateEqc(tm, *i2);
789 : : }
790 [ + + ]: 3120360 : if (!normalized.isNull())
791 : : {
792 [ - + ][ - + ]: 398767 : Assert(tm->isValue(normalized));
[ - - ]
793 : 398767 : typeConstSet.add(tb, normalized);
794 : 398767 : assignConstantRep(tm, *i2, normalized);
795 [ + - ]: 797534 : Trace("model-builder") << " Eval: Setting constant rep of "
796 : 398767 : << (*i2) << " to " << normalized << endl;
797 : 398767 : changed = true;
798 : 398767 : noRepSet->erase(i2);
799 : : }
800 : : else
801 : : {
802 [ + + ]: 2721600 : if (evaluable)
803 : : {
804 : 12728 : evaluableSet.insert(tb);
805 : : }
806 : : // If assignable, remember there is an equivalence class that is
807 : : // not assigned and assignable.
808 [ + + ]: 2721600 : if (assignableEqc.find(*i2) != assignableEqc.end())
809 : : {
810 : 2708980 : unassignedAssignable = true;
811 : : }
812 : : }
813 : : }
814 : : }
815 : :
816 : : // 2. Normalize any non-const representative terms for this type
817 : 787583 : set<Node>* repSet = typeRepSet.getSet(t);
818 [ + + ][ + + ]: 787583 : if (repSet != NULL && !repSet->empty())
[ + + ]
819 : : {
820 [ + - ]: 659194 : Trace("model-builder")
821 : 329597 : << " Normalization phase, working on type: " << t << endl;
822 : 329597 : d_normalizedCache.clear();
823 [ + + ]: 2738040 : for (i = repSet->begin(); i != repSet->end();)
824 : : {
825 [ - + ][ - + ]: 2408450 : Assert(assertedReps.find(*i) != assertedReps.end());
[ - - ]
826 : 4816890 : Node rep = assertedReps[*i];
827 : 4816890 : Node normalized = normalize(tm, rep, false);
828 [ + - ]: 4816890 : Trace("model-builder")
829 : 0 : << " Normalizing rep (" << rep << "), normalized to ("
830 : 0 : << normalized << ")"
831 [ - + ][ - - ]: 2408450 : << ", isValue=" << tm->isValue(normalized) << std::endl;
832 [ + + ]: 2408450 : if (tm->isValue(normalized))
833 : : {
834 : 72343 : changed = true;
835 : 72343 : typeConstSet.add(tb, normalized);
836 : 72343 : assignConstantRep(tm, *i, normalized);
837 : 72343 : assertedReps.erase(*i);
838 : 72343 : i2 = i;
839 : 72343 : ++i;
840 : 72343 : repSet->erase(i2);
841 : : }
842 : : else
843 : : {
844 [ + + ]: 2336100 : if (normalized != rep)
845 : : {
846 : 42396 : assertedReps[*i] = normalized;
847 : 42396 : changed = true;
848 : : }
849 : 2336100 : ++i;
850 : : }
851 : : }
852 : : }
853 : : }
854 : : } while (changed);
855 : :
856 [ + + ]: 140442 : if (!unassignedAssignable)
857 : : {
858 : 35036 : break;
859 : : }
860 : :
861 : : // 3. Assign unassigned assignable EC's using type enumeration - assign a
862 : : // value *different* from all other EC's if the type is infinite
863 : : // Assign first value from type enumerator otherwise - for finite types, we
864 : : // rely on polite framework to ensure that EC's that have to be
865 : : // different are different.
866 : :
867 : : // Only make assignments on a type if:
868 : : // 1. there are no terms that share the same base type with un-normalized
869 : : // representatives
870 : : // 2. there are no terms that share teh same base type that are unevaluated
871 : : // evaluable terms
872 : : // Alternatively, if 2 or 3 don't hold but we are in a special
873 : : // deadlock-breaking mode where assignOne is true, go ahead and make one
874 : : // assignment
875 : 105406 : changed = false;
876 : : // must iterate over the ordered type list to ensure that we do not
877 : : // enumerate values with subterms
878 : : // having types that we are currently enumerating (when possible)
879 : : // for example, this ensures we enumerate uninterpreted sort U before (List
880 : : // of U) and (Array U U)
881 : : // however, it does not break cyclic type dependencies for mutually
882 : : // recursive datatypes, but this is handled
883 : : // by recording all subterms of enumerated values in TypeSet::addSubTerms.
884 [ + + ]: 535255 : for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
885 : : {
886 : 429849 : TypeNode t = *type_it;
887 : : // continue if there are no more equivalence classes of this type to
888 : : // assign
889 : 429849 : std::set<Node>* noRepSetPtr = typeNoRepSet.getSet(t);
890 [ + + ]: 429849 : if (noRepSetPtr == NULL)
891 : : {
892 : 37729 : continue;
893 : : }
894 : 392120 : set<Node>& noRepSet = *noRepSetPtr;
895 [ + + ]: 392120 : if (noRepSet.empty())
896 : : {
897 : 223984 : continue;
898 : : }
899 : :
900 : : // get properties of this type
901 : 168136 : bool isCorecursive = false;
902 [ + + ]: 168136 : if (t.isDatatype())
903 : : {
904 : 159517 : const DType& dt = t.getDType();
905 : 159517 : isCorecursive =
906 : 319034 : dt.isCodatatype()
907 : 159517 : && (!d_env.isFiniteType(t) || dt.isRecursiveSingleton(t));
908 : : }
909 : : #ifdef CVC5_ASSERTIONS
910 : 168136 : bool isUSortFiniteRestricted = false;
911 [ + + ]: 168136 : if (options().quantifiers.finiteModelFind)
912 : : {
913 [ + + ][ + + ]: 10558 : isUSortFiniteRestricted = !t.isUninterpretedSort() && involvesUSort(t);
[ + + ][ - - ]
914 : : }
915 : : #endif
916 : :
917 : 168136 : TypeNode tb = t;
918 [ + + ]: 168136 : if (!assignOne)
919 : : {
920 : 117864 : set<Node>* repSet = typeRepSet.getSet(tb);
921 [ + + ][ + + ]: 117864 : if (repSet != NULL && !repSet->empty())
[ + + ]
922 : : {
923 : 107284 : continue;
924 : : }
925 [ + + ]: 10580 : if (evaluableSet.find(tb) != evaluableSet.end())
926 : : {
927 : 1646 : continue;
928 : : }
929 : : }
930 [ + - ]: 118412 : Trace("model-builder") << " Assign phase, working on type: " << t
931 : 59206 : << endl;
932 : : bool assignable, evaluable CVC5_UNUSED;
933 : 59206 : std::map<Node, Assigner>::iterator itAssigner;
934 : 59206 : std::map<Node, Node>::iterator itAssignerM;
935 : 59206 : set<Node>* repSet = typeRepSet.getSet(t);
936 [ + + ]: 104209 : for (i = noRepSet.begin(); i != noRepSet.end();)
937 : : {
938 : 94503 : i2 = i;
939 : 94503 : ++i;
940 [ + + ]: 94503 : if (evaluableEqc.find(*i2) != evaluableEqc.end())
941 : : {
942 : : // we never assign to evaluable equivalence classes
943 : 1823 : continue;
944 : : }
945 : : // check whether it has an assigner object
946 : 92680 : itAssignerM = eqcToAssignerMaster.find(*i2);
947 [ + + ]: 92680 : if (itAssignerM != eqcToAssignerMaster.end())
948 : : {
949 : : // Take the master's assigner. Notice we don't care which order
950 : : // equivalence classes are assigned. For instance, the master can
951 : : // be assigned after one of its slaves.
952 : 35 : itAssigner = eqcToAssigner.find(itAssignerM->second);
953 : : }
954 : : else
955 : : {
956 : 92645 : itAssigner = eqcToAssigner.find(*i2);
957 : : }
958 [ + + ]: 92680 : if (itAssigner != eqcToAssigner.end())
959 : : {
960 : 47 : assignable = isAssignerActive(tm, itAssigner->second);
961 : : }
962 : : else
963 : : {
964 : 92633 : assignable = assignableEqc.find(*i2) != assignableEqc.end();
965 : : }
966 [ + - ]: 185360 : Trace("model-builder-debug")
967 : 0 : << " eqc " << *i2 << " is assignable=" << assignable
968 : 92680 : << std::endl;
969 [ + - ]: 92680 : if (assignable)
970 : : {
971 : : // this assertion ensures that if we are assigning to a term of
972 : : // Boolean type, then the term must be assignable.
973 : : // Note we only assign to terms of Boolean type if the term occurs in
974 : : // a singleton equivalence class; otherwise the term would have been
975 : : // in the equivalence class of true or false and would not need
976 : : // assigning.
977 : 92680 : Assert(!t.isBoolean() || isAssignable(*i2));
978 : 92680 : Node n;
979 [ + + ]: 92680 : if (itAssigner != eqcToAssigner.end())
980 : : {
981 [ + - ]: 94 : Trace("model-builder-debug")
982 : 47 : << "Get value from assigner for finite type..." << std::endl;
983 : : // if it has an assigner, get the value from the assigner.
984 : 47 : n = itAssigner->second.getNextAssignment();
985 [ - + ][ - + ]: 47 : Assert(!n.isNull());
[ - - ]
986 : : }
987 [ + + ][ + + ]: 92633 : else if (t.isUninterpretedSort() || !d_env.isFiniteType(t))
[ + + ][ + + ]
[ - - ]
988 : : {
989 : : // If its interpreted as infinite, we get a fresh value that does
990 : : // not occur in the model.
991 : : // Note we also consider uninterpreted sorts to be infinite here
992 : : // regardless of whether the cardinality class of t is
993 : : // CardinalityClass::INTERPRETED_FINITE.
994 : : // This is required because the UF solver does not explicitly
995 : : // assign uninterpreted constants to equivalence classes in its
996 : : // collectModelValues method. Doing so would have the same effect
997 : : // as running the code in this case.
998 : : bool success;
999 : 18 : do
1000 : : {
1001 [ + - ]: 185028 : Trace("model-builder-debug") << "Enumerate term of type " << t
1002 : 92514 : << std::endl;
1003 : 92514 : n = typeConstSet.nextTypeEnum(t);
1004 : : //--- AJR: this code checks whether n is a legal value
1005 [ - + ][ - + ]: 92514 : Assert(!n.isNull());
[ - - ]
1006 : 92514 : success = true;
1007 [ + - ]: 185028 : Trace("model-builder-debug") << "Check if excluded : " << n
1008 : 92514 : << std::endl;
1009 : : #ifdef CVC5_ASSERTIONS
1010 [ + + ]: 92514 : if (isUSortFiniteRestricted)
1011 : : {
1012 : : // must not involve uninterpreted constants beyond cardinality
1013 : : // bound (which assumed to coincide with #eqc)
1014 : : // this is just an assertion now, since TypeEnumeratorProperties
1015 : : // should ensure that only legal values are enumerated wrt this
1016 : : // constraint.
1017 : 3256 : std::map<Node, bool> visited;
1018 : 3256 : success = !isExcludedUSortValue(eqc_usort_count, n, visited);
1019 [ - + ]: 3256 : if (!success)
1020 : : {
1021 [ - - ]: 0 : Trace("model-builder")
1022 : 0 : << "Excluded value for " << t << " : " << n
1023 : 0 : << " due to out of range uninterpreted constant."
1024 : 0 : << std::endl;
1025 : : }
1026 [ - + ][ - + ]: 3256 : Assert(success);
[ - - ]
1027 : : }
1028 : : #endif
1029 [ + - ][ + + ]: 92514 : if (success && isCorecursive)
1030 : : {
1031 [ + + ][ + + ]: 57 : if (repSet != NULL && !repSet->empty())
[ + + ]
1032 : : {
1033 : : // in the case of codatatypes, check if it is in the set of
1034 : : // values that we cannot assign
1035 : 48 : success = !isExcludedCdtValue(n, repSet, assertedReps, *i2);
1036 [ + + ]: 48 : if (!success)
1037 : : {
1038 [ + - ]: 36 : Trace("model-builder")
1039 : 0 : << "Excluded value : " << n
1040 : 0 : << " due to alpha-equivalent codatatype expression."
1041 : 18 : << std::endl;
1042 : : }
1043 : : }
1044 : : }
1045 : : //---
1046 [ + + ]: 92514 : } while (!success);
1047 [ - + ][ - + ]: 92496 : Assert(!n.isNull());
[ - - ]
1048 : : }
1049 : : else
1050 : : {
1051 : : // Otherwise, we get the first value from the type enumerator.
1052 [ + - ]: 274 : Trace("model-builder-debug")
1053 : 137 : << "Get first value from finite type..." << std::endl;
1054 : 137 : TypeEnumerator te(t);
1055 : 137 : n = *te;
1056 : : }
1057 [ + - ]: 92680 : Trace("model-builder-debug") << "...got " << n << std::endl;
1058 : 92680 : assignConstantRep(tm, *i2, n);
1059 : 92680 : changed = true;
1060 : 92680 : noRepSet.erase(i2);
1061 [ + + ]: 92680 : if (assignOne)
1062 : : {
1063 : 49500 : assignOne = false;
1064 : 49500 : break;
1065 : : }
1066 : : }
1067 : : }
1068 : : }
1069 : :
1070 : : // Corner case - I'm not sure this can even happen - but it's theoretically
1071 : : // possible to have a cyclical dependency
1072 : : // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In
1073 : : // this case, neither one will get assigned because we are waiting
1074 : : // to be able to evaluate. But we will never be able to evaluate because
1075 : : // the variables that need to be assigned are in
1076 : : // these same EC's. In this case, repeat the whole fixed-point computation
1077 : : // with the difference that the first EC
1078 : : // that has both assignable and evaluable expressions will get assigned.
1079 [ + + ]: 105406 : if (!changed)
1080 : : {
1081 [ + - ]: 49500 : Trace("model-builder-debug") << "...must assign one" << std::endl;
1082 : : // Avoid infinite loops: if we are in a deadlock, we abort model building
1083 : : // unsuccessfully here.
1084 [ - + ]: 49500 : if (assignOne)
1085 : : {
1086 : 0 : Assert (false) << "Reached a deadlock during model construction";
1087 : : Trace("model-builder-debug") << "...avoid loop, fail" << std::endl;
1088 : : return false;
1089 : : }
1090 : 49500 : assignOne = true;
1091 : : }
1092 : 105406 : }
1093 : :
1094 : : #ifdef CVC5_ASSERTIONS
1095 : : // Assert that all representatives have been converted to constants
1096 [ + + ]: 54663 : for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it)
1097 : : {
1098 : 19627 : std::set<Node>& repSet = TypeSet::getSet(it);
1099 [ - + ]: 19627 : if (!repSet.empty())
1100 : : {
1101 [ - - ]: 0 : Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size()
1102 : 0 : << ", repSet = " << repSet << endl;
1103 : 0 : Trace("model-builder-debug") << tm->getEqualityEngine()->debugPrintEqc();
1104 : 0 : Assert(false);
1105 : : }
1106 : : }
1107 : : #endif /* CVC5_ASSERTIONS */
1108 : :
1109 [ + - ]: 35036 : Trace("model-builder") << "Copy representatives to model..." << std::endl;
1110 : 35036 : tm->d_reps.clear();
1111 : 35036 : std::map<Node, Node>::iterator itMap;
1112 [ + + ]: 1197700 : for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap)
1113 : : {
1114 : : // The "constant" representative is a model value, which may be a lambda
1115 : : // if higher-order. We now can go back and normalize its subterms.
1116 : : // This is necessary if we assigned a lambda value whose body contains
1117 : : // a free constant symbol that was assigned in this method.
1118 : 2325320 : Node normc = itMap->second;
1119 [ + + ]: 1162660 : if (!normc.isConst())
1120 : : {
1121 : 470 : normc = normalize(tm, normc, true);
1122 : : }
1123 : : // mark this as the final representative
1124 : 1162660 : tm->assignRepresentative(itMap->first, normc, true);
1125 : : }
1126 : :
1127 [ + - ]: 35036 : Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
1128 : : // Make sure every EC has a rep
1129 [ - + ]: 35036 : for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap)
1130 : : {
1131 : 0 : tm->assignRepresentative(itMap->first, itMap->second, false);
1132 : : }
1133 [ + + ]: 70697 : for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it)
1134 : : {
1135 : 35661 : set<Node>& noRepSet = TypeSet::getSet(it);
1136 [ + + ]: 37957 : for (const Node& node : noRepSet)
1137 : : {
1138 : 2296 : tm->assignRepresentative(node, node, false);
1139 : : }
1140 : : }
1141 : :
1142 : : // modelBuilder-specific initialization
1143 [ - + ]: 35036 : if (!processBuildModel(tm))
1144 : : {
1145 [ - - ]: 0 : Trace("model-builder")
1146 : 0 : << "TheoryEngineModelBuilder: fail process build model." << std::endl;
1147 : 0 : return false;
1148 : : }
1149 [ + - ]: 35036 : Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl;
1150 : 35036 : return true;
1151 : : }
1152 : :
1153 : 4410 : void TheoryEngineModelBuilder::postProcessModel(bool incomplete, TheoryModel* m)
1154 : : {
1155 : : // if we are incomplete, there is no guarantee on the model.
1156 : : // thus, we do not check the model here.
1157 [ + + ]: 4410 : if (incomplete)
1158 : : {
1159 : 1861 : return;
1160 : : }
1161 [ - + ][ - + ]: 2549 : Assert(m != nullptr);
[ - - ]
1162 : : // debug-check the model if the checkModels() is enabled.
1163 [ + + ]: 2549 : if (options().smt.debugCheckModels)
1164 : : {
1165 : 432 : debugCheckModel(m);
1166 : : }
1167 : : }
1168 : :
1169 : 432 : void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
1170 : : {
1171 : 432 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
1172 : 432 : std::map<Node, Node>::iterator itMap;
1173 : : // Check that every term evaluates to its representative in the model
1174 : 8070 : for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
1175 [ + + ]: 8070 : !eqcs_i.isFinished();
1176 : 7638 : ++eqcs_i)
1177 : : {
1178 : : // eqc is the equivalence class representative
1179 : 15276 : Node eqc = (*eqcs_i);
1180 : : // get the representative
1181 : 15276 : Node rep = tm->getRepresentative(eqc);
1182 [ + + ][ - + ]: 7638 : if (!rep.isConst() && eqc.getType().isBoolean())
[ + + ][ - + ]
[ - - ]
1183 : : {
1184 : : // if Boolean, it does not necessarily have a constant representative, use
1185 : : // get value instead
1186 : 0 : rep = tm->getValue(eqc);
1187 : 0 : AlwaysAssert(rep.isConst());
1188 : : }
1189 : 7638 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
1190 [ + + ]: 37963 : for (; !eqc_i.isFinished(); ++eqc_i)
1191 : : {
1192 : 60650 : Node n = *eqc_i;
1193 [ - + ][ - - ]: 60650 : AlwaysAssert(rep.getType() == n.getType())
1194 : 30325 : << "Representative " << rep << " of " << n
1195 [ - + ][ - - ]: 30325 : << " violates type constraints (" << rep.getType() << " and "
1196 [ - + ][ - + ]: 30325 : << n.getType() << ")";
[ - - ]
1197 : 60650 : Node val = tm->getValue(n);
1198 [ + + ]: 30325 : if (val != rep)
1199 : : {
1200 : 432 : std::stringstream err;
1201 : 216 : err << "Failed representative check:" << std::endl
1202 : 216 : << "n: " << n << std::endl
1203 : 432 : << "getValue(n): " << val << std::endl
1204 : 216 : << "rep: " << rep << std::endl;
1205 [ - + ][ - - ]: 216 : if (val.isConst() && rep.isConst())
[ - + ]
1206 : : {
1207 : 0 : AlwaysAssert(val == rep) << err.str();
1208 : : }
1209 [ + + ]: 216 : else if (rewrite(val) != rewrite(rep))
1210 : : {
1211 : : // if it does not evaluate, it is just a warning, which may be the
1212 : : // case for non-constant values, e.g. lambdas. Furthermore we only
1213 : : // throw this warning if rewriting cannot show they are equal.
1214 : 37 : warning() << err.str();
1215 : : }
1216 : : }
1217 : : }
1218 : : }
1219 : :
1220 : : // builder-specific debugging
1221 : 432 : debugModel(tm);
1222 : 432 : }
1223 : :
1224 : 2928370 : Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
1225 : : {
1226 : 2928370 : std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
1227 [ + + ]: 2928370 : if (itMap != d_constantReps.end())
1228 : : {
1229 : 18 : r = (*itMap).second;
1230 : : // if d_constantReps stores a constant, we are done, otherwise we process
1231 : : // it below.
1232 [ - + ]: 18 : if (r.isConst())
1233 : : {
1234 : 0 : return r;
1235 : : }
1236 : : }
1237 : 2928370 : NodeMap::iterator it = d_normalizedCache.find(r);
1238 [ + + ]: 2928370 : if (it != d_normalizedCache.end())
1239 : : {
1240 : 31820 : return (*it).second;
1241 : : }
1242 [ + - ]: 2896550 : Trace("model-builder-debug") << "do normalize on " << r << std::endl;
1243 : 5793110 : Node retNode = r;
1244 [ + + ]: 2896550 : if (r.getNumChildren() > 0)
1245 : : {
1246 : 2889040 : std::vector<Node> children;
1247 [ + + ]: 2889040 : if (r.getMetaKind() == kind::metakind::PARAMETERIZED)
1248 : : {
1249 : 2433610 : children.push_back(r.getOperator());
1250 : : }
1251 [ + + ]: 8846790 : for (size_t i = 0, nchild = r.getNumChildren(); i < nchild; ++i)
1252 : : {
1253 : 11915500 : Node ri = r[i];
1254 : 5957740 : bool recurse = true;
1255 [ + + ]: 5957740 : if (!ri.isConst())
1256 : : {
1257 [ + + ]: 4443260 : if (m->d_equalityEngine->hasTerm(ri))
1258 : : {
1259 : : itMap =
1260 : 4410140 : d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
1261 [ + + ]: 4410140 : if (itMap != d_constantReps.end())
1262 : : {
1263 : 791005 : ri = (*itMap).second;
1264 [ + - ]: 791005 : Trace("model-builder-debug") << i << ": const child " << ri << std::endl;
1265 : : // need to recurse if d_constantReps stores a non-constant
1266 : 791005 : recurse = !ri.isConst();
1267 : : }
1268 [ + + ]: 3619130 : else if (!evalOnly)
1269 : : {
1270 : 3546580 : recurse = false;
1271 [ + - ]: 3546580 : Trace("model-builder-debug") << i << ": keep " << ri << std::endl;
1272 : : }
1273 : : }
1274 : : else
1275 : : {
1276 [ + - ]: 33118 : Trace("model-builder-debug") << i << ": no hasTerm " << ri << std::endl;
1277 : : }
1278 [ + + ]: 4443260 : if (recurse)
1279 : : {
1280 : 105800 : ri = normalize(m, ri, evalOnly);
1281 : : }
1282 : : }
1283 : 5957740 : children.push_back(ri);
1284 : : }
1285 : 2889040 : retNode = nodeManager()->mkNode(r.getKind(), children);
1286 : 2889040 : retNode = rewrite(retNode);
1287 : : }
1288 : 2896550 : d_normalizedCache[r] = retNode;
1289 : 2896550 : return retNode;
1290 : : }
1291 : :
1292 : 1566 : bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m)
1293 : : {
1294 : 1566 : return true;
1295 : : }
1296 : :
1297 : 34207 : bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m)
1298 : : {
1299 [ + - ]: 34207 : if (m->areFunctionValuesEnabled())
1300 : : {
1301 : 34207 : assignFunctions(m);
1302 : : }
1303 : 34207 : return true;
1304 : : }
1305 : :
1306 : 2962 : void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
1307 : : {
1308 [ - + ][ - + ]: 2962 : Assert(!logicInfo().isHigherOrder());
[ - - ]
1309 : 5924 : uf::UfModelTree ufmt(f);
1310 : : options::DefaultFunctionValueMode dfvm =
1311 : 2962 : options().theory.defaultFunctionValueMode;
1312 : 5924 : Node default_v;
1313 [ + + ]: 14459 : for (size_t i = 0; i < m->d_uf_terms[f].size(); i++)
1314 : : {
1315 : 22994 : Node un = m->d_uf_terms[f][i];
1316 : 22994 : vector<TNode> children;
1317 : 11497 : children.push_back(f);
1318 [ + - ]: 11497 : Trace("model-builder-debug") << " process term : " << un << std::endl;
1319 [ + + ]: 56133 : for (size_t j = 0; j < un.getNumChildren(); ++j)
1320 : : {
1321 : 89272 : Node rc = m->getRepresentative(un[j]);
1322 [ + - ][ - + ]: 89272 : Trace("model-builder-debug2") << " get rep : " << un[j] << " returned "
[ - - ]
1323 : 44636 : << rc << std::endl;
1324 [ - + ][ - + ]: 44636 : Assert(rewrite(rc) == rc);
[ - - ]
1325 : 44636 : children.push_back(rc);
1326 : : }
1327 : 22994 : Node simp = nodeManager()->mkNode(un.getKind(), children);
1328 : 22994 : Node v = m->getRepresentative(un);
1329 [ + - ]: 22994 : Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")"
1330 : 11497 : << endl;
1331 : 11497 : ufmt.setValue(m, simp, v);
1332 [ + + ]: 11497 : if (dfvm == options::DefaultFunctionValueMode::FIRST)
1333 : : {
1334 : 11491 : default_v = v;
1335 : : }
1336 : : }
1337 : 5924 : TypeNode rangeType = f.getType().getRangeType();
1338 [ + + ]: 2962 : if (dfvm == options::DefaultFunctionValueMode::HOLE)
1339 : : {
1340 : 2 : NodeManager* nm = nodeManager();
1341 : 2 : SkolemManager* sm = nm->getSkolemManager();
1342 : 2 : std::vector<Node> cacheVals;
1343 : 2 : cacheVals.push_back(nm->mkConst(SortToTerm(rangeType)));
1344 : 2 : default_v = sm->mkSkolemFunction(SkolemId::GROUND_TERM, cacheVals);
1345 : : }
1346 [ + + ]: 2960 : else if (default_v.isNull())
1347 : : {
1348 : : // choose default value from model if none exists
1349 : 2 : TypeEnumerator te(rangeType);
1350 : 2 : default_v = (*te);
1351 : : }
1352 : 2962 : ufmt.setDefaultValue(m, default_v);
1353 : 2962 : bool condenseFuncValues = options().theory.condenseFunctionValues;
1354 [ + - ]: 2962 : if (condenseFuncValues)
1355 : : {
1356 : 2962 : ufmt.simplify();
1357 : : }
1358 : 5924 : std::stringstream ss;
1359 : 2962 : ss << "_arg_";
1360 [ + - ]: 2962 : Rewriter* r = condenseFuncValues ? d_env.getRewriter() : nullptr;
1361 : 2962 : Node val = ufmt.getFunctionValue(ss.str(), r);
1362 [ + - ]: 2962 : Trace("model-builder-debug") << "...assign via function" << std::endl;
1363 : 2962 : m->assignFunctionDefinition(f, val);
1364 : : // ufmt.debugPrint( std::cout, m );
1365 : 2962 : }
1366 : :
1367 : 2296 : void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
1368 : : {
1369 [ - + ][ - + ]: 2296 : Assert(logicInfo().isHigherOrder());
[ - - ]
1370 : 4592 : TypeNode type = f.getType();
1371 : 4592 : std::vector<TypeNode> argTypes = type.getArgTypes();
1372 : 4592 : std::vector<Node> args;
1373 : 4592 : std::vector<TNode> apply_args;
1374 : : options::DefaultFunctionValueMode dfvm =
1375 : 2296 : options().theory.defaultFunctionValueMode;
1376 [ + + ]: 5024 : for (unsigned i = 0; i < argTypes.size(); i++)
1377 : : {
1378 : 5456 : Node v = nodeManager()->mkBoundVar(argTypes[i]);
1379 : 2728 : args.push_back(v);
1380 [ + + ]: 2728 : if (i > 0)
1381 : : {
1382 : 432 : apply_args.push_back(v);
1383 : : }
1384 : : }
1385 : : // Depending on the default value mode, maybe set the current value (curr).
1386 : : // We also remember a default value (currPre) in case there are no terms
1387 : : // to assign below.
1388 : 4592 : TypeNode rangeType = type.getRangeType();
1389 : 4592 : Node curr, currPre;
1390 [ - + ]: 2296 : if (dfvm == options::DefaultFunctionValueMode::HOLE)
1391 : : {
1392 : 0 : NodeManager* nm = nodeManager();
1393 : 0 : SkolemManager* sm = nm->getSkolemManager();
1394 : 0 : std::vector<Node> cacheVals;
1395 : 0 : cacheVals.push_back(nm->mkConst(SortToTerm(rangeType)));
1396 : 0 : currPre = sm->mkSkolemFunction(SkolemId::GROUND_TERM, cacheVals);
1397 : 0 : curr = currPre;
1398 : : }
1399 : : else
1400 : : {
1401 : 4592 : TypeEnumerator te(rangeType);
1402 : 2296 : currPre = (*te);
1403 [ - + ]: 2296 : if (dfvm == options::DefaultFunctionValueMode::FIRST_ENUM)
1404 : : {
1405 : 0 : curr = currPre;
1406 : : }
1407 : : }
1408 : 2296 : curr = currPre;
1409 : 2296 : std::map<Node, std::vector<Node> >::iterator itht = m->d_ho_uf_terms.find(f);
1410 [ + - ]: 2296 : if (itht != m->d_ho_uf_terms.end())
1411 : : {
1412 [ + + ]: 21971 : for (size_t i = 0; i < itht->second.size(); i++)
1413 : : {
1414 : 39350 : Node hn = itht->second[i];
1415 [ + - ]: 19675 : Trace("model-builder-debug") << " process : " << hn << std::endl;
1416 [ - + ][ - + ]: 19675 : Assert(hn.getKind() == Kind::HO_APPLY);
[ - - ]
1417 [ - + ][ - + ]: 19675 : Assert(m->areEqual(hn[0], f));
[ - - ]
1418 : 59025 : Node hni = m->getRepresentative(hn[1]);
1419 [ + - ]: 39350 : Trace("model-builder-debug2")
1420 [ - + ][ - - ]: 19675 : << " get rep : " << hn[1] << " returned " << hni << std::endl;
1421 [ - + ][ - + ]: 19675 : Assert(hni.getType() == args[0].getType());
[ - - ]
1422 : 19675 : hni = rewrite(args[0].eqNode(hni));
1423 : 39350 : Node hnv = m->getRepresentative(hn);
1424 [ + - ]: 39350 : Trace("model-builder-debug2") << " get rep val : " << hn
1425 : 19675 : << " returned " << hnv << std::endl;
1426 : : // hnv is expected to be constant but may not be the case if e.g. a non-trivial
1427 : : // lambda is given as argument to this function.
1428 [ + + ]: 19675 : if (!apply_args.empty())
1429 : : {
1430 : : // Convert to lambda, which is necessary if hnv is a function array
1431 : : // constant.
1432 : 1244 : hnv = uf::FunctionConst::toLambda(hnv);
1433 : 2488 : Assert(!hnv.isNull() && hnv.getKind() == Kind::LAMBDA
1434 : : && hnv[0].getNumChildren() + 1 == args.size());
1435 : 1244 : std::vector<TNode> largs;
1436 [ + + ]: 2531 : for (unsigned j = 0; j < hnv[0].getNumChildren(); j++)
1437 : : {
1438 : 1287 : largs.push_back(hnv[0][j]);
1439 : : }
1440 [ - + ][ - + ]: 1244 : Assert(largs.size() == apply_args.size());
[ - - ]
1441 : 2488 : hnv = hnv[1].substitute(
1442 : 1244 : largs.begin(), largs.end(), apply_args.begin(), apply_args.end());
1443 : 1244 : hnv = rewrite(hnv);
1444 : : }
1445 [ - + ][ - + ]: 19675 : Assert(hnv.getType() == curr.getType());
[ - - ]
1446 [ - + ]: 19675 : if (curr.isNull())
1447 : : {
1448 : 0 : curr = hnv;
1449 : : }
1450 : : else
1451 : : {
1452 : 19675 : curr = nodeManager()->mkNode(Kind::ITE, hni, hnv, curr);
1453 : : }
1454 : : }
1455 : : }
1456 : : // if curr was not set, we set it to currPre.
1457 [ - + ]: 2296 : if (curr.isNull())
1458 : : {
1459 : 0 : curr = currPre;
1460 : : }
1461 : 2296 : Node val = nodeManager()->mkNode(
1462 : 4592 : Kind::LAMBDA, nodeManager()->mkNode(Kind::BOUND_VAR_LIST, args), curr);
1463 [ + - ]: 2296 : Trace("model-builder-debug") << "...assign via ho function" << std::endl;
1464 : 2296 : m->assignFunctionDefinition(f, val);
1465 : 2296 : }
1466 : :
1467 : 35036 : void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
1468 : : {
1469 [ - + ]: 35036 : if (!options().theory.assignFunctionValues)
1470 : : {
1471 : 0 : return;
1472 : : }
1473 [ + - ]: 35036 : Trace("model-builder") << "Assigning function values..." << std::endl;
1474 : 35036 : std::vector<Node> funcs_to_assign = m->getFunctionsToAssign();
1475 : :
1476 [ + + ]: 35036 : if (logicInfo().isHigherOrder())
1477 : : {
1478 : : // sort based on type size if higher-order
1479 [ + - ]: 858 : Trace("model-builder") << "Sort functions by type..." << std::endl;
1480 : 858 : SortTypeSize sts;
1481 : 858 : std::sort(funcs_to_assign.begin(), funcs_to_assign.end(), sts);
1482 : : }
1483 : :
1484 [ - + ]: 35036 : if (TraceIsOn("model-builder"))
1485 : : {
1486 [ - - ]: 0 : Trace("model-builder") << "...have " << funcs_to_assign.size()
1487 : 0 : << " functions to assign:" << std::endl;
1488 [ - - ]: 0 : for (unsigned k = 0; k < funcs_to_assign.size(); k++)
1489 : : {
1490 : 0 : Node f = funcs_to_assign[k];
1491 [ - - ]: 0 : Trace("model-builder") << " [" << k << "] : " << f << " : "
1492 : 0 : << f.getType() << std::endl;
1493 : : }
1494 : : }
1495 : :
1496 : : // construct function values
1497 [ + + ]: 40294 : for (unsigned k = 0; k < funcs_to_assign.size(); k++)
1498 : : {
1499 : 10516 : Node f = funcs_to_assign[k];
1500 [ + - ]: 5258 : Trace("model-builder") << " Function #" << k << " is " << f << std::endl;
1501 [ + + ]: 5258 : if (!logicInfo().isHigherOrder())
1502 : : {
1503 [ + - ]: 5924 : Trace("model-builder") << " Assign function value for " << f
1504 : 2962 : << " based on APPLY_UF" << std::endl;
1505 : 2962 : assignFunction(m, f);
1506 : : }
1507 : : else
1508 : : {
1509 [ + - ]: 4592 : Trace("model-builder") << " Assign function value for " << f
1510 : 2296 : << " based on curried HO_APPLY" << std::endl;
1511 : 2296 : assignHoFunction(m, f);
1512 : : }
1513 : : }
1514 [ + - ]: 35036 : Trace("model-builder") << "Finished assigning function values." << std::endl;
1515 : : }
1516 : :
1517 : : } // namespace theory
1518 : : } // namespace cvc5::internal
|
