GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus_sampler.h Lines: 3 3 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_sampler.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Fabian Wolff
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 sygus_sampler
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
19
20
#include <map>
21
#include "theory/evaluator.h"
22
#include "theory/quantifiers/lazy_trie.h"
23
#include "theory/quantifiers/sygus/term_database_sygus.h"
24
#include "theory/quantifiers/term_enumeration.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace quantifiers {
29
30
/** SygusSampler
31
 *
32
 * This class can be used to test whether two expressions are equivalent
33
 * by random sampling. We use this class for the following options:
34
 *
35
 * sygus-rr-synth: synthesize candidate rewrite rules by finding two terms
36
 * t1 and t2 do not rewrite to the same term, but are identical when considering
37
 * a set of sample points, and
38
 *
39
 * sygus-rr-verify: detect unsound rewrite rules by finding two terms t1 and
40
 * t2 that rewrite to the same term, but not identical when considering a set
41
 * of sample points.
42
 *
43
 * To use this class:
44
 * (1) Call initialize( tds, f, nsamples) where f is sygus datatype term.
45
 * (2) For terms n1....nm enumerated that correspond to builtin analog of sygus
46
 * term f, we call registerTerm( n1 )....registerTerm( nm ). It may be the case
47
 * that registerTerm( ni ) returns nj for some j < i. In this case, we have that
48
 * ni and nj are equivalent under the sample points in this class.
49
 *
50
 * For example, say the grammar for f is:
51
 *   A = 0 | 1 | x | y | A+A | ite( B, A, A )
52
 *   B = A <= A
53
 * If we call initialize( tds, f, 5 ), this class will generate 5 random sample
54
 * points for (x,y), say (0,0), (1,1), (0,1), (1,0), (2,2). The return values
55
 * of successive calls to registerTerm are listed below.
56
 *   registerTerm( 0 ) -> 0
57
 *   registerTerm( x ) -> x
58
 *   registerTerm( x+y ) -> x+y
59
 *   registerTerm( y+x ) -> x+y
60
 *   registerTerm( x+ite(x <= 1+1, 0, y ) ) -> x
61
 * Notice that the number of sample points can be configured for the above
62
 * options using sygus-samples=N.
63
 */
64
class SygusSampler : public LazyTrieEvaluator
65
{
66
 public:
67
  SygusSampler();
68
6971
  ~SygusSampler() override {}
69
70
  /** initialize
71
   *
72
   * tn : the return type of terms we will be testing with this class,
73
   * vars : the variables we are testing substitutions for,
74
   * nsamples : number of sample points this class will test,
75
   * unique_type_ids : if this is set to true, then we consider each variable
76
   * in vars to have a unique "type id". A type id is a finer-grained notion of
77
   * type that is used to determine when a rewrite rule is redundant.
78
   */
79
  virtual void initialize(TypeNode tn,
80
                          const std::vector<Node>& vars,
81
                          unsigned nsamples,
82
                          bool unique_type_ids = false);
83
  /** initialize sygus
84
   *
85
   * qe : pointer to quantifiers engine,
86
   * f : a term of some SyGuS datatype type whose values we will be
87
   * testing under the free variables in the grammar of f,
88
   * nsamples : number of sample points this class will test,
89
   * useSygusType : whether we will register terms with this sampler that have
90
   * the same type as f. If this flag is false, then we will be registering
91
   * terms of the analog of the type of f, that is, the builtin type that
92
   * f's type encodes in the deep embedding.
93
   */
94
  virtual void initializeSygus(TermDbSygus* tds,
95
                               Node f,
96
                               unsigned nsamples,
97
                               bool useSygusType);
98
  /** register term n with this sampler database
99
   *
100
   * forceKeep is whether we wish to force that n is chosen as a representative
101
   * value in the trie.
102
   */
103
  virtual Node registerTerm(Node n, bool forceKeep = false);
104
  /** get number of sample points */
105
1105
  unsigned getNumSamplePoints() const { return d_samples.size(); }
106
  /** get variables, adds d_vars to vars */
107
  void getVariables(std::vector<Node>& vars) const;
108
  /** get sample point
109
   *
110
   * Appends sample point #index to the vector pt, d_vars to vars.
111
   */
112
  void getSamplePoint(unsigned index,
113
                      std::vector<Node>& pt);
114
  /** Add pt to the set of sample points considered by this sampler */
115
  void addSamplePoint(std::vector<Node>& pt);
116
  /** evaluate n on sample point index */
117
  Node evaluate(Node n, unsigned index) override;
118
  /**
119
   * Compute the variables from the domain of d_var_index that occur in n,
120
   * store these in the vector fvs.
121
   */
122
  void computeFreeVariables(Node n, std::vector<Node>& fvs);
123
  /**
124
   * Returns the index of a sample point such that the evaluation of a and b
125
   * diverge, or -1 if no such sample point exists.
126
   */
127
  int getDiffSamplePointIndex(Node a, Node b);
128
129
  //--------------------------queries about terms
130
  /** is contiguous
131
   *
132
   * This returns whether n's free variables (terms occurring in the range of
133
   * d_type_vars) are a prefix of the list of variables in d_type_vars for each
134
   * type id. For instance, if d_type_vars[id] = { x, y } for some id, then
135
   * 0, x, x+y, y+x are contiguous but y is not. This is useful for excluding
136
   * terms from consideration that are alpha-equivalent to others.
137
   */
138
  bool isContiguous(Node n);
139
  /** is ordered
140
   *
141
   * This returns whether n's free variables are in order with respect to
142
   * variables in d_type_vars for each type. For instance, if
143
   * d_type_vars[id] = { x, y } for some id, then 0, x, x+y are ordered but
144
   * y and y+x are not.
145
   */
146
  bool isOrdered(Node n);
147
  /** is linear
148
   *
149
   * This returns whether n contains at most one occurrence of each free
150
   * variable. For example, x, x+y are linear, but x+x, (x-y)+y, (x+0)+(x+0) are
151
   * non-linear.
152
   */
153
  bool isLinear(Node n);
154
  /** check variables
155
   *
156
   * This returns false if !isOrdered(n) and checkOrder is true or !isLinear(n)
157
   * if checkLinear is true, or false otherwise.
158
   */
159
  bool checkVariables(Node n, bool checkOrder, bool checkLinear);
160
  /** contains free variables
161
   *
162
   * Returns true if the free variables of b are a subset of those in a, where
163
   * we require a strict subset if strict is true. Free variables are those that
164
   * occur in the range d_type_vars.
165
   */
166
  bool containsFreeVariables(Node a, Node b, bool strict = false);
167
  //--------------------------end queries about terms
168
  /** check equivalent
169
   *
170
   * Check whether bv and bvr are equivalent on all sample points, print
171
   * an error if not. Used with --sygus-rr-verify.
172
   */
173
  void checkEquivalent(Node bv, Node bvr);
174
175
 protected:
176
  /** sygus term database of d_qe */
177
  TermDbSygus* d_tds;
178
  /** term enumerator object (used for random sampling) */
179
  TermEnumeration d_tenum;
180
  /** samples */
181
  std::vector<std::vector<Node> > d_samples;
182
  /** evaluator class */
183
  Evaluator d_eval;
184
  /** data structure to check duplication of sample points */
185
377356
  class PtTrie
186
  {
187
   public:
188
    /** add pt to this trie, returns true if pt is not a duplicate. */
189
    bool add(std::vector<Node>& pt);
190
191
   private:
192
    /** the children of this node */
193
    std::map<Node, PtTrie> d_children;
194
  };
195
  /** a trie for samples */
196
  PtTrie d_samples_trie;
197
  /** the sygus type for this sampler (if applicable). */
198
  TypeNode d_ftn;
199
  /** whether we are registering terms of sygus types with this sampler */
200
  bool d_use_sygus_type;
201
  /**
202
   * For each (sygus) type, a map from builtin terms to the sygus term they
203
   * correspond to.
204
   */
205
  std::map<TypeNode, std::map<Node, Node> > d_builtin_to_sygus;
206
  /** all variables we are sampling values for */
207
  std::vector<Node> d_vars;
208
  /** type variables
209
   *
210
   * We group variables according to "type ids". Two variables have the same
211
   * type id if they have indistinguishable status according to this sampler.
212
   * This is a finer-grained grouping than types. For example, two variables
213
   * of the same type may have different type ids if they occur as constructors
214
   * of a different set of sygus types in the grammar we are considering.
215
   * For instance, we assign x and y different type ids in this grammar:
216
   *   A -> B + C
217
   *   B -> x | 0 | 1
218
   *   C -> y
219
   * Type ids are computed for each variable in d_vars during initialize(...).
220
   *
221
   * For each type id, a list of variables in the grammar we are considering,
222
   * for that type. These typically correspond to the arguments of the
223
   * function-to-synthesize whose grammar we are considering.
224
   */
225
  std::map<unsigned, std::vector<Node> > d_type_vars;
226
  /**
227
   * A map all variables in the grammar we are considering to their index in
228
   * d_type_vars.
229
   */
230
  std::map<Node, unsigned> d_var_index;
231
  /**  Map from variables to the id (the domain of d_type_vars). */
232
  std::map<Node, unsigned> d_type_ids;
233
  /** constants
234
   *
235
   * For each type, a list of constants in the grammar we are considering, for
236
   * that type.
237
   */
238
  std::map<TypeNode, std::vector<Node> > d_type_consts;
239
  /** a lazy trie for each type
240
   *
241
   * This stores the evaluation of all terms registered to this class.
242
   *
243
   * Notice if we are registering sygus terms with this class, then terms
244
   * are grouped into this trie according to their sygus type, and not their
245
   * builtin type. For example, for grammar:
246
   *   A -> x | B+1
247
   *   B -> x | 0 | 1 | B+B
248
   * If we register C^B_+( C^B_x(), C^B_0() ) and C^A_x() with this class,
249
   * then x+0 is registered to d_trie[B] and x is registered to d_trie[A],
250
   * and no rewrite rule is reported. The reason for this is that otherwise
251
   * we would end up reporting many useless rewrites since the same builtin
252
   * term can be generated by multiple sygus types (e.g. C^B_x() and C^A_x()).
253
   */
254
  std::map<TypeNode, LazyTrie> d_trie;
255
  /** is this sampler valid?
256
   *
257
   * A sampler can be invalid if sample points cannot be generated for a type
258
   * of an argument to function f.
259
   */
260
  bool d_is_valid;
261
  /** initialize samples
262
   *
263
   * Adds nsamples sample points to d_samples.
264
   */
265
  void initializeSamples(unsigned nsamples);
266
  /** get random value for a type
267
   *
268
   * Returns a random value for the given type based on the random number
269
   * generator. Currently, supported types:
270
   *
271
   * Bool, Bitvector : returns a random value in the range of that type.
272
   * Int, String : returns a random string of values in (base 10) of random
273
   * length, currently by a repeated coin flip.
274
   * Real : returns the division of two random integers, where the denominator
275
   * is omitted if it is zero.
276
   */
277
  Node getRandomValue(TypeNode tn);
278
  /** get sygus random value
279
   *
280
   * Returns a random value based on the sygus type tn. The return value is
281
   * a constant in the analog type of tn. This function chooses either to
282
   * return a random value, or otherwise will construct a constant based on
283
   * a random constructor of tn whose builtin operator is not a variable.
284
   *
285
   * rchance: the chance that the call to this function will be forbidden
286
   * from making recursive calls and instead must return a value based on
287
   * a nullary constructor of tn or based on getRandomValue above.
288
   * rinc: the percentage to increment rchance on recursive calls.
289
   *
290
   * For example, consider the grammar:
291
   *   A -> x | y | 0 | 1 | +( A, A ) | ite( B, A, A )
292
   *   B -> A = A
293
   * If we call this function on A and rchance is 0.0, there are five evenly
294
   * chosen possibilities, either we return a random value via getRandomValue
295
   * above, or we choose one of the four non-variable constructors of A.
296
   * Say we choose ite, then we recursively call this function for
297
   * B, A, and A, which return constants c1, c2, and c3. Then, this function
298
   * returns the rewritten form of ite( c1, c2, c3 ).
299
   * If on the other hand, rchance was 0.5 and rand() < 0.5. Then, we force
300
   * this call to terminate by either selecting a random value via
301
   * getRandomValue, 0 or 1.
302
   */
303
  Node getSygusRandomValue(TypeNode tn,
304
                           double rchance,
305
                           double rinc,
306
                           unsigned depth = 0);
307
  /** map from sygus types to non-variable constructors */
308
  std::map<TypeNode, std::vector<unsigned> > d_rvalue_cindices;
309
  /** map from sygus types to non-variable nullary constructors */
310
  std::map<TypeNode, std::vector<unsigned> > d_rvalue_null_cindices;
311
  /** the random string alphabet */
312
  std::vector<unsigned> d_rstring_alphabet;
313
  /** map from variables to sygus types that include them */
314
  std::map<Node, std::vector<TypeNode> > d_var_sygus_types;
315
  /** map from constants to sygus types that include them */
316
  std::map<Node, std::vector<TypeNode> > d_const_sygus_types;
317
  /** register sygus type, initializes the above two data structures */
318
  void registerSygusType(TypeNode tn);
319
};
320
321
} /* CVC4::theory::quantifiers namespace */
322
} /* CVC4::theory namespace */
323
} /* CVC4 namespace */
324
325
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */