Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of theory model buidler class.
11 : : */
12 : : #include "theory/theory_model_builder.h"
13 : :
14 : : #include "expr/dtype.h"
15 : : #include "expr/dtype_cons.h"
16 : : #include "expr/skolem_manager.h"
17 : : #include "expr/sort_to_term.h"
18 : : #include "expr/sort_type_size.h"
19 : : #include "options/quantifiers_options.h"
20 : : #include "options/smt_options.h"
21 : : #include "options/strings_options.h"
22 : : #include "options/theory_options.h"
23 : : #include "options/uf_options.h"
24 : : #include "smt/env.h"
25 : : #include "theory/rewriter.h"
26 : : #include "theory/uf/function_const.h"
27 : : #include "theory/uf/theory_uf_model.h"
28 : : #include "util/uninterpreted_sort_value.h"
29 : :
30 : : using namespace std;
31 : : using namespace cvc5::internal::kind;
32 : : using namespace cvc5::context;
33 : :
34 : : namespace cvc5::internal {
35 : : namespace theory {
36 : :
37 : 57768 : TheoryEngineModelBuilder::TheoryEngineModelBuilder(Env& env) : EnvObj(env) {}
38 : :
39 : 12 : void TheoryEngineModelBuilder::Assigner::initialize(
40 : : TypeNode tn, TypeEnumeratorProperties* tep, const std::vector<Node>& aes)
41 : : {
42 : 12 : d_te.reset(new TypeEnumerator(tn, tep));
43 : 12 : d_assignExcSet.insert(d_assignExcSet.end(), aes.begin(), aes.end());
44 : 12 : }
45 : :
46 : 47 : Node TheoryEngineModelBuilder::Assigner::getNextAssignment()
47 : : {
48 [ - + ][ - + ]: 47 : Assert(d_te != nullptr);
[ - - ]
49 : 47 : Node n;
50 : 47 : bool success = false;
51 : 47 : TypeEnumerator& te = *d_te;
52 : : // Check if we have run out of elements. This should never happen; if it
53 : : // does we assert false and return null.
54 [ - + ]: 47 : if (te.isFinished())
55 : : {
56 : 0 : DebugUnhandled();
57 : : return Node::null();
58 : : }
59 : : // must increment until we find one that is not in the assignment
60 : : // exclusion set
61 : : do
62 : : {
63 : 57 : n = *te;
64 : 57 : success = std::find(d_assignExcSet.begin(), d_assignExcSet.end(), n)
65 : 114 : == d_assignExcSet.end();
66 : : // increment regardless of fail or succeed, to set up the next value
67 : 57 : ++te;
68 [ + + ]: 57 : } while (!success);
69 : 47 : return n;
70 : 47 : }
71 : :
72 : 424922 : Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
73 : : {
74 : 424922 : eq::EqClassIterator eqc_i = eq::EqClassIterator(r, m->d_equalityEngine);
75 [ + + ]: 438908 : for (; !eqc_i.isFinished(); ++eqc_i)
76 : : {
77 : 429523 : Node n = *eqc_i;
78 [ + - ]: 429523 : Trace("model-builder-debug") << "Look at term : " << n << std::endl;
79 [ + + ]: 429523 : if (!isAssignable(n))
80 : : {
81 [ + - ]: 428304 : Trace("model-builder-debug") << "...try to normalize" << std::endl;
82 : 428304 : Node normalized = normalize(m, n, true);
83 [ + - ]: 856608 : Trace("model-builder-debug")
84 : 0 : << "...return " << normalized
85 [ - + ][ - - ]: 428304 : << ", isValue=" << m->isValue(normalized) << std::endl;
86 [ + + ]: 428304 : if (m->isValue(normalized))
87 : : {
88 : 415537 : return normalized;
89 : : }
90 [ + + ]: 428304 : }
91 [ + + ]: 429523 : }
92 : 9385 : return Node::null();
93 : : }
94 : :
95 : 47 : bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
96 : : {
97 [ + + ]: 47 : if (a.d_isActive)
98 : : {
99 : 35 : return true;
100 : : }
101 : 12 : std::vector<Node>& eset = a.d_assignExcSet;
102 : 12 : std::map<Node, Node>::iterator it;
103 [ + + ]: 34 : for (unsigned i = 0, size = eset.size(); i < size; i++)
104 : : {
105 : : // Members of exclusion set must have values, otherwise we are not yet
106 : : // assignable.
107 : 22 : Node er = eset[i];
108 [ + + ]: 22 : if (tm->isValue(er))
109 : : {
110 : : // already processed
111 : 16 : continue;
112 : : }
113 : : // Assignable members of assignment exclusion set should be representatives
114 : : // of their equivalence classes. This ensures we look up the constant
115 : : // representatives for assignable members of assignment exclusion sets.
116 [ - + ][ - + ]: 6 : Assert(er == tm->getRepresentative(er));
[ - - ]
117 : 6 : it = d_constantReps.find(er);
118 [ - + ]: 6 : if (it == d_constantReps.end())
119 : : {
120 [ - - ]: 0 : Trace("model-build-aes")
121 : 0 : << "isAssignerActive: not active due to " << er << std::endl;
122 : 0 : return false;
123 : : }
124 : : // update
125 : 6 : eset[i] = it->second;
126 [ + + ][ - ]: 22 : }
127 [ + - ]: 12 : Trace("model-build-aes") << "isAssignerActive: active!" << std::endl;
128 : 12 : a.d_isActive = true;
129 : 12 : return true;
130 : : }
131 : :
132 : 6039404 : bool TheoryEngineModelBuilder::isAssignable(TNode n)
133 : : {
134 : 6039404 : Kind k = n.getKind();
135 [ + + ][ + + ]: 6039404 : if (k == Kind::SELECT || k == Kind::APPLY_SELECTOR || k == Kind::SEQ_NTH)
[ + + ]
136 : : {
137 : : // selectors are always assignable (where we guarantee that they are not
138 : : // evaluatable here)
139 [ + + ]: 489779 : if (!logicInfo().isHigherOrder())
140 : : {
141 [ - + ][ - + ]: 488009 : Assert(!n.getType().isFunction());
[ - - ]
142 : 488009 : return true;
143 : : }
144 : : else
145 : : {
146 : : // might be a function field
147 : 1770 : return !n.getType().isFunction();
148 : : }
149 : : }
150 [ + + ][ + + ]: 5549625 : else if (k == Kind::FLOATINGPOINT_COMPONENT_SIGN || k == Kind::SEP_NIL)
151 : : {
152 : : // - Extracting the sign of a floating-point number acts similar to a
153 : : // selector on a datatype, i.e. if `(sign x)` wasn't assigned a value, we
154 : : // can pick an arbitrary one. Note that the other components of a
155 : : // floating-point number should always be assigned a value.
156 : : // - sep.nil is a nullary constant that acts like a variable and thus is
157 : : // assignable.
158 : 3108 : return true;
159 : : }
160 : : else
161 : : {
162 : : // non-function variables, and fully applied functions
163 [ + + ]: 5546517 : if (!logicInfo().isHigherOrder())
164 : : {
165 : : // no functions exist, all functions are fully applied
166 [ - + ][ - + ]: 4850324 : Assert(k != Kind::HO_APPLY);
[ - - ]
167 [ - + ][ - + ]: 4850324 : Assert(!n.getType().isFunction());
[ - - ]
168 [ + + ][ + + ]: 4850324 : return n.isVar() || k == Kind::APPLY_UF;
169 : : }
170 : : else
171 : : {
172 [ + + ][ + + ]: 1392386 : return (n.isVar() && !n.getType().isFunction()) || k == Kind::APPLY_UF
[ - - ]
173 : 1392386 : || (k == Kind::HO_APPLY && n[0].getType().getNumChildren() == 2);
174 : : }
175 : : }
176 : : }
177 : :
178 : 5751829 : void TheoryEngineModelBuilder::addAssignableSubterms(TNode n,
179 : : TheoryModel* tm,
180 : : NodeSet& cache)
181 : : {
182 [ + + ]: 5751829 : if (n.isClosure())
183 : : {
184 : 81847 : return;
185 : : }
186 [ + + ]: 5669982 : if (cache.find(n) != cache.end())
187 : : {
188 : 2664088 : return;
189 : : }
190 [ + + ]: 3005894 : if (isAssignable(n))
191 : : {
192 : 1274724 : tm->d_equalityEngine->addTerm(n);
193 : : }
194 [ + + ]: 6153791 : for (TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it)
195 : : {
196 : 3147897 : addAssignableSubterms(*child_it, tm, cache);
197 : : }
198 : 3005894 : cache.insert(n);
199 : : }
200 : :
201 : 1237896 : void TheoryEngineModelBuilder::assignConstantRep(TheoryModel* tm,
202 : : Node eqc,
203 : : Node constRep)
204 : : {
205 : 1237896 : d_constantReps[eqc] = constRep;
206 [ + - ]: 2475792 : Trace("model-builder") << " Assign: Setting constant rep of " << eqc
207 : 1237896 : << " to " << constRep << endl;
208 : 1237896 : tm->d_rep_set.setTermForRepresentative(constRep, eqc);
209 : 1237896 : }
210 : :
211 : 49 : bool TheoryEngineModelBuilder::isExcludedCdtValue(
212 : : Node val,
213 : : std::set<Node>* repSet,
214 : : std::map<Node, Node>& assertedReps,
215 : : Node eqc)
216 : : {
217 [ + - ]: 98 : Trace("model-builder-debug")
218 : 0 : << "Is " << val << " and excluded codatatype value for " << eqc << "? "
219 : 49 : << std::endl;
220 [ + + ]: 103 : for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i)
221 : : {
222 [ - + ][ - + ]: 72 : Assert(assertedReps.find(*i) != assertedReps.end());
[ - - ]
223 : 72 : Node rep = assertedReps[*i];
224 [ + - ]: 72 : Trace("model-builder-debug") << " Rep : " << rep << std::endl;
225 : : // check whether it is possible that rep will be assigned the same value
226 : : // as val.
227 [ + + ]: 72 : if (isCdtValueMatch(val, rep))
228 : : {
229 : 18 : return true;
230 : : }
231 [ + + ]: 72 : }
232 : 31 : return false;
233 : : }
234 : :
235 : 170 : bool TheoryEngineModelBuilder::isCdtValueMatch(Node v, Node r)
236 : : {
237 [ + + ]: 170 : if (r == v)
238 : : {
239 : : // values equal match trivially
240 : 40 : return true;
241 : : }
242 [ + - ][ + + ]: 130 : else if (v.isConst() && r.isConst())
[ + + ]
243 : : {
244 : : // distinct constant values do not match
245 : 8 : return false;
246 : : }
247 [ + + ]: 122 : else if (r.getKind() == Kind::APPLY_CONSTRUCTOR)
248 : : {
249 [ - + ]: 72 : if (v.getKind() != Kind::APPLY_CONSTRUCTOR)
250 : : {
251 : 0 : Assert(v.getKind() == Kind::CODATATYPE_BOUND_VARIABLE);
252 : : // v is the position of a loop. It may be possible to match, we return
253 : : // true, which is an over-approximation of when it is unsafe to use v.
254 : 0 : return true;
255 : : }
256 [ + + ]: 72 : if (v.getOperator() == r.getOperator())
257 : : {
258 [ + + ]: 116 : for (size_t i = 0, nchild = v.getNumChildren(); i < nchild; i++)
259 : : {
260 [ + + ]: 98 : if (!isCdtValueMatch(v[i], r[i]))
261 : : {
262 : : // if one child fails to match, we cannot match
263 : 40 : return false;
264 : : }
265 : : }
266 : 18 : return true;
267 : : }
268 : : // operators do not match
269 : 14 : return false;
270 : : }
271 [ + + ]: 50 : else if (v.getKind() == Kind::APPLY_CONSTRUCTOR)
272 : : {
273 : : // v has a constructor in a position that we have yet to fill in r.
274 : : // we are either a finite type in which case this subfield of r can be
275 : : // assigned a default value (or otherwise would have been split on).
276 : : // otherwise we are an infinite type and the subfield of r will be
277 : : // chosen not to clash with the subfield of v.
278 : 32 : return false;
279 : : }
280 : 18 : return true;
281 : : }
282 : :
283 : 1203 : bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) const
284 : : {
285 [ + + ]: 1203 : if (tn.isUninterpretedSort())
286 : : {
287 : 4 : return true;
288 : : }
289 [ + + ]: 1199 : else if (tn.isArray())
290 : : {
291 [ - - ]: 20 : return involvesUSort(tn.getArrayIndexType())
292 [ + - ][ - + ]: 20 : || involvesUSort(tn.getArrayConstituentType());
[ + - ][ + - ]
[ - - ]
293 : : }
294 [ + + ]: 1179 : else if (tn.isSet())
295 : : {
296 : 4 : return involvesUSort(tn.getSetElementType());
297 : : }
298 [ + + ]: 1175 : else if (tn.isDatatype())
299 : : {
300 : 1071 : const DType& dt = tn.getDType();
301 : 1071 : return dt.involvesUninterpretedType();
302 : : }
303 : : else
304 : : {
305 : 104 : return false;
306 : : }
307 : : }
308 : :
309 : 3707 : bool TheoryEngineModelBuilder::isExcludedUSortValue(
310 : : std::map<TypeNode, unsigned>& eqc_usort_count,
311 : : Node v,
312 : : std::map<Node, bool>& visited)
313 : : {
314 [ - + ][ - + ]: 3707 : Assert(v.isConst());
[ - - ]
315 [ + + ]: 3707 : if (visited.find(v) == visited.end())
316 : : {
317 : 3268 : visited[v] = true;
318 : 3268 : TypeNode tn = v.getType();
319 [ + + ]: 3268 : if (tn.isUninterpretedSort())
320 : : {
321 [ + - ]: 266 : Trace("model-builder-debug")
322 : 133 : << "Is excluded usort value : " << v << " " << tn << std::endl;
323 : 133 : unsigned card = eqc_usort_count[tn];
324 [ + - ]: 133 : Trace("model-builder-debug") << " Cardinality is " << card << std::endl;
325 : : unsigned index =
326 : 133 : v.getConst<UninterpretedSortValue>().getIndex().toUnsignedInt();
327 [ + - ]: 133 : Trace("model-builder-debug") << " Index is " << index << std::endl;
328 [ - + ][ - - ]: 133 : return index > 0 && index >= card;
329 : : }
330 [ + + ]: 5929 : for (unsigned i = 0; i < v.getNumChildren(); i++)
331 : : {
332 [ - + ]: 2794 : if (isExcludedUSortValue(eqc_usort_count, v[i], visited))
333 : : {
334 : 0 : return true;
335 : : }
336 : : }
337 [ + + ]: 3268 : }
338 : 3574 : return false;
339 : : }
340 : :
341 : 923792 : void TheoryEngineModelBuilder::addToTypeList(
342 : : TypeNode tn,
343 : : std::vector<TypeNode>& type_list,
344 : : std::unordered_set<TypeNode>& visiting)
345 : : {
346 [ + + ]: 923792 : if (std::find(type_list.begin(), type_list.end(), tn) == type_list.end())
347 : : {
348 [ + + ]: 292742 : if (visiting.find(tn) == visiting.end())
349 : : {
350 : 55771 : visiting.insert(tn);
351 : : /* This must make a recursive call on all types that are subterms of
352 : : * values of the current type.
353 : : * Note that recursive traversal here is over enumerated expressions
354 : : * (very low expression depth). */
355 [ + + ]: 55771 : if (tn.isArray())
356 : : {
357 : 570 : addToTypeList(tn.getArrayIndexType(), type_list, visiting);
358 : 570 : addToTypeList(tn.getArrayConstituentType(), type_list, visiting);
359 : : }
360 [ + + ]: 55201 : else if (tn.isSet())
361 : : {
362 : 1422 : addToTypeList(tn.getSetElementType(), type_list, visiting);
363 : : }
364 [ + + ]: 53779 : else if (tn.isDatatype())
365 : : {
366 : 22694 : const DType& dt = tn.getDType();
367 [ + + ]: 150668 : for (unsigned i = 0; i < dt.getNumConstructors(); i++)
368 : : {
369 : : // Note that we may be a parameteric datatype, in which case the
370 : : // instantiated sorts need to be considered.
371 : 127974 : TypeNode ctn = dt[i].getInstantiatedConstructorType(tn);
372 [ + + ]: 389728 : for (const TypeNode& ctnc : ctn)
373 : : {
374 : 261754 : addToTypeList(ctnc, type_list, visiting);
375 : 261754 : }
376 : 127974 : }
377 : : }
378 [ - + ][ - + ]: 55771 : Assert(std::find(type_list.begin(), type_list.end(), tn)
[ - - ]
379 : : == type_list.end());
380 : 55771 : type_list.push_back(tn);
381 : : }
382 : : }
383 : 923792 : }
384 : :
385 : 35585 : bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
386 : : {
387 [ + - ]: 35585 : Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
388 : :
389 [ + - ]: 71170 : Trace("model-builder")
390 : 35585 : << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl;
391 : : // model-builder specific initialization
392 [ - + ]: 35585 : if (!preProcessBuildModel(tm))
393 : : {
394 [ - - ]: 0 : Trace("model-builder")
395 : 0 : << "TheoryEngineModelBuilder: fail preprocess build model."
396 : 0 : << std::endl;
397 : 0 : return false;
398 : : }
399 : :
400 [ + - ]: 71170 : Trace("model-builder")
401 : : << "TheoryEngineModelBuilder: Add assignable subterms "
402 : 0 : ", collect representatives and compute assignable information..."
403 : 35585 : << std::endl;
404 : :
405 : : // type enumerator properties
406 : 35585 : bool tepFixUSortCard = options().quantifiers.finiteModelFind;
407 : 35585 : uint32_t tepStrAlphaCard = options().strings.stringsAlphaCard;
408 : 35585 : TypeEnumeratorProperties tep(tepFixUSortCard, tepStrAlphaCard);
409 : :
410 : : // In the first step of model building, we do a traversal of the
411 : : // equality engine and record the information in the following:
412 : :
413 : : // The constant representatives, per equivalence class
414 : 35585 : d_constantReps.clear();
415 : : // The representatives that have been asserted by theories. This includes
416 : : // non-constant "skeletons" that have been specified by parametric theories.
417 : 35585 : std::map<Node, Node> assertedReps;
418 : : // A parition of the set of equivalence classes that have:
419 : : // (1) constant representatives,
420 : : // (2) an assigned representative specified by a theory in collectModelInfo,
421 : : // (3) no assigned representative.
422 : 35585 : TypeSet typeConstSet, typeRepSet, typeNoRepSet;
423 : : // An ordered list of types, such that T1 comes before T2 if T1 is a
424 : : // "component type" of T2, e.g. U comes before (Set U). This is only strictly
425 : : // necessary for finite model finding + parametric types instantiated with
426 : : // uninterpreted sorts, but is probably a good idea to do in general since it
427 : : // leads to models with smaller term sizes. -AJR
428 : 35585 : std::vector<TypeNode> type_list;
429 : : // The count of equivalence classes per sort (for finite model finding).
430 : 35585 : std::map<TypeNode, unsigned> eqc_usort_count;
431 : :
432 : : // the set of equivalence classes that are "assignable", i.e. those that have
433 : : // an assignable expression in them (see isAssignable), and have not already
434 : : // been assigned a constant.
435 : 35585 : std::unordered_set<Node> assignableEqc;
436 : : // The set of equivalence classes that are "evaluable", i.e. those that have
437 : : // an expression in them that is not assignable, and have not already been
438 : : // assigned a constant.
439 : 35585 : std::unordered_set<Node> evaluableEqc;
440 : : // Assigner objects for relevant equivalence classes that require special
441 : : // ways of assigning values, e.g. those that take into account assignment
442 : : // exclusion sets.
443 : 35585 : std::map<Node, Assigner> eqcToAssigner;
444 : : // A map from equivalence classes to the equivalence class that it shares an
445 : : // assigner object with (all elements in the range of this map are in the
446 : : // domain of eqcToAssigner).
447 : 35585 : std::map<Node, Node> eqcToAssignerMaster;
448 : :
449 : : // Loop through equivalence classes of the equality engine of the model.
450 : 35585 : eq::EqualityEngine* ee = tm->d_equalityEngine;
451 : 35585 : NodeSet assignableCache;
452 : 35585 : std::map<Node, Node>::iterator itm;
453 : 35585 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
454 : : // should we compute assigner objects?
455 : 35585 : bool computeAssigners = tm->hasAssignmentExclusionSets();
456 : : // the set of exclusion sets we have processed
457 : 35585 : std::unordered_set<Node> processedExcSet;
458 [ + + ]: 1279228 : for (; !eqcs_i.isFinished(); ++eqcs_i)
459 : : {
460 : 1243643 : Node eqc = *eqcs_i;
461 [ + - ]: 1243643 : Trace("model-builder") << " Processing EQC " << eqc << std::endl;
462 : : // Information computed for each equivalence class
463 : :
464 : : // The assigned represenative and constant representative
465 : 1243643 : Node rep, constRep;
466 : : // is constant rep a "base model value" (see TheoryModel::isBaseModelValue)
467 : 1243643 : bool constRepBaseModelValue = false;
468 : : // A flag set to true if the current equivalence class is assignable (see
469 : : // assignableEqc).
470 : 1243643 : bool assignable = false;
471 : : // Set to true if the current equivalence class is evaluatable (see
472 : : // evaluableEqc).
473 : 1243643 : bool evaluable = false;
474 : : // Set to true if a term in the current equivalence class has been given an
475 : : // assignment exclusion set.
476 : 1243643 : bool hasESet CVC5_UNUSED = false;
477 : : // Set to true if we found that a term in the current equivalence class has
478 : : // been given an assignment exclusion set, and we have not seen this term
479 : : // as part of a previous assignment exclusion group. In other words, when
480 : : // this flag is true we construct a new assigner object with the current
481 : : // equivalence class as its master.
482 : 1243643 : bool foundESet = false;
483 : : // The assignment exclusion set for the current equivalence class.
484 : 1243643 : std::vector<Node> eset;
485 : : // The group to which this equivalence class belongs when exclusion sets
486 : : // were assigned (see the argument group of
487 : : // TheoryModel::getAssignmentExclusionSet).
488 : 1243643 : std::vector<Node> esetGroup;
489 : :
490 : : // Loop through terms in this EC
491 : 1243643 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
492 [ + + ]: 3847575 : for (; !eqc_i.isFinished(); ++eqc_i)
493 : : {
494 : 2603932 : Node n = *eqc_i;
495 [ + - ]: 2603932 : Trace("model-builder") << " Processing Term: " << n << endl;
496 : :
497 : : // For each term n in this equivalence class, below we register its
498 : : // assignable subterms, compute whether it is a constant or assigned
499 : : // representative, then if we don't have a constant representative,
500 : : // compute information regarding how we will assign values.
501 : :
502 : : // (1) Add assignable subterms, which ensures that e.g. models for
503 : : // uninterpreted functions take into account all subterms in the
504 : : // equality engine of the model
505 : 2603932 : addAssignableSubterms(n, tm, assignableCache);
506 : : // model-specific processing of the term
507 : 2603932 : tm->addTermInternal(n);
508 : :
509 : : // compute whether n is assignable
510 [ + + ]: 2603932 : if (!isAssignable(n))
511 : : {
512 : : // (2) Record constant representative or assign representative, if
513 : : // applicable. We check if n is a value here, e.g. a term for which
514 : : // isConst returns true, or a lambda. The latter is required only for
515 : : // higher-order.
516 [ + + ]: 1329208 : if (tm->isValue(n))
517 : : {
518 : : // In some cases, there can be multiple terms in the same equivalence
519 : : // class are considered values, e.g., when real algebraic numbers did
520 : : // not simplify to rational values or real.pi was used as a model
521 : : // value. We distinguish three kinds of model values: constants,
522 : : // non-constant base values and non-base values, and we use them in
523 : : // this order of preference.
524 : : // We print a trace message if there is more than one model value in
525 : : // the same equivalence class. We throw a debug failure if there are
526 : : // at least two base model values in the same equivalence class that
527 : : // do not compare equal.
528 : 578874 : bool assignConstRep = false;
529 : 578874 : bool isBaseValue = tm->isBaseModelValue(n);
530 [ + + ]: 578874 : if (constRep.isNull())
531 : : {
532 : 578866 : assignConstRep = true;
533 : : }
534 : : else
535 : : {
536 : : // This is currently a trace message, as it often triggers for
537 : : // non-linear arithmetic before the model is refined enough to
538 : : // e.g. show transcendental function apps are not equal to rationals
539 [ + - ]: 16 : Trace("model-warn") << "Model values in the same equivalence class "
540 : 8 : << constRep << " " << n << std::endl;
541 [ - + ]: 8 : if (!constRepBaseModelValue)
542 : : {
543 : 0 : assignConstRep = isBaseValue;
544 : : }
545 [ + + ]: 8 : else if (isBaseValue)
546 : : {
547 : 2 : Node isEqual = rewrite(constRep.eqNode(n));
548 [ + - ][ + - ]: 1 : if (isEqual.isConst() && isEqual.getConst<bool>())
[ + - ]
549 : : {
550 : 1 : assignConstRep = n.isConst();
551 : : }
552 : : else
553 : : {
554 : 0 : DebugUnhandled() << "Distinct base model values in the same "
555 : 0 : "equivalence class "
556 : 0 : << constRep << " " << n << std::endl;
557 : : }
558 : 1 : }
559 : : }
560 [ + + ]: 578874 : if (assignConstRep)
561 : : {
562 : 578866 : constRep = n;
563 [ + - ]: 1157732 : Trace("model-builder") << " ..ConstRep( " << eqc
564 : 578866 : << " ) = " << constRep << std::endl;
565 : 578866 : constRepBaseModelValue = isBaseValue;
566 : : }
567 : : // if we have a constant representative, nothing else matters
568 : 578874 : continue;
569 : 578874 : }
570 : :
571 : : // If we don't have a constant rep, check if this is an assigned rep.
572 : 750334 : itm = tm->d_reps.find(n);
573 [ + + ]: 750334 : if (itm != tm->d_reps.end())
574 : : {
575 : : // Notice that this equivalence class may contain multiple terms that
576 : : // were specified as being a representative, since e.g. datatypes may
577 : : // assert representative for two constructor terms that are not in the
578 : : // care graph and are merged during collectModeInfo due to equality
579 : : // information from another theory. We overwrite the value of rep in
580 : : // these cases here.
581 : 72506 : rep = itm->second;
582 [ + - ]: 145012 : Trace("model-builder")
583 : 72506 : << " ..Rep( " << eqc << " ) = " << rep << std::endl;
584 : : }
585 : :
586 : : // (3) Finally, process assignable information
587 : : // We are evaluable typically if we are not assignable. However the
588 : : // one exception is that higher-order variables when in HOL should be
589 : : // considered neither assignable nor evaluable, which we check for here.
590 : 750334 : evaluable = !n.isVar();
591 : : // expressions that are not assignable should not be given assignment
592 : : // exclusion sets
593 [ - + ][ - + ]: 750334 : Assert(!tm->getAssignmentExclusionSet(n, esetGroup, eset));
[ - - ]
594 : 750334 : continue;
595 : 750334 : }
596 : 1274724 : assignable = true;
597 [ + + ]: 1274724 : if (!computeAssigners)
598 : : {
599 : : // we don't compute assigners, skip
600 : 1274477 : continue;
601 : : }
602 : : // process the assignment exclusion set for term n
603 : : // was it processed based on a master exclusion group (see
604 : : // eqcToAssignerMaster)?
605 [ + + ]: 247 : if (processedExcSet.find(n) != processedExcSet.end())
606 : : {
607 : : // Should not have two assignment exclusion sets for the same
608 : : // equivalence class
609 [ - + ][ - + ]: 35 : Assert(!hasESet);
[ - - ]
610 [ - + ][ - + ]: 35 : Assert(eqcToAssignerMaster.find(eqc) != eqcToAssignerMaster.end());
[ - - ]
611 : : // already processed as a slave term
612 : 35 : hasESet = true;
613 : 35 : continue;
614 : : }
615 : : // was it assigned one?
616 [ + + ]: 212 : if (tm->getAssignmentExclusionSet(n, esetGroup, eset))
617 : : {
618 : : // Should not have two assignment exclusion sets for the same
619 : : // equivalence class
620 [ - + ][ - + ]: 12 : Assert(!hasESet);
[ - - ]
621 : 12 : foundESet = true;
622 : 12 : hasESet = true;
623 : : }
624 [ + + ]: 2603932 : }
625 : :
626 : : // finished traversing the equality engine
627 : 1243643 : TypeNode eqct = eqc.getType();
628 : : // count the number of equivalence classes of sorts in finite model finding
629 [ + + ]: 1243643 : if (options().quantifiers.finiteModelFind)
630 : : {
631 [ + + ]: 19551 : if (eqct.isUninterpretedSort())
632 : : {
633 : : // we never assign uninterpreted sorts a priori.
634 [ - + ][ - + ]: 5301 : Assert(constRep.isNull());
[ - - ]
635 : 5301 : eqc_usort_count[eqct]++;
636 : : // For uninterpreted sorts when finite model finding is enabled,
637 : : // we preemptively assign the next value in the enumeration here.
638 : : // This is important because uninterpreted sorts are considered
639 : : // "INTERPRETED_FINITE" cardinality when finite model finding is
640 : : // enabled, and hence would otherwise be assigned using the finite
641 : : // case below (assigning them to the first value), which we do not
642 : : // want. Instead, all initial equivalence classes of uninterpreted
643 : : // sorts are assigned distinct values, and all further values
644 : : // (e.g. terms introduced as subfields of datatypes) are assign
645 : : // arbitrary values.
646 : 5301 : constRep = typeConstSet.nextTypeEnum(eqct);
647 [ + - ]: 10602 : Trace("model-value-enum") << "Enum fmf usort " << eqct << " "
648 : 5301 : << constRep << " for " << eqc << std::endl;
649 : : }
650 : : }
651 : : // Assign representative for this equivalence class
652 [ + + ]: 1243643 : if (!constRep.isNull())
653 : : {
654 : : // Theories should not specify a rep if there is already a constant in the
655 : : // equivalence class. However, it may be the case that the representative
656 : : // specified by a theory may be merged with a constant based on equality
657 : : // information from another class. Thus, rep may be non-null here.
658 : : // Regardless, we assign constRep as the representative here.
659 : 584167 : assignConstantRep(tm, eqc, constRep);
660 : 584167 : typeConstSet.add(eqct, constRep);
661 : 584167 : continue;
662 : : }
663 [ + + ]: 659476 : else if (!rep.isNull())
664 : : {
665 : 72325 : assertedReps[eqc] = rep;
666 : 72325 : typeRepSet.add(eqct, eqc);
667 : 72325 : std::unordered_set<TypeNode> visiting;
668 : 72325 : addToTypeList(eqct, type_list, visiting);
669 : 72325 : }
670 : : else
671 : : {
672 : 587151 : typeNoRepSet.add(eqct, eqc);
673 : 587151 : std::unordered_set<TypeNode> visiting;
674 : 587151 : addToTypeList(eqct, type_list, visiting);
675 : 587151 : }
676 : :
677 [ + + ]: 659476 : if (assignable)
678 : : {
679 : 238346 : assignableEqc.insert(eqc);
680 : : }
681 [ + + ]: 659476 : if (evaluable)
682 : : {
683 : 490722 : evaluableEqc.insert(eqc);
684 : : }
685 : : // If we found an assignment exclusion set, we construct a new assigner
686 : : // object.
687 [ + + ]: 659476 : if (foundESet)
688 : : {
689 : : // we don't accept assignment exclusion sets for evaluable eqc
690 [ - + ][ - + ]: 12 : Assert(!evaluable);
[ - - ]
691 : : // construct the assigner
692 : 12 : Assigner& a = eqcToAssigner[eqc];
693 : : // Take the representatives of each term in the assignment exclusion
694 : : // set, which ensures we can look up their value in d_constReps later.
695 : 12 : std::vector<Node> aes;
696 [ + + ]: 34 : for (const Node& e : eset)
697 : : {
698 : : // Should only supply terms that occur in the model or constants
699 : : // in assignment exclusion sets.
700 : 22 : Assert(tm->hasTerm(e) || e.isConst());
701 [ + - ][ + - ]: 44 : Node er = tm->hasTerm(e) ? tm->getRepresentative(e) : e;
[ - - ]
702 : 22 : aes.push_back(er);
703 : 22 : }
704 : : // initialize
705 : 12 : a.initialize(eqc.getType(), &tep, aes);
706 : : // all others in the group are slaves of this
707 [ + + ]: 59 : for (const Node& g : esetGroup)
708 : : {
709 [ - + ][ - + ]: 47 : Assert(isAssignable(g));
[ - - ]
710 [ - + ]: 47 : if (!tm->hasTerm(g))
711 : : {
712 : : // Ignore those that aren't in the model, in the case the user
713 : : // has supplied an assignment exclusion set to a variable not in
714 : : // the model.
715 : 0 : continue;
716 : : }
717 : 47 : Node gr = tm->getRepresentative(g);
718 [ + + ]: 47 : if (gr != eqc)
719 : : {
720 : 35 : eqcToAssignerMaster[gr] = eqc;
721 : : // remember that this term has been processed
722 : 35 : processedExcSet.insert(g);
723 : : }
724 : 47 : }
725 : 12 : }
726 [ + + ][ + + ]: 4164478 : }
[ + + ][ + + ]
[ + + ][ + + ]
727 : :
728 : : // Now finished initialization
729 : :
730 : : // Compute type enumerator properties. This code ensures we do not
731 : : // enumerate terms that have uninterpreted constants that violate the
732 : : // bounds imposed by finite model finding. For example, if finite
733 : : // model finding insists that there are only 2 values { U1, U2 } of type U,
734 : : // then the type enumerator for list of U should enumerate:
735 : : // nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ...
736 : : // instead of enumerating (cons U3 nil).
737 [ + + ]: 35585 : if (options().quantifiers.finiteModelFind)
738 : : {
739 : 1557 : tep.d_fixed_usort_card = true;
740 : 1557 : for (std::map<TypeNode, unsigned>::iterator it = eqc_usort_count.begin();
741 [ + + ]: 4465 : it != eqc_usort_count.end();
742 : 2908 : ++it)
743 : : {
744 [ + - ]: 5816 : Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : "
745 : 2908 : << it->second << std::endl;
746 : 2908 : tep.d_fixed_card[it->first] = Integer(it->second);
747 : : }
748 : 1557 : typeConstSet.setTypeEnumeratorProperties(&tep);
749 : : }
750 : :
751 : : // Need to ensure that each EC has a constant representative.
752 : :
753 [ + - ]: 35585 : Trace("model-builder") << "Processing EC's..." << std::endl;
754 : :
755 : 35585 : TypeSet::iterator it;
756 : 35585 : vector<TypeNode>::iterator type_it;
757 : 35585 : set<Node>::iterator i, i2;
758 : 35585 : bool changed, unassignedAssignable, assignOne = false;
759 : 35585 : set<TypeNode> evaluableSet;
760 : :
761 : : // Double-fixed-point loop
762 : : // Outer loop handles a special corner case (see code at end of loop for
763 : : // details)
764 : : for (;;)
765 : : {
766 : : // Inner fixed-point loop: we are trying to learn constant values for every
767 : : // EC. Each time through this loop, we process all of the
768 : : // types by type and may learn some new EC values. EC's in one type may
769 : : // depend on EC's in another type, so we need a fixed-point loop
770 : : // to ensure that we learn as many EC values as possible
771 [ + + ]: 217444 : do
772 : : {
773 : 217444 : changed = false;
774 : 217444 : unassignedAssignable = false;
775 : 217444 : evaluableSet.clear();
776 : :
777 : : // Iterate over all types we've seen
778 [ + + ]: 974748 : for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
779 : : {
780 : 757304 : TypeNode t = *type_it;
781 : 757304 : TypeNode tb = t;
782 : 757304 : set<Node>* noRepSet = typeNoRepSet.getSet(t);
783 : :
784 : : // 1. Try to evaluate the EC's in this type
785 [ + + ][ + + ]: 757304 : if (noRepSet != nullptr && !noRepSet->empty())
[ + + ]
786 : : {
787 [ + - ]: 567344 : Trace("model-builder")
788 : 283672 : << " Eval phase, working on type: " << t << endl;
789 : : bool evaluable;
790 : 283672 : d_normalizedCache.clear();
791 [ + + ]: 3056453 : for (i = noRepSet->begin(); i != noRepSet->end();)
792 : : {
793 : 2772781 : i2 = i;
794 : 2772781 : ++i;
795 [ + - ]: 5545562 : Trace("model-builder-debug")
796 : 2772781 : << "Look at eqc : " << (*i2) << std::endl;
797 : 2772781 : Node normalized;
798 : : // only possible to normalize if we are evaluable
799 : 2772781 : evaluable = evaluableEqc.find(*i2) != evaluableEqc.end();
800 [ + + ]: 2772781 : if (evaluable)
801 : : {
802 : 424922 : normalized = evaluateEqc(tm, *i2);
803 : : }
804 [ + + ]: 2772781 : if (!normalized.isNull())
805 : : {
806 [ - + ][ - + ]: 415537 : Assert(tm->isValue(normalized));
[ - - ]
807 : 415537 : typeConstSet.add(tb, normalized);
808 : 415537 : assignConstantRep(tm, *i2, normalized);
809 [ + - ]: 831074 : Trace("model-builder") << " Eval: Setting constant rep of "
810 : 415537 : << (*i2) << " to " << normalized << endl;
811 : 415537 : changed = true;
812 : 415537 : noRepSet->erase(i2);
813 : : }
814 : : else
815 : : {
816 [ + + ]: 2357244 : if (evaluable)
817 : : {
818 : 9385 : evaluableSet.insert(tb);
819 : : }
820 : : // If assignable, remember there is an equivalence class that is
821 : : // not assigned and assignable.
822 [ + + ]: 2357244 : if (assignableEqc.find(*i2) != assignableEqc.end())
823 : : {
824 : 2342554 : unassignedAssignable = true;
825 : : }
826 : : }
827 : 2772781 : }
828 : : }
829 : :
830 : : // 2. Normalize any non-const representative terms for this type
831 : 757304 : set<Node>* repSet = typeRepSet.getSet(t);
832 [ + + ][ + + ]: 757304 : if (repSet != nullptr && !repSet->empty())
[ + + ]
833 : : {
834 [ + - ]: 667190 : Trace("model-builder")
835 : 333595 : << " Normalization phase, working on type: " << t << endl;
836 : 333595 : d_normalizedCache.clear();
837 [ + + ]: 2291821 : for (i = repSet->begin(); i != repSet->end();)
838 : : {
839 [ - + ][ - + ]: 1958226 : Assert(assertedReps.find(*i) != assertedReps.end());
[ - - ]
840 : 1958226 : Node rep = assertedReps[*i];
841 : 1958226 : Node normalized = normalize(tm, rep, false);
842 [ + - ]: 3916452 : Trace("model-builder")
843 : 0 : << " Normalizing rep (" << rep << "), normalized to ("
844 : 0 : << normalized << ")"
845 [ - + ][ - - ]: 1958226 : << ", isValue=" << tm->isValue(normalized) << std::endl;
846 [ + + ]: 1958226 : if (tm->isValue(normalized))
847 : : {
848 : 72325 : changed = true;
849 : 72325 : typeConstSet.add(tb, normalized);
850 : 72325 : assignConstantRep(tm, *i, normalized);
851 : 72325 : assertedReps.erase(*i);
852 : 72325 : i2 = i;
853 : 72325 : ++i;
854 : 72325 : repSet->erase(i2);
855 : : }
856 : : else
857 : : {
858 [ + + ]: 1885901 : if (normalized != rep)
859 : : {
860 : 41638 : assertedReps[*i] = normalized;
861 : 41638 : changed = true;
862 : : }
863 : 1885901 : ++i;
864 : : }
865 : 1958226 : }
866 : : }
867 : 757304 : }
868 : : } while (changed);
869 : :
870 [ + + ]: 138637 : if (!unassignedAssignable)
871 : : {
872 : 35585 : break;
873 : : }
874 : :
875 : : // 3. Assign unassigned assignable EC's using type enumeration - assign a
876 : : // value *different* from all other EC's if the type is infinite
877 : : // Assign first value from type enumerator otherwise - for finite types, we
878 : : // rely on polite framework to ensure that EC's that have to be
879 : : // different are different.
880 : :
881 : : // Only make assignments on a type if:
882 : : // 1. there are no terms that share the same base type with un-normalized
883 : : // representatives
884 : : // 2. there are no terms that share teh same base type that are unevaluated
885 : : // evaluable terms
886 : : // Alternatively, if 2 or 3 don't hold but we are in a special
887 : : // deadlock-breaking mode where assignOne is true, go ahead and make one
888 : : // assignment
889 : 103052 : changed = false;
890 : : // must iterate over the ordered type list to ensure that we do not
891 : : // enumerate values with subterms
892 : : // having types that we are currently enumerating (when possible)
893 : : // for example, this ensures we enumerate uninterpreted sort U before (List
894 : : // of U) and (Array U U)
895 : : // however, it does not break cyclic type dependencies for mutually
896 : : // recursive datatypes, but this is handled
897 : : // by recording all subterms of enumerated values in TypeSet::addSubTerms.
898 [ + + ]: 509844 : for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
899 : : {
900 : 406792 : TypeNode t = *type_it;
901 : : // continue if there are no more equivalence classes of this type to
902 : : // assign
903 : 406792 : std::set<Node>* noRepSetPtr = typeNoRepSet.getSet(t);
904 [ + + ]: 406792 : if (noRepSetPtr == nullptr)
905 : : {
906 : 38149 : continue;
907 : : }
908 : 368643 : set<Node>& noRepSet = *noRepSetPtr;
909 [ + + ]: 368643 : if (noRepSet.empty())
910 : : {
911 : 205030 : continue;
912 : : }
913 : :
914 : : // get properties of this type
915 : 163613 : bool isCorecursive = false;
916 [ + + ]: 163613 : if (t.isDatatype())
917 : : {
918 : 154323 : const DType& dt = t.getDType();
919 : 154323 : isCorecursive =
920 : 308646 : dt.isCodatatype()
921 : 154323 : && (!d_env.isFiniteType(t) || dt.isRecursiveSingleton(t));
922 : : }
923 : : #ifdef CVC5_ASSERTIONS
924 : 163613 : bool isUSortFiniteRestricted = false;
925 [ + + ]: 163613 : if (options().quantifiers.finiteModelFind)
926 : : {
927 [ + - ][ + + ]: 1159 : isUSortFiniteRestricted = !t.isUninterpretedSort() && involvesUSort(t);
[ + - ][ - - ]
928 : : }
929 : : #endif
930 : :
931 : 163613 : TypeNode tb = t;
932 [ + + ]: 163613 : if (!assignOne)
933 : : {
934 : 115729 : set<Node>* repSet = typeRepSet.getSet(tb);
935 [ + + ][ + + ]: 115729 : if (repSet != nullptr && !repSet->empty())
[ + + ]
936 : : {
937 : 103844 : continue;
938 : : }
939 [ + + ]: 11885 : if (evaluableSet.find(tb) != evaluableSet.end())
940 : : {
941 : 945 : continue;
942 : : }
943 : : }
944 [ + - ]: 117648 : Trace("model-builder")
945 : 58824 : << " Assign phase, working on type: " << t << endl;
946 : : bool assignable, evaluable CVC5_UNUSED;
947 : 58824 : std::map<Node, Assigner>::iterator itAssigner;
948 : 58824 : std::map<Node, Node>::iterator itAssignerM;
949 : 58824 : set<Node>* repSet = typeRepSet.getSet(t);
950 [ + + ]: 179098 : for (i = noRepSet.begin(); i != noRepSet.end();)
951 : : {
952 : 168084 : i2 = i;
953 : 168084 : ++i;
954 [ + + ]: 168084 : if (evaluableEqc.find(*i2) != evaluableEqc.end())
955 : : {
956 [ + - ]: 478 : Trace("model-builder")
957 : 239 : << " ...do not assign to evaluatable eqc " << *i2 << std::endl;
958 : : // we never assign to evaluable equivalence classes
959 : 239 : continue;
960 : : }
961 : : // check whether it has an assigner object
962 : 167845 : itAssignerM = eqcToAssignerMaster.find(*i2);
963 [ + + ]: 167845 : if (itAssignerM != eqcToAssignerMaster.end())
964 : : {
965 : : // Take the master's assigner. Notice we don't care which order
966 : : // equivalence classes are assigned. For instance, the master can
967 : : // be assigned after one of its slaves.
968 : 35 : itAssigner = eqcToAssigner.find(itAssignerM->second);
969 : : }
970 : : else
971 : : {
972 : 167810 : itAssigner = eqcToAssigner.find(*i2);
973 : : }
974 [ + + ]: 167845 : if (itAssigner != eqcToAssigner.end())
975 : : {
976 : 47 : assignable = isAssignerActive(tm, itAssigner->second);
977 : : }
978 : : else
979 : : {
980 : 167798 : assignable = assignableEqc.find(*i2) != assignableEqc.end();
981 : : }
982 [ + - ]: 335690 : Trace("model-builder-debug")
983 : 0 : << " eqc " << *i2 << " is assignable=" << assignable
984 : 167845 : << std::endl;
985 [ + + ]: 167845 : if (assignable)
986 : : {
987 : : // this assertion ensures that if we are assigning to a term of
988 : : // Boolean type, then the term must be assignable.
989 : : // Note we only assign to terms of Boolean type if the term occurs in
990 : : // a singleton equivalence class; otherwise the term would have been
991 : : // in the equivalence class of true or false and would not need
992 : : // assigning.
993 : 165867 : Assert(!t.isBoolean() || isAssignable(*i2));
994 : 165867 : Node n;
995 [ + + ]: 165867 : if (itAssigner != eqcToAssigner.end())
996 : : {
997 [ + - ]: 94 : Trace("model-builder-debug")
998 : 47 : << "Get value from assigner for finite type..." << std::endl;
999 : : // if it has an assigner, get the value from the assigner.
1000 : 47 : n = itAssigner->second.getNextAssignment();
1001 [ - + ][ - + ]: 47 : Assert(!n.isNull());
[ - - ]
1002 : : }
1003 [ + + ]: 165820 : else if (!d_env.isFiniteType(t))
1004 : : {
1005 : : // If its infinite, we get a fresh value that does not occur in the
1006 : : // model. Note that uninterpreted sorts are handled in the finite
1007 : : // case below in the case that finite model finding is enabled.
1008 : : bool success;
1009 : : do
1010 : : {
1011 [ + - ]: 331306 : Trace("model-builder-debug")
1012 : 165653 : << "Enumerate term of type " << t << std::endl;
1013 : 165653 : n = typeConstSet.nextTypeEnum(t);
1014 : : //--- AJR: this code checks whether n is a legal value
1015 [ - + ][ - + ]: 165653 : Assert(!n.isNull());
[ - - ]
1016 : 165653 : success = true;
1017 [ + - ]: 331306 : Trace("model-builder-debug")
1018 : 165653 : << "Check if excluded : " << n << std::endl;
1019 : : #ifdef CVC5_ASSERTIONS
1020 [ + + ]: 165653 : if (isUSortFiniteRestricted)
1021 : : {
1022 : : // must not involve uninterpreted constants beyond cardinality
1023 : : // bound (which assumed to coincide with #eqc)
1024 : : // this is just an assertion now, since TypeEnumeratorProperties
1025 : : // should ensure that only legal values are enumerated wrt this
1026 : : // constraint.
1027 : 913 : std::map<Node, bool> visited;
1028 : 913 : success = !isExcludedUSortValue(eqc_usort_count, n, visited);
1029 [ - + ]: 913 : if (!success)
1030 : : {
1031 [ - - ]: 0 : Trace("model-builder")
1032 : 0 : << "Excluded value for " << t << " : " << n
1033 : 0 : << " due to out of range uninterpreted constant."
1034 : 0 : << std::endl;
1035 : : }
1036 [ - + ][ - + ]: 913 : Assert(success);
[ - - ]
1037 : 913 : }
1038 : : #endif
1039 [ + - ][ + + ]: 165653 : if (success && isCorecursive)
1040 : : {
1041 [ + - ][ + + ]: 57 : if (repSet != nullptr && !repSet->empty())
[ + + ]
1042 : : {
1043 : : // in the case of codatatypes, check if it is in the set of
1044 : : // values that we cannot assign
1045 : 49 : success = !isExcludedCdtValue(n, repSet, assertedReps, *i2);
1046 [ + + ]: 49 : if (!success)
1047 : : {
1048 [ + - ]: 36 : Trace("model-builder")
1049 : 0 : << "Excluded value : " << n
1050 : 0 : << " due to alpha-equivalent codatatype expression."
1051 : 18 : << std::endl;
1052 : : }
1053 : : }
1054 : : }
1055 : : //---
1056 [ + + ]: 165653 : } while (!success);
1057 [ - + ][ - + ]: 165635 : Assert(!n.isNull());
[ - - ]
1058 [ + - ]: 331270 : Trace("model-value-enum") << "Enum infinite " << t << " " << n
1059 : 165635 : << " for " << *i2 << std::endl;
1060 : : }
1061 : : else
1062 : : {
1063 : : // Otherwise, we get the first value from the type enumerator.
1064 : : // Note that uninterpreted sorts in finite model finding assign
1065 : : // an arbitrary constant when unassigned. This case is applied
1066 : : // e.g. for datatypes over uninterpreted sorts, where subfields
1067 : : // of the datatype may be introduced when assigning arbitrary
1068 : : // values.
1069 [ + - ]: 370 : Trace("model-builder-debug")
1070 : 185 : << "Get first value from finite type..." << std::endl;
1071 : 185 : TypeEnumerator te(t);
1072 : 185 : n = *te;
1073 [ + - ]: 370 : Trace("model-value-enum") << "Enum finite " << t << " " << n
1074 : 185 : << " for " << *i2 << std::endl;
1075 : 185 : }
1076 [ + - ]: 165867 : Trace("model-builder-debug") << "...got " << n << std::endl;
1077 : 165867 : assignConstantRep(tm, *i2, n);
1078 : 165867 : changed = true;
1079 : 165867 : noRepSet.erase(i2);
1080 [ + + ]: 165867 : if (assignOne)
1081 : : {
1082 : 47810 : assignOne = false;
1083 : 47810 : break;
1084 : : }
1085 [ + + ]: 165867 : }
1086 : : }
1087 [ + + ][ + + ]: 511581 : }
1088 : :
1089 : : // Corner case - I'm not sure this can even happen - but it's theoretically
1090 : : // possible to have a cyclical dependency
1091 : : // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In
1092 : : // this case, neither one will get assigned because we are waiting
1093 : : // to be able to evaluate. But we will never be able to evaluate because
1094 : : // the variables that need to be assigned are in
1095 : : // these same EC's. In this case, repeat the whole fixed-point computation
1096 : : // with the difference that the first EC
1097 : : // that has both assignable and evaluable expressions will get assigned.
1098 [ + + ]: 103052 : if (!changed)
1099 : : {
1100 [ + - ]: 47810 : Trace("model-builder-debug") << "...must assign one" << std::endl;
1101 : : // Avoid infinite loops: if we are in a deadlock, we abort model building
1102 : : // unsuccessfully here.
1103 [ - + ]: 47810 : if (assignOne)
1104 : : {
1105 : 0 : Assert(false) << "Reached a deadlock during model construction";
1106 : : Trace("model-builder-debug") << "...avoid loop, fail" << std::endl;
1107 : : return false;
1108 : : }
1109 : 47810 : assignOne = true;
1110 : : }
1111 : 103052 : }
1112 : :
1113 : : #ifdef CVC5_ASSERTIONS
1114 : : // Assert that all representatives have been converted to constants
1115 [ + + ]: 55482 : for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it)
1116 : : {
1117 : 19897 : std::set<Node>& repSet = TypeSet::getSet(it);
1118 [ - + ]: 19897 : if (!repSet.empty())
1119 : : {
1120 [ - - ]: 0 : Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size()
1121 : 0 : << ", repSet = " << repSet << endl;
1122 : 0 : Trace("model-builder-debug") << tm->getEqualityEngine()->debugPrintEqc();
1123 : 0 : DebugUnhandled();
1124 : : }
1125 : : }
1126 : : #endif /* CVC5_ASSERTIONS */
1127 : :
1128 [ + - ]: 35585 : Trace("model-builder") << "Copy representatives to model..." << std::endl;
1129 : 35585 : tm->d_reps.clear();
1130 : 35585 : std::map<Node, Node>::iterator itMap;
1131 [ + + ]: 1273481 : for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap)
1132 : : {
1133 : : // The "constant" representative is a model value, which may be a lambda
1134 : : // if higher-order. We now can go back and normalize its subterms.
1135 : : // This is necessary if we assigned a lambda value whose body contains
1136 : : // a free constant symbol that was assigned in this method.
1137 : 1237896 : Node normc = itMap->second;
1138 [ + + ]: 1237896 : if (!normc.isConst())
1139 : : {
1140 : 581 : normc = normalize(tm, normc, true);
1141 : : }
1142 : : // mark this as the final representative
1143 : 1237896 : tm->assignRepresentative(itMap->first, normc, true);
1144 : 1237896 : }
1145 : :
1146 [ + - ]: 35585 : Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
1147 : : // Make sure every EC has a rep
1148 [ - + ]: 35585 : for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap)
1149 : : {
1150 : 0 : tm->assignRepresentative(itMap->first, itMap->second, false);
1151 : : }
1152 [ + + ]: 74553 : for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it)
1153 : : {
1154 : 38968 : set<Node>& noRepSet = TypeSet::getSet(it);
1155 [ + + ]: 44715 : for (const Node& node : noRepSet)
1156 : : {
1157 : 5747 : tm->assignRepresentative(node, node, false);
1158 : : }
1159 : : }
1160 : :
1161 : : // modelBuilder-specific initialization
1162 [ - + ]: 35585 : if (!processBuildModel(tm))
1163 : : {
1164 [ - - ]: 0 : Trace("model-builder")
1165 : 0 : << "TheoryEngineModelBuilder: fail process build model." << std::endl;
1166 : 0 : return false;
1167 : : }
1168 [ + - ]: 35585 : Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl;
1169 : 35585 : return true;
1170 : 35585 : }
1171 : :
1172 : 4421 : void TheoryEngineModelBuilder::postProcessModel(bool incomplete, TheoryModel* m)
1173 : : {
1174 [ + - ]: 4421 : Trace("model-builder") << "postProcessModel" << std::endl;
1175 : : // Note that we do not insist that functions are assigned here, they can
1176 : : // continue to be built on demand in the theory model.
1177 : : // if we are incomplete, there is no guarantee on the model.
1178 : : // thus, we do not check the model here.
1179 [ + + ]: 4421 : if (incomplete)
1180 : : {
1181 : 1586 : return;
1182 : : }
1183 [ - + ][ - + ]: 2835 : Assert(m != nullptr);
[ - - ]
1184 : : // debug-check the model if the checkModels() is enabled.
1185 [ + + ]: 2835 : if (options().smt.debugCheckModels)
1186 : : {
1187 : 548 : debugCheckModel(m);
1188 : : }
1189 : : }
1190 : :
1191 : 548 : void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
1192 : : {
1193 : 548 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
1194 : 548 : std::map<Node, Node>::iterator itMap;
1195 : : // Check that every term evaluates to its representative in the model
1196 : 548 : for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
1197 [ + + ]: 10415 : !eqcs_i.isFinished();
1198 : 9867 : ++eqcs_i)
1199 : : {
1200 : : // eqc is the equivalence class representative
1201 : 9867 : Node eqc = (*eqcs_i);
1202 : : // get the representative
1203 : 9867 : Node rep = tm->getRepresentative(eqc);
1204 [ + + ][ - + ]: 9867 : if (!rep.isConst() && eqc.getType().isBoolean())
[ + + ][ - + ]
[ - - ]
1205 : : {
1206 : : // if Boolean, it does not necessarily have a constant representative, use
1207 : : // get value instead
1208 : 0 : rep = tm->getValue(eqc);
1209 : 0 : AlwaysAssert(rep.isConst());
1210 : : }
1211 : 9867 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
1212 [ + + ]: 45202 : for (; !eqc_i.isFinished(); ++eqc_i)
1213 : : {
1214 : 35335 : Node n = *eqc_i;
1215 [ - + ][ - - ]: 106005 : AlwaysAssert(CVC5_EQUAL(rep.getType(), n.getType()))
1216 : 35335 : << "Representative " << rep << " of " << n
1217 [ - + ][ - - ]: 35335 : << " violates type constraints (" << rep.getType() << " and "
1218 [ - + ][ - + ]: 35335 : << n.getType() << ")";
[ - - ]
1219 : 35335 : Node val = tm->getValue(n);
1220 [ + + ]: 35335 : if (val != rep)
1221 : : {
1222 : 587 : std::stringstream err;
1223 : 587 : err << "Failed representative check:" << std::endl
1224 : 587 : << "n: " << n << std::endl
1225 : 1174 : << "getValue(n): " << val << std::endl
1226 : 587 : << "rep: " << rep << std::endl;
1227 [ - + ][ - - ]: 587 : if (val.isConst() && rep.isConst())
[ - + ]
1228 : : {
1229 : 0 : AlwaysAssert(val == rep) << err.str();
1230 : : }
1231 [ + + ]: 2935 : else if (!CVC5_EQUAL(rewrite(val), rewrite(rep)))
1232 : : {
1233 : : // if it does not evaluate, it is just a warning, which may be the
1234 : : // case for non-constant values, e.g. lambdas. Furthermore we only
1235 : : // throw this warning if rewriting cannot show they are equal.
1236 : 37 : warning() << err.str();
1237 : : }
1238 : 587 : }
1239 : 35335 : }
1240 : 9867 : }
1241 : :
1242 : : // builder-specific debugging
1243 : 548 : debugModel(tm);
1244 : 548 : }
1245 : :
1246 : 2525376 : Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
1247 : : {
1248 : 2525376 : std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
1249 [ + + ]: 2525376 : if (itMap != d_constantReps.end())
1250 : : {
1251 : 18 : r = (*itMap).second;
1252 : : // if d_constantReps stores a constant, we are done, otherwise we process
1253 : : // it below.
1254 [ - + ]: 18 : if (r.isConst())
1255 : : {
1256 : 0 : return r;
1257 : : }
1258 : : }
1259 : 2525376 : NodeMap::iterator it = d_normalizedCache.find(r);
1260 [ + + ]: 2525376 : if (it != d_normalizedCache.end())
1261 : : {
1262 : 44312 : return (*it).second;
1263 : : }
1264 [ + - ]: 2481064 : Trace("model-builder-debug") << "do normalize on " << r << std::endl;
1265 : 2481064 : Node retNode = r;
1266 [ + + ]: 2481064 : if (r.getNumChildren() > 0)
1267 : : {
1268 : 2472117 : std::vector<Node> children;
1269 [ + + ]: 2472117 : if (r.getMetaKind() == kind::metakind::PARAMETERIZED)
1270 : : {
1271 : 1988493 : children.push_back(r.getOperator());
1272 : : }
1273 [ + + ]: 7500194 : for (size_t i = 0, nchild = r.getNumChildren(); i < nchild; ++i)
1274 : : {
1275 : 5028077 : Node ri = r[i];
1276 : 5028077 : bool recurse = true;
1277 [ + + ]: 5028077 : if (!ri.isConst())
1278 : : {
1279 [ + + ]: 3755528 : if (m->d_equalityEngine->hasTerm(ri))
1280 : : {
1281 : : itMap =
1282 : 3710499 : d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
1283 [ + + ]: 3710499 : if (itMap != d_constantReps.end())
1284 : : {
1285 : 750736 : ri = (*itMap).second;
1286 [ + - ]: 1501472 : Trace("model-builder-debug")
1287 : 750736 : << i << ": const child " << ri << std::endl;
1288 : : // need to recurse if d_constantReps stores a non-constant
1289 : 750736 : recurse = !ri.isConst();
1290 : : }
1291 [ + + ]: 2959763 : else if (!evalOnly)
1292 : : {
1293 : 2866666 : recurse = false;
1294 [ + - ]: 2866666 : Trace("model-builder-debug") << i << ": keep " << ri << std::endl;
1295 : : }
1296 : : }
1297 : : else
1298 : : {
1299 [ + - ]: 90058 : Trace("model-builder-debug")
1300 : 45029 : << i << ": no hasTerm " << ri << std::endl;
1301 : : }
1302 [ + + ]: 3755528 : if (recurse)
1303 : : {
1304 : 138265 : ri = normalize(m, ri, evalOnly);
1305 : : }
1306 : : }
1307 : 5028077 : children.push_back(ri);
1308 : 5028077 : }
1309 : 2472117 : retNode = nodeManager()->mkNode(r.getKind(), children);
1310 : 2472117 : retNode = rewrite(retNode);
1311 : 2472117 : }
1312 : 2481064 : d_normalizedCache[r] = retNode;
1313 : 2481064 : return retNode;
1314 : 2481064 : }
1315 : :
1316 : 1609 : bool TheoryEngineModelBuilder::preProcessBuildModel(CVC5_UNUSED TheoryModel* m)
1317 : : {
1318 : 1609 : return true;
1319 : : }
1320 : :
1321 : 35585 : bool TheoryEngineModelBuilder::processBuildModel(CVC5_UNUSED TheoryModel* m)
1322 : : {
1323 : 35585 : return true;
1324 : : }
1325 : :
1326 : : } // namespace theory
1327 : : } // namespace cvc5::internal
|
