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-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * 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, getFunctionsToAssign
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);
258 : : /** are a and b equal in the equality engine of this model? */
259 : : bool areEqual(TNode a, TNode b);
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 : 28035 : eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; }
264 : : // ------------------- end general equality queries
265 : :
266 : : /** Get value function.
267 : : * This should be called only after a ModelBuilder
268 : : * has called buildModel(...) on this model.
269 : : */
270 : : Node getValue(TNode n) const;
271 : :
272 : : //---------------------------- separation logic
273 : : /** set the heap and value sep.nil is equal to */
274 : : void setHeapModel(Node h, Node neq);
275 : : /** get the heap and value sep.nil is equal to */
276 : : bool getHeapModel(Node& h, Node& neq) const;
277 : : //---------------------------- end separation logic
278 : :
279 : : /** get domain elements for uninterpreted sort t */
280 : : std::vector<Node> getDomainElements(TypeNode t) const;
281 : : /** get the representative set object */
282 : 215038 : const RepSet* getRepSet() const { return &d_rep_set; }
283 : : /** get the representative set object (FIXME: remove this, see #1199) */
284 : 77766 : RepSet* getRepSetPtr() { return &d_rep_set; }
285 : :
286 : : //---------------------------- model cores
287 : : /** True if a model core has been computed for this model. */
288 : : bool isUsingModelCore() const;
289 : : /** set using model core */
290 : : void setUsingModelCore();
291 : : /** record model core symbol */
292 : : void recordModelCoreSymbol(Node sym);
293 : : /** Return whether symbol expr is in the model core. */
294 : : bool isModelCoreSymbol(Node sym) const;
295 : : //---------------------------- end model cores
296 : :
297 : : //---------------------------- function values
298 : : /** Does this model have terms for the given uninterpreted function? */
299 : : bool hasUfTerms(Node f) const;
300 : : /** Get the terms for uninterpreted function f */
301 : : const std::vector<Node>& getUfTerms(Node f) const;
302 : : /** are function values enabled? */
303 : : bool areFunctionValuesEnabled() const;
304 : : /** assign function value f to definition f_def */
305 : : void assignFunctionDefinition( Node f, Node f_def );
306 : : /** have we assigned function f? */
307 : : bool hasAssignedFunctionDefinition(Node f) const;
308 : : /** get the list of functions to assign.
309 : : * This list will contain all terms of function type that are terms in d_equalityEngine.
310 : : * If higher-order is enabled, we ensure that this list is sorted by type size.
311 : : * This allows us to assign functions T -> T before ( T x T ) -> T and before ( T -> T ) -> T,
312 : : * which is required for "dag form" model construction (see TheoryModelBuilder::assignHoFunction).
313 : : */
314 : : std::vector< Node > getFunctionsToAssign();
315 : : //---------------------------- end function values
316 : : /** Get the name of this model */
317 : : const std::string& getName() const;
318 : : /**
319 : : * For debugging, print the equivalence classes of the underlying equality
320 : : * engine.
321 : : */
322 : : std::string debugPrintModelEqc() const;
323 : :
324 : : /**
325 : : * Is the node n a "value"? This is true if n is a "base value", where
326 : : * a base value is one where isConst() returns true, a constant-like
327 : : * value (e.g. a real algebraic number) or if n is a lambda or witness
328 : : * term.
329 : : *
330 : : * We also return true for rewritten nodes whose leafs are base values.
331 : : * For example, (str.++ (witness ((x String)) (= (str.len x) 1000)) "A") is
332 : : * a value.
333 : : */
334 : : bool isValue(TNode node) const;
335 : :
336 : : protected:
337 : : /**
338 : : * Get cardinality for sort, where t is an uninterpreted sort.
339 : : * @param t The sort.
340 : : * @return the cardinality of the sort, which is the number of representatives
341 : : * for that sort, or 1 if none exist.
342 : : */
343 : : size_t getCardinality(const TypeNode& t) const;
344 : : /**
345 : : * Assign that n is the representative of the equivalence class r.
346 : : * @param r The equivalence class
347 : : * @param n Its assigned representative
348 : : * @param isFinal Whether the assignment is final, which impacts whether
349 : : * we additionally assign function definitions if we are higher-order and
350 : : * r is a function.
351 : : */
352 : : void assignRepresentative(const Node& r, const Node& n, bool isFinal = true);
353 : : /** Unique name of this model */
354 : : std::string d_name;
355 : : /** equality engine containing all known equalities/disequalities */
356 : : eq::EqualityEngine* d_equalityEngine;
357 : : /** a set of kinds that are unevaluated */
358 : : std::unordered_set<Kind, kind::KindHashFunction> d_unevaluated_kinds;
359 : : /** a set of kinds that are semi-evaluated */
360 : : std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
361 : : /** The set of irrelevant kinds */
362 : : std::set<Kind> d_irrKinds;
363 : : /**
364 : : * Map of representatives of equality engine to used representatives in
365 : : * representative set
366 : : */
367 : : std::map<Node, Node> d_reps;
368 : : /** Map of terms to their assignment exclusion set. */
369 : : std::map<Node, std::vector<Node> > d_assignExcSet;
370 : : /**
371 : : * Map of terms to their "assignment exclusion set master". After a call to
372 : : * setAssignmentExclusionSetGroup, the master of each term in group
373 : : * (except group[0]) is set to group[0], which stores the assignment
374 : : * exclusion set for that group in the above map.
375 : : */
376 : : std::map<Node, Node> d_aesMaster;
377 : : /** Reverse of the above map */
378 : : std::map<Node, std::vector<Node> > d_aesSlaves;
379 : : /** stores set of representatives for each type */
380 : : RepSet d_rep_set;
381 : : /** true/false nodes */
382 : : Node d_true;
383 : : Node d_false;
384 : : /** are we using model cores? */
385 : : bool d_using_model_core;
386 : : /** symbols that are in the model core */
387 : : std::unordered_set<Node> d_model_core;
388 : : /** Get model value function.
389 : : *
390 : : * This function is a helper function for getValue.
391 : : */
392 : : Node getModelValue(TNode n) const;
393 : : /** add term internal
394 : : *
395 : : * This will do any model-specific processing necessary for n,
396 : : * such as constraining the interpretation of uninterpreted functions.
397 : : * This is called once for all terms in the equality engine, just before
398 : : * a model builder constructs this model.
399 : : */
400 : : virtual void addTermInternal(TNode n);
401 : : /**
402 : : * Is base model value? This is a helper method for isValue, returns true
403 : : * if n is a base model value.
404 : : */
405 : : bool isBaseModelValue(TNode n) const;
406 : : /** Is assignable function. This returns true if n is not a lambda. */
407 : : bool isAssignableUf(const Node& n) const;
408 : : /**
409 : : * Evaluate semi-evaluated term. This determines if there is a term n' that is
410 : : * in the equality engine of this model that is congruent to n, if so, it
411 : : * returns the model value of n', otherwise this returns the null term.
412 : : * @param n The term to evaluate. We assume it is in rewritten form and
413 : : * has a semi-evaluated kind (e.g. APPLY_SELECTOR).
414 : : * @return The entailed model value for n, if it exists.
415 : : */
416 : : Node evaluateSemiEvalTerm(TNode n) const;
417 : : /**
418 : : * @return The model values of the arguments of n.
419 : : */
420 : : std::vector<Node> getModelValueArgs(TNode n) const;
421 : :
422 : : private:
423 : : /** cache for getModelValue */
424 : : mutable std::unordered_map<Node, Node> d_modelCache;
425 : : /** whether we have computed d_semiEvalCache yet */
426 : : mutable bool d_semiEvalCacheSet;
427 : : /** cache used for evaluateSemiEvalTerm */
428 : : mutable std::unordered_map<Node, NodeTrie> d_semiEvalCache;
429 : :
430 : : //---------------------------- separation logic
431 : : /** the value of the heap */
432 : : Node d_sep_heap;
433 : : /** the value of the nil element */
434 : : Node d_sep_nil_eq;
435 : : //---------------------------- end separation logic
436 : :
437 : : //---------------------------- function values
438 : : /** a map from functions f to a list of all APPLY_UF terms with operator f */
439 : : std::map<Node, std::vector<Node> > d_uf_terms;
440 : : /** a map from functions f to a list of all HO_APPLY terms with first argument
441 : : * f */
442 : : std::map<Node, std::vector<Node> > d_ho_uf_terms;
443 : : /** whether function models are enabled */
444 : : bool d_enableFuncModels;
445 : : /**
446 : : * Map from function terms to the (lambda) definitions
447 : : * After the model is built, the domain of this map is all terms of function
448 : : * type that appear as terms in d_equalityEngine.
449 : : */
450 : : std::map<Node, Node> d_uf_models;
451 : : //---------------------------- end function values
452 : : };/* class TheoryModel */
453 : :
454 : : } // namespace theory
455 : : } // namespace cvc5::internal
456 : :
457 : : #endif /* CVC5__THEORY__THEORY_MODEL_H */
|
