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