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 : 64651 : 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 : : //-----------------------------------virtual functions
90 : : /** pre-process build model
91 : : * Do pre-processing specific to this model builder.
92 : : * Called in step (2) of the build construction,
93 : : * described above.
94 : : */
95 : : virtual bool preProcessBuildModel(TheoryModel* m);
96 : : /** process build model
97 : : * Do processing specific to this model builder.
98 : : * Called in step (5) of the build construction,
99 : : * described above.
100 : : * By default, this assigns values to each function
101 : : * that appears in m's equality engine.
102 : : */
103 : : virtual bool processBuildModel(TheoryModel* m);
104 : : /** debug the model
105 : : * Check assertions and printing debug information for the model.
106 : : * Calls after step (5) described above is complete.
107 : : */
108 : 15 : virtual void debugModel(CVC5_UNUSED TheoryModel* m) {}
109 : : //-----------------------------------end virtual functions
110 : :
111 : : /** Debug check model.
112 : : *
113 : : * This throws an assertion failure if the model contains an equivalence
114 : : * class with two terms t1 and t2 such that t1^M != t2^M.
115 : : */
116 : : void debugCheckModel(TheoryModel* m);
117 : :
118 : : /** Evaluate equivalence class
119 : : *
120 : : * If this method returns a non-null node c, then c is a constant and some
121 : : * term in the equivalence class of r evaluates to c based on the current
122 : : * state of the model m.
123 : : */
124 : : Node evaluateEqc(TheoryModel* m, TNode r);
125 : : /** is n an assignable expression?
126 : : *
127 : : * A term n is an assignable expression if its value is unconstrained by a
128 : : * standard model. Examples of assignable terms are:
129 : : * - variables,
130 : : * - applications of array select,
131 : : * - applications of datatype selectors,
132 : : * - applications of uninterpreted functions.
133 : : * Assignable terms must be first-order, that is, all instances of the above
134 : : * terms are not assignable if they have a higher-order (function) type.
135 : : */
136 : : bool isAssignable(TNode n);
137 : : /** add assignable subterms
138 : : * Adds all assignable subterms of n to tm's equality engine.
139 : : */
140 : : void addAssignableSubterms(TNode n, TheoryModel* tm, NodeSet& cache);
141 : : /** normalize representative r
142 : : *
143 : : * This returns a term that is equivalent to r's
144 : : * interpretation in the model m. It may do so
145 : : * by rewriting the application of r's operator to the
146 : : * result of normalizing each of r's children, if
147 : : * each child is constant.
148 : : */
149 : : Node normalize(TheoryModel* m, TNode r, bool evalOnly);
150 : : /** assign constant representative
151 : : *
152 : : * Called when equivalence class eqc is assigned a constant
153 : : * representative const_rep.
154 : : *
155 : : * eqc should be a representative of tm's equality engine.
156 : : */
157 : : void assignConstantRep(TheoryModel* tm, Node eqc, Node const_rep);
158 : : /** add to type list
159 : : *
160 : : * This adds to type_list the list of types that tn is built from.
161 : : * For example, if tn is (Array Int Bool) and type_list is empty,
162 : : * then we append ( Int, Bool, (Array Int Bool) ) to type_list.
163 : : */
164 : : void addToTypeList(TypeNode tn,
165 : : std::vector<TypeNode>& type_list,
166 : : std::unordered_set<TypeNode>& visiting);
167 : :
168 : : private:
169 : : /** normalized cache
170 : : * A temporary cache mapping terms to their
171 : : * normalized form, used during buildModel.
172 : : */
173 : : NodeMap d_normalizedCache;
174 : : /** mapping from terms to the constant associated with their equivalence class
175 : : */
176 : : std::map<Node, Node> d_constantReps;
177 : :
178 : : /** Theory engine model builder assigner class
179 : : *
180 : : * This manages the assignment of values to terms of a given type.
181 : : * In particular, it is a wrapper around a type enumerator that is restricted
182 : : * by a set of values that it cannot generate, called an "assignment exclusion
183 : : * set".
184 : : */
185 : : class Assigner
186 : : {
187 : : public:
188 : 12 : Assigner() : d_te(nullptr), d_isActive(false) {}
189 : : /**
190 : : * Initialize this assigner to generate values of type tn, with properties
191 : : * tep and assignment exclusion set aes.
192 : : */
193 : : void initialize(TypeNode tn,
194 : : TypeEnumeratorProperties* tep,
195 : : const std::vector<Node>& aes);
196 : : /** get the next term in the enumeration
197 : : *
198 : : * This method returns the next legal term based on type enumeration, where
199 : : * a term is legal it does not belong to the assignment exclusion set of
200 : : * this assigner. If no more terms exist, this method returns null. This
201 : : * should never be the case due to the conditions ensured by theory solvers
202 : : * for finite types. If it is the case, we give an assertion failure.
203 : : */
204 : : Node getNextAssignment();
205 : : /** The type enumerator */
206 : : std::unique_ptr<TypeEnumerator> d_te;
207 : : /** The assignment exclusion set of this Assigner */
208 : : std::vector<Node> d_assignExcSet;
209 : : /**
210 : : * Is active, flag set to true when all values in d_assignExcSet are
211 : : * constant.
212 : : */
213 : : bool d_isActive;
214 : : };
215 : : /** Is the given Assigner ready to assign values?
216 : : *
217 : : * This returns true if all values in the assignment exclusion set of a have
218 : : * a known value according to the state of this model builder (via a lookup
219 : : * in d_constantReps). It updates the assignment exclusion vector of a to
220 : : * these values whenever possible.
221 : : */
222 : : bool isAssignerActive(TheoryModel* tm, Assigner& a);
223 : : //------------------------------------for codatatypes
224 : : /** is v an excluded codatatype value?
225 : : *
226 : : * If this returns true, then v is a value
227 : : * that cannot be used during enumeration in step (4)
228 : : * of model construction.
229 : : *
230 : : * repSet is the set of representatives of the same type as v,
231 : : * assertedReps is a map from representatives t,
232 : : * eqc is the equivalence class that v reside.
233 : : *
234 : : * This function is used to avoid alpha-equivalent
235 : : * assignments for codatatype terms, described in
236 : : * Reynolds/Blanchette CADE 2015. In particular,
237 : : * this function returns true if v is in
238 : : * the set V^{x}_I from page 9, where x is eqc
239 : : * and I is the model we are building.
240 : : */
241 : : bool isExcludedCdtValue(Node v,
242 : : std::set<Node>* repSet,
243 : : std::map<Node, Node>& assertedReps,
244 : : Node eqc);
245 : : /** is codatatype value match
246 : : *
247 : : * Takes as arguments a codatatype value v, and a codatatype term r of the
248 : : * same sort.
249 : : *
250 : : * It returns true if it is possible that the value of r will be forced to
251 : : * be equal to v during model construction. A return value of false indicates
252 : : * that it is safe to use value v to avoid merging with r.
253 : : */
254 : : static bool isCdtValueMatch(Node v, Node r);
255 : : //------------------------------------end for codatatypes
256 : :
257 : : //---------------------------------for debugging finite model finding
258 : : /** does type tn involve an uninterpreted sort? */
259 : : bool involvesUSort(TypeNode tn) const;
260 : : /** is v an excluded value based on uninterpreted sorts?
261 : : * This gives an assertion failure in the case that v contains
262 : : * an uninterpreted constant whose index is out of the bounds
263 : : * specified by eqc_usort_count.
264 : : */
265 : : bool isExcludedUSortValue(std::map<TypeNode, unsigned>& eqc_usort_count,
266 : : Node v,
267 : : std::map<Node, bool>& visited);
268 : : //---------------------------------end for debugging finite model finding
269 : : }; /* class TheoryEngineModelBuilder */
270 : :
271 : : } // namespace theory
272 : : } // namespace cvc5::internal
273 : :
274 : : #endif /* CVC5__THEORY__THEORY_MODEL_BUILDER_H */
|
