GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_model.h Lines: 4 4 100.0 %
Date: 2021-03-23 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_model.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Clark Barrett, Mathias Preiner
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_H
18
#define CVC4__THEORY__THEORY_MODEL_H
19
20
#include <unordered_map>
21
#include <unordered_set>
22
23
#include "theory/ee_setup_info.h"
24
#include "theory/rep_set.h"
25
#include "theory/substitutions.h"
26
#include "theory/type_enumerator.h"
27
#include "theory/type_set.h"
28
#include "theory/uf/equality_engine.h"
29
30
namespace CVC4 {
31
namespace theory {
32
33
/** Theory Model class.
34
 *
35
 * This class represents a model produced by the TheoryEngine.
36
 * The data structures used to represent a model are:
37
 * (1) d_equalityEngine : an equality engine object, which stores
38
 *     an equivalence relation over all terms that exist in
39
 *     the current set of assertions.
40
 * (2) d_substitutions : a substitution map storing cases of
41
 *     explicitly solved terms, for instance during preprocessing.
42
 * (3) d_reps : a map from equivalence class representatives of
43
 *     the equality engine to the (constant) representatives
44
 *     assigned to that equivalence class.
45
 * (4) d_uf_models : a map from uninterpreted functions to their
46
 *     lambda representation.
47
 * (5) d_rep_set : a data structure that allows interpretations
48
 *     for types to be represented as terms. This is useful for
49
 *     finite model finding.
50
 *
51
 * These data structures are built after a full effort check with
52
 * no lemmas sent, within a call to:
53
 *    TheoryEngineModelBuilder::buildModel(...)
54
 * which includes subcalls to TheoryX::collectModelInfo(...) calls.
55
 *
56
 * These calls may modify the model object using the interface
57
 * functions below, including:
58
 * - assertEquality, assertPredicate, assertSkeleton,
59
 *   assertEqualityEngine.
60
 * - assignFunctionDefinition
61
 *
62
 * This class provides several interface functions:
63
 * - hasTerm, getRepresentative, areEqual, areDisequal
64
 * - getEqualityEngine
65
 * - getRepSet
66
 * - hasAssignedFunctionDefinition, getFunctionsToAssign
67
 * - getValue
68
 *
69
 * The above functions can be used for a model m after it has been
70
 * successfully built, i.e. when m->isBuiltSuccess() returns true.
71
 *
72
 * Additionally, all of the above functions, with the exception of getValue,
73
 * can be used during step (5) of TheoryEngineModelBuilder::buildModel, as
74
 * documented in theory_model_builder.h. In particular, we make calls to the
75
 * above functions such as getRepresentative() when assigning total
76
 * interpretations for uninterpreted functions.
77
 */
78
class TheoryModel
79
{
80
  friend class TheoryEngineModelBuilder;
81
public:
82
  TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
83
  virtual ~TheoryModel();
84
  /**
85
   * Finish init, where ee is the equality engine the model should use.
86
   */
87
  void finishInit(eq::EqualityEngine* ee);
88
89
  /** reset the model */
90
  virtual void reset();
91
  //---------------------------- for building the model
92
  /** Adds a substitution from x to t. */
93
  void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
94
  /** assert equality holds in the model
95
   *
96
   * This method returns true if and only if the equality engine of this model
97
   * is consistent after asserting the equality to this model.
98
   */
99
  bool assertEquality(TNode a, TNode b, bool polarity);
100
  /** assert predicate holds in the model
101
   *
102
   * This method returns true if and only if the equality engine of this model
103
   * is consistent after asserting the predicate to this model.
104
   */
105
  bool assertPredicate(TNode a, bool polarity);
106
  /** assert all equalities/predicates in equality engine hold in the model
107
   *
108
   * This method returns true if and only if the equality engine of this model
109
   * is consistent after asserting the equality engine to this model.
110
   */
111
  bool assertEqualityEngine(const eq::EqualityEngine* ee,
112
                            const std::set<Node>* termSet = NULL);
113
  /** assert skeleton
114
   *
115
   * This method gives a "skeleton" for the model value of the equivalence
116
   * class containing n. This should be an application of interpreted function
117
   * (e.g. datatype constructor, array store, set union chain). The subterms of
118
   * this term that are variables or terms that belong to other theories will
119
   * be filled in with model values.
120
   *
121
   * For example, if we call assertSkeleton on (C x y) where C is a datatype
122
   * constructor and x and y are variables, then the equivalence class of
123
   * (C x y) will be interpreted in m as (C x^m y^m) where
124
   * x^m = m->getValue( x ) and y^m = m->getValue( y ).
125
   *
126
   * It should be called during model generation, before final representatives
127
   * are chosen. In the case of TheoryEngineModelBuilder, it should be called
128
   * during Theory's collectModelInfo( ... ) functions.
129
   */
130
  void assertSkeleton(TNode n);
131
  /** set assignment exclusion set
132
   *
133
   * This method sets the "assignment exclusion set" for term n. This is a
134
   * set of terms whose value n must be distinct from in the model.
135
   *
136
   * This method should be used sparingly, and in a way such that model
137
   * building is still guaranteed to succeed. Term n is intended to be an
138
   * assignable term, typically of finite type. Thus, for example, this method
139
   * should not be called with a vector eset that is greater than the
140
   * cardinality of the type of n. Additionally, this method should not be
141
   * called in a way that introduces cyclic dependencies on the assignment order
142
   * of terms in the model. For example, providing { y } as the assignment
143
   * exclusion set of x and { x } as the assignment exclusion set of y will
144
   * cause model building to fail.
145
   *
146
   * The vector eset should contain only terms that occur in the model, or
147
   * are constants.
148
   *
149
   * Additionally, we (currently) require that an assignment exclusion set
150
   * should not be set for two terms in the same equivalence class, or to
151
   * equivalence classes with an assignable term. Otherwise an
152
   * assertion will be thrown by TheoryEngineModelBuilder during model building.
153
   */
154
  void setAssignmentExclusionSet(TNode n, const std::vector<Node>& eset);
155
  /** set assignment exclusion set group
156
   *
157
   * Given group = { x_1, ..., x_n }, this is semantically equivalent to calling
158
   * the above method on the following pairs of arguments:
159
   *   x1, eset
160
   *   x2, eset + { x_1 }
161
   *   ...
162
   *   xn, eset + { x_1, ..., x_{n-1} }
163
   * Similar restrictions should be considered as above when applying this
164
   * method to ensure that model building will succeed. Notice that for
165
   * efficiency, the implementation of how the above information is stored
166
   * may avoid constructing n copies of eset.
167
   */
168
  void setAssignmentExclusionSetGroup(const std::vector<TNode>& group,
169
                                      const std::vector<Node>& eset);
170
  /** get assignment exclusion set for term n
171
   *
172
   * If n has been given an assignment exclusion set, then this method returns
173
   * true and the set is added to eset. Otherwise, the method returns false.
174
   *
175
   * Additionally, if n was assigned an assignment exclusion set via a call to
176
   * setAssignmentExclusionSetGroup, it adds all members that were passed
177
   * in the first argument of that call to the vector group. Otherwise, it
178
   * adds n itself to group.
179
   */
180
  bool getAssignmentExclusionSet(TNode n,
181
                                 std::vector<Node>& group,
182
                                 std::vector<Node>& eset);
183
  /** have any assignment exclusion sets been created? */
184
  bool hasAssignmentExclusionSets() const;
185
  /** record approximation
186
   *
187
   * This notifies this model that the value of n was approximated in this
188
   * model such that the predicate pred (involving n) holds. For example,
189
   * for transcendental functions, we may determine an error bound on the
190
   * value of a transcendental function, say c-e <= y <= c+e where
191
   * c and e are constants. We call this function with n set to sin( x ) and
192
   * pred set to c-e <= sin( x ) <= c+e.
193
   *
194
   * If recordApproximation is called at least once during the model
195
   * construction process, then check-model is not guaranteed to succeed.
196
   * However, there are cases where we can establish the input is satisfiable
197
   * without constructing an exact model. For example, if x=.77, sin(x)=.7, and
198
   * say we have computed c=.7 and e=.01 as an approximation in the above
199
   * example, then we may reason that the set of assertions { sin(x)>.6 } is
200
   * satisfiable, albiet without establishing an exact (irrational) value for
201
   * sin(x).
202
   *
203
   * This function is simply for bookkeeping, it does not affect the model
204
   * construction process.
205
   */
206
  void recordApproximation(TNode n, TNode pred);
207
  /**
208
   * Same as above, but with a witness constant. This ensures that the
209
   * approximation predicate is of the form (or (= n witness) pred). This
210
   * is useful if the user wants to know a possible concrete value in
211
   * the range of the predicate.
212
   */
213
  void recordApproximation(TNode n, TNode pred, Node witness);
214
  /** set unevaluate/semi-evaluated kind
215
   *
216
   * This informs this model how it should interpret applications of terms with
217
   * kind k in getModelValue. We distinguish four categories of kinds:
218
   *
219
   * [1] "Evaluated"
220
   * This includes (standard) interpreted symbols like NOT, PLUS, UNION, etc.
221
   * These operators can be characterized by the invariant that they are
222
   * "evaluatable". That is, if they are applied to only constants, the rewriter
223
   * is guaranteed to rewrite the application to a constant. When getting
224
   * the model value of <k>( t1...tn ) where k is a kind of this category, we
225
   * compute the (constant) value of t1...tn, say this returns c1...cn, we
226
   * return the (constant) result of rewriting <k>( c1...cn ).
227
   *
228
   * [2] "Unevaluated"
229
   * This includes interpreted symbols like FORALL, EXISTS,
230
   * CARDINALITY_CONSTRAINT, that are not evaluatable. When getting a model
231
   * value for a term <k>( t1...tn ) where k is a kind of this category, we
232
   * check whether <k>( t1...tn ) exists in the equality engine of this model.
233
   * If it does, we return its representative, otherwise we return the term
234
   * itself.
235
   *
236
   * [3] "Semi-evaluated"
237
   * This includes kinds like BITVECTOR_ACKERMANNIZE_UDIV and others, typically
238
   * those that correspond to abstractions. Like unevaluated kinds, these
239
   * kinds do not have an evaluator. In contrast to unevaluated kinds, we
240
   * interpret a term <k>( t1...tn ) not appearing in the equality engine as an
241
   * arbitrary value instead of the term itself.
242
   *
243
   * [4] APPLY_UF, where getting the model value depends on an internally
244
   * constructed representation of a lambda model value (d_uf_models).
245
   * It is optional whether this kind is "evaluated" or "semi-evaluated".
246
   * In the case that it is "evaluated", get model rewrites the application
247
   * of the lambda model value of its operator to its evaluated arguments.
248
   *
249
   * By default, all kinds are considered "evaluated". The following methods
250
   * change the interpretation of various (non-APPLY_UF) kinds to one of the
251
   * above categories and should be called by the theories that own the kind
252
   * during Theory::finishInit. We set APPLY_UF to be semi-interpreted when
253
   * this model does not enabled function values (this is the case for the model
254
   * of TheoryEngine when the option assignFunctionValues is set to false).
255
   */
256
  void setUnevaluatedKind(Kind k);
257
  void setSemiEvaluatedKind(Kind k);
258
  /**
259
   * Set irrelevant kind. These kinds do not impact model generation, that is,
260
   * registered terms in theories of this kind do not need to be sent to
261
   * the model. An example is APPLY_TESTER.
262
   */
263
  void setIrrelevantKind(Kind k);
264
  /**
265
   * Get the set of irrelevant kinds that have been registered by the above
266
   * method.
267
   */
268
  const std::set<Kind>& getIrrelevantKinds() const;
269
  /** is legal elimination
270
   *
271
   * Returns true if x -> val is a legal elimination of variable x.
272
   * In particular, this ensures that val does not have any subterms that
273
   * are of unevaluated kinds.
274
   */
275
  bool isLegalElimination(TNode x, TNode val);
276
  //---------------------------- end building the model
277
278
  // ------------------- general equality queries
279
  /** does the equality engine of this model have term a? */
280
  bool hasTerm(TNode a);
281
  /** get the representative of a in the equality engine of this model */
282
  Node getRepresentative(TNode a);
283
  /** are a and b equal in the equality engine of this model? */
284
  bool areEqual(TNode a, TNode b);
285
  /** are a and b disequal in the equality engine of this model? */
286
  bool areDisequal(TNode a, TNode b);
287
  /** get the equality engine for this model */
288
7009
  eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; }
289
  // ------------------- end general equality queries
290
291
  /** Get value function.
292
   * This should be called only after a ModelBuilder
293
   * has called buildModel(...) on this model.
294
   */
295
  Node getValue(TNode n) const;
296
  /** get comments */
297
  void getComments(std::ostream& out) const;
298
299
  //---------------------------- separation logic
300
  /** set the heap and value sep.nil is equal to */
301
  void setHeapModel(Node h, Node neq);
302
  /** get the heap and value sep.nil is equal to */
303
  bool getHeapModel(Node& h, Node& neq) const;
304
  //---------------------------- end separation logic
305
306
  /** is the list of approximations non-empty? */
307
  bool hasApproximations() const;
308
  /** get approximations */
309
  std::vector<std::pair<Node, Node> > getApproximations() const;
310
  /** get domain elements for uninterpreted sort t */
311
  std::vector<Node> getDomainElements(TypeNode t) const;
312
  /** get the representative set object */
313
188850
  const RepSet* getRepSet() const { return &d_rep_set; }
314
  /** get the representative set object (FIXME: remove this, see #1199) */
315
13943
  RepSet* getRepSetPtr() { return &d_rep_set; }
316
317
  //---------------------------- model cores
318
  /** set using model core */
319
  void setUsingModelCore();
320
  /** record model core symbol */
321
  void recordModelCoreSymbol(Node sym);
322
  /** Return whether symbol expr is in the model core. */
323
  bool isModelCoreSymbol(Node sym) const;
324
  //---------------------------- end model cores
325
326
  /** get cardinality for sort */
327
  Cardinality getCardinality(TypeNode t) const;
328
329
  //---------------------------- function values
330
  /** a map from functions f to a list of all APPLY_UF terms with operator f */
331
  std::map< Node, std::vector< Node > > d_uf_terms;
332
  /** a map from functions f to a list of all HO_APPLY terms with first argument f */
333
  std::map< Node, std::vector< Node > > d_ho_uf_terms;
334
  /** are function values enabled? */
335
  bool areFunctionValuesEnabled() const;
336
  /** assign function value f to definition f_def */
337
  void assignFunctionDefinition( Node f, Node f_def );
338
  /** have we assigned function f? */
339
13908
  bool hasAssignedFunctionDefinition( Node f ) const { return d_uf_models.find( f )!=d_uf_models.end(); }
340
  /** get the list of functions to assign.
341
  * This list will contain all terms of function type that are terms in d_equalityEngine.
342
  * If higher-order is enabled, we ensure that this list is sorted by type size.
343
  * This allows us to assign functions T -> T before ( T x T ) -> T and before ( T -> T ) -> T,
344
  * which is required for "dag form" model construction (see TheoryModelBuilder::assignHoFunction).
345
  */
346
  std::vector< Node > getFunctionsToAssign();
347
  //---------------------------- end function values
348
  /** Get the name of this model */
349
  const std::string& getName() const;
350
  /**
351
   * For debugging, print the equivalence classes of the underlying equality
352
   * engine.
353
   */
354
  std::string debugPrintModelEqc() const;
355
356
 protected:
357
  /** Unique name of this model */
358
  std::string d_name;
359
  /** substitution map for this model */
360
  SubstitutionMap d_substitutions;
361
  /** equality engine containing all known equalities/disequalities */
362
  eq::EqualityEngine* d_equalityEngine;
363
  /** approximations (see recordApproximation) */
364
  std::map<Node, Node> d_approximations;
365
  /** list of all approximations */
366
  std::vector<std::pair<Node, Node> > d_approx_list;
367
  /** a set of kinds that are unevaluated */
368
  std::unordered_set<Kind, kind::KindHashFunction> d_unevaluated_kinds;
369
  /** a set of kinds that are semi-evaluated */
370
  std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
371
  /** The set of irrelevant kinds */
372
  std::set<Kind> d_irrKinds;
373
  /**
374
   * Map of representatives of equality engine to used representatives in
375
   * representative set
376
   */
377
  std::map<Node, Node> d_reps;
378
  /** Map of terms to their assignment exclusion set. */
379
  std::map<Node, std::vector<Node> > d_assignExcSet;
380
  /**
381
   * Map of terms to their "assignment exclusion set master". After a call to
382
   * setAssignmentExclusionSetGroup, the master of each term in group
383
   * (except group[0]) is set to group[0], which stores the assignment
384
   * exclusion set for that group in the above map.
385
   */
386
  std::map<Node, Node> d_aesMaster;
387
  /** Reverse of the above map */
388
  std::map<Node, std::vector<Node> > d_aesSlaves;
389
  /** stores set of representatives for each type */
390
  RepSet d_rep_set;
391
  /** true/false nodes */
392
  Node d_true;
393
  Node d_false;
394
  /** comment stream to include in printing */
395
  std::stringstream d_comment_str;
396
  /** are we using model cores? */
397
  bool d_using_model_core;
398
  /** symbols that are in the model core */
399
  std::unordered_set<Node, NodeHashFunction> d_model_core;
400
  /** Get model value function.
401
   *
402
   * This function is a helper function for getValue.
403
   */
404
  Node getModelValue(TNode n) const;
405
  /** add term internal
406
   *
407
   * This will do any model-specific processing necessary for n,
408
   * such as constraining the interpretation of uninterpreted functions.
409
   * This is called once for all terms in the equality engine, just before
410
   * a model builder constructs this model.
411
   */
412
  virtual void addTermInternal(TNode n);
413
 private:
414
  /** cache for getModelValue */
415
  mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
416
417
  //---------------------------- separation logic
418
  /** the value of the heap */
419
  Node d_sep_heap;
420
  /** the value of the nil element */
421
  Node d_sep_nil_eq;
422
  //---------------------------- end separation logic
423
424
  //---------------------------- function values
425
  /** whether function models are enabled */
426
  bool d_enableFuncModels;
427
  /** map from function terms to the (lambda) definitions
428
  * After the model is built, the domain of this map is all terms of function
429
  * type that appear as terms in d_equalityEngine.
430
  */
431
  std::map<Node, Node> d_uf_models;
432
  //---------------------------- end function values
433
};/* class TheoryModel */
434
435
}/* CVC4::theory namespace */
436
}/* CVC4 namespace */
437
438
#endif /* CVC4__THEORY__THEORY_MODEL_H */