1 /********************* */
2 /*! \file theory_model.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Clark Barrett, Mathias Preiner
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__THEORY_MODEL_H
18 #define CVC4__THEORY__THEORY_MODEL_H
20 #include <unordered_map>
21 #include <unordered_set>
23 #include "theory/ee_setup_info.h"
24 #include "theory/rep_set.h"
25 #include "theory/substitutions.h"
26 #include "theory/type_enumerator.h"
27 #include "theory/type_set.h"
28 #include "theory/uf/equality_engine.h"
33 /** Theory Model class.
35 * This class represents a model produced by the TheoryEngine.
36 * The data structures used to represent a model are:
37 * (1) d_equalityEngine : an equality engine object, which stores
38 * an equivalence relation over all terms that exist in
39 * the current set of assertions.
40 * (2) d_substitutions : a substitution map storing cases of
41 * explicitly solved terms, for instance during preprocessing.
42 * (3) d_reps : a map from equivalence class representatives of
43 * the equality engine to the (constant) representatives
44 * assigned to that equivalence class.
45 * (4) d_uf_models : a map from uninterpreted functions to their
46 * lambda representation.
47 * (5) 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.
51 * These data structures are built after a full effort check with
52 * no lemmas sent, within a call to:
53 * TheoryEngineModelBuilder::buildModel(...)
54 * which includes subcalls to TheoryX::collectModelInfo(...) calls.
56 * These calls may modify the model object using the interface
57 * functions below, including:
58 * - assertEquality, assertPredicate, assertSkeleton,
59 * assertEqualityEngine.
60 * - assignFunctionDefinition
62 * This class provides several interface functions:
63 * - hasTerm, getRepresentative, areEqual, areDisequal
66 * - hasAssignedFunctionDefinition, getFunctionsToAssign
69 * The above functions can be used for a model m after it has been
70 * successfully built, i.e. when m->isBuiltSuccess() returns true.
72 * Additionally, all of the above functions, with the exception of getValue,
73 * can be used during step (5) of TheoryEngineModelBuilder::buildModel, as
74 * documented in theory_model_builder.h. In particular, we make calls to the
75 * above functions such as getRepresentative() when assigning total
76 * interpretations for uninterpreted functions.
80 friend class TheoryEngineModelBuilder
;
82 TheoryModel(context::Context
* c
, std::string name
, bool enableFuncModels
);
83 virtual ~TheoryModel();
85 * Finish init, where ee is the equality engine the model should use.
87 void finishInit(eq::EqualityEngine
* ee
);
89 /** reset the model */
91 //---------------------------- for building the model
92 /** Adds a substitution from x to t. */
93 void addSubstitution(TNode x
, TNode t
, bool invalidateCache
= true);
94 /** assert equality holds in the model
96 * This method returns true if and only if the equality engine of this model
97 * is consistent after asserting the equality to this model.
99 bool assertEquality(TNode a
, TNode b
, bool polarity
);
100 /** assert predicate holds in the model
102 * This method returns true if and only if the equality engine of this model
103 * is consistent after asserting the predicate to this model.
105 bool assertPredicate(TNode a
, bool polarity
);
106 /** assert all equalities/predicates in equality engine hold in the model
108 * This method returns true if and only if the equality engine of this model
109 * is consistent after asserting the equality engine to this model.
111 bool assertEqualityEngine(const eq::EqualityEngine
* ee
,
112 const std::set
<Node
>* termSet
= NULL
);
115 * This method gives a "skeleton" for the model value of the equivalence
116 * class containing n. This should be an application of interpreted function
117 * (e.g. datatype constructor, array store, set union chain). The subterms of
118 * this term that are variables or terms that belong to other theories will
119 * be filled in with model values.
121 * For example, if we call assertSkeleton on (C x y) where C is a datatype
122 * constructor and x and y are variables, then the equivalence class of
123 * (C x y) will be interpreted in m as (C x^m y^m) where
124 * x^m = m->getValue( x ) and y^m = m->getValue( y ).
126 * It should be called during model generation, before final representatives
127 * are chosen. In the case of TheoryEngineModelBuilder, it should be called
128 * during Theory's collectModelInfo( ... ) functions.
130 void assertSkeleton(TNode n
);
131 /** set assignment exclusion set
133 * This method sets the "assignment exclusion set" for term n. This is a
134 * set of terms whose value n must be distinct from in the model.
136 * This method should be used sparingly, and in a way such that model
137 * building is still guaranteed to succeed. Term n is intended to be an
138 * assignable term, typically of finite type. Thus, for example, this method
139 * should not be called with a vector eset that is greater than the
140 * cardinality of the type of n. Additionally, this method should not be
141 * called in a way that introduces cyclic dependencies on the assignment order
142 * of terms in the model. For example, providing { y } as the assignment
143 * exclusion set of x and { x } as the assignment exclusion set of y will
144 * cause model building to fail.
146 * The vector eset should contain only terms that occur in the model, or
149 * Additionally, we (currently) require that an assignment exclusion set
150 * should not be set for two terms in the same equivalence class, or to
151 * equivalence classes with an assignable term. Otherwise an
152 * assertion will be thrown by TheoryEngineModelBuilder during model building.
154 void setAssignmentExclusionSet(TNode n
, const std::vector
<Node
>& eset
);
155 /** set assignment exclusion set group
157 * Given group = { x_1, ..., x_n }, this is semantically equivalent to calling
158 * the above method on the following pairs of arguments:
162 * xn, eset + { x_1, ..., x_{n-1} }
163 * Similar restrictions should be considered as above when applying this
164 * method to ensure that model building will succeed. Notice that for
165 * efficiency, the implementation of how the above information is stored
166 * may avoid constructing n copies of eset.
168 void setAssignmentExclusionSetGroup(const std::vector
<TNode
>& group
,
169 const std::vector
<Node
>& eset
);
170 /** get assignment exclusion set for term n
172 * If n has been given an assignment exclusion set, then this method returns
173 * true and the set is added to eset. Otherwise, the method returns false.
175 * Additionally, if n was assigned an assignment exclusion set via a call to
176 * setAssignmentExclusionSetGroup, it adds all members that were passed
177 * in the first argument of that call to the vector group. Otherwise, it
178 * adds n itself to group.
180 bool getAssignmentExclusionSet(TNode n
,
181 std::vector
<Node
>& group
,
182 std::vector
<Node
>& eset
);
183 /** have any assignment exclusion sets been created? */
184 bool hasAssignmentExclusionSets() const;
185 /** record approximation
187 * This notifies this model that the value of n was approximated in this
188 * model such that the predicate pred (involving n) holds. For example,
189 * for transcendental functions, we may determine an error bound on the
190 * value of a transcendental function, say c-e <= y <= c+e where
191 * c and e are constants. We call this function with n set to sin( x ) and
192 * pred set to c-e <= sin( x ) <= c+e.
194 * If recordApproximation is called at least once during the model
195 * construction process, then check-model is not guaranteed to succeed.
196 * However, there are cases where we can establish the input is satisfiable
197 * without constructing an exact model. For example, if x=.77, sin(x)=.7, and
198 * say we have computed c=.7 and e=.01 as an approximation in the above
199 * example, then we may reason that the set of assertions { sin(x)>.6 } is
200 * satisfiable, albiet without establishing an exact (irrational) value for
203 * This function is simply for bookkeeping, it does not affect the model
204 * construction process.
206 void recordApproximation(TNode n
, TNode pred
);
208 * Same as above, but with a witness constant. This ensures that the
209 * approximation predicate is of the form (or (= n witness) pred). This
210 * is useful if the user wants to know a possible concrete value in
211 * the range of the predicate.
213 void recordApproximation(TNode n
, TNode pred
, Node witness
);
214 /** set unevaluate/semi-evaluated kind
216 * This informs this model how it should interpret applications of terms with
217 * kind k in getModelValue. We distinguish four categories of kinds:
220 * This includes (standard) interpreted symbols like NOT, PLUS, UNION, etc.
221 * These operators can be characterized by the invariant that they are
222 * "evaluatable". That is, if they are applied to only constants, the rewriter
223 * is guaranteed to rewrite the application to a constant. When getting
224 * the model value of <k>( t1...tn ) where k is a kind of this category, we
225 * compute the (constant) value of t1...tn, say this returns c1...cn, we
226 * return the (constant) result of rewriting <k>( c1...cn ).
229 * This includes interpreted symbols like FORALL, EXISTS,
230 * CARDINALITY_CONSTRAINT, that are not evaluatable. When getting a model
231 * value for a term <k>( t1...tn ) where k is a kind of this category, we
232 * check whether <k>( t1...tn ) exists in the equality engine of this model.
233 * If it does, we return its representative, otherwise we return the term
236 * [3] "Semi-evaluated"
237 * This includes kinds like BITVECTOR_ACKERMANNIZE_UDIV and others, typically
238 * those that correspond to abstractions. Like unevaluated kinds, these
239 * kinds do not have an evaluator. In contrast to unevaluated kinds, we
240 * interpret a term <k>( t1...tn ) not appearing in the equality engine as an
241 * arbitrary value instead of the term itself.
243 * [4] APPLY_UF, where getting the model value depends on an internally
244 * constructed representation of a lambda model value (d_uf_models).
245 * It is optional whether this kind is "evaluated" or "semi-evaluated".
246 * In the case that it is "evaluated", get model rewrites the application
247 * of the lambda model value of its operator to its evaluated arguments.
249 * By default, all kinds are considered "evaluated". The following methods
250 * change the interpretation of various (non-APPLY_UF) kinds to one of the
251 * above categories and should be called by the theories that own the kind
252 * during Theory::finishInit. We set APPLY_UF to be semi-interpreted when
253 * this model does not enabled function values (this is the case for the model
254 * of TheoryEngine when the option assignFunctionValues is set to false).
256 void setUnevaluatedKind(Kind k
);
257 void setSemiEvaluatedKind(Kind k
);
259 * Set irrelevant kind. These kinds do not impact model generation, that is,
260 * registered terms in theories of this kind do not need to be sent to
261 * the model. An example is APPLY_TESTER.
263 void setIrrelevantKind(Kind k
);
265 * Get the set of irrelevant kinds that have been registered by the above
268 const std::set
<Kind
>& getIrrelevantKinds() const;
269 /** is legal elimination
271 * Returns true if x -> val is a legal elimination of variable x.
272 * In particular, this ensures that val does not have any subterms that
273 * are of unevaluated kinds.
275 bool isLegalElimination(TNode x
, TNode val
);
276 //---------------------------- end building the model
278 // ------------------- general equality queries
279 /** does the equality engine of this model have term a? */
280 bool hasTerm(TNode a
);
281 /** get the representative of a in the equality engine of this model */
282 Node
getRepresentative(TNode a
);
283 /** are a and b equal in the equality engine of this model? */
284 bool areEqual(TNode a
, TNode b
);
285 /** are a and b disequal in the equality engine of this model? */
286 bool areDisequal(TNode a
, TNode b
);
287 /** get the equality engine for this model */
288 eq::EqualityEngine
* getEqualityEngine() { return d_equalityEngine
; }
289 // ------------------- end general equality queries
291 /** Get value function.
292 * This should be called only after a ModelBuilder
293 * has called buildModel(...) on this model.
295 Node
getValue(TNode n
) const;
297 void getComments(std::ostream
& out
) const;
299 //---------------------------- separation logic
300 /** set the heap and value sep.nil is equal to */
301 void setHeapModel(Node h
, Node neq
);
302 /** get the heap and value sep.nil is equal to */
303 bool getHeapModel(Node
& h
, Node
& neq
) const;
304 //---------------------------- end separation logic
306 /** is the list of approximations non-empty? */
307 bool hasApproximations() const;
308 /** get approximations */
309 std::vector
<std::pair
<Node
, Node
> > getApproximations() const;
310 /** get domain elements for uninterpreted sort t */
311 std::vector
<Node
> getDomainElements(TypeNode t
) const;
312 /** get the representative set object */
313 const RepSet
* getRepSet() const { return &d_rep_set
; }
314 /** get the representative set object (FIXME: remove this, see #1199) */
315 RepSet
* getRepSetPtr() { return &d_rep_set
; }
317 //---------------------------- model cores
318 /** set using model core */
319 void setUsingModelCore();
320 /** record model core symbol */
321 void recordModelCoreSymbol(Node sym
);
322 /** Return whether symbol expr is in the model core. */
323 bool isModelCoreSymbol(Node sym
) const;
324 //---------------------------- end model cores
326 /** get cardinality for sort */
327 Cardinality
getCardinality(TypeNode t
) const;
329 //---------------------------- function values
330 /** a map from functions f to a list of all APPLY_UF terms with operator f */
331 std::map
< Node
, std::vector
< Node
> > d_uf_terms
;
332 /** a map from functions f to a list of all HO_APPLY terms with first argument f */
333 std::map
< Node
, std::vector
< Node
> > d_ho_uf_terms
;
334 /** are function values enabled? */
335 bool areFunctionValuesEnabled() const;
336 /** assign function value f to definition f_def */
337 void assignFunctionDefinition( Node f
, Node f_def
);
338 /** have we assigned function f? */
339 bool hasAssignedFunctionDefinition( Node f
) const { return d_uf_models
.find( f
)!=d_uf_models
.end(); }
340 /** get the list of functions to assign.
341 * This list will contain all terms of function type that are terms in d_equalityEngine.
342 * If higher-order is enabled, we ensure that this list is sorted by type size.
343 * This allows us to assign functions T -> T before ( T x T ) -> T and before ( T -> T ) -> T,
344 * which is required for "dag form" model construction (see TheoryModelBuilder::assignHoFunction).
346 std::vector
< Node
> getFunctionsToAssign();
347 //---------------------------- end function values
348 /** Get the name of this model */
349 const std::string
& getName() const;
352 /** Unique name of this model */
354 /** substitution map for this model */
355 SubstitutionMap d_substitutions
;
356 /** equality engine containing all known equalities/disequalities */
357 eq::EqualityEngine
* d_equalityEngine
;
358 /** approximations (see recordApproximation) */
359 std::map
<Node
, Node
> d_approximations
;
360 /** list of all approximations */
361 std::vector
<std::pair
<Node
, Node
> > d_approx_list
;
362 /** a set of kinds that are unevaluated */
363 std::unordered_set
<Kind
, kind::KindHashFunction
> d_unevaluated_kinds
;
364 /** a set of kinds that are semi-evaluated */
365 std::unordered_set
<Kind
, kind::KindHashFunction
> d_semi_evaluated_kinds
;
366 /** The set of irrelevant kinds */
367 std::set
<Kind
> d_irrKinds
;
369 * Map of representatives of equality engine to used representatives in
372 std::map
<Node
, Node
> d_reps
;
373 /** Map of terms to their assignment exclusion set. */
374 std::map
<Node
, std::vector
<Node
> > d_assignExcSet
;
376 * Map of terms to their "assignment exclusion set master". After a call to
377 * setAssignmentExclusionSetGroup, the master of each term in group
378 * (except group[0]) is set to group[0], which stores the assignment
379 * exclusion set for that group in the above map.
381 std::map
<Node
, Node
> d_aesMaster
;
382 /** Reverse of the above map */
383 std::map
<Node
, std::vector
<Node
> > d_aesSlaves
;
384 /** stores set of representatives for each type */
386 /** true/false nodes */
389 /** comment stream to include in printing */
390 std::stringstream d_comment_str
;
391 /** are we using model cores? */
392 bool d_using_model_core
;
393 /** symbols that are in the model core */
394 std::unordered_set
<Node
, NodeHashFunction
> d_model_core
;
395 /** Get model value function.
397 * This function is a helper function for getValue.
399 Node
getModelValue(TNode n
) const;
400 /** add term internal
402 * This will do any model-specific processing necessary for n,
403 * such as constraining the interpretation of uninterpreted functions.
404 * This is called once for all terms in the equality engine, just before
405 * a model builder constructs this model.
407 virtual void addTermInternal(TNode n
);
410 /** cache for getModelValue */
411 mutable std::unordered_map
<Node
, Node
, NodeHashFunction
> d_modelCache
;
413 //---------------------------- separation logic
414 /** the value of the heap */
416 /** the value of the nil element */
418 //---------------------------- end separation logic
420 //---------------------------- function values
421 /** whether function models are enabled */
422 bool d_enableFuncModels
;
423 /** map from function terms to the (lambda) definitions
424 * After the model is built, the domain of this map is all terms of function
425 * type that appear as terms in d_equalityEngine.
427 std::map
<Node
, Node
> d_uf_models
;
428 //---------------------------- end function values
429 };/* class TheoryModel */
431 }/* CVC4::theory namespace */
432 }/* CVC4 namespace */
434 #endif /* CVC4__THEORY__THEORY_MODEL_H */