GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/cegis_unif.h Lines: 5 5 100.0 %
Date: 2021-03-23 Branches: 13 26 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cegis_unif.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Andres Noetzli
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 cegis with unification techinques
13
 **/
14
#include "cvc4_private.h"
15
16
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
17
#define CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
18
19
#include <map>
20
#include <vector>
21
22
#include "theory/decision_strategy.h"
23
#include "theory/quantifiers/sygus/cegis.h"
24
#include "theory/quantifiers/sygus/sygus_unif_rl.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace quantifiers {
29
30
/** Cegis Unif Enumerators Decision Strategy
31
 *
32
 * This class enforces a decision strategy that limits the number of
33
 * unique values given to the set of heads of evaluation points and conditions
34
 * enumerators for these points, which are variables of sygus datatype type that
35
 * are introduced by CegisUnif.
36
 *
37
 * It maintains a set of guards, call them G_uq_1 ... G_uq_n, where the
38
 * semantics of G_uq_i is "for each type, the heads of evaluation points of that
39
 * type are interpreted as a value in a set whose cardinality is at most i".
40
 * We also enforce that the number of condition enumerators for evaluation
41
 * points is equal to (n-1).
42
 *
43
 * To enforce this, we introduce sygus enumerator(s) of the same type as the
44
 * heads of evaluation points and condition enumerators registered to this class
45
 * and add lemmas that enforce that these terms are equal to at least one
46
 * enumerator (see registerEvalPtAtSize).
47
 */
48
2188
class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
49
{
50
 public:
51
  CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
52
                                QuantifiersState& qs,
53
                                QuantifiersInferenceManager& qim,
54
                                SynthConjecture* parent);
55
  /** Make the n^th literal of this strategy (G_uq_n).
56
   *
57
   * This call may add new lemmas of the form described above
58
   * registerEvalPtAtValue on the output channel of d_qe.
59
   */
60
  Node mkLiteral(unsigned n) override;
61
  /** identify */
62
226905
  std::string identify() const override
63
  {
64
226905
    return std::string("cegis_unif_num_enums");
65
  }
66
67
  /** initialize candidates
68
   *
69
   * Notify this class that it will be managing enumerators for the vector
70
   * of strategy points es. This function should only be called once.
71
   *
72
   * Each strategy point in es should be such that we are using a
73
   * synthesis-by-unification approach for its candidate.
74
   */
75
  void initialize(const std::vector<Node>& es,
76
                  const std::map<Node, Node>& e_to_cond,
77
                  const std::map<Node, std::vector<Node>>& strategy_lemmas);
78
79
  /*
80
   * Do not hide the zero-argument version of initialize() inherited from the
81
   * base class
82
   */
83
  using DecisionStrategy::initialize;
84
85
  /** get the current set of enumerators for strategy point e
86
   *
87
   * Index 0 adds the set of return value enumerators to es, index 1 adds the
88
   * set of condition enumerators to es.
89
   */
90
  void getEnumeratorsForStrategyPt(Node e,
91
                                   std::vector<Node>& es,
92
                                   unsigned index) const;
93
  /** register evaluation point for candidate
94
   *
95
   * This notifies this class that eis is a set of heads of evaluation points
96
   * for strategy point e, where e was passed to initialize in the vector es.
97
   *
98
   * This may add new lemmas of the form described above
99
   * registerEvalPtAtSize on the output channel of d_qe.
100
   */
101
  void registerEvalPts(const std::vector<Node>& eis, Node e);
102
103
 private:
104
  /** reference to quantifier engine */
105
  QuantifiersEngine* d_qe;
106
  /** Reference to the quantifiers inference manager */
107
  QuantifiersInferenceManager& d_qim;
108
  /** sygus term database of d_qe */
109
  TermDbSygus* d_tds;
110
  /** reference to the parent conjecture */
111
  SynthConjecture* d_parent;
112
  /**
113
   * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
114
   * FMCAD 2019). This is determined by option::sygusUnifPi().
115
   */
116
  bool d_useCondPool;
117
  /** whether this module has been initialized */
118
  bool d_initialized;
119
  /** null node */
120
  Node d_null;
121
  /** information per initialized type */
122
17
  class StrategyPtInfo
123
  {
124
   public:
125
17
    StrategyPtInfo() {}
126
    /** strategy point for this type */
127
    Node d_pt;
128
    /** the set of enumerators we have allocated for this strategy point
129
     *
130
     * Index 0 stores the return value enumerators, and index 1 stores the
131
     * conditional enumerators. We have that
132
     *   d_enums[0].size()==d_enums[1].size()+1.
133
     */
134
    std::vector<Node> d_enums[2];
135
    /** the type of conditional enumerators for this strategy point  */
136
    TypeNode d_ce_type;
137
    /**
138
     * The set of evaluation points of this type. In models, we ensure that
139
     * each of these are equal to one of d_enums[0].
140
     */
141
    std::vector<Node> d_eval_points;
142
    /** symmetry breaking lemma template for this strategy point
143
     *
144
     * Each pair stores (the symmetry breaking lemma template, argument (to be
145
     * instantiated) of symmetry breaking lemma template).
146
     *
147
     * Index 0 stores the symmetry breaking lemma template for return values,
148
     * index 1 stores the template for conditions.
149
     */
150
    std::pair<Node, Node> d_sbt_lemma_tmpl[2];
151
  };
152
  /** map strategy points to the above info */
153
  std::map<Node, StrategyPtInfo> d_ce_info;
154
  /** the "virtual" enumerator
155
   *
156
   * This enumerator is used for enforcing fairness. In particular, we relate
157
   * its size to the number of conditions allocated by this class such that:
158
   *    ~G_uq_i => size(d_virtual_enum) >= floor( log2( i-1 ) )
159
   * In other words, if we are using (i-1) conditions in our solution,
160
   * the size of the virtual enumerator is at least the floor of the log (base
161
   * two) of (i-1). Due to the default fairness scheme in the quantifier-free
162
   * datatypes solver (if --sygus-fair-max is enabled), this ensures that other
163
   * enumerators are allowed to have at least this size. This affect other
164
   * fairness schemes in an analogous fashion. In particular, we enumerate
165
   * based on the tuples for (term size, #conditions):
166
   *   (0,0), (0,1)                                             [size 0]
167
   *   (0,2), (0,3), (1,1), (1,2), (1,3)                        [size 1]
168
   *   (0,4), ..., (0,7), (1,4), ..., (1,7), (2,0), ..., (2,7)  [size 2]
169
   *   (0,8), ..., (0,15), (1,8), ..., (1,15), ...              [size 3]
170
   */
171
  Node d_virtual_enum;
172
  /** Registers an enumerator and adds symmetry breaking lemmas
173
   *
174
   * The symmetry breaking lemmas are generated according to the stored
175
   * information from the enumerator's respective strategy point and whether it
176
   * is a condition or return value enumerator. For the latter we add symmetry
177
   * breaking lemmas that force enumerators to consider values in an increasing
178
   * order of size.
179
   */
180
  void setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index);
181
  /** register evaluation point at size
182
   *
183
   * This sends a lemma of the form:
184
   *   G_uq_n => ei = d1 V ... V ei = dn
185
   * on the output channel of d_qe, where d1...dn are sygus enumerators of the
186
   * same type as e and ei, and ei is an evaluation point of strategy point e.
187
   */
188
  void registerEvalPtAtSize(Node e, Node ei, Node guq_lit, unsigned n);
189
};
190
191
/** Synthesizes functions in a data-driven SyGuS approach
192
 *
193
 * Data is derived from refinement lemmas generated through the regular CEGIS
194
 * approach. SyGuS is used to generate terms for classifying the data
195
 * (e.g. using decision tree learning) and thus generate a candidates for
196
 * functions-to-synthesize.
197
 *
198
 * This approach is inspired by the divide and conquer synthesis through
199
 * unification approach by Alur et al. TACAS 2017, by ICE-based invariant
200
 * synthesis from Garg et al. CAV 2014 and POPL 2016, and Padhi et al. PLDI 2016
201
 *
202
 * This module mantains a set of functions-to-synthesize and a set of term
203
 * enumerators. When new terms are enumerated it tries to learn new candidate
204
 * solutions, which are verified outside this module. If verification fails a
205
 * refinement lemma is generated, which this module sends to the utility that
206
 * learns candidates.
207
 */
208
class CegisUnif : public Cegis
209
{
210
 public:
211
  CegisUnif(QuantifiersEngine* qe,
212
            QuantifiersState& qs,
213
            QuantifiersInferenceManager& qim,
214
            SynthConjecture* p);
215
  ~CegisUnif() override;
216
  /** Retrieves enumerators for constructing solutions
217
   *
218
   * Non-unification candidates have themselves as enumerators, while for
219
   * unification candidates we add their conditonal enumerators to enums if
220
   * their respective guards are set in the current model
221
   */
222
  void getTermList(const std::vector<Node>& candidates,
223
                   std::vector<Node>& enums) override;
224
225
  /** Communicates refinement lemma to unification utility and external modules
226
   *
227
   * For the lemma to be sent to the external modules it adds a guard from the
228
   * parent conjecture which establishes that if the conjecture has a solution
229
   * then it must satisfy this refinement lemma
230
   *
231
   * For the lemma to be sent to the unification utility it purifies the
232
   * arguments of the function-to-synthensize such that all of its applications
233
   * are over concrete values. E.g.:
234
   *   f(f(f(0))) > 1
235
   * becomes
236
   *   f(0) != c1 v f(c1) != c2 v f(c2) > 1
237
   * in which c1 and c2 are concrete integer values
238
   *
239
   * Note that the lemma is in the deep embedding, which means that the above
240
   * example would actually correspond to
241
   *   eval(d, 0) != c1 v eval(d, c1) != c2 v eval(d, c2) > 1
242
   * in which d is the deep embedding of the function-to-synthesize f
243
   */
244
  void registerRefinementLemma(const std::vector<Node>& vars,
245
                               Node lem,
246
                               std::vector<Node>& lems) override;
247
248
 private:
249
  /** do cegis-implementation-specific initialization for this class */
250
  bool processInitialize(Node conj,
251
                         Node n,
252
                         const std::vector<Node>& candidates,
253
                         std::vector<Node>& lemmas) override;
254
  /** Tries to build new candidate solutions with new enumerated expressions
255
   *
256
   * This function relies on a data-driven unification-based approach for
257
   * constructing solutions for the functions-to-synthesize. See SygusUnifRl for
258
   * more details.
259
   *
260
   * Calls to this function are such that terms is the list of active
261
   * enumerators (returned by getTermList), and term_values are their current
262
   * model values. This function registers { terms -> terms_values } in
263
   * the database of values that have been enumerated, which are in turn used
264
   * for constructing candidate solutions when possible.
265
   *
266
   * This function also excludes models where (terms = terms_values) by adding
267
   * blocking clauses to lems. For example, for grammar:
268
   *   A -> A+A | x | 1 | 0
269
   * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
270
   *   ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
271
   * to lems, where G is active guard of the enumerator d (see
272
   * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
273
   * indicates that d should not be given the model value +( x, 1 ) anymore,
274
   * since { d -> +( x, 1 ) } has now been added to the database of this class.
275
   */
276
  bool processConstructCandidates(const std::vector<Node>& enums,
277
                                  const std::vector<Node>& enum_values,
278
                                  const std::vector<Node>& candidates,
279
                                  std::vector<Node>& candidate_values,
280
                                  bool satisfiedRl,
281
                                  std::vector<Node>& lems) override;
282
  /** communicate condition values to solution building utility
283
   *
284
   * for each unification candidate and for each strategy point associated with
285
   * it, set in d_sygus_unif the condition values (unif_cvalues) for respective
286
   * condition enumerators (unif_cenums)
287
   */
288
  void setConditions(const std::map<Node, std::vector<Node>>& unif_cenums,
289
                     const std::map<Node, std::vector<Node>>& unif_cvalues,
290
                     std::vector<Node>& lems);
291
  /** set values of condition enumerators based on current enumerator assignment
292
   *
293
   * enums and enum_values are the enumerators registered in getTermList and
294
   * their values retrieved by the parent SynthConjecture module, respectively.
295
   *
296
   * unif_cenums and unif_cvalues associate the conditional enumerators of each
297
   * strategy point of each unification candidate with their respective model
298
   * values
299
   *
300
   * This function also generates inter-enumerator symmetry breaking for return
301
   * values, such that their model values are ordered by size
302
   *
303
   * returns true if no symmetry breaking lemmas were generated for the return
304
   * value enumerators, false otherwise
305
   */
306
  bool getEnumValues(const std::vector<Node>& enums,
307
                     const std::vector<Node>& enum_values,
308
                     std::map<Node, std::vector<Node>>& unif_cenums,
309
                     std::map<Node, std::vector<Node>>& unif_cvalues,
310
                     std::vector<Node>& lems);
311
312
  /**
313
   * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
314
   * FMCAD 2019). This is determined by option::sygusUnifPi().
315
   */
316
  bool usingConditionPool() const;
317
  /**
318
   * Sygus unif utility. This class implements the core algorithm (e.g. decision
319
   * tree learning) that this module relies upon.
320
   */
321
  SygusUnifRl d_sygus_unif;
322
  /** enumerator manager utility */
323
  CegisUnifEnumDecisionStrategy d_u_enum_manager;
324
  /* The null node */
325
  Node d_null;
326
  /** the unification candidates */
327
  std::vector<Node> d_unif_candidates;
328
  /** the non-unification candidates */
329
  std::vector<Node> d_non_unif_candidates;
330
  /** list of strategy points per candidate */
331
  std::map<Node, std::vector<Node>> d_cand_to_strat_pt;
332
  /** map from conditional enumerators to their strategy point */
333
  std::map<Node, Node> d_cenum_to_strat_pt;
334
}; /* class CegisUnif */
335
336
}  // namespace quantifiers
337
}  // namespace theory
338
}  // namespace CVC4
339
340
#endif