1 

/********************* */ 
2 

/*! \file theory_model.h 
3 

** \verbatim 
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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief Model class 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__THEORY_MODEL_H 
18 

#define CVC4__THEORY__THEORY_MODEL_H 
19 


20 

#include <unordered_map> 
21 

#include <unordered_set> 
22 


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" 
29 


30 

namespace CVC4 { 
31 

namespace theory { 
32 


33 

/** Theory Model class. 
34 

* 
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. 
50 

* 
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. 
55 

* 
56 

* These calls may modify the model object using the interface 
57 

* functions below, including: 
58 

*  assertEquality, assertPredicate, assertSkeleton, 
59 

* assertEqualityEngine. 
60 

*  assignFunctionDefinition 
61 

* 
62 

* This class provides several interface functions: 
63 

*  hasTerm, getRepresentative, areEqual, areDisequal 
64 

*  getEqualityEngine 
65 

*  getRepSet 
66 

*  hasAssignedFunctionDefinition, getFunctionsToAssign 
67 

*  getValue 
68 

* 
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. 
71 

* 
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. 
77 

*/ 
78 

class TheoryModel 
79 

{ 
80 

friend class TheoryEngineModelBuilder; 
81 

public: 
82 

TheoryModel(context::Context* c, std::string name, bool enableFuncModels); 
83 

virtual ~TheoryModel(); 
84 

/** 
85 

* Finish init, where ee is the equality engine the model should use. 
86 

*/ 
87 

void finishInit(eq::EqualityEngine* ee); 
88 


89 

/** reset the model */ 
90 

virtual void reset(); 
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 
95 

* 
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. 
98 

*/ 
99 

bool assertEquality(TNode a, TNode b, bool polarity); 
100 

/** assert predicate holds in the model 
101 

* 
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. 
104 

*/ 
105 

bool assertPredicate(TNode a, bool polarity); 
106 

/** assert all equalities/predicates in equality engine hold in the model 
107 

* 
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. 
110 

*/ 
111 

bool assertEqualityEngine(const eq::EqualityEngine* ee, 
112 

const std::set<Node>* termSet = NULL); 
113 

/** assert skeleton 
114 

* 
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. 
120 

* 
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 ). 
125 

* 
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. 
129 

*/ 
130 

void assertSkeleton(TNode n); 
131 

/** set assignment exclusion set 
132 

* 
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. 
135 

* 
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. 
145 

* 
146 

* The vector eset should contain only terms that occur in the model, or 
147 

* are constants. 
148 

* 
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. 
153 

*/ 
154 

void setAssignmentExclusionSet(TNode n, const std::vector<Node>& eset); 
155 

/** set assignment exclusion set group 
156 

* 
157 

* Given group = { x_1, ..., x_n }, this is semantically equivalent to calling 
158 

* the above method on the following pairs of arguments: 
159 

* x1, eset 
160 

* x2, eset + { x_1 } 
161 

* ... 
162 

* xn, eset + { x_1, ..., x_{n1} } 
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. 
167 

*/ 
168 

void setAssignmentExclusionSetGroup(const std::vector<TNode>& group, 
169 

const std::vector<Node>& eset); 
170 

/** get assignment exclusion set for term n 
171 

* 
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. 
174 

* 
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. 
179 

*/ 
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 
186 

* 
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 ce <= 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 ce <= sin( x ) <= c+e. 
193 

* 
194 

* If recordApproximation is called at least once during the model 
195 

* construction process, then checkmodel 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 
201 

* sin(x). 
202 

* 
203 

* This function is simply for bookkeeping, it does not affect the model 
204 

* construction process. 
205 

*/ 
206 

void recordApproximation(TNode n, TNode pred); 
207 

/** 
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. 
212 

*/ 
213 

void recordApproximation(TNode n, TNode pred, Node witness); 
214 

/** set unevaluate/semievaluated kind 
215 

* 
216 

* This informs this model how it should interpret applications of terms with 
217 

* kind k in getModelValue. We distinguish four categories of kinds: 
218 

* 
219 

* [1] "Evaluated" 
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 ). 
227 

* 
228 

* [2] "Unevaluated" 
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 
234 

* itself. 
235 

* 
236 

* [3] "Semievaluated" 
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. 
242 

* 
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 "semievaluated". 
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. 
248 

* 
249 

* By default, all kinds are considered "evaluated". The following methods 
250 

* change the interpretation of various (nonAPPLY_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 semiinterpreted 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). 
255 

*/ 
256 

void setUnevaluatedKind(Kind k); 
257 

void setSemiEvaluatedKind(Kind k); 
258 

/** 
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. 
262 

*/ 
263 

void setIrrelevantKind(Kind k); 
264 

/** 
265 

* Get the set of irrelevant kinds that have been registered by the above 
266 

* method. 
267 

*/ 
268 

const std::set<Kind>& getIrrelevantKinds() const; 
269 

/** is legal elimination 
270 

* 
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. 
274 

*/ 
275 

bool isLegalElimination(TNode x, TNode val); 
276 

// end building the model 
277 


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 
6997 
eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; } 
289 

//  end general equality queries 
290 


291 

/** Get value function. 
292 

* This should be called only after a ModelBuilder 
293 

* has called buildModel(...) on this model. 
294 

*/ 
295 

Node getValue(TNode n) const; 
296 

/** get comments */ 
297 

void getComments(std::ostream& out) const; 
298 


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 
305 


306 

/** is the list of approximations nonempty? */ 
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 
188846 
const RepSet* getRepSet() const { return &d_rep_set; } 
314 

/** get the representative set object (FIXME: remove this, see #1199) */ 
315 
13919 
RepSet* getRepSetPtr() { return &d_rep_set; } 
316 


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 
325 


326 

/** get cardinality for sort */ 
327 

Cardinality getCardinality(TypeNode t) const; 
328 


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 
13904 
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 higherorder 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). 
345 

*/ 
346 

std::vector< Node > getFunctionsToAssign(); 
347 

// end function values 
348 

/** Get the name of this model */ 
349 

const std::string& getName() const; 
350 

/** 
351 

* For debugging, print the equivalence classes of the underlying equality 
352 

* engine. 
353 

*/ 
354 

std::string debugPrintModelEqc() const; 
355 


356 

protected: 
357 

/** Unique name of this model */ 
358 

std::string d_name; 
359 

/** substitution map for this model */ 
360 

SubstitutionMap d_substitutions; 
361 

/** equality engine containing all known equalities/disequalities */ 
362 

eq::EqualityEngine* d_equalityEngine; 
363 

/** approximations (see recordApproximation) */ 
364 

std::map<Node, Node> d_approximations; 
365 

/** list of all approximations */ 
366 

std::vector<std::pair<Node, Node> > d_approx_list; 
367 

/** a set of kinds that are unevaluated */ 
368 

std::unordered_set<Kind, kind::KindHashFunction> d_unevaluated_kinds; 
369 

/** a set of kinds that are semievaluated */ 
370 

std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds; 
371 

/** The set of irrelevant kinds */ 
372 

std::set<Kind> d_irrKinds; 
373 

/** 
374 

* Map of representatives of equality engine to used representatives in 
375 

* representative set 
376 

*/ 
377 

std::map<Node, Node> d_reps; 
378 

/** Map of terms to their assignment exclusion set. */ 
379 

std::map<Node, std::vector<Node> > d_assignExcSet; 
380 

/** 
381 

* Map of terms to their "assignment exclusion set master". After a call to 
382 

* setAssignmentExclusionSetGroup, the master of each term in group 
383 

* (except group[0]) is set to group[0], which stores the assignment 
384 

* exclusion set for that group in the above map. 
385 

*/ 
386 

std::map<Node, Node> d_aesMaster; 
387 

/** Reverse of the above map */ 
388 

std::map<Node, std::vector<Node> > d_aesSlaves; 
389 

/** stores set of representatives for each type */ 
390 

RepSet d_rep_set; 
391 

/** true/false nodes */ 
392 

Node d_true; 
393 

Node d_false; 
394 

/** comment stream to include in printing */ 
395 

std::stringstream d_comment_str; 
396 

/** are we using model cores? */ 
397 

bool d_using_model_core; 
398 

/** symbols that are in the model core */ 
399 

std::unordered_set<Node, NodeHashFunction> d_model_core; 
400 

/** Get model value function. 
401 

* 
402 

* This function is a helper function for getValue. 
403 

*/ 
404 

Node getModelValue(TNode n) const; 
405 

/** add term internal 
406 

* 
407 

* This will do any modelspecific processing necessary for n, 
408 

* such as constraining the interpretation of uninterpreted functions. 
409 

* This is called once for all terms in the equality engine, just before 
410 

* a model builder constructs this model. 
411 

*/ 
412 

virtual void addTermInternal(TNode n); 
413 

private: 
414 

/** cache for getModelValue */ 
415 

mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache; 
416 


417 

// separation logic 
418 

/** the value of the heap */ 
419 

Node d_sep_heap; 
420 

/** the value of the nil element */ 
421 

Node d_sep_nil_eq; 
422 

// end separation logic 
423 


424 

// function values 
425 

/** whether function models are enabled */ 
426 

bool d_enableFuncModels; 
427 

/** map from function terms to the (lambda) definitions 
428 

* After the model is built, the domain of this map is all terms of function 
429 

* type that appear as terms in d_equalityEngine. 
430 

*/ 
431 

std::map<Node, Node> d_uf_models; 
432 

// end function values 
433 

};/* class TheoryModel */ 
434 


435 

}/* CVC4::theory namespace */ 
436 

}/* CVC4 namespace */ 
437 


438 

#endif /* CVC4__THEORY__THEORY_MODEL_H */ 