1 

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

/*! \file theory_model_builder.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Mathias Preiner, Tim King 
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_BUILDER_H 
18 

#define CVC4__THEORY__THEORY_MODEL_BUILDER_H 
19 


20 

#include <unordered_map> 
21 

#include <unordered_set> 
22 


23 

#include "theory/theory_model.h" 
24 


25 

namespace CVC4 { 
26 


27 

class TheoryEngine; 
28 


29 

namespace theory { 
30 


31 

/** TheoryEngineModelBuilder class 
32 

* 
33 

* This is the class used by TheoryEngine 
34 

* for constructing TheoryModel objects, which is the class 
35 

* that represents models for a set of assertions. 
36 

* 
37 

* A call to TheoryEngineModelBuilder::buildModel(...) is made 
38 

* after a full effort check passes with no theory solvers 
39 

* adding lemmas or conflicts, and theory combination passes 
40 

* with no splits on shared terms. If buildModel is successful, 
41 

* this will set up the data structures in TheoryModel to represent 
42 

* a model for the current set of assertions. 
43 

*/ 
44 

class TheoryEngineModelBuilder 
45 

{ 
46 

typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; 
47 

typedef std::unordered_set<Node, NodeHashFunction> NodeSet; 
48 


49 

public: 
50 

TheoryEngineModelBuilder(); 
51 
17162 
virtual ~TheoryEngineModelBuilder() {} 
52 

/** 
53 

* Should be called only on models m after they have been prepared 
54 

* (e.g. using ModelManager). In other words, the equality engine of model 
55 

* m contains all relevant information from each theory that is needed 
56 

* for building a model. This class is responsible simply for ensuring 
57 

* that all equivalence classes of the equality engine of m are assigned 
58 

* constants. 
59 

* 
60 

* This constructs the model m, via the following steps: 
61 

* (1) builderspecified preprocessing, 
62 

* (2) find the equivalence classes of m's 
63 

* equality engine that initially contain constants, 
64 

* (3) assign constants to all equivalence classes 
65 

* of m's equality engine, through alternating 
66 

* iterations of evaluation and enumeration, 
67 

* (4) builderspecific processing, which includes assigning total 
68 

* interpretations to uninterpreted functions. 
69 

* 
70 

* This function returns false if any of the above 
71 

* steps results in a lemma sent on an output channel. 
72 

* Lemmas may be sent on an output channel by this 
73 

* builder in steps (2) or (5), for instance, if the model we 
74 

* are building fails to satisfy a quantified formula. 
75 

* 
76 

* @param m The model to build 
77 

* @return true if the model was successfully built. 
78 

*/ 
79 

bool buildModel(TheoryModel* m); 
80 


81 

/** postprocess model 
82 

* 
83 

* This is called when m is a model that will be returned to the user. This 
84 

* method checks the internal consistency of the model if we are in a debug 
85 

* build. 
86 

*/ 
87 

void postProcessModel(bool incomplete, TheoryModel* m); 
88 


89 

protected: 
90 


91 

//virtual functions 
92 

/** preprocess build model 
93 

* Do preprocessing specific to this model builder. 
94 

* Called in step (2) of the build construction, 
95 

* described above. 
96 

*/ 
97 

virtual bool preProcessBuildModel(TheoryModel* m); 
98 

/** process build model 
99 

* Do processing specific to this model builder. 
100 

* Called in step (5) of the build construction, 
101 

* described above. 
102 

* By default, this assigns values to each function 
103 

* that appears in m's equality engine. 
104 

*/ 
105 

virtual bool processBuildModel(TheoryModel* m); 
106 

/** debug the model 
107 

* Check assertions and printing debug information for the model. 
108 

* Calls after step (5) described above is complete. 
109 

*/ 
110 
109 
virtual void debugModel(TheoryModel* m) {} 
111 

//end virtual functions 
112 


113 

/** Debug check model. 
114 

* 
115 

* This throws an assertion failure if the model contains an equivalence 
116 

* class with two terms t1 and t2 such that t1^M != t2^M. 
117 

*/ 
118 

void debugCheckModel(TheoryModel* m); 
119 


120 

/** Evaluate equivalence class 
121 

* 
122 

* If this method returns a nonnull node c, then c is a constant and some 
123 

* term in the equivalence class of r evaluates to c based on the current 
124 

* state of the model m. 
125 

*/ 
126 

Node evaluateEqc(TheoryModel* m, TNode r); 
127 

/** is n an assignable expression? 
128 

* 
129 

* A term n is an assignable expression if its value is unconstrained by a 
130 

* standard model. Examples of assignable terms are: 
131 

*  variables, 
132 

*  applications of array select, 
133 

*  applications of datatype selectors, 
134 

*  applications of uninterpreted functions. 
135 

* Assignable terms must be firstorder, that is, all instances of the above 
136 

* terms are not assignable if they have a higherorder (function) type. 
137 

*/ 
138 

bool isAssignable(TNode n); 
139 

/** add assignable subterms 
140 

* Adds all assignable subterms of n to tm's equality engine. 
141 

*/ 
142 

void addAssignableSubterms(TNode n, TheoryModel* tm, NodeSet& cache); 
143 

/** normalize representative r 
144 

* 
145 

* This returns a term that is equivalent to r's 
146 

* interpretation in the model m. It may do so 
147 

* by rewriting the application of r's operator to the 
148 

* result of normalizing each of r's children, if 
149 

* each child is constant. 
150 

*/ 
151 

Node normalize(TheoryModel* m, TNode r, bool evalOnly); 
152 

/** assign constant representative 
153 

* 
154 

* Called when equivalence class eqc is assigned a constant 
155 

* representative const_rep. 
156 

* 
157 

* eqc should be a representative of tm's equality engine. 
158 

*/ 
159 

void assignConstantRep(TheoryModel* tm, Node eqc, Node const_rep); 
160 

/** add to type list 
161 

* 
162 

* This adds to type_list the list of types that tn is built from. 
163 

* For example, if tn is (Array Int Bool) and type_list is empty, 
164 

* then we append ( Int, Bool, (Array Int Bool) ) to type_list. 
165 

*/ 
166 

void addToTypeList( 
167 

TypeNode tn, 
168 

std::vector<TypeNode>& type_list, 
169 

std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting); 
170 

/** assign function f based on the model m. 
171 

* This construction is based on "table form". For example: 
172 

* (f 0 1) = 1 
173 

* (f 0 2) = 2 
174 

* (f 1 1) = 3 
175 

* ... 
176 

* becomes: 
177 

* f = (lambda xy. (ite (and (= x 0) (= y 1)) 1 
178 

* (ite (and (= x 0) (= y 2)) 2 
179 

* (ite (and (= x 1) (= y 1)) 3 ...))) 
180 

*/ 
181 

void assignFunction(TheoryModel* m, Node f); 
182 

/** assign function f based on the model m. 
183 

* This construction is based on "dag form". For example: 
184 

* (f 0 1) = 1 
185 

* (f 0 2) = 2 
186 

* (f 1 1) = 3 
187 

* ... 
188 

* becomes: 
189 

* f = (lambda xy. (ite (= x 0) (ite (= y 1) 1 
190 

* (ite (= y 2) 2 ...)) 
191 

* (ite (= x 1) (ite (= y 1) 3 ...) 
192 

* ...)) 
193 

* 
194 

* where the above is represented as a directed acyclic graph (dag). 
195 

* This construction is accomplished by assigning values to (f c) 
196 

* terms before f, e.g. 
197 

* (f 0) = (lambda y. (ite (= y 1) 1 
198 

* (ite (= y 2) 2 ...)) 
199 

* (f 1) = (lambda y. (ite (= y 1) 3 ...)) 
200 

* where 
201 

* f = (lambda xy. (ite (= x 0) ((f 0) y) 
202 

* (ite (= x 1) ((f 1) y) ...)) 
203 

*/ 
204 

void assignHoFunction(TheoryModel* m, Node f); 
205 

/** assign functions 
206 

* 
207 

* Assign all unassigned functions in the model m (those returned by 
208 

* TheoryModel::getFunctionsToAssign), 
209 

* using the two functions above. Currently: 
210 

* If ufHo is disabled, we call assignFunction for all functions. 
211 

* If ufHo is enabled, we call assignHoFunction. 
212 

*/ 
213 

void assignFunctions(TheoryModel* m); 
214 


215 

private: 
216 

/** normalized cache 
217 

* A temporary cache mapping terms to their 
218 

* normalized form, used during buildModel. 
219 

*/ 
220 

NodeMap d_normalizedCache; 
221 

/** mapping from terms to the constant associated with their equivalence class 
222 

*/ 
223 

std::map<Node, Node> d_constantReps; 
224 


225 

/** Theory engine model builder assigner class 
226 

* 
227 

* This manages the assignment of values to terms of a given type. 
228 

* In particular, it is a wrapper around a type enumerator that is restricted 
229 

* by a set of values that it cannot generate, called an "assignment exclusion 
230 

* set". 
231 

*/ 
232 
8 
class Assigner 
233 

{ 
234 

public: 
235 
8 
Assigner() : d_te(nullptr), d_isActive(false) {} 
236 

/** 
237 

* Initialize this assigner to generate values of type tn, with properties 
238 

* tep and assignment exclusion set aes. 
239 

*/ 
240 

void initialize(TypeNode tn, 
241 

TypeEnumeratorProperties* tep, 
242 

const std::vector<Node>& aes); 
243 

/** get the next term in the enumeration 
244 

* 
245 

* This method returns the next legal term based on type enumeration, where 
246 

* a term is legal it does not belong to the assignment exclusion set of 
247 

* this assigner. If no more terms exist, this method returns null. This 
248 

* should never be the case due to the conditions ensured by theory solvers 
249 

* for finite types. If it is the case, we give an assertion failure. 
250 

*/ 
251 

Node getNextAssignment(); 
252 

/** The type enumerator */ 
253 

std::unique_ptr<TypeEnumerator> d_te; 
254 

/** The assignment exclusion set of this Assigner */ 
255 

std::vector<Node> d_assignExcSet; 
256 

/** 
257 

* Is active, flag set to true when all values in d_assignExcSet are 
258 

* constant. 
259 

*/ 
260 

bool d_isActive; 
261 

}; 
262 

/** Is the given Assigner ready to assign values? 
263 

* 
264 

* This returns true if all values in the assignment exclusion set of a have 
265 

* a known value according to the state of this model builder (via a lookup 
266 

* in d_constantReps). It updates the assignment exclusion vector of a to 
267 

* these values whenever possible. 
268 

*/ 
269 

bool isAssignerActive(TheoryModel* tm, Assigner& a); 
270 

//for codatatypes 
271 

/** is v an excluded codatatype value? 
272 

* 
273 

* If this returns true, then v is a value 
274 

* that cannot be used during enumeration in step (4) 
275 

* of model construction. 
276 

* 
277 

* repSet is the set of representatives of the same type as v, 
278 

* assertedReps is a map from representatives t, 
279 

* eqc is the equivalence class that v reside. 
280 

* 
281 

* This function is used to avoid alphaequivalent 
282 

* assignments for codatatype terms, described in 
283 

* Reynolds/Blanchette CADE 2015. In particular, 
284 

* this function returns true if v is in 
285 

* the set V^{x}_I from page 9, where x is eqc 
286 

* and I is the model we are building. 
287 

*/ 
288 

bool isExcludedCdtValue(Node v, 
289 

std::set<Node>* repSet, 
290 

std::map<Node, Node>& assertedReps, 
291 

Node eqc); 
292 

/** is codatatype value match 
293 

* 
294 

* This returns true if v is r{ eqc > t } for some t. 
295 

* If this function returns true, then t above is 
296 

* stored in eqc_m. 
297 

*/ 
298 

bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m); 
299 

//end for codatatypes 
300 


301 

//for debugging finite model finding 
302 

/** does type tn involve an uninterpreted sort? */ 
303 

bool involvesUSort(TypeNode tn); 
304 

/** is v an excluded value based on uninterpreted sorts? 
305 

* This gives an assertion failure in the case that v contains 
306 

* an uninterpreted constant whose index is out of the bounds 
307 

* specified by eqc_usort_count. 
308 

*/ 
309 

bool isExcludedUSortValue(std::map<TypeNode, unsigned>& eqc_usort_count, 
310 

Node v, 
311 

std::map<Node, bool>& visited); 
312 

//end for debugging finite model finding 
313 


314 

}; /* class TheoryEngineModelBuilder */ 
315 


316 

} /* CVC4::theory namespace */ 
317 

} /* CVC4 namespace */ 
318 


319 

#endif /* CVC4__THEORY__THEORY_MODEL_BUILDER_H */ 