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