GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_model_builder.h Lines: 4 4 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
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) 2009-2021 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.\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) builder-specified pre-processing,
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) builder-specific 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
  /** pre-process build model
93
   * Do pre-processing 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 non-null 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 first-order, that is, all instances of the above
136
   * terms are not assignable if they have a higher-order (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 alpha-equivalent
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 */