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

Line Exec Source
1
/*********************                                                        */
2
/*! \file enum_stream_substitution.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Andrew Reynolds, 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 class for streaming concrete values (through substitutions) from
13
 ** enumerated abstract ones
14
 **/
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
19
20
#include "expr/node.h"
21
#include "theory/quantifiers/sygus/synth_conjecture.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace quantifiers {
26
27
/** Streamer of different values according to variable permutations
28
 *
29
 * Generates a new value (modulo rewriting) when queried in which its variables
30
 * are permuted (see EnumStreamSubstitution for more details).
31
 */
32
class EnumStreamPermutation
33
{
34
 public:
35
  EnumStreamPermutation(quantifiers::TermDbSygus* tds);
36
2
  ~EnumStreamPermutation() {}
37
  /** resets utility
38
   *
39
   * for each subset of the variables in value (according to their
40
   * subclasses_classes), a permutation utility is initialized
41
   */
42
  void reset(Node value);
43
  /** computes next permutation, if any, of value
44
   *
45
   * a "next" permutation is determined by having at least one new permutation
46
   * in one of the variable subclasses in the value.
47
   *
48
   * For example, if the variables of value (OP x1 x2 x3 x4) are partioned into
49
   * {{x1, x4}, {x2, x3}} then the sequence of getNext() is
50
   *
51
   * (OP x4 x2 x3 x1)
52
   * (OP x1 x3 x2 x4)
53
   * (OP x4 x3 x2 x1)
54
   *
55
   * Moreover, new values are only considered if they are unique modulo
56
   * rewriting. If for example OP were "+", then no next value would exist,
57
   * while if OP were "-" the only next value would be: (- x4 x2 x3 x1)
58
   *
59
   * Since the same variable can occur in different subfield types (and
60
   * therefore their datatype equivalents would have different types) a map from
61
   * variables to sets of constructors (see var_cons) is used to build
62
   * substitutions in a proper way when generating different combinations.
63
   */
64
  Node getNext();
65
  /** retrieve variables in class with given id */
66
  const std::vector<Node>& getVarsClass(unsigned id) const;
67
  /** retrieve number of variables being permuted from subclass with given id */
68
  unsigned getVarClassSize(unsigned id) const;
69
70
 private:
71
  /** sygus term database of current quantifiers engine */
72
  quantifiers::TermDbSygus* d_tds;
73
  /** maps subclass ids to subset of d_vars with that subclass id */
74
  std::map<unsigned, std::vector<Node>> d_var_classes;
75
  /** maps variables to subfield types with constructors for
76
   * the that variable, which are themselves associated with the respective
77
   * constructors */
78
  std::map<Node, std::map<TypeNode, Node>> d_var_tn_cons;
79
  /** whether first query */
80
  bool d_first;
81
  /** value to which we are generating permutations */
82
  Node d_value;
83
  /** generated permutations (modulo rewriting) */
84
  std::unordered_set<Node, NodeHashFunction> d_perm_values;
85
  /** retrieves variables occurring in value */
86
  void collectVars(Node n,
87
                   std::vector<Node>& vars,
88
                   std::unordered_set<Node, NodeHashFunction>& visited);
89
  /** Utility for stepwise application of Heap's algorithm for permutation
90
   *
91
   * see https://en.wikipedia.org/wiki/Heap%27s_algorithm
92
   */
93
6
  class PermutationState
94
  {
95
   public:
96
    PermutationState(const std::vector<Node>& vars);
97
    /** computes next permutation, i.e. execute one step of Heap's algorithm
98
     *
99
     * returns true if one exists, false otherwise
100
     *
101
     * when a new permutation is generated the the new variable arrangement is
102
     * stored in d_last_perm (in terms of d_vars' indices)
103
     */
104
    bool getNextPermutation();
105
    /** resets permutation state to initial variable ordering */
106
    void reset();
107
    /** retrieves last variable permutation
108
     *
109
     * vars is populated with the new variable arrangement
110
     */
111
    void getLastPerm(std::vector<Node>& vars);
112
    /** retrieve variables being permuted */
113
    const std::vector<Node>& getVars() const;
114
115
   private:
116
    /** variables being permuted */
117
    std::vector<Node> d_vars;
118
    /** last computed permutation of variables */
119
    std::vector<unsigned> d_last_perm;
120
    /** auxiliary position list for generating permutations */
121
    std::vector<unsigned> d_seq;
122
    /** current index being permuted */
123
    unsigned d_curr_ind;
124
  };
125
  /** permutation state of each variable subclass */
126
  std::vector<PermutationState> d_perm_state_class;
127
  /** current variable subclass being permuted */
128
  unsigned d_curr_ind;
129
};
130
131
/** Streamer of concrete values for enumerator
132
 *
133
 * When a given enumerator is "variable agnostic", only values in which
134
 * variables are ordered are chosen for it (see
135
 * TermDbSygus::registerEnumerator). If such values are seen as "abstract", in
136
 * the sense that each represent a set of values, this class can be used to
137
 * stream all the concrete values that correspond to them.
138
 *
139
 * For example a variable agnostic enumerator that contains three variables, x1,
140
 * x2, x3, in which x1 < x2 < x3, for which an "abstract" value (OP x1 x2) is
141
 * derived, will lead to the stream of "concrete" values
142
 *
143
 * (OP x1 x2)
144
 * (OP x1 x3)
145
 * (OP x2 x3)
146
 *
147
 * (OP x2 x1)
148
 * (OP x3 x1)
149
 * (OP x3 x2)
150
 *
151
 * in which for each permutation of the variables in the abstract value ([x1,
152
 * x2] and [x2, x1] in the above) we generate all the substitutions through
153
 * ordered combinations of the variables of the enumerator ([x1, x2], [x1, x3],
154
 * and [x2, x3] in the above).
155
 *
156
 * Moreover the permutations are generated modulo rewriting, s.t. if two
157
 * permutations are equivalent, only one is used.
158
 *
159
 * It should be noted that the variables of a variable agnostic enumerator are
160
 * kept in independent "subclasses" (see TermDbSygus::getSubclassForVar).
161
 * Therefore when streaming concrete values, permutations and combinations are
162
 * generated by the product of the permutations and combinations of each class.
163
 */
164
class EnumStreamSubstitution
165
{
166
 public:
167
  EnumStreamSubstitution(quantifiers::TermDbSygus* tds);
168
2
  ~EnumStreamSubstitution() {}
169
  /** initializes utility
170
   *
171
   * the combinations are generated from a initial set of variables (for now all
172
   * variables in given type).
173
   */
174
  void initialize(TypeNode tn);
175
  /** resets value for which substitutions will be generated through
176
   * combinations
177
   *
178
   * For each variable subclass in this utility, a subset is chosen with as
179
   * many variables as in the same variable subclass of value's variables.
180
   *
181
   * The combinations are performed modulo subclasses. For each subclass of the
182
   * given variables, a combination utility is initialized.
183
   *
184
   * For example, if the initial variable set is partioned into
185
   *
186
   * {1 -> {x1, x4}, 2 -> {x2, x3, x6}, 3 -> {x5}}
187
   *
188
   * and value's variables into
189
   *
190
   * {1 -> {x1, x4}, 2 -> {x2}, 3 -> {}}
191
   *
192
   * then the combination utilities are initialized such that for class 1 all
193
   * ordered subsets with two variables are chosen; for class 2 all ordered
194
   * subsets with one variable; and for class 3 no combination can be chosen.
195
   */
196
  void resetValue(Node value);
197
  /** computes next combination, if any, of value
198
   *
199
   * a "next" combination is determined by having at least one new combination
200
   * in one of the variable subclasses in the initial set of variables. If no
201
   * new combination exists, the cycle restarts with a new base value generated
202
   * by EnumStreamPermutation::getNext() (see above).
203
   *
204
   * This layered approach (of deriving all combinations for each permutation)
205
   * allows to consider only ordered combinations to generate all possible
206
   * variations of the base value. See the example in EnumStreamSubstitution for
207
   * further details.
208
   */
209
  Node getNext();
210
211
 private:
212
  /** sygus term database of current quantifiers engine */
213
  quantifiers::TermDbSygus* d_tds;
214
  /** type this utility has been initialized for */
215
  TypeNode d_tn;
216
  /** current value */
217
  Node d_value;
218
  /** maps subclass ids to d_tn's variables with that subclass id */
219
  std::map<unsigned, std::vector<Node>> d_var_classes;
220
  /** maps variables to subfield types with constructors for
221
   * the that variable, which are themselves associated with the respective
222
   * constructors */
223
  std::map<Node, std::map<TypeNode, Node>> d_var_tn_cons;
224
  /** last value generated after a combination
225
   *
226
   * If getNext() has been called, this is the return value of the most recent
227
   * call to getNext(). Otherwise, this value is null.
228
   */
229
  Node d_last;
230
  /** generated combinations */
231
  std::unordered_set<Node, NodeHashFunction> d_comb_values;
232
  /** permutation utility */
233
  EnumStreamPermutation d_stream_permutations;
234
  /** Utility for stepwise generation of ordered subsets of size k from n
235
   * variables */
236
6
  class CombinationState
237
  {
238
   public:
239
    CombinationState(unsigned n,
240
                     unsigned k,
241
                     unsigned subclass_id,
242
                     const std::vector<Node>& vars);
243
    /** computes next combination
244
     *
245
     * returns true if one exists, false otherwise
246
     */
247
    bool getNextCombination();
248
    /** resets combination state to first k variables in vars */
249
    void reset();
250
    /** retrieves last variable combination
251
     *
252
     * variables in new combination are stored in argument vars
253
     */
254
    void getLastComb(std::vector<Node>& vars);
255
    /** retrieve subclass id */
256
    const unsigned getSubclassId() const;
257
258
   private:
259
    /** subclass id of variables being combined */
260
    unsigned d_subclass_id;
261
    /** number of variables */
262
    unsigned d_n;
263
    /** size of subset */
264
    unsigned d_k;
265
    /** last combination state */
266
    std::vector<unsigned> d_last_comb;
267
    /** variables from which combination is extracted */
268
    std::vector<Node> d_vars;
269
  };
270
  /** combination state for each variable subclass */
271
  std::vector<CombinationState> d_comb_state_class;
272
  /** current class being combined */
273
  unsigned d_curr_ind;
274
};
275
276
/**
277
 * An enumerated value generator based on the above class. This is
278
 * SynthConjecture's interface to using the above utility.
279
 */
280
4
class EnumStreamConcrete : public EnumValGenerator
281
{
282
 public:
283
2
  EnumStreamConcrete(quantifiers::TermDbSygus* tds) : d_ess(tds) {}
284
  /** initialize this class with enumerator e */
285
  void initialize(Node e) override;
286
  /** get that value v was enumerated */
287
  void addValue(Node v) override;
288
  /** increment */
289
  bool increment() override;
290
  /** get the current value enumerated by this class */
291
  Node getCurrent() override;
292
293
 private:
294
  /** stream substitution utility */
295
  EnumStreamSubstitution d_ess;
296
  /** the current term generated by this class */
297
  Node d_currTerm;
298
};
299
300
}  // namespace quantifiers
301
}  // namespace theory
302
}  // namespace CVC4
303
304
#endif