GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_unif_io.h Lines: 13 13 100.0 %
Date: 2021-03-22 Branches: 6 10 60.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_unif_io.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Haniel Barbosa
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_unif_io
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
19
20
#include <map>
21
#include "theory/quantifiers/sygus/sygus_unif.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace quantifiers {
26
27
class SygusUnifIo;
28
29
/** Unification context
30
  *
31
  * This class maintains state information during calls to
32
  * SygusUnifIo::constructSolution, which implements unification-based
33
  * approaches for constructing solutions to synthesis conjectures.
34
  */
35
84
class UnifContextIo : public UnifContext
36
{
37
 public:
38
  UnifContextIo();
39
  /** get current role */
40
  NodeRole getCurrentRole() override;
41
42
  /**
43
   * This intiializes this context based on information in sui regarding the
44
   * kinds of examples it contains.
45
   */
46
  void initialize(SygusUnifIo* sui);
47
48
  //----------for ITE strategy
49
  /** the value of the context conditional
50
  *
51
  * This stores a list of Boolean constants that is the same length of the
52
  * number of input/output example pairs we are considering. For each i,
53
  * if d_vals[i] = true, i/o pair #i is active according to this context
54
  * if d_vals[i] = false, i/o pair #i is inactive according to this context
55
  */
56
  std::vector<Node> d_vals;
57
  /** update the examples
58
  *
59
  * if pol=true, this method updates d_vals to d_vals & vals
60
  * if pol=false, this method updates d_vals to d_vals & ( ~vals )
61
  */
62
  bool updateContext(SygusUnifIo* sui, std::vector<Node>& vals, bool pol);
63
  //----------end for ITE strategy
64
65
  //----------for CONCAT strategies
66
  /** the position in the strings
67
  *
68
  * For each i/o example pair, this stores the length of the current solution
69
  * for the input of the pair, where the solution for that input is a prefix
70
  * or
71
  * suffix of the output of the pair. For example, if our i/o pairs are:
72
  *   f( "abcd" ) = "abcdcd"
73
  *   f( "aa" ) = "aacd"
74
  * If the solution we have currently constructed is str.++( x1, "c", ... ),
75
  * then d_str_pos = ( 5, 3 ), where notice that
76
  *   str.++( "abc", "c" ) is a prefix of "abcdcd" and
77
  *   str.++( "aa", "c" ) is a prefix of "aacd".
78
  */
79
  std::vector<unsigned> d_str_pos;
80
  /** update the string examples
81
  *
82
  * This method updates d_str_pos to d_str_pos + pos, and updates the current
83
  * role to nrole.
84
  */
85
  bool updateStringPosition(SygusUnifIo* sui,
86
                            std::vector<size_t>& pos,
87
                            NodeRole nrole);
88
  /** get current strings
89
  *
90
  * This returns the prefix/suffix of the string constants stored in vals
91
  * of size d_str_pos, and stores the result in ex_vals. For example, if vals
92
  * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add
93
  * "d" and "de" to ex_vals.
94
  */
95
  void getCurrentStrings(SygusUnifIo* sui,
96
                         const std::vector<Node>& vals,
97
                         std::vector<Node>& ex_vals);
98
  /** get string increment
99
  *
100
  * If this method returns true, then inc and tot are updated such that
101
  *   for all active indices i,
102
  *      vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and
103
  *      inc[i] = str.len(vals[i])
104
  *   for all inactive indices i, inc[i] = 0
105
  * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total
106
  * number of characters incremented across all examples.
107
  */
108
  bool getStringIncrement(SygusUnifIo* sui,
109
                          bool isPrefix,
110
                          const std::vector<Node>& ex_vals,
111
                          const std::vector<Node>& vals,
112
                          std::vector<size_t>& inc,
113
                          size_t& tot);
114
  /** returns true if ex_vals[i] = vals[i] for all active indices i. */
115
  bool isStringSolved(SygusUnifIo* sui,
116
                      const std::vector<Node>& ex_vals,
117
                      const std::vector<Node>& vals);
118
  //----------end for CONCAT strategies
119
120
  /** visited role
121
  *
122
  * This is the current set of enumerator/node role pairs we are currently
123
  * visiting. This set is cleared when the context is updated.
124
  */
125
  std::map<Node, std::map<NodeRole, bool>> d_visit_role;
126
127
 private:
128
  /** true and false nodes */
129
  Node d_true;
130
  Node d_false;
131
  /** current role (see getCurrentRole). */
132
  NodeRole d_curr_role;
133
};
134
135
/** Subsumption trie
136
*
137
* This class manages a set of terms for a PBE sygus enumerator.
138
*
139
* In PBE sygus, we are interested in, for each term t, the set of I/O examples
140
* that it satisfies, which can be represented by a vector of Booleans.
141
* For example, given conjecture:
142
*   f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5
143
* If solutions for f are of the form (lambda x. [term]), then:
144
*   Term x satisfies 0001,
145
*   Term x+1 satisfies 1100,
146
*   Term 2 satisfies 0100.
147
* Above, term 2 is subsumed by term x+1, since the set of I/O examples that
148
* x+1 satisfies are a superset of those satisfied by 2.
149
*/
150
10929
class SubsumeTrie
151
{
152
 public:
153
10929
  SubsumeTrie() {}
154
  /**
155
  * Adds term t to the trie, removes all terms that are subsumed by t from the
156
  * trie and adds them to subsumed. The set of I/O examples that t satisfies
157
  * is given by (pol ? vals : !vals).
158
  */
159
  Node addTerm(Node t,
160
               const std::vector<Node>& vals,
161
               bool pol,
162
               std::vector<Node>& subsumed);
163
  /**
164
  * Adds term c to the trie, without calculating/updating based on
165
  * subsumption. This is useful for using this class to store conditionals
166
  * in ITE strategies, where any conditional whose set of vals is unique
167
  * (as opposed to not subsumed) is useful.
168
  */
169
  Node addCond(Node c, const std::vector<Node>& vals, bool pol);
170
  /**
171
    * Returns the set of terms that are subsumed by (pol ? vals : !vals).
172
    */
173
  void getSubsumed(const std::vector<Node>& vals,
174
                   bool pol,
175
                   std::vector<Node>& subsumed);
176
  /**
177
    * Returns the set of terms that subsume (pol ? vals : !vals). This
178
    * is for instance useful when determining whether there exists a term
179
    * that satisfies all active examples in the decision tree learning
180
    * algorithm.
181
    */
182
  void getSubsumedBy(const std::vector<Node>& vals,
183
                     bool pol,
184
                     std::vector<Node>& subsumed_by);
185
  /**
186
   * Get the leaves of the trie, which we store in the map v. We consider their
187
   * evaluation on points such that (pol ? vals : !vals) is true.
188
   *
189
   * v[-1] stores the children that always evaluate to !pol,
190
   * v[1] stores the children that always evaluate to pol,
191
   * v[0] stores the children that both evaluate to true and false for at least
192
   * one example.
193
   */
194
  void getLeaves(const std::vector<Node>& vals,
195
                 bool pol,
196
                 std::map<int, std::vector<Node>>& v);
197
  /** is this trie empty? */
198
5965
  bool isEmpty() { return d_term.isNull() && d_children.empty(); }
199
  /** clear this trie */
200
33
  void clear()
201
  {
202
33
    d_term = Node::null();
203
33
    d_children.clear();
204
33
  }
205
206
 private:
207
  /** the term at this node */
208
  Node d_term;
209
  /** the children nodes of this trie */
210
  std::map<Node, SubsumeTrie> d_children;
211
  /** helper function for above functions */
212
  Node addTermInternal(Node t,
213
                       const std::vector<Node>& vals,
214
                       bool pol,
215
                       std::vector<Node>& subsumed,
216
                       bool spol,
217
                       unsigned index,
218
                       int status,
219
                       bool checkExistsOnly,
220
                       bool checkSubsume);
221
  /** helper function for above functions
222
   *
223
   * This adds to v[-1], v[0], v[1] the children of the trie that occur
224
   * along paths that contain only false (v[-1]), a mix of true/false (v[0]),
225
   * and only true (v[1]) values for respectively for relevant points.
226
   *
227
   * vals/pol is used to determine the relevant points, which impacts which
228
   * paths of the trie to traverse on this call.
229
   * In particular, all points such that (pol ? vals[index] : !vals[index])
230
   * are relevant.
231
   *
232
   * Paths that contain an unknown value for any relevant point are not
233
   * traversed. In the larger picture, this ensures that terms are not used in a
234
   * way such that their unknown value is relevant to the overall behavior of
235
   * a synthesis solution.
236
   *
237
   * status holds the current value of v (0,1,-1) that we will be adding to.
238
   */
239
  void getLeavesInternal(const std::vector<Node>& vals,
240
                         bool pol,
241
                         std::map<int, std::vector<Node>>& v,
242
                         unsigned index,
243
                         int status);
244
};
245
246
class SynthConjecture;
247
248
/** Sygus unification I/O utility
249
 *
250
 * This class implement synthesis-by-unification, where the specification is
251
 * I/O examples.
252
 *
253
 * Since I/O specifications for multiple functions can be fully separated, we
254
 * assume that this class is used only for a single function to synthesize.
255
 *
256
 * In addition to the base class which maintains a strategy tree, this class
257
 * maintains:
258
 * (1) A set of input/output examples that are the specification for f.
259
 * (2) A set of terms that have been enumerated for enumerators (d_ecache). This
260
 * can be updated via calls to notifyEnumeration.
261
 */
262
class SygusUnifIo : public SygusUnif
263
{
264
  friend class UnifContextIo;
265
266
 public:
267
  SygusUnifIo(SynthConjecture* p);
268
  ~SygusUnifIo();
269
270
  /** initialize
271
   *
272
   * This initializes this class for solving PBE conjectures for
273
   * function-to-synthesize f.
274
   *
275
   * We only initialize for one function f, since I/O specifications across
276
   * multiple functions can be separated.
277
   */
278
  void initializeCandidate(
279
      QuantifiersEngine* qe,
280
      Node f,
281
      std::vector<Node>& enums,
282
      std::map<Node, std::vector<Node>>& strategy_lemmas) override;
283
  /** Notify enumeration */
284
  void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
285
286
  /** Construct solution */
287
  bool constructSolution(std::vector<Node>& sols,
288
                         std::vector<Node>& lemmas) override;
289
 protected:
290
  /** The synthesis conjecture */
291
  SynthConjecture* d_parent;
292
  /** the function-to-synthesize */
293
  Node d_candidate;
294
  /**
295
   * Whether we will try to construct solution on the next call to
296
   * constructSolution. This flag is set to true when we successfully
297
   * register a new value for an enumerator.
298
   */
299
  bool d_check_sol;
300
  /** The number of values we have enumerated for all enumerators. */
301
  unsigned d_cond_count;
302
  /** The solution for the function of this class, if one has been found */
303
  Node d_solution;
304
  /** the term size of the above solution */
305
  unsigned d_sol_term_size;
306
  /** partial solutions
307
   *
308
   * Maps indices for I/O points to a list of solutions for that point, for each
309
   * type. We may have more than one type for solutions, e.g. for grammar:
310
   *   A -> ite( A, B, C ) | ...
311
   * where terms of type B and C can both act as solutions.
312
   */
313
  std::map<size_t,
314
           std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>>
315
      d_psolutions;
316
  /**
317
   * This flag is set to true if the solution construction was
318
   * non-deterministic with respect to failure/success.
319
   *
320
   * The solution construction for the string concatenation strategy is
321
   * non-deterministic with respect to success/failure. That is, choosing
322
   * a particular string may lead to being unsolvable in the recursive calls,
323
   * whereas others may not. For example, if our pool of enumerated strings is:
324
   *   { "A", x, "B" }
325
   * and our I/O example is:
326
   *   f( "AC" ) = "ACB"
327
   * then choosing to consider a solution of the form ( "A" ++ _ ) leads
328
   * to a recursive call where we are solving for f' in:
329
   *   "A" ++ f'("AC") = "ACB"
330
   * which is unsolvable since we cannot generate a term starting with "C"
331
   * from the pool above. Whereas if we would have chosen ( x ++ _ ), this
332
   * leads to a recursive call where we are solving for f' in:
333
   *   "AC" ++ f'("AC") = "ACB"
334
   * which can be closed with "B", giving us (x ++ "B") as a solution.
335
   */
336
  bool d_sol_cons_nondet;
337
  /**
338
   * Whether we are using information gain heuristic during solution
339
   * construction.
340
   */
341
  bool d_solConsUsingInfoGain;
342
  /** true and false nodes */
343
  Node d_true;
344
  Node d_false;
345
  /** input of I/O examples */
346
  std::vector<std::vector<Node>> d_examples;
347
  /** output of I/O examples */
348
  std::vector<Node> d_examples_out;
349
350
  /**
351
  * This class stores information regarding an enumerator, including:
352
  * a database of values that have been enumerated for this enumerator.
353
  */
354
213
  class EnumCache
355
  {
356
   public:
357
213
    EnumCache() {}
358
    /**
359
    * Notify this class that the term v has been enumerated for this enumerator.
360
    * Its evaluation under the set of examples in sui are stored in results.
361
    */
362
    void addEnumValue(Node v, std::vector<Node>& results);
363
    /**
364
    * Notify this class that slv is the complete solution to the synthesis
365
    * conjecture. This occurs rarely, for instance, when during an ITE strategy
366
    * we find that a single enumerated term covers all examples.
367
    */
368
33
    void setSolved(Node slv) { d_enum_solved = slv; }
369
    /** Have we been notified that a complete solution exists? */
370
1881
    bool isSolved() { return !d_enum_solved.isNull(); }
371
    /** Get the complete solution to the synthesis conjecture. */
372
70
    Node getSolved() { return d_enum_solved; }
373
    /** Values that have been enumerated for this enumerator */
374
    std::vector<Node> d_enum_vals;
375
    /**
376
      * This either stores the values of f( I ) for inputs
377
      * or the value of f( I ) = O if d_role==enum_io
378
      */
379
    std::vector<std::vector<Node>> d_enum_vals_res;
380
    /**
381
    * The set of values in d_enum_vals that have been "subsumed" by others
382
    * (see SubsumeTrie for explanation of subsumed).
383
    */
384
    std::vector<Node> d_enum_subsume;
385
    /** Map from values to their index in d_enum_vals. */
386
    std::map<Node, unsigned> d_enum_val_to_index;
387
    /**
388
    * A subsumption trie containing the values in d_enum_vals. Depending on the
389
    * role of this enumerator, values may either be added to d_term_trie with
390
    * subsumption (if role=enum_io), or without (if role=enum_ite_condition or
391
    * enum_concat_term).
392
    */
393
    SubsumeTrie d_term_trie;
394
395
   private:
396
    /**
397
      * Whether an enumerated value for this conjecture has solved the entire
398
      * conjecture.
399
      */
400
    Node d_enum_solved;
401
  };
402
  /** maps enumerators to the information above */
403
  std::map<Node, EnumCache> d_ecache;
404
  /** Construct solution node
405
   *
406
   * This is called for the (single) function-to-synthesize during a call to
407
   * constructSolution. If this returns a non-null node, then that term is a
408
   * solution for the function-to-synthesize in the overall conjecture.
409
   */
410
  Node constructSolutionNode(std::vector<Node>& lemmas);
411
  /** domain-specific enumerator exclusion techniques
412
   *
413
   * Returns true if the value v for e can be excluded based on a
414
   * domain-specific exclusion technique like the ones below.
415
   *
416
   * results : the values of v under the input examples,
417
   * exp : if this function returns true, then exp contains a (possibly
418
   * generalize) explanation for why v can be excluded.
419
   */
420
  bool getExplanationForEnumeratorExclude(
421
      Node e,
422
      Node v,
423
      std::vector<Node>& results,
424
      std::vector<Node>& exp);
425
  /** returns true if we can exlude values of e based on negative str.contains
426
   *
427
   * Values v for e may be excluded if we realize that the value of v under the
428
   * substitution for some input example will never be contained in some output
429
   * example. For details on this technique, see NegContainsSygusInvarianceTest
430
   * in sygus_invariance.h.
431
   *
432
   * This function depends on whether e is being used to enumerate values
433
   * for any node that is conditional in the strategy graph. For example,
434
   * nodes that are children of ITE strategy nodes are conditional. If any node
435
   * is conditional, then this function returns false.
436
   */
437
  bool useStrContainsEnumeratorExclude(Node e);
438
  /** cache for the above function */
439
  std::map<Node, bool> d_use_str_contains_eexc;
440
  /**
441
   * cache for the above function, stores whether enumerators e are in
442
   * a conditional context, e.g. used for enumerating the return values for
443
   * leaves of ITE trees.
444
   */
445
  std::map<Node, bool> d_use_str_contains_eexc_conditional;
446
447
  /** the unification context used within constructSolution */
448
  UnifContextIo d_context;
449
  /** initialize construct solution */
450
  void initializeConstructSol() override;
451
  /** initialize construct solution for */
452
  void initializeConstructSolFor(Node f) override;
453
  /** construct solution */
454
  Node constructSol(Node f,
455
                    Node e,
456
                    NodeRole nrole,
457
                    int ind,
458
                    std::vector<Node>& lemmas) override;
459
  /** construct best conditional
460
   *
461
   * This returns the condition in conds that maximizes information gain with
462
   * respect to the current active points in d_context. For example, see
463
   * Alur et al. TACAS 2017 for an example of information gain.
464
   */
465
  Node constructBestConditional(Node ce,
466
                                const std::vector<Node>& conds) override;
467
};
468
469
} /* CVC4::theory::quantifiers namespace */
470
} /* CVC4::theory namespace */
471
} /* CVC4 namespace */
472
473
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */