1 /********************* */
2 /*! \file theory_model.h
4 ** Top contributors (to current version):
5 ** Clark Barrett, Morgan Deters, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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 "smt/model.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.
78 class TheoryModel
: public Model
80 friend class TheoryEngineModelBuilder
;
82 TheoryModel(context::Context
* c
, std::string name
, bool enableFuncModels
);
83 ~TheoryModel() override
;
85 /** reset the model */
89 * Have we attempted to build this model since the last
90 * call to reset? Notice for model building techniques
91 * that are not guaranteed to succeed (such as
92 * when quantified formulas are enabled), a true return
93 * value does not imply that this is a model of the
96 bool isBuilt() { return d_modelBuilt
; }
99 * Was this model successfully built since the last call to reset?
101 bool isBuiltSuccess() { return d_modelBuiltSuccess
; }
102 //---------------------------- for building the model
103 /** Adds a substitution from x to t. */
104 void addSubstitution(TNode x
, TNode t
, bool invalidateCache
= true);
105 /** assert equality holds in the model
107 * This method returns true if and only if the equality engine of this model
108 * is consistent after asserting the equality to this model.
110 bool assertEquality(TNode a
, TNode b
, bool polarity
);
111 /** assert predicate holds in the model
113 * This method returns true if and only if the equality engine of this model
114 * is consistent after asserting the predicate to this model.
116 bool assertPredicate(TNode a
, bool polarity
);
117 /** assert all equalities/predicates in equality engine hold in the model
119 * This method returns true if and only if the equality engine of this model
120 * is consistent after asserting the equality engine to this model.
122 bool assertEqualityEngine(const eq::EqualityEngine
* ee
,
123 std::set
<Node
>* termSet
= NULL
);
126 * This method gives a "skeleton" for the model value of the equivalence
127 * class containing n. This should be an application of interpreted function
128 * (e.g. datatype constructor, array store, set union chain). The subterms of
129 * this term that are variables or terms that belong to other theories will
130 * be filled in with model values.
132 * For example, if we call assertSkeleton on (C x y) where C is a datatype
133 * constructor and x and y are variables, then the equivalence class of
134 * (C x y) will be interpreted in m as (C x^m y^m) where
135 * x^m = m->getValue( x ) and y^m = m->getValue( y ).
137 * It should be called during model generation, before final representatives
138 * are chosen. In the case of TheoryEngineModelBuilder, it should be called
139 * during Theory's collectModelInfo( ... ) functions.
141 void assertSkeleton(TNode n
);
142 /** record approximation
144 * This notifies this model that the value of n was approximated in this
145 * model such that the predicate pred (involving n) holds. For example,
146 * for transcendental functions, we may determine an error bound on the
147 * value of a transcendental function, say c-e <= y <= c+e where
148 * c and e are constants. We call this function with n set to sin( x ) and
149 * pred set to c-e <= sin( x ) <= c+e.
151 * If recordApproximation is called at least once during the model
152 * construction process, then check-model is not guaranteed to succeed.
153 * However, there are cases where we can establish the input is satisfiable
154 * without constructing an exact model. For example, if x=.77, sin(x)=.7, and
155 * say we have computed c=.7 and e=.01 as an approximation in the above
156 * example, then we may reason that the set of assertions { sin(x)>.6 } is
157 * satisfiable, albiet without establishing an exact (irrational) value for
160 * This function is simply for bookkeeping, it does not affect the model
161 * construction process.
163 void recordApproximation(TNode n
, TNode pred
);
164 /** set unevaluate/semi-evaluated kind
166 * This informs this model how it should interpret applications of terms with
167 * kind k in getModelValue. We distinguish four categories of kinds:
170 * This includes (standard) interpreted symbols like NOT, PLUS, UNION, etc.
171 * These operators can be characterized by the invariant that they are
172 * "evaluatable". That is, if they are applied to only constants, the rewriter
173 * is guaranteed to rewrite the application to a constant. When getting
174 * the model value of <k>( t1...tn ) where k is a kind of this category, we
175 * compute the (constant) value of t1...tn, say this returns c1...cn, we
176 * return the (constant) result of rewriting <k>( c1...cn ).
179 * This includes interpreted symbols like FORALL, EXISTS,
180 * CARDINALITY_CONSTRAINT, that are not evaluatable. When getting a model
181 * value for a term <k>( t1...tn ) where k is a kind of this category, we
182 * check whether <k>( t1...tn ) exists in the equality engine of this model.
183 * If it does, we return its representative, otherwise we return the term
186 * [3] "Semi-evaluated"
187 * This includes kinds like BITVECTOR_ACKERMANNIZE_UDIV and others, typically
188 * those that correspond to abstractions. Like unevaluated kinds, these
189 * kinds do not have an evaluator. In contrast to unevaluated kinds, we
190 * interpret a term <k>( t1...tn ) not appearing in the equality engine as an
191 * arbitrary value instead of the term itself.
193 * [4] APPLY_UF, where getting the model value depends on an internally
194 * constructed representation of a lambda model value (d_uf_models).
195 * It is optional whether this kind is "evaluated" or "semi-evaluated".
196 * In the case that it is "evaluated", get model rewrites the application
197 * of the lambda model value of its operator to its evaluated arguments.
199 * By default, all kinds are considered "evaluated". The following methods
200 * change the interpretation of various (non-APPLY_UF) kinds to one of the
201 * above categories and should be called by the theories that own the kind
202 * during Theory::finishInit. We set APPLY_UF to be semi-interpreted when
203 * this model does not enabled function values (this is the case for the model
204 * of TheoryEngine when the option assignFunctionValues is set to false).
206 void setUnevaluatedKind(Kind k
);
207 void setSemiEvaluatedKind(Kind k
);
208 //---------------------------- end building the model
210 // ------------------- general equality queries
211 /** does the equality engine of this model have term a? */
212 bool hasTerm(TNode a
);
213 /** get the representative of a in the equality engine of this model */
214 Node
getRepresentative(TNode a
);
215 /** are a and b equal in the equality engine of this model? */
216 bool areEqual(TNode a
, TNode b
);
217 /** are a and b disequal in the equality engine of this model? */
218 bool areDisequal(TNode a
, TNode b
);
219 /** get the equality engine for this model */
220 eq::EqualityEngine
* getEqualityEngine() { return d_equalityEngine
; }
221 // ------------------- end general equality queries
223 /** Get value function.
224 * This should be called only after a ModelBuilder
225 * has called buildModel(...) on this model.
226 * useDontCares is whether to return Node::null() if
227 * n does not occur in the equality engine.
229 Node
getValue(TNode n
, bool useDontCares
= false) const;
231 void getComments(std::ostream
& out
) const override
;
233 //---------------------------- separation logic
234 /** set the heap and value sep.nil is equal to */
235 void setHeapModel(Node h
, Node neq
);
236 /** get the heap and value sep.nil is equal to */
237 bool getHeapModel(Expr
& h
, Expr
& neq
) const override
;
238 //---------------------------- end separation logic
240 /** is the list of approximations non-empty? */
241 bool hasApproximations() const override
;
242 /** get approximations */
243 std::vector
<std::pair
<Expr
, Expr
> > getApproximations() const override
;
244 /** get the representative set object */
245 const RepSet
* getRepSet() const { return &d_rep_set
; }
246 /** get the representative set object (FIXME: remove this, see #1199) */
247 RepSet
* getRepSetPtr() { return &d_rep_set
; }
248 /** return whether this node is a don't-care */
249 bool isDontCare(Expr expr
) const override
;
250 /** get value function for Exprs. */
251 Expr
getValue(Expr expr
) const override
;
252 /** get cardinality for sort */
253 Cardinality
getCardinality(Type t
) const override
;
254 /** print representative debug function */
255 void printRepresentativeDebug( const char* c
, Node r
);
256 /** print representative function */
257 void printRepresentative( std::ostream
& out
, Node r
);
259 //---------------------------- function values
260 /** a map from functions f to a list of all APPLY_UF terms with operator f */
261 std::map
< Node
, std::vector
< Node
> > d_uf_terms
;
262 /** a map from functions f to a list of all HO_APPLY terms with first argument f */
263 std::map
< Node
, std::vector
< Node
> > d_ho_uf_terms
;
264 /** are function values enabled? */
265 bool areFunctionValuesEnabled() const;
266 /** assign function value f to definition f_def */
267 void assignFunctionDefinition( Node f
, Node f_def
);
268 /** have we assigned function f? */
269 bool hasAssignedFunctionDefinition( Node f
) const { return d_uf_models
.find( f
)!=d_uf_models
.end(); }
270 /** get the list of functions to assign.
271 * This list will contain all terms of function type that are terms in d_equalityEngine.
272 * If higher-order is enabled, we ensure that this list is sorted by type size.
273 * This allows us to assign functions T -> T before ( T x T ) -> T and before ( T -> T ) -> T,
274 * which is required for "dag form" model construction (see TheoryModelBuilder::assignHoFunction).
276 std::vector
< Node
> getFunctionsToAssign();
277 //---------------------------- end function values
279 /** substitution map for this model */
280 SubstitutionMap d_substitutions
;
281 /** whether we have tried to build this model in the current context */
283 /** whether this model has been built successfully */
284 bool d_modelBuiltSuccess
;
285 /** special local context for our equalityEngine so we can clear it
286 * independently of search context */
287 context::Context
* d_eeContext
;
288 /** equality engine containing all known equalities/disequalities */
289 eq::EqualityEngine
* d_equalityEngine
;
290 /** approximations (see recordApproximation) */
291 std::map
<Node
, Node
> d_approximations
;
292 /** list of all approximations */
293 std::vector
<std::pair
<Node
, Node
> > d_approx_list
;
294 /** a set of kinds that are not evaluated */
295 std::unordered_set
<Kind
, kind::KindHashFunction
> d_not_evaluated_kinds
;
296 /** a set of kinds that are semi-evaluated */
297 std::unordered_set
<Kind
, kind::KindHashFunction
> d_semi_evaluated_kinds
;
298 /** map of representatives of equality engine to used representatives in
299 * representative set */
300 std::map
<Node
, Node
> d_reps
;
301 /** stores set of representatives for each type */
303 /** true/false nodes */
306 /** comment stream to include in printing */
307 std::stringstream d_comment_str
;
308 /** Get model value function.
310 * This function is a helper function for getValue.
311 * hasBoundVars is whether n may contain bound variables
312 * useDontCares is whether to return Node::null() if
313 * n does not occur in the equality engine.
315 Node
getModelValue(TNode n
,
316 bool hasBoundVars
= false,
317 bool useDontCares
= false) const;
318 /** add term internal
320 * This will do any model-specific processing necessary for n,
321 * such as constraining the interpretation of uninterpreted functions.
322 * This is called once for all terms in the equality engine, just before
323 * a model builder constructs this model.
325 virtual void addTermInternal(TNode n
);
328 /** cache for getModelValue */
329 mutable std::unordered_map
<Node
, Node
, NodeHashFunction
> d_modelCache
;
331 //---------------------------- separation logic
332 /** the value of the heap */
334 /** the value of the nil element */
336 //---------------------------- end separation logic
338 //---------------------------- function values
339 /** whether function models are enabled */
340 bool d_enableFuncModels
;
341 /** map from function terms to the (lambda) definitions
342 * After the model is built, the domain of this map is all terms of function
343 * type that appear as terms in d_equalityEngine.
345 std::map
<Node
, Node
> d_uf_models
;
346 //---------------------------- end function values
347 };/* class TheoryModel */
349 }/* CVC4::theory namespace */
350 }/* CVC4 namespace */
352 #endif /* __CVC4__THEORY__THEORY_MODEL_H */