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

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_enumerator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 sygus_enumerator
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
19
20
#include <map>
21
#include <unordered_set>
22
#include "expr/node.h"
23
#include "expr/type_node.h"
24
#include "theory/quantifiers/sygus/synth_conjecture.h"
25
#include "theory/quantifiers/sygus/term_database_sygus.h"
26
27
namespace CVC4 {
28
namespace theory {
29
namespace quantifiers {
30
31
class SynthConjecture;
32
class SygusPbe;
33
34
/** SygusEnumerator
35
 *
36
 * This class is used for enumerating all terms of a sygus datatype type. At
37
 * a high level, it is used as an alternative approach to sygus datatypes
38
 * solver as a candidate generator in a synthesis loop. It filters terms based
39
 * on redundancy criteria, for instance, it does not generate two terms whose
40
 * builtin terms (TermDb::sygusToBuiltin) can be shown to be equivalent via
41
 * rewriting. It enumerates terms in order of sygus term size
42
 * (TermDb::getSygusTermSize).
43
 *
44
 * It also can be configured to enumerates sygus terms with free variables,
45
 * (as opposed to variables bound in the formal arguments list of the
46
 * function-to-synthesize), where each free variable appears in exactly one
47
 * subterm. For grammar:
48
 *   S -> 0 | 1 | x | S+S
49
 * this enumerator will generate the stream:
50
 *   z1, C_0, C_1, C_x, C_+(z1, z2), C_+(z1, C_1), C_+(C_1, C_1) ...
51
 * and so on, where z1 and z2 are variables of sygus datatype type S. We call
52
 * these "shapes". This feature can be enabled by setting enumShapes to true
53
 * in the constructor below.
54
 */
55
class SygusEnumerator : public EnumValGenerator
56
{
57
 public:
58
  SygusEnumerator(TermDbSygus* tds,
59
                  SynthConjecture* p,
60
                  SygusStatistics& s,
61
                  bool enumShapes = false);
62
386
  ~SygusEnumerator() {}
63
  /** initialize this class with enumerator e */
64
  void initialize(Node e) override;
65
  /** Inform this generator that abstract value v was enumerated. */
66
  void addValue(Node v) override;
67
  /** increment */
68
  bool increment() override;
69
  /** Get the next concrete value generated by this class. */
70
  Node getCurrent() override;
71
  /** Are we enumerating shapes? */
72
  bool isEnumShapes() const;
73
74
 private:
75
  /** pointer to term database sygus */
76
  TermDbSygus* d_tds;
77
  /** pointer to the synth conjecture that owns this enumerator */
78
  SynthConjecture* d_parent;
79
  /** reference to the statistics of parent */
80
  SygusStatistics& d_stats;
81
  /** Whether we are enumerating shapes */
82
  bool d_enumShapes;
83
  /** Term cache
84
   *
85
   * This stores a list of terms for a given sygus type. The key features of
86
   * this data structure are that terms are stored in order of size,
87
   * indices can be recorded that indicate where terms of size n begin for each
88
   * natural number n, and redundancy criteria are used for discarding terms
89
   * that are not relevant. This includes discarding terms whose builtin version
90
   * is the same up to T-rewriting with another, or is equivalent under
91
   * examples, if the conjecture in question is in examples form and
92
   * sygusSymBreakPbe is enabled.
93
   *
94
   * This class also computes static information about sygus types that is
95
   * relevant for enumeration. Primarily, this includes mapping constructors
96
   * to "constructor classes". Two sygus constructors can be placed in the same
97
   * constructor class if their constructor weight is equal, and the tuple
98
   * of their argument types are the same. For example, for:
99
   *   A -> A+B | A-B | A*B | A+A | A | x
100
   * The first three constructors above can be placed in the same constructor
101
   * class, assuming they have identical weights. Constructor classes are used
102
   * as an optimization when enumerating terms, since they expect the same
103
   * tuple of argument terms for constructing a term of a fixed size.
104
   *
105
   * Constructor classes are allocated such that the constructor weights are
106
   * in ascending order. This allows us to avoid constructors whose weight
107
   * is greater than n while we are trying to enumerate terms of sizes strictly
108
   * less than n.
109
   *
110
   * Constructor class 0 is reserved for nullary operators with weight 0. This
111
   * is an optimization so that such constructors can be skipped for sizes
112
   * greater than 0, since we know all terms generated by these constructors
113
   * have size 0.
114
   */
115
394
  class TermCache
116
  {
117
   public:
118
    TermCache();
119
    /** initialize this cache */
120
    void initialize(SygusStatistics* s,
121
                    Node e,
122
                    TypeNode tn,
123
                    TermDbSygus* tds,
124
                    ExampleEvalCache* ece = nullptr);
125
    /** get last constructor class index for weight
126
     *
127
     * This returns a minimal index n such that all constructor classes at
128
     * index < n have weight at most w.
129
     */
130
    unsigned getLastConstructorClassIndexForWeight(unsigned w) const;
131
    /** get num constructor classes */
132
    unsigned getNumConstructorClasses() const;
133
    /** get the constructor indices for constructor class i */
134
    void getConstructorClass(unsigned i, std::vector<unsigned>& cclass) const;
135
    /** get argument types for constructor class i */
136
    void getTypesForConstructorClass(unsigned i,
137
                                     std::vector<TypeNode>& types) const;
138
    /** get constructor weight for constructor class i */
139
    unsigned getWeightForConstructorClass(unsigned i) const;
140
141
    /**
142
     * Add sygus term n to this cache, return true if the term was unique based
143
     * on the redundancy criteria used by this class.
144
     */
145
    bool addTerm(Node n);
146
    /**
147
     * Indicate to this cache that we are finished enumerating terms of the
148
     * current size.
149
     */
150
    void pushEnumSizeIndex();
151
    /** Get the current size of terms that we are enumerating */
152
    unsigned getEnumSize() const;
153
    /** get the index at which size s terms start, where s <= getEnumSize() */
154
    unsigned getIndexForSize(unsigned s) const;
155
    /** get the index^th term successfully added to this cache */
156
    Node getTerm(unsigned index) const;
157
    /** get the number of terms successfully added to this cache */
158
    unsigned getNumTerms() const;
159
    /** are we finished enumerating terms? */
160
    bool isComplete() const;
161
    /** set that we are finished enumerating terms */
162
    void setComplete();
163
164
   private:
165
    /** reference to the statistics of parent */
166
    SygusStatistics* d_stats;
167
    /** the enumerator this cache is for */
168
    Node d_enum;
169
    /** the sygus type of terms in this cache */
170
    TypeNode d_tn;
171
    /** pointer to term database sygus */
172
    TermDbSygus* d_tds;
173
    /**
174
     * Pointer to the example evaluation cache utility (used for symmetry
175
     * breaking).
176
     */
177
    ExampleEvalCache* d_eec;
178
    //-------------------------static information about type
179
    /** is d_tn a sygus type? */
180
    bool d_isSygusType;
181
    /** number of constructor classes */
182
    unsigned d_numConClasses;
183
    /** Map from weights to the starting constructor class for that weight. */
184
    std::map<unsigned, unsigned> d_weightToCcIndex;
185
    /** Information for each constructor class */
186
    class ConstructorClass
187
    {
188
     public:
189
1012
      ConstructorClass() : d_weight(0) {}
190
1012
      ~ConstructorClass() {}
191
      /** The indices of the constructors in this constructor class */
192
      std::vector<unsigned> d_cons;
193
      /** The argument types of the constructor class */
194
      std::vector<TypeNode> d_types;
195
      /** Constructor weight */
196
      unsigned d_weight;
197
    };
198
    std::map<unsigned, ConstructorClass> d_cclass;
199
    /** constructor to indices */
200
    std::map<unsigned, std::vector<unsigned>> d_cToCIndices;
201
    //-------------------------end static information about type
202
203
    /** the list of sygus terms we have enumerated */
204
    std::vector<Node> d_terms;
205
    /** the set of builtin terms corresponding to the above list */
206
    std::unordered_set<Node, NodeHashFunction> d_bterms;
207
    /**
208
     * The index of first term whose size is greater than or equal to that size,
209
     * if it exists.
210
     */
211
    std::map<unsigned, unsigned> d_sizeStartIndex;
212
    /** the maximum size of terms we have stored in this cache so far */
213
    unsigned d_sizeEnum;
214
    /** whether this term cache is complete */
215
    bool d_isComplete;
216
    /** sampler (for --sygus-rr-verify) */
217
    quantifiers::SygusSampler d_samplerRrV;
218
    /** is the above sampler initialized? */
219
    bool d_sampleRrVInit;
220
  };
221
  /** above cache for each sygus type */
222
  std::map<TypeNode, TermCache> d_tcache;
223
  /** initialize term cache for type tn */
224
  void initializeTermCache(TypeNode tn);
225
226
  /** virtual class for term enumerators */
227
  class TermEnum
228
  {
229
   public:
230
    TermEnum();
231
4240
    virtual ~TermEnum() {}
232
    /** get the current size of terms we are enumerating */
233
    unsigned getCurrentSize();
234
    /** get the current term of the enumerator */
235
    virtual Node getCurrent() = 0;
236
    /** increment the enumerator, return false if the enumerator is finished */
237
    virtual bool increment() = 0;
238
239
   protected:
240
    /** pointer to the sygus enumerator class */
241
    SygusEnumerator* d_se;
242
    /** the (sygus) type of terms we are enumerating */
243
    TypeNode d_tn;
244
    /** the current size of terms we are enumerating */
245
    unsigned d_currSize;
246
  };
247
  class TermEnumMaster;
248
  /** A "slave" enumerator
249
   *
250
   * A slave enumerator simply iterates over an index in a given term cache,
251
   * and relies on a pointer to a "master" enumerator to generate new terms
252
   * whenever necessary.
253
   *
254
   * This class maintains the following invariants, for tc=d_se->d_tcache[d_tn]:
255
   * (1) d_index < tc.getNumTerms(),
256
   * (2) d_currSize is the term size of tc.getTerm( d_index ),
257
   * (3) d_hasIndexNextEnd is (d_currSize < tc.getEnumSize()),
258
   * (4) If d_hasIndexNextEnd is true, then
259
   *       d_indexNextEnd = tc.getIndexForSize(d_currSize+1), and
260
   *       d_indexNextEnd > d_index.
261
   *
262
   * Intuitively, these invariants say (1) d_index is a valid index in the
263
   * term cache, (2) d_currSize is the sygus term size of getCurrent(), (3)
264
   * d_hasIndexNextEnd indicates whether d_indexNextEnd is valid, and (4)
265
   * d_indexNextEnd is the index in the term cache where terms of the current
266
   * size end, if such an index exists.
267
   */
268
3846
  class TermEnumSlave : public TermEnum
269
  {
270
   public:
271
    TermEnumSlave();
272
    /**
273
     * Initialize this enumerator to enumerate terms of type tn whose size is in
274
     * the range [sizeMin, sizeMax], inclusive. If this function returns true,
275
     * then getCurrent() will return the first term in the stream, which is
276
     * non-empty. Further terms are generated by increment()/getCurrent().
277
     */
278
    bool initialize(SygusEnumerator* se,
279
                    TypeNode tn,
280
                    unsigned sizeMin,
281
                    unsigned sizeMax);
282
    /** get the current term of the enumerator */
283
    Node getCurrent() override;
284
    /** increment the enumerator */
285
    bool increment() override;
286
287
   private:
288
    /** the maximum size of terms this enumerator should enumerate */
289
    unsigned d_sizeLim;
290
    /** the current index in the term cache we are considering */
291
    unsigned d_index;
292
    /** the index in the term cache where terms of the current size end */
293
    unsigned d_indexNextEnd;
294
    /** whether d_indexNextEnd refers to a valid index */
295
    bool d_hasIndexNextEnd;
296
    /** pointer to the master enumerator of type d_tn */
297
    TermEnum* d_master;
298
    /** validate invariants on d_index, d_indexNextEnd, d_hasIndexNextEnd */
299
    bool validateIndex();
300
    /** validate invariants on  d_indexNextEnd, d_hasIndexNextEnd  */
301
    void validateIndexNextEnd();
302
  };
303
  /** Class for "master" enumerators
304
   *
305
   * This enumerator is used to generate new terms of a given type d_tn. It
306
   * generates all terms of type d_tn that are not redundant based on the
307
   * current criteria.
308
   *
309
   * To enumerate terms, this class performs the following steps as necessary
310
   * during a call to increment():
311
   * - Fix the size of terms "d_currSize" we are currently enumerating,
312
   * - Set the constructor class "d_consClassNum" whose constructors are the top
313
   * symbol of the current term we are constructing. All constructors from this
314
   * class have the same weight, which we store in d_ccWeight,
315
   * - Initialize the current children "d_children" so that the sum of their
316
   * current sizes is exactly (d_currSize - d_ccWeight),
317
   * - Increment the current set of children until a new tuple of terms is
318
   * considered,
319
   * - Set the constructor "d_consNum" from within the constructor class,
320
   * - Build the current term and check whether it is not redundant according
321
   * to the term cache of its type.
322
   *
323
   * We say this enumerator is active if initialize(...) returns true, and the
324
   * last call (if any) to increment returned true.
325
   *
326
   * This class maintains the following invariants, for tc=d_se->d_tcache[d_tn],
327
   * if it is active:
328
   * (1) getCurrent() is tc.getTerm(tc.getNumTerms()-1),
329
   * (2) tc.pushEnumSizeIndex() has been called by this class exactly
330
   * getCurrentSize() times.
331
   * In other words, (1) getCurrent() is always the last term in the term cache
332
   * of the type of this enumerator tc, and (2) the size counter of tc is in
333
   * sync with the current size of this enumerator, that is, the master
334
   * enumerator is responsible for communicating size boundaries to its term
335
   * cache.
336
   */
337
375
  class TermEnumMaster : public TermEnum
338
  {
339
   public:
340
    TermEnumMaster();
341
    /**
342
     * Initialize this enumerator to enumerate (all) terms of type tn, modulo
343
     * the redundancy criteria used by this class.
344
     */
345
    bool initialize(SygusEnumerator* se, TypeNode tn);
346
    /** get the current term of the enumerator */
347
    Node getCurrent() override;
348
    /** increment the enumerator
349
     *
350
     * Returns true if there are more terms to enumerate, in which case a
351
     * subsequent call to getCurrent() returns the next enumerated term. This
352
     * method returns false if the last call to increment() has yet to
353
     * terminate. This can happen for recursive datatypes where a slave
354
     * enumerator may request that this class increment the next term. We avoid
355
     * an infinite loop by guarding this with the d_isIncrementing flag and
356
     * return false.
357
     */
358
    bool increment() override;
359
360
   private:
361
    /** pointer to term database sygus */
362
    TermDbSygus* d_tds;
363
    /** are we enumerating shapes? */
364
    bool d_enumShapes;
365
    /** have we initialized the shape enumeration? */
366
    bool d_enumShapesInit;
367
    /** are we currently inside a increment() call? */
368
    bool d_isIncrementing;
369
    /** cache for getCurrent() */
370
    Node d_currTerm;
371
    /** is d_currTerm set */
372
    bool d_currTermSet;
373
    //----------------------------- current constructor class information
374
    /** the next constructor class we are using */
375
    unsigned d_consClassNum;
376
    /** the constructors in the current constructor class */
377
    std::vector<unsigned> d_ccCons;
378
    /** the types of the current constructor class */
379
    std::vector<TypeNode> d_ccTypes;
380
    /** the operator weight for the constructor class */
381
    unsigned d_ccWeight;
382
    //----------------------------- end current constructor class information
383
    /** If >0, 1 + the index in d_ccCons we are considering */
384
    unsigned d_consNum;
385
    /** the child enumerators for this enumerator */
386
    std::map<unsigned, TermEnumSlave> d_children;
387
    /** the current sum of current sizes of the enumerators in d_children */
388
    unsigned d_currChildSize;
389
    /**
390
     * The number of indices, starting from zero, in d_children that point to
391
     * initialized slave enumerators.
392
     */
393
    unsigned d_childrenValid;
394
    /** initialize children
395
     *
396
     * Initialize all the remaining uninitialized children of this enumerator.
397
     * If this method returns true, then each of d_children are
398
     * initialized to be slave enumerators of the argument types indicated by
399
     * d_ccTypes, and the sum of their current sizes (d_currChildSize) is
400
     * exactly (d_currSize - d_ccWeight). If this method returns false, then
401
     * it was not possible to initialize the children such that they meet the
402
     * size requirements, and such that the assignments from children to size
403
     * has not already been considered. In this case, all updates to d_children
404
     * are reverted and d_currChildSize and d_childrenValid are reset to their
405
     * values prior to this call.
406
     */
407
    bool initializeChildren();
408
    /** initialize child
409
     *
410
     * Initialize child i to enumerate terms whose size is at least sizeMin,
411
     * and whose maximum size is the largest size such that we can still
412
     * construct terms for the given constructor class and the current children
413
     * whose size is not more than the current size d_currSize. Additionally,
414
     * if i is the last child, we modify sizeMin such that it is exactly the
415
     * size of terms needed for the children to sum up to size d_currSize.
416
     */
417
    bool initializeChild(unsigned i, unsigned sizeMin);
418
    /** increment internal, helper for increment() */
419
    bool incrementInternal();
420
    /**
421
     * The vector children is a set of terms given to
422
     *    NodeManager::mkNode(APPLY_CONSTRUCTOR, children)
423
     * This converts children so that all sygus free variables are unique. Note
424
     * that the first child is a constructor operator and should be skipped.
425
     */
426
    void childrenToShape(std::vector<Node>& children);
427
    /**
428
     * Convert n into shape based on the variable counters. For example if
429
     * vcounter is { Int -> 7 }, then (+ x1 x2) is converted to (+ x7 x8) and
430
     * vouncter is updated to { Int -> 9 }.
431
     */
432
    Node convertShape(Node n, std::map<TypeNode, int>& vcounter);
433
  };
434
  /** an interpreted value enumerator
435
   *
436
   * This enumerator uses the builtin type enumerator for a given type. It
437
   * is used to fill in concrete holes into "any constant" constructors
438
   * when sygus-repair-const is not enabled. The number of terms of size n
439
   * is m^n, where m is configurable via --sygus-active-gen-enum-cfactor=m.
440
   */
441
22
  class TermEnumMasterInterp : public TermEnum
442
  {
443
   public:
444
    TermEnumMasterInterp(TypeNode tn);
445
    /** initialize this enumerator */
446
    bool initialize(SygusEnumerator* se, TypeNode tn);
447
    /** get the current term of the enumerator */
448
    Node getCurrent() override;
449
    /** increment the enumerator */
450
    bool increment() override;
451
452
   private:
453
    /** the type enumerator */
454
    TypeEnumerator d_te;
455
    /** the current number of terms we are enumerating for the given size */
456
    unsigned d_currNumConsts;
457
    /** the next end threshold */
458
    unsigned d_nextIndexEnd;
459
  };
460
  /** a free variable enumerator
461
   *
462
   * This enumerator enumerates canonical free variables for a given type.
463
   * The n^th variable in this stream is assigned size n. This enumerator is
464
   * used in conjunction with sygus-repair-const to generate solutions with
465
   * constant holes. In this approach, free variables are arguments to
466
   * any-constant constructors. This is required so that terms with holes are
467
   * unique up to rewriting when appropriate.
468
   */
469
8
  class TermEnumMasterFv : public TermEnum
470
  {
471
   public:
472
    TermEnumMasterFv();
473
    /** initialize this enumerator */
474
    bool initialize(SygusEnumerator* se, TypeNode tn);
475
    /** get the current term of the enumerator */
476
    Node getCurrent() override;
477
    /** increment the enumerator */
478
    bool increment() override;
479
  };
480
  /** the master enumerator for each sygus type */
481
  std::map<TypeNode, TermEnumMaster> d_masterEnum;
482
  /** the master enumerator for each non-sygus type */
483
  std::map<TypeNode, TermEnumMasterFv> d_masterEnumFv;
484
  /** the master enumerator for each non-sygus type */
485
  std::map<TypeNode, std::unique_ptr<TermEnumMasterInterp>> d_masterEnumInt;
486
  /** the sygus enumerator this class is for */
487
  Node d_enum;
488
  /** the type of d_enum */
489
  TypeNode d_etype;
490
  /** pointer to the master enumerator of type d_etype */
491
  TermEnum* d_tlEnum;
492
  /** the abort size, caches the value of --sygus-abort-size */
493
  int d_abortSize;
494
  /** get master enumerator for type tn */
495
  TermEnum* getMasterEnumForType(TypeNode tn);
496
  //-------------------------------- externally specified symmetry breaking
497
  /** set of constructors we disallow at top level
498
   *
499
   * A constructor C is disallowed at the top level if a symmetry breaking
500
   * lemma that entails ~is-C( d_enum ) was registered to
501
   * TermDbSygus::registerSymBreakLemma.
502
   */
503
  std::unordered_set<Node, NodeHashFunction> d_sbExcTlCons;
504
  //-------------------------------- end externally specified symmetry breaking
505
};
506
507
}  // namespace quantifiers
508
}  // namespace theory
509
}  // namespace CVC4
510
511
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */