Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mathias Preiner, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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_BUILDER_H
19 : : #define CVC5__THEORY__THEORY_MODEL_BUILDER_H
20 : :
21 : : #include <unordered_map>
22 : : #include <unordered_set>
23 : :
24 : : #include "smt/env_obj.h"
25 : : #include "theory/theory_model.h"
26 : :
27 : : namespace cvc5::internal {
28 : :
29 : : class Env;
30 : :
31 : : namespace theory {
32 : :
33 : : /** TheoryEngineModelBuilder class
34 : : *
35 : : * This is the class used by TheoryEngine
36 : : * for constructing TheoryModel objects, which is the class
37 : : * that represents models for a set of assertions.
38 : : *
39 : : * A call to TheoryEngineModelBuilder::buildModel(...) is made
40 : : * after a full effort check passes with no theory solvers
41 : : * adding lemmas or conflicts, and theory combination passes
42 : : * with no splits on shared terms. If buildModel is successful,
43 : : * this will set up the data structures in TheoryModel to represent
44 : : * a model for the current set of assertions.
45 : : */
46 : : class TheoryEngineModelBuilder : protected EnvObj
47 : : {
48 : : typedef std::unordered_map<Node, Node> NodeMap;
49 : : typedef std::unordered_set<Node> NodeSet;
50 : :
51 : : public:
52 : : TheoryEngineModelBuilder(Env& env);
53 : 65048 : virtual ~TheoryEngineModelBuilder() {}
54 : : /**
55 : : * Should be called only on models m after they have been prepared
56 : : * (e.g. using ModelManager). In other words, the equality engine of model
57 : : * m contains all relevant information from each theory that is needed
58 : : * for building a model. This class is responsible simply for ensuring
59 : : * that all equivalence classes of the equality engine of m are assigned
60 : : * constants.
61 : : *
62 : : * This constructs the model m, via the following steps:
63 : : * (1) builder-specified pre-processing,
64 : : * (2) find the equivalence classes of m's
65 : : * equality engine that initially contain constants,
66 : : * (3) assign constants to all equivalence classes
67 : : * of m's equality engine, through alternating
68 : : * iterations of evaluation and enumeration,
69 : : * (4) builder-specific processing, which includes assigning total
70 : : * interpretations to uninterpreted functions.
71 : : *
72 : : * This function returns false if any of the above
73 : : * steps results in a lemma sent on an output channel.
74 : : * Lemmas may be sent on an output channel by this
75 : : * builder in steps (2) or (5), for instance, if the model we
76 : : * are building fails to satisfy a quantified formula.
77 : : *
78 : : * @param m The model to build
79 : : * @return true if the model was successfully built.
80 : : */
81 : : bool buildModel(TheoryModel* m);
82 : :
83 : : /** postprocess model
84 : : *
85 : : * This is called when m is a model that will be returned to the user. This
86 : : * method checks the internal consistency of the model if we are in a debug
87 : : * build.
88 : : */
89 : : void postProcessModel(bool incomplete, TheoryModel* m);
90 : :
91 : : protected:
92 : :
93 : : //-----------------------------------virtual functions
94 : : /** pre-process build model
95 : : * Do pre-processing specific to this model builder.
96 : : * Called in step (2) of the build construction,
97 : : * described above.
98 : : */
99 : : virtual bool preProcessBuildModel(TheoryModel* m);
100 : : /** process build model
101 : : * Do processing specific to this model builder.
102 : : * Called in step (5) of the build construction,
103 : : * described above.
104 : : * By default, this assigns values to each function
105 : : * that appears in m's equality engine.
106 : : */
107 : : virtual bool processBuildModel(TheoryModel* m);
108 : : /** debug the model
109 : : * Check assertions and printing debug information for the model.
110 : : * Calls after step (5) described above is complete.
111 : : */
112 : 10 : virtual void debugModel(TheoryModel* m) {}
113 : : //-----------------------------------end virtual functions
114 : :
115 : : /** Debug check model.
116 : : *
117 : : * This throws an assertion failure if the model contains an equivalence
118 : : * class with two terms t1 and t2 such that t1^M != t2^M.
119 : : */
120 : : void debugCheckModel(TheoryModel* m);
121 : :
122 : : /** Evaluate equivalence class
123 : : *
124 : : * If this method returns a non-null node c, then c is a constant and some
125 : : * term in the equivalence class of r evaluates to c based on the current
126 : : * state of the model m.
127 : : */
128 : : Node evaluateEqc(TheoryModel* m, TNode r);
129 : : /** is n an assignable expression?
130 : : *
131 : : * A term n is an assignable expression if its value is unconstrained by a
132 : : * standard model. Examples of assignable terms are:
133 : : * - variables,
134 : : * - applications of array select,
135 : : * - applications of datatype selectors,
136 : : * - applications of uninterpreted functions.
137 : : * Assignable terms must be first-order, that is, all instances of the above
138 : : * terms are not assignable if they have a higher-order (function) type.
139 : : */
140 : : bool isAssignable(TNode n);
141 : : /** add assignable subterms
142 : : * Adds all assignable subterms of n to tm's equality engine.
143 : : */
144 : : void addAssignableSubterms(TNode n, TheoryModel* tm, NodeSet& cache);
145 : : /** normalize representative r
146 : : *
147 : : * This returns a term that is equivalent to r's
148 : : * interpretation in the model m. It may do so
149 : : * by rewriting the application of r's operator to the
150 : : * result of normalizing each of r's children, if
151 : : * each child is constant.
152 : : */
153 : : Node normalize(TheoryModel* m, TNode r, bool evalOnly);
154 : : /** assign constant representative
155 : : *
156 : : * Called when equivalence class eqc is assigned a constant
157 : : * representative const_rep.
158 : : *
159 : : * eqc should be a representative of tm's equality engine.
160 : : */
161 : : void assignConstantRep(TheoryModel* tm, Node eqc, Node const_rep);
162 : : /** add to type list
163 : : *
164 : : * This adds to type_list the list of types that tn is built from.
165 : : * For example, if tn is (Array Int Bool) and type_list is empty,
166 : : * then we append ( Int, Bool, (Array Int Bool) ) to type_list.
167 : : */
168 : : void addToTypeList(TypeNode tn,
169 : : std::vector<TypeNode>& type_list,
170 : : std::unordered_set<TypeNode>& visiting);
171 : : /** assign function f based on the model m.
172 : : * This construction is based on "table form". For example:
173 : : * (f 0 1) = 1
174 : : * (f 0 2) = 2
175 : : * (f 1 1) = 3
176 : : * ...
177 : : * becomes:
178 : : * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1
179 : : * (ite (and (= x 0) (= y 2)) 2
180 : : * (ite (and (= x 1) (= y 1)) 3 ...)))
181 : : */
182 : : void assignFunction(TheoryModel* m, Node f);
183 : : /** assign function f based on the model m.
184 : : * This construction is based on "dag form". For example:
185 : : * (f 0 1) = 1
186 : : * (f 0 2) = 2
187 : : * (f 1 1) = 3
188 : : * ...
189 : : * becomes:
190 : : * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
191 : : * (ite (= y 2) 2 ...))
192 : : * (ite (= x 1) (ite (= y 1) 3 ...)
193 : : * ...))
194 : : *
195 : : * where the above is represented as a directed acyclic graph (dag).
196 : : * This construction is accomplished by assigning values to (f c)
197 : : * terms before f, e.g.
198 : : * (f 0) = (lambda y. (ite (= y 1) 1
199 : : * (ite (= y 2) 2 ...))
200 : : * (f 1) = (lambda y. (ite (= y 1) 3 ...))
201 : : * where
202 : : * f = (lambda xy. (ite (= x 0) ((f 0) y)
203 : : * (ite (= x 1) ((f 1) y) ...))
204 : : */
205 : : void assignHoFunction(TheoryModel* m, Node f);
206 : : /** assign functions
207 : : *
208 : : * Assign all unassigned functions in the model m (those returned by
209 : : * TheoryModel::getFunctionsToAssign),
210 : : * using the two functions above. Currently:
211 : : * If HO logic is disabled, we call assignFunction for all functions.
212 : : * If HO logic is enabled, we call assignHoFunction.
213 : : */
214 : : void assignFunctions(TheoryModel* m);
215 : :
216 : : private:
217 : : /** normalized cache
218 : : * A temporary cache mapping terms to their
219 : : * normalized form, used during buildModel.
220 : : */
221 : : NodeMap d_normalizedCache;
222 : : /** mapping from terms to the constant associated with their equivalence class
223 : : */
224 : : std::map<Node, Node> d_constantReps;
225 : :
226 : : /** Theory engine model builder assigner class
227 : : *
228 : : * This manages the assignment of values to terms of a given type.
229 : : * In particular, it is a wrapper around a type enumerator that is restricted
230 : : * by a set of values that it cannot generate, called an "assignment exclusion
231 : : * set".
232 : : */
233 : : class Assigner
234 : : {
235 : : public:
236 : 12 : Assigner() : d_te(nullptr), d_isActive(false) {}
237 : : /**
238 : : * Initialize this assigner to generate values of type tn, with properties
239 : : * tep and assignment exclusion set aes.
240 : : */
241 : : void initialize(TypeNode tn,
242 : : TypeEnumeratorProperties* tep,
243 : : const std::vector<Node>& aes);
244 : : /** get the next term in the enumeration
245 : : *
246 : : * This method returns the next legal term based on type enumeration, where
247 : : * a term is legal it does not belong to the assignment exclusion set of
248 : : * this assigner. If no more terms exist, this method returns null. This
249 : : * should never be the case due to the conditions ensured by theory solvers
250 : : * for finite types. If it is the case, we give an assertion failure.
251 : : */
252 : : Node getNextAssignment();
253 : : /** The type enumerator */
254 : : std::unique_ptr<TypeEnumerator> d_te;
255 : : /** The assignment exclusion set of this Assigner */
256 : : std::vector<Node> d_assignExcSet;
257 : : /**
258 : : * Is active, flag set to true when all values in d_assignExcSet are
259 : : * constant.
260 : : */
261 : : bool d_isActive;
262 : : };
263 : : /** Is the given Assigner ready to assign values?
264 : : *
265 : : * This returns true if all values in the assignment exclusion set of a have
266 : : * a known value according to the state of this model builder (via a lookup
267 : : * in d_constantReps). It updates the assignment exclusion vector of a to
268 : : * these values whenever possible.
269 : : */
270 : : bool isAssignerActive(TheoryModel* tm, Assigner& a);
271 : : //------------------------------------for codatatypes
272 : : /** is v an excluded codatatype value?
273 : : *
274 : : * If this returns true, then v is a value
275 : : * that cannot be used during enumeration in step (4)
276 : : * of model construction.
277 : : *
278 : : * repSet is the set of representatives of the same type as v,
279 : : * assertedReps is a map from representatives t,
280 : : * eqc is the equivalence class that v reside.
281 : : *
282 : : * This function is used to avoid alpha-equivalent
283 : : * assignments for codatatype terms, described in
284 : : * Reynolds/Blanchette CADE 2015. In particular,
285 : : * this function returns true if v is in
286 : : * the set V^{x}_I from page 9, where x is eqc
287 : : * and I is the model we are building.
288 : : */
289 : : bool isExcludedCdtValue(Node v,
290 : : std::set<Node>* repSet,
291 : : std::map<Node, Node>& assertedReps,
292 : : Node eqc);
293 : : /** is codatatype value match
294 : : *
295 : : * Takes as arguments a codatatype value v, and a codatatype term r of the
296 : : * same sort.
297 : : *
298 : : * It returns true if it is possible that the value of r will be forced to
299 : : * be equal to v during model construction. A return value of false indicates
300 : : * that it is safe to use value v to avoid merging with r.
301 : : */
302 : : static bool isCdtValueMatch(Node v, Node r);
303 : : //------------------------------------end for codatatypes
304 : :
305 : : //---------------------------------for debugging finite model finding
306 : : /** does type tn involve an uninterpreted sort? */
307 : : bool involvesUSort(TypeNode tn) const;
308 : : /** is v an excluded value based on uninterpreted sorts?
309 : : * This gives an assertion failure in the case that v contains
310 : : * an uninterpreted constant whose index is out of the bounds
311 : : * specified by eqc_usort_count.
312 : : */
313 : : bool isExcludedUSortValue(std::map<TypeNode, unsigned>& eqc_usort_count,
314 : : Node v,
315 : : std::map<Node, bool>& visited);
316 : : //---------------------------------end for debugging finite model finding
317 : : }; /* class TheoryEngineModelBuilder */
318 : :
319 : : } // namespace theory
320 : : } // namespace cvc5::internal
321 : :
322 : : #endif /* CVC5__THEORY__THEORY_MODEL_BUILDER_H */
|
