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 : : * Model class.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__THEORY_MODEL_H
16 : : #define CVC5__THEORY__THEORY_MODEL_H
17 : :
18 : : #include <unordered_map>
19 : : #include <unordered_set>
20 : :
21 : : #include "expr/node_trie.h"
22 : : #include "smt/env_obj.h"
23 : : #include "theory/ee_setup_info.h"
24 : : #include "theory/rep_set.h"
25 : : #include "theory/type_enumerator.h"
26 : : #include "theory/type_set.h"
27 : : #include "theory/uf/equality_engine.h"
28 : :
29 : : namespace cvc5::internal {
30 : :
31 : : class Env;
32 : :
33 : : namespace theory {
34 : :
35 : : /** Theory Model class.
36 : : *
37 : : * This class represents a model produced by the TheoryEngine.
38 : : * The data structures used to represent a model are:
39 : : * (1) d_equalityEngine : an equality engine object, which stores
40 : : * an equivalence relation over all terms that exist in
41 : : * the current set of assertions.
42 : : * (2) d_reps : a map from equivalence class representatives of
43 : : * the equality engine to the (constant) representatives
44 : : * assigned to that equivalence class.
45 : : * (3) d_uf_models : a map from uninterpreted functions to their
46 : : * lambda representation.
47 : : * (4) d_rep_set : a data structure that allows interpretations
48 : : * for types to be represented as terms. This is useful for
49 : : * finite model finding.
50 : : * Additionally, models are dependent on top-level substitutions stored in the
51 : : * d_env class.
52 : : *
53 : : * These data structures are built after a full effort check with
54 : : * no lemmas sent, within a call to:
55 : : * TheoryEngineModelBuilder::buildModel(...)
56 : : * which includes subcalls to TheoryX::collectModelInfo(...) calls.
57 : : *
58 : : * These calls may modify the model object using the interface
59 : : * functions below, including:
60 : : * - assertEquality, assertPredicate, assertSkeleton,
61 : : * assertEqualityEngine.
62 : : * - assignFunctionDefinition
63 : : *
64 : : * This class provides several interface functions:
65 : : * - hasTerm, getRepresentative, areEqual, areDisequal
66 : : * - getEqualityEngine
67 : : * - getRepSet
68 : : * - hasAssignedFunctionDefinition
69 : : * - getValue
70 : : *
71 : : * The above functions can be used for a model m after it has been
72 : : * successfully built, i.e. when m->isBuiltSuccess() returns true.
73 : : *
74 : : * Additionally, all of the above functions, with the exception of getValue,
75 : : * can be used during step (5) of TheoryEngineModelBuilder::buildModel, as
76 : : * documented in theory_model_builder.h. In particular, we make calls to the
77 : : * above functions such as getRepresentative() when assigning total
78 : : * interpretations for uninterpreted functions.
79 : : */
80 : : class TheoryModel : protected EnvObj
81 : : {
82 : : friend class TheoryEngineModelBuilder;
83 : :
84 : : public:
85 : : TheoryModel(Env& env, std::string name, bool enableFuncModels);
86 : : virtual ~TheoryModel();
87 : : /**
88 : : * Finish init, where ee is the equality engine the model should use.
89 : : */
90 : : void finishInit(eq::EqualityEngine* ee);
91 : :
92 : : /** reset the model */
93 : : virtual void reset();
94 : : //---------------------------- for building the model
95 : : /** assert equality holds in the model
96 : : *
97 : : * This method returns true if and only if the equality engine of this model
98 : : * is consistent after asserting the equality to this model.
99 : : */
100 : : bool assertEquality(TNode a, TNode b, bool polarity);
101 : : /** assert predicate holds in the model
102 : : *
103 : : * This method returns true if and only if the equality engine of this model
104 : : * is consistent after asserting the predicate to this model.
105 : : */
106 : : bool assertPredicate(TNode a, bool polarity);
107 : : /** assert all equalities/predicates in equality engine hold in the model
108 : : *
109 : : * This method returns true if and only if the equality engine of this model
110 : : * is consistent after asserting the equality engine to this model.
111 : : */
112 : : bool assertEqualityEngine(const eq::EqualityEngine* ee,
113 : : const std::set<Node>* termSet = NULL);
114 : : /** assert skeleton
115 : : *
116 : : * This method gives a "skeleton" for the model value of the equivalence
117 : : * class containing n. This should be an application of interpreted function
118 : : * (e.g. datatype constructor, array store, set union chain). The subterms of
119 : : * this term that are variables or terms that belong to other theories will
120 : : * be filled in with model values.
121 : : *
122 : : * For example, if we call assertSkeleton on (C x y) where C is a datatype
123 : : * constructor and x and y are variables, then the equivalence class of
124 : : * (C x y) will be interpreted in m as (C x^m y^m) where
125 : : * x^m = m->getValue( x ) and y^m = m->getValue( y ).
126 : : *
127 : : * It should be called during model generation, before final representatives
128 : : * are chosen. In the case of TheoryEngineModelBuilder, it should be called
129 : : * during Theory's collectModelInfo( ... ) functions.
130 : : */
131 : : void assertSkeleton(TNode n);
132 : : /** set assignment exclusion set
133 : : *
134 : : * This method sets the "assignment exclusion set" for term n. This is a
135 : : * set of terms whose value n must be distinct from in the model.
136 : : *
137 : : * This method should be used sparingly, and in a way such that model
138 : : * building is still guaranteed to succeed. Term n is intended to be an
139 : : * assignable term, typically of finite type. Thus, for example, this method
140 : : * should not be called with a vector eset that is greater than the
141 : : * cardinality of the type of n. Additionally, this method should not be
142 : : * called in a way that introduces cyclic dependencies on the assignment order
143 : : * of terms in the model. For example, providing { y } as the assignment
144 : : * exclusion set of x and { x } as the assignment exclusion set of y will
145 : : * cause model building to fail.
146 : : *
147 : : * The vector eset should contain only terms that occur in the model, or
148 : : * are constants.
149 : : *
150 : : * Additionally, we (currently) require that an assignment exclusion set
151 : : * should not be set for two terms in the same equivalence class, or to
152 : : * equivalence classes with an assignable term. Otherwise an
153 : : * assertion will be thrown by TheoryEngineModelBuilder during model building.
154 : : */
155 : : void setAssignmentExclusionSet(TNode n, const std::vector<Node>& eset);
156 : : /** set assignment exclusion set group
157 : : *
158 : : * Given group = { x_1, ..., x_n }, this is semantically equivalent to calling
159 : : * the above method on the following pairs of arguments:
160 : : * x1, eset
161 : : * x2, eset + { x_1 }
162 : : * ...
163 : : * xn, eset + { x_1, ..., x_{n-1} }
164 : : * Similar restrictions should be considered as above when applying this
165 : : * method to ensure that model building will succeed. Notice that for
166 : : * efficiency, the implementation of how the above information is stored
167 : : * may avoid constructing n copies of eset.
168 : : */
169 : : void setAssignmentExclusionSetGroup(const std::vector<TNode>& group,
170 : : const std::vector<Node>& eset);
171 : : /** get assignment exclusion set for term n
172 : : *
173 : : * If n has been given an assignment exclusion set, then this method returns
174 : : * true and the set is added to eset. Otherwise, the method returns false.
175 : : *
176 : : * Additionally, if n was assigned an assignment exclusion set via a call to
177 : : * setAssignmentExclusionSetGroup, it adds all members that were passed
178 : : * in the first argument of that call to the vector group. Otherwise, it
179 : : * adds n itself to group.
180 : : */
181 : : bool getAssignmentExclusionSet(TNode n,
182 : : std::vector<Node>& group,
183 : : std::vector<Node>& eset);
184 : : /** have any assignment exclusion sets been created? */
185 : : bool hasAssignmentExclusionSets() const;
186 : : /** set unevaluate/semi-evaluated kind
187 : : *
188 : : * This informs this model how it should interpret applications of terms with
189 : : * kind k in getModelValue. We distinguish four categories of kinds:
190 : : *
191 : : * [1] "Evaluated"
192 : : * This includes (standard) interpreted symbols like NOT, ADD, SET_UNION,
193 : : * etc. These operators can be characterized by the invariant that they are
194 : : * "evaluatable". That is, if they are applied to only constants, the rewriter
195 : : * is guaranteed to rewrite the application to a constant. When getting
196 : : * the model value of <k>( t1...tn ) where k is a kind of this category, we
197 : : * compute the (constant) value of t1...tn, say this returns c1...cn, we
198 : : * return the (constant) result of rewriting <k>( c1...cn ).
199 : : *
200 : : * [2] "Unevaluated"
201 : : * This includes interpreted symbols like FORALL, EXISTS,
202 : : * CARDINALITY_CONSTRAINT, that are not evaluatable. When getting a model
203 : : * value for a term <k>( t1...tn ) where k is a kind of this category, we
204 : : * check whether <k>( t1...tn ) exists in the equality engine of this model.
205 : : * If it does, we return its representative, otherwise we return the term
206 : : * itself.
207 : : *
208 : : * [3] "Semi-evaluated"
209 : : * This includes kinds like BITVECTOR_ACKERMANNIZE_UDIV, APPLY_SELECTOR and.
210 : : * SEQ_NTH. Like unevaluated kinds, these kinds do not have an evaluator for
211 : : * (some) inputs. In contrast to unevaluated kinds, we interpret a term
212 : : * <k>( t1...tn ) not appearing in the equality engine as an arbitrary value
213 : : * instead of the term itself.
214 : : *
215 : : * [4] APPLY_UF, where getting the model value depends on an internally
216 : : * constructed representation of a lambda model value (d_uf_models).
217 : : * It is optional whether this kind is "evaluated" or "semi-evaluated".
218 : : * In the case that it is "evaluated", get model rewrites the application
219 : : * of the lambda model value of its operator to its evaluated arguments.
220 : : *
221 : : * By default, all kinds are considered "evaluated". The following methods
222 : : * change the interpretation of various (non-APPLY_UF) kinds to one of the
223 : : * above categories and should be called by the theories that own the kind
224 : : * during Theory::finishInit. We set APPLY_UF to be semi-interpreted when
225 : : * this model does not enabled function values (this is the case for the model
226 : : * of TheoryEngine when the option assignFunctionValues is set to false).
227 : : */
228 : : void setUnevaluatedKind(Kind k);
229 : : void setSemiEvaluatedKind(Kind k);
230 : : /**
231 : : * Set irrelevant kind. These kinds do not impact model generation, that is,
232 : : * registered terms in theories of this kind do not need to be sent to
233 : : * the model. An example is APPLY_TESTER.
234 : : */
235 : : void setIrrelevantKind(Kind k);
236 : : /**
237 : : * Get the set of irrelevant kinds that have been registered by the above
238 : : * method.
239 : : */
240 : : const std::set<Kind>& getIrrelevantKinds() const;
241 : : /** is legal elimination
242 : : *
243 : : * Returns true if x -> val is a legal elimination for a variable x.
244 : : * In particular, this ensures that val does not have any subterms that
245 : : * are of unevaluated kinds.
246 : : */
247 : : bool isLegalElimination(TNode val);
248 : : //---------------------------- end building the model
249 : :
250 : : // ------------------- general equality queries
251 : : /** does the equality engine of this model have term a? */
252 : : bool hasTerm(TNode a);
253 : : /** get the representative of a in the equality engine of this model */
254 : : Node getRepresentative(TNode a) const;
255 : : /** are a and b equal in the equality engine of this model? */
256 : : bool areEqual(TNode a, TNode b) const;
257 : : /** are a and b disequal in the equality engine of this model? */
258 : : bool areDisequal(TNode a, TNode b);
259 : : /** get the equality engine for this model */
260 : 141928 : eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; }
261 : : // ------------------- end general equality queries
262 : :
263 : : /**
264 : : * Get value function.
265 : : * This should be called only after a ModelBuilder has called buildModel(...)
266 : : * on this model.
267 : : * @param n The term to get the value of.
268 : : * @return The value of n.
269 : : */
270 : : Node getValue(TNode n) const;
271 : :
272 : : /**
273 : : * Simplify n based on the values in this class. This applies a substitution
274 : : * over the free symbols on n and rewrites.
275 : : * This should be called only after a ModelBuilder has called buildModel(...)
276 : : * on this model.
277 : : * @param n The term to simplify.
278 : : * @return The simplified form of n.
279 : : */
280 : : Node simplify(TNode n) const;
281 : :
282 : : //---------------------------- separation logic
283 : : /** set the heap and value sep.nil is equal to */
284 : : void setHeapModel(Node h, Node neq);
285 : : /** get the heap and value sep.nil is equal to */
286 : : bool getHeapModel(Node& h, Node& neq) const;
287 : : //---------------------------- end separation logic
288 : :
289 : : /** get domain elements for uninterpreted sort t */
290 : : std::vector<Node> getDomainElements(TypeNode t) const;
291 : : /** get the representative set object */
292 : 204718 : const RepSet* getRepSet() const { return &d_rep_set; }
293 : : /** get the representative set object (FIXME: remove this, see #1199) */
294 : 59034 : RepSet* getRepSetPtr() { return &d_rep_set; }
295 : :
296 : : //---------------------------- model cores
297 : : /** True if a model core has been computed for this model. */
298 : : bool isUsingModelCore() const;
299 : : /** set using model core */
300 : : void setUsingModelCore();
301 : : /** record model core symbol */
302 : : void recordModelCoreSymbol(Node sym);
303 : : /** Return whether symbol expr is in the model core. */
304 : : bool isModelCoreSymbol(Node sym) const;
305 : : //---------------------------- end model cores
306 : :
307 : : //---------------------------- function values
308 : : /** Does this model have terms for the given uninterpreted function? */
309 : : bool hasUfTerms(Node f) const;
310 : : /** Get the terms for uninterpreted function f */
311 : : const std::vector<Node>& getUfTerms(Node f) const;
312 : : /** are function values enabled? */
313 : : bool areFunctionValuesEnabled() const;
314 : : /** assign function value f to definition f_def */
315 : : void assignFunctionDefinition(Node f, Node f_def) const;
316 : : /** have we assigned function f? */
317 : : bool hasAssignedFunctionDefinition(Node f) const;
318 : : //---------------------------- end function values
319 : : /** Get the name of this model */
320 : : const std::string& getName() const;
321 : : /**
322 : : * For debugging, print the equivalence classes of the underlying equality
323 : : * engine.
324 : : */
325 : : std::string debugPrintModelEqc() const;
326 : :
327 : : /**
328 : : * Is the node n a "value"? This is true if n is a "base value", where
329 : : * a base value is one where isConst() returns true, a constant-like
330 : : * value (e.g. a real algebraic number) or if n is a lambda or witness
331 : : * term.
332 : : *
333 : : * We also return true for rewritten nodes whose leafs are base values.
334 : : * For example, (str.++ (witness ((x String)) (= (str.len x) 1000)) "A") is
335 : : * a value.
336 : : */
337 : : bool isValue(TNode node) const;
338 : :
339 : : protected:
340 : : /**
341 : : * Get cardinality for sort, where t is an uninterpreted sort.
342 : : * @param t The sort.
343 : : * @return the cardinality of the sort, which is the number of representatives
344 : : * for that sort, or 1 if none exist.
345 : : */
346 : : size_t getCardinality(const TypeNode& t) const;
347 : : /**
348 : : * Assign that n is the representative of the equivalence class r.
349 : : * @param r The equivalence class
350 : : * @param n Its assigned representative
351 : : * @param isFinal Whether the assignment is final, which impacts whether
352 : : * we additionally assign function definitions if we are higher-order and
353 : : * r is a function.
354 : : */
355 : : void assignRepresentative(const Node& r, const Node& n, bool isFinal = true);
356 : : /**
357 : : * Assign function f, which is called on demand when the model for f is
358 : : * required by this class (e.g. in getValue or getRepresentative).
359 : : * If not higher-order, this construction is based on "table form". For
360 : : * example:
361 : : * (f 0 1) = 1
362 : : * (f 0 2) = 2
363 : : * (f 1 1) = 3
364 : : * ...
365 : : * becomes:
366 : : * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1
367 : : * (ite (and (= x 0) (= y 2)) 2
368 : : * (ite (and (= x 1) (= y 1)) 3 ...))).
369 : : * If higher-order, we call assignFunctionDefaultHo instead.
370 : : * @param f The function to assign.
371 : : */
372 : : void assignFunctionDefault(Node f) const;
373 : : /**
374 : : * Assign function f when the logic is higher-order. This is called on demand
375 : : * when the model for f is required by his class.
376 : : * This construction is based on "dag form". For example:
377 : : * (f 0 1) = 1
378 : : * (f 0 2) = 2
379 : : * (f 1 1) = 3
380 : : * ...
381 : : * becomes:
382 : : * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
383 : : * (ite (= y 2) 2 ...))
384 : : * (ite (= x 1) (ite (= y 1) 3 ...)
385 : : * ...))
386 : : *
387 : : * where the above is represented as a directed acyclic graph (dag).
388 : : * This construction is accomplished by assigning values to (f c)
389 : : * terms before f, e.g.
390 : : * (f 0) = (lambda y. (ite (= y 1) 1
391 : : * (ite (= y 2) 2 ...))
392 : : * (f 1) = (lambda y. (ite (= y 1) 3 ...))
393 : : * where
394 : : * f = (lambda xy. (ite (= x 0) ((f 0) y)
395 : : * (ite (= x 1) ((f 1) y) ...))
396 : : * @param f The function to assign.
397 : : */
398 : : void assignFunctionDefaultHo(Node f) const;
399 : : /** Unique name of this model */
400 : : std::string d_name;
401 : : /** equality engine containing all known equalities/disequalities */
402 : : eq::EqualityEngine* d_equalityEngine;
403 : : /** a set of kinds that are unevaluated */
404 : : std::unordered_set<Kind, kind::KindHashFunction> d_unevaluated_kinds;
405 : : /** a set of kinds that are semi-evaluated */
406 : : std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
407 : : /** The set of irrelevant kinds */
408 : : std::set<Kind> d_irrKinds;
409 : : /**
410 : : * Map of representatives of equality engine to used representatives in
411 : : * representative set
412 : : */
413 : : mutable std::map<Node, Node> d_reps;
414 : : /** Map of terms to their assignment exclusion set. */
415 : : std::map<Node, std::vector<Node> > d_assignExcSet;
416 : : /**
417 : : * Map of terms to their "assignment exclusion set master". After a call to
418 : : * setAssignmentExclusionSetGroup, the master of each term in group
419 : : * (except group[0]) is set to group[0], which stores the assignment
420 : : * exclusion set for that group in the above map.
421 : : */
422 : : std::map<Node, Node> d_aesMaster;
423 : : /** Reverse of the above map */
424 : : std::map<Node, std::vector<Node> > d_aesSlaves;
425 : : /** stores set of representatives for each type */
426 : : RepSet d_rep_set;
427 : : /** true/false nodes */
428 : : Node d_true;
429 : : Node d_false;
430 : : /** are we using model cores? */
431 : : bool d_using_model_core;
432 : : /** symbols that are in the model core */
433 : : std::unordered_set<Node> d_model_core;
434 : : /** Get model value function.
435 : : *
436 : : * This function is a helper function for getValue.
437 : : */
438 : : Node getModelValue(TNode n) const;
439 : : /** add term internal
440 : : *
441 : : * This will do any model-specific processing necessary for n,
442 : : * such as constraining the interpretation of uninterpreted functions.
443 : : * This is called once for all terms in the equality engine, just before
444 : : * a model builder constructs this model.
445 : : */
446 : : virtual void addTermInternal(TNode n);
447 : : /**
448 : : * Is base model value? This is a helper method for isValue, returns true
449 : : * if n is a base model value.
450 : : */
451 : : bool isBaseModelValue(TNode n) const;
452 : : /** Is assignable function. This returns true if n is not a lambda. */
453 : : bool isAssignableUf(const Node& n) const;
454 : : /**
455 : : * Evaluate semi-evaluated term. This determines if there is a term n' that is
456 : : * in the equality engine of this model that is congruent to n, if so, it
457 : : * returns the model value of n', otherwise this returns the null term.
458 : : * @param n The term to evaluate. We assume it is in rewritten form and
459 : : * has a semi-evaluated kind (e.g. APPLY_SELECTOR).
460 : : * @return The entailed model value for n, if it exists.
461 : : */
462 : : Node evaluateSemiEvalTerm(TNode n) const;
463 : : /**
464 : : * @return The model values of the arguments of n.
465 : : */
466 : : std::vector<Node> getModelValueArgs(TNode n) const;
467 : :
468 : : private:
469 : : /** cache for getModelValue */
470 : : mutable std::unordered_map<Node, Node> d_modelCache;
471 : : /** whether we have computed d_semiEvalCache yet */
472 : : mutable bool d_semiEvalCacheSet;
473 : : /** cache used for evaluateSemiEvalTerm */
474 : : mutable std::unordered_map<Node, NodeTrie> d_semiEvalCache;
475 : :
476 : : //---------------------------- separation logic
477 : : /** the value of the heap */
478 : : Node d_sep_heap;
479 : : /** the value of the nil element */
480 : : Node d_sep_nil_eq;
481 : : //---------------------------- end separation logic
482 : :
483 : : //---------------------------- function values
484 : : /** a map from functions f to a list of all APPLY_UF terms with operator f */
485 : : std::map<Node, std::vector<Node> > d_uf_terms;
486 : : /** a map from functions f to a list of all HO_APPLY terms with first argument
487 : : * f */
488 : : std::map<Node, std::vector<Node> > d_ho_uf_terms;
489 : : /** whether function models are enabled */
490 : : bool d_enableFuncModels;
491 : : /**
492 : : * Map from function terms to the (lambda) definitions
493 : : * After the model is built, the domain of this map is all terms of function
494 : : * type that appear as terms in d_equalityEngine.
495 : : */
496 : : mutable std::map<Node, Node> d_uf_models;
497 : : //---------------------------- end function values
498 : : };/* class TheoryModel */
499 : :
500 : : } // namespace theory
501 : : } // namespace cvc5::internal
502 : :
503 : : #endif /* CVC5__THEORY__THEORY_MODEL_H */
|
