GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/rep_set.h Lines: 9 14 64.3 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file rep_set.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Morgan Deters
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 Representative set class and utilities
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__REP_SET_H
18
#define CVC4__THEORY__REP_SET_H
19
20
#include <map>
21
#include <vector>
22
23
#include "expr/node.h"
24
#include "expr/type_node.h"
25
26
namespace CVC4 {
27
namespace theory {
28
29
class QuantifiersEngine;
30
31
/** representative set
32
 *
33
 * This class contains finite lists of values for types, typically values and
34
 * types that exist
35
 * in the equality engine of a model object.  In the following, "representative"
36
 * means a value that exists in this set.
37
 *
38
 * This class is used for finite model finding and other exhaustive
39
 * instantiation-based
40
 * methods. The class goes beyond just maintaining a list of values that occur
41
 * in the equality engine in the following ways:
42
43
 * (1) It maintains a partial mapping from representatives to a term that has
44
 * that value in the current
45
 * model.  This is important because algorithms like the instantiation method in
46
 * Reynolds et al CADE 2013
47
 * act on "term models" where domains in models are interpreted as a set of
48
 * representative terms. Hence,
49
 * instead of instantiating with e.g. uninterpreted constants u, we instantiate
50
 * with the corresponding term that is interpreted as u.
51
52
 * (2) It is mutable, calls to add(...) and complete(...) may modify this class
53
 * as necessary, for instance
54
 * in the case that there are no ground terms of a type that occurs in a
55
 * quantified formula, or for
56
 * exhaustive instantiation strategies that enumerate over small interpreted
57
 * finite types.
58
 */
59
11935
class RepSet {
60
 public:
61
11938
  RepSet(){}
62
63
  /** map from types to the list of representatives
64
   * TODO : as part of #1199, encapsulate this
65
   */
66
  std::map< TypeNode, std::vector< Node > > d_type_reps;
67
  /** clear the set */
68
  void clear();
69
  /** does this set have representatives of type tn? */
70
17265
  bool hasType(TypeNode tn) const { return d_type_reps.count(tn) > 0; }
71
  /** does this set have representative n of type tn? */
72
  bool hasRep(TypeNode tn, Node n) const;
73
  /** get the number of representatives for type */
74
  size_t getNumRepresentatives(TypeNode tn) const;
75
  /** get representative at index */
76
  Node getRepresentative(TypeNode tn, unsigned i) const;
77
  /**
78
   * Returns the representatives of a type for a `type_node` if one exists.
79
   * Otherwise, returns nullptr.
80
   */
81
  const std::vector<Node>* getTypeRepsOrNull(TypeNode type_node) const;
82
83
  /** add representative n for type tn, where n has type tn */
84
  void add( TypeNode tn, Node n );
85
  /** returns index in d_type_reps for node n */
86
  int getIndexFor( Node n ) const;
87
  /** complete the list for type t
88
   * Resets d_type_reps[tn] and repopulates by running the type enumerator for
89
   * that type exhaustively.
90
   * This should only be called for small finite interpreted types.
91
   */
92
  bool complete( TypeNode t );
93
  /** get term for representative
94
   * Returns a term that is interpreted as representative n in the current
95
   * model, null otherwise.
96
   */
97
  Node getTermForRepresentative(Node n) const;
98
  /** set term for representative
99
   * Called when t is interpreted as value n. Subsequent class to
100
   * getTermForRepresentative( n ) will return t.
101
   */
102
  void setTermForRepresentative(Node n, Node t);
103
  /** get existing domain value, with possible exclusions
104
    *   This function returns a term in d_type_reps[tn] but not in exclude
105
    */
106
  Node getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const;
107
  /** debug print */
108
  void toStream(std::ostream& out);
109
110
 private:
111
  /** whether the list of representatives for types are complete */
112
  std::map<TypeNode, bool> d_type_complete;
113
  /** map from representatives to their index in d_type_reps */
114
  std::map<Node, int> d_tmap;
115
  /** map from values to terms they were assigned for */
116
  std::map<Node, Node> d_values_to_terms;
117
};/* class RepSet */
118
119
//representative domain
120
typedef std::vector< int > RepDomain;
121
122
class RepBoundExt;
123
124
/**
125
 * Representative set iterator enumeration type, which indicates how the
126
 * bound on a variable was determined.
127
 */
128
enum RsiEnumType
129
{
130
  // the bound on the variable is invalid
131
  ENUM_INVALID = 0,
132
  // the bound on the variable was determined in the default way, i.e. based
133
  // on an enumeration of terms in the model.
134
  ENUM_DEFAULT,
135
  // The bound on the variable was determined in a custom way, i.e. via a
136
  // quantifiers module like the BoundedIntegers module.
137
  ENUM_CUSTOM,
138
};
139
140
/** Rep set iterator.
141
 *
142
 * This class is used for iterating over (tuples of) terms
143
 * in the domain(s) of a RepSet.
144
 *
145
 * To use it, first it must
146
 * be initialized with a call to:
147
 * - setQuantifier or setFunctionDomain
148
 * which initializes the d_owner field and sets up
149
 * initial information.
150
 *
151
 * Then, we increment over the tuples of terms in the
152
 * domains of the owner of this iterator using:
153
 * - increment and incrementAtIndex
154
 *
155
 * TODO (#1199): this class needs further documentation.
156
 */
157
class RepSetIterator {
158
public:
159
 RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr);
160
4377
 ~RepSetIterator() {}
161
 /** set that this iterator will be iterating over instantiations for a
162
  * quantifier */
163
 bool setQuantifier(Node q);
164
 /** set that this iterator will be iterating over the domain of a function */
165
 bool setFunctionDomain(Node op);
166
 /** increment the iterator */
167
 int increment();
168
 /** increment the iterator at index
169
  * This increments the i^th field of the
170
  * iterator, for examples, see operator next_i
171
  * in Figure 2 of Reynolds et al. CADE 2013.
172
  */
173
 int incrementAtIndex(int i);
174
 /** is the iterator finished? */
175
 bool isFinished() const;
176
 /** get domain size of the i^th field of this iterator */
177
 unsigned domainSize(unsigned i);
178
 /** Get the type of terms in the i^th field of this iterator */
179
 TypeNode getTypeOf(unsigned i) const;
180
 /**
181
  * Get the value for the i^th field in the tuple we are currently considering.
182
  * If valTerm is true, we return a term instead of a value by calling
183
  * RepSet::getTermForRepresentative on the value.
184
  */
185
 Node getCurrentTerm(unsigned i, bool valTerm = false) const;
186
 /** get the number of terms in the tuple we are considering */
187
103690
 unsigned getNumTerms() const { return d_index_order.size(); }
188
 /** get current terms */
189
 void getCurrentTerms(std::vector<Node>& terms) const;
190
 /** get index order, returns var # */
191
 unsigned getIndexOrder(unsigned v) { return d_index_order[v]; }
192
 /** get variable order, returns index # */
193
1532
 unsigned getVariableOrder(unsigned i) { return d_var_order[i]; }
194
 /** is incomplete
195
  * Returns true if we are iterating over a strict subset of
196
  * the domain of the quantified formula or function.
197
  */
198
7414
 bool isIncomplete() { return d_incomplete; }
199
 /** debug print methods */
200
 void debugPrint(const char* c);
201
 void debugPrintSmall(const char* c);
202
 // TODO (#1199): these should be private
203
 /** enumeration type for each field */
204
 std::vector<RsiEnumType> d_enum_type;
205
 /** the current tuple we are considering */
206
 std::vector<int> d_index;
207
208
private:
209
 /** rep set associated with this iterator */
210
 const RepSet* d_rs;
211
 /** rep set external bound information for this iterator */
212
 RepBoundExt* d_rext;
213
 /** types we are considering */
214
 std::vector<TypeNode> d_types;
215
 /** for each argument, the domain we are iterating over */
216
 std::vector<std::vector<Node> > d_domain_elements;
217
 /** initialize
218
  * This is called when the owner of this iterator is set.
219
  * It initializes the typing information for the types
220
  * that are involved in this iterator, initializes the
221
  * domain elements we are iterating over, and variable
222
  * and index orderings we are considering.
223
  */
224
 bool initialize();
225
 /** owner
226
  * This is the term that we are iterating for, which may either be:
227
  * (1) a quantified formula, or
228
  * (2) a function.
229
  */
230
 Node d_owner;
231
 /** reset index, 1:success, 0:empty, -1:fail */
232
 int resetIndex(unsigned i, bool initial = false);
233
 /** set index order (see below) */
234
 void setIndexOrder(std::vector<unsigned>& indexOrder);
235
 /** do reset increment the iterator at index=counter */
236
 int do_reset_increment(int counter, bool initial = false);
237
 /** ordering for variables we are iterating over
238
 *  For example, given reps = { a, b } and quantifier
239
 *    forall( x, y, z ) P( x, y, z )
240
 *  with d_index_order = { 2, 0, 1 },
241
 *    then we consider instantiations in this order:
242
 *      a/x a/y a/z
243
 *      a/x b/y a/z
244
 *      b/x a/y a/z
245
 *      b/x b/y a/z
246
 *      ...
247
 */
248
 std::vector<unsigned> d_index_order;
249
 /** Map from variables to the index they are considered at
250
 * For example, if d_index_order = { 2, 0, 1 }
251
 *    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
252
 */
253
 std::map<unsigned, unsigned> d_var_order;
254
 /** incomplete flag */
255
 bool d_incomplete;
256
};/* class RepSetIterator */
257
258
/** Representative bound external
259
 *
260
 * This class manages bound information
261
 * for an instance of a RepSetIterator.
262
 * Its main functionalities are to set
263
 * bounds on the domain of the iterator
264
 * over quantifiers and function arguments.
265
 */
266
4377
class RepBoundExt
267
{
268
 public:
269
4377
  virtual ~RepBoundExt() {}
270
  /** set bound
271
   *
272
   * This method initializes the vector "elements"
273
   * with list of terms to iterate over for the i^th
274
   * field of owner, where owner may be :
275
   * (1) A function, in which case we are iterating
276
   *     over domain elements of its argument type,
277
   * (2) A quantified formula, in which case we are
278
   *     iterating over domain elements of the type
279
   *     of its i^th bound variable.
280
   */
281
  virtual RsiEnumType setBound(Node owner,
282
                               unsigned i,
283
                               std::vector<Node>& elements) = 0;
284
  /** reset index
285
   *
286
   * This method initializes iteration for the i^th
287
   * field of owner, based on the current state of
288
   * the iterator rsi. It initializes the vector
289
   * "elements" with all appropriate terms to
290
   * iterate over in this context.
291
   * initial is whether this is the first call
292
   * to this function for this iterator.
293
   *
294
   * This method returns false if we were unable
295
   * to establish (finite) bounds for the current
296
   * field we are considering, which indicates that
297
   * the iterator will terminate with a failure.
298
   */
299
  virtual bool resetIndex(RepSetIterator* rsi,
300
                          Node owner,
301
                          unsigned i,
302
                          bool initial,
303
                          std::vector<Node>& elements)
304
  {
305
    return true;
306
  }
307
  /** initialize representative set for type
308
   *
309
   * Returns true if the representative set associated
310
   * with this bound has been given a complete interpretation
311
   * for type tn.
312
   */
313
  virtual bool initializeRepresentativesForType(TypeNode tn) { return false; }
314
  /** get variable order
315
   * If this method returns true, then varOrder is the order
316
   * in which we want to consider variables for the iterator.
317
   * If this method returns false, then varOrder is unchanged
318
   * and the RepSetIterator is free to choose a default
319
   * variable order.
320
   */
321
  virtual bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
322
  {
323
    return false;
324
  }
325
};
326
327
}/* CVC4::theory namespace */
328
}/* CVC4 namespace */
329
330
#endif /* CVC4__THEORY__REP_SET_H */