GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_unif_rl.h Lines: 7 7 100.0 %
Date: 2021-03-22 Branches: 14 46 30.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_unif_rl.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 sygus_unif_rl
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
19
20
#include <map>
21
#include "options/main_options.h"
22
#include "theory/quantifiers/sygus/sygus_unif.h"
23
24
#include "theory/quantifiers/lazy_trie.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace quantifiers {
29
30
using BoolNodePair = std::pair<bool, Node>;
31
using BoolNodePairHashFunction =
32
    PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>;
33
using BoolNodePairMap =
34
    std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>;
35
using NodePairMap = std::unordered_map<Node, Node, NodeHashFunction>;
36
using NodePair = std::pair<Node, Node>;
37
38
class SynthConjecture;
39
40
/** Sygus unification Refinement Lemmas utility
41
 *
42
 * This class implement synthesis-by-unification, where the specification is a
43
 * set of refinement lemmas. With respect to SygusUnif, it's main interface
44
 * function is addExample, which adds a refinement lemma to the specification.
45
 */
46
class SygusUnifRl : public SygusUnif
47
{
48
 public:
49
  SygusUnifRl(SynthConjecture* p);
50
  ~SygusUnifRl();
51
52
  /** initialize */
53
  void initializeCandidate(
54
      QuantifiersEngine* qe,
55
      Node f,
56
      std::vector<Node>& enums,
57
      std::map<Node, std::vector<Node>>& strategy_lemmas) override;
58
59
  /** Notify enumeration (unused) */
60
  void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
61
  /** Construct solution */
62
  bool constructSolution(std::vector<Node>& sols,
63
                         std::vector<Node>& lemmas) override;
64
  /** add refinement lemma
65
   *
66
   * This adds a lemma to the specification. It returns the purified form
67
   * of the lemma based on the method purifyLemma below. The method adds the
68
   * head of "evaluation points" to the map eval_hds, where an evaluation point
69
   * is a term of the form:
70
   *   ev( e1, c1...cn )
71
   * where ev is an evaluation function for the sygus deep embedding, e1 is of
72
   * sygus datatype type (the "head" of the evaluation point), and c1...cn are
73
   * constants. If ev( e1, c1...cn ) is the purified form of ev( e, t1...tn ),
74
   * then e1 is added to eval_hds[e]. We add evaluation points to eval_hds only
75
   * for those terms that are newly generated by this call (and have not been
76
   * returned by a previous call to this method).
77
   */
78
  Node addRefLemma(Node lemma, std::map<Node, std::vector<Node>>& eval_hds);
79
  /**
80
   * whether f is being synthesized with unification strategies. This can be
81
   * checked through wehether f has conditional or point enumerators (we use the
82
   * former)
83
   */
84
  bool usingUnif(Node f) const;
85
  /** get condition for evaluation point
86
   *
87
   * Returns the strategy point corresponding to the condition of the strategy
88
   * point e.
89
   */
90
  Node getConditionForEvaluationPoint(Node e) const;
91
  /** set conditional enumerators
92
   *
93
   * This informs this class that the current set of conditions for evaluation
94
   * point e are enumerated by "enums" and have values "conds"; "guard" is
95
   * Boolean variable whose semantics correspond to "there is a solution using
96
   * at most enums.size() conditions."
97
   */
98
  void setConditions(Node e,
99
                     Node guard,
100
                     const std::vector<Node>& enums,
101
                     const std::vector<Node>& conds);
102
103
  /** retrieve the head of evaluation points for candidate c, if any */
104
  std::vector<Node> getEvalPointHeads(Node c);
105
106
  /**
107
   * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
108
   * FMCAD 2019). This is determined by option::sygusUnifPi().
109
   */
110
  bool usingConditionPool() const;
111
  /** Whether we are additionally using information gain.  */
112
  bool usingConditionPoolInfoGain() const;
113
114
 protected:
115
  /** reference to the parent conjecture */
116
  SynthConjecture* d_parent;
117
  /** Whether we are using condition pool enumeration */
118
  bool d_useCondPool;
119
  /** Whether we are additionally using information gain heuristics */
120
  bool d_useCondPoolIGain;
121
  /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */
122
  std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
123
  /** construct sol */
124
  Node constructSol(Node f,
125
                    Node e,
126
                    NodeRole nrole,
127
                    int ind,
128
                    std::vector<Node>& lemmas) override;
129
  /** collects data from refinement lemmas to drive solution construction
130
   *
131
   * In particular it rebuilds d_app_to_pt whenever d_prev_rlemmas is different
132
   * from d_rlemmas, in which case we may have added or removed data points
133
   */
134
  void initializeConstructSol() override;
135
  /** initialize construction solution for function-to-synthesize f */
136
  void initializeConstructSolFor(Node f) override;
137
  /** maps unif functions-to~synhesize to their last built solutions */
138
  std::map<Node, Node> d_cand_to_sol;
139
  /*
140
    --------------------------------------------------------------
141
        Purification
142
    --------------------------------------------------------------
143
  */
144
  /**
145
   * maps heads of applications of a unif function-to-synthesize to their tuple
146
   * of arguments (which constitute a "data point" aka an "evaluation point")
147
   */
148
  std::map<Node, std::vector<Node>> d_hd_to_pt;
149
  /** maps unif candidates to heads of their evaluation points */
150
  std::map<Node, std::vector<Node>> d_cand_to_eval_hds;
151
  /**
152
   * maps applications of unif functions-to-synthesize to the result of their
153
   * purification */
154
  std::map<Node, Node> d_app_to_purified;
155
  /** maps unif functions-to-synthesize to counters of heads of evaluation
156
   * points */
157
  std::map<Node, unsigned> d_cand_to_hd_count;
158
  /**
159
   * This is called on the refinement lemma and will rewrite applications of
160
   * functions-to-synthesize to their respective purified form, i.e. such that
161
   * all unification functions are applied over concrete values. Moreover
162
   * unification functions are also rewritten such that every different tuple of
163
   * arguments has a fresh function symbol applied to it.
164
   *
165
   * Non-unification functions are also equated to their model values when they
166
   * occur as arguments of unification functions.
167
   *
168
   * A vector of guards with the (negated) equalities between the original
169
   * arguments and their model values is populated accordingly.
170
   *
171
   * When the traversal encounters an application of a unification
172
   * function-to-synthesize it will proceed to ensure that the arguments of that
173
   * function application are constants (ensureConst becomes "true"). If an
174
   * applicatin of a non-unif function-to-synthesize is reached, the requirement
175
   * is lifted (ensureConst becomes "false"). This avoides introducing spurious
176
   * equalities in model_guards.
177
   *
178
   * For example if "f" is being synthesized with a unification strategy and "g"
179
   * is not then the application
180
   *   f(g(f(g(0))))=1
181
   * would be purified into
182
   *   g(0) = c1 ^ g(f1(c1)) = c3 => f2(c3)
183
   *
184
   * Similarly
185
   *   f(+(0,f(g(0))))
186
   * would be purified into
187
   *   g(0) = c1 ^ f1(c1) = c2 => f2(+(0,c2))
188
   *
189
   * This function also populates the maps between candidates, heads and
190
   * evaluation points
191
   */
192
  Node purifyLemma(Node n,
193
                   bool ensureConst,
194
                   std::vector<Node>& model_guards,
195
                   BoolNodePairMap& cache);
196
  /*
197
    --------------------------------------------------------------
198
        Strategy information
199
    --------------------------------------------------------------
200
  */
201
  /**
202
   * This class stores the necessary information for building a decision tree
203
   * for a particular node in the strategy tree of a candidate variable f.
204
   */
205
  class DecisionTreeInfo
206
  {
207
   public:
208
17
    DecisionTreeInfo()
209
17
        : d_unif(nullptr), d_strategy(nullptr), d_strategy_index(0)
210
    {
211
17
    }
212
17
    ~DecisionTreeInfo() {}
213
    /** initializes this class */
214
    void initialize(Node cond_enum,
215
                    SygusUnifRl* unif,
216
                    SygusUnifStrategy* strategy,
217
                    unsigned strategy_index);
218
    /** returns index of strategy information of strategy node for this DT */
219
    unsigned getStrategyIndex() const;
220
    /** builds solution, if possible, using the given constructor
221
     *
222
     * A solution is possible when all different valued heads can be separated,
223
     * i.e. the current set of conditions separates them in a decision tree
224
     */
225
    Node buildSol(Node cons, std::vector<Node>& lemmas);
226
    /** bulids a solution by considering all condition values ever enumerated */
227
    Node buildSolAllCond(Node cons, std::vector<Node>& lemmas);
228
    /** builds a solution by incrementally adding points and conditions to DT
229
     *
230
     * Differently from the above method, here a condition is only added to the
231
     * DT when it's necessary for resolving a separation conflict (i.e. heads
232
     * with different values in the same leaf of the DT). Only one value per
233
     * condition enumerated is considered.
234
     *
235
     * If a solution cannot be built, then there are more conflicts to be
236
     * resolved than condition enumerators. A conflict lemma is added to lemmas
237
     * that forces a new assigment in which the conflict is removed (heads are
238
     * made equal) or a new condition is enumerated to try to separate them.
239
     */
240
    Node buildSolMinCond(Node cons, std::vector<Node>& lemmas);
241
    /** reference to parent unif util */
242
    SygusUnifRl* d_unif;
243
    /** enumerator template (if no templates, nodes in pair are Node::null()) */
244
    NodePair d_template;
245
    /** enumerated condition values, this is set by setConditions(...). */
246
    std::vector<Node> d_conds;
247
    /** gathered evaluation point heads */
248
    std::vector<Node> d_hds;
249
    /** all enumerated model values for conditions */
250
    std::unordered_set<Node, NodeHashFunction> d_cond_mvs;
251
    /** get condition enumerator */
252
17
    Node getConditionEnumerator() const { return d_cond_enum; }
253
    /** set conditions */
254
    void setConditions(Node guard,
255
                       const std::vector<Node>& enums,
256
                       const std::vector<Node>& conds);
257
258
   private:
259
    /** true and false nodes */
260
    Node d_true;
261
    Node d_false;
262
    /** Accumulates solutions built when considering all enumerated condition
263
     * values (which may generate repeated solutions) */
264
    std::unordered_set<Node, NodeHashFunction> d_sols;
265
    /**
266
     * Conditional enumerator variables corresponding to the condition values in
267
     * d_conds. These are used for generating separation lemmas during
268
     * buildSol. This is set by setConditions(...).
269
     */
270
    std::vector<Node> d_enums;
271
    /**
272
     * The guard literal whose semantics is "we need at most d_enums.size()
273
     * conditions in our solution. This is set by setConditions(...).
274
     */
275
    Node d_guard;
276
    /**
277
     * reference to inferred strategy for the function-to-synthesize this DT is
278
     * associated with
279
     */
280
    SygusUnifStrategy* d_strategy;
281
    /** index of strategy information of strategy node this DT is based on
282
     *
283
     * this is the index of the strategy (d_strats[index]) in the strategy node
284
     * to which this decision tree corresponds, which can be accessed through
285
     * the above strategy reference
286
     */
287
    unsigned d_strategy_index;
288
    /**
289
     * The enumerator in the strategy tree that stores conditions of the
290
     * decision tree.
291
     */
292
    Node d_cond_enum;
293
    /** extracts solution from decision tree built
294
     *
295
     * Depending on the active options, the decision tree might be rebuilt
296
     * before a solution is extracted, for example to optimize size (smaller
297
     * DTs) or chance of having a general solution (information gain heuristics)
298
     */
299
    Node extractSol(Node cons, std::map<Node, Node>& hd_mv);
300
301
    /** rebuild decision tree using information gain heuristic
302
     *
303
     * In a scenario in which the decision tree potentially contains more
304
     * conditions than necessary, it is beneficial to rebuild it in a way that
305
     * "better" conditions occurr closer to the top.
306
     *
307
     * The information gain heuristic selects conditions that lead to a
308
     * greater reduction of the Shannon entropy in the set of points
309
     */
310
    void recomputeSolHeuristically(std::map<Node, Node>& hd_mv);
311
    /** recursively select (best) conditions to split heads
312
     *
313
     * At each call picks the best condition based on the information gain
314
     * heuristic and splits the set of heads accordingly, then recurses on
315
     * them.
316
     *
317
     * The base case is a set being fully classified (i.e. all heads have the
318
     * same value)
319
     *
320
     * hds is the set of evaluation point heads we must classify with the
321
     * values in conds. The classification is guided by how a condition value
322
     * splits the heads through its evaluation on the points associated with
323
     * the heads. The metric is based on the model values of the heads (hd_mv)
324
     * in the resulting splits.
325
     *
326
     * ind is the current level of indentation (for debugging)
327
     */
328
    void buildDtInfoGain(std::vector<Node>& hds,
329
                         std::vector<Node> conds,
330
                         std::map<Node, Node>& hd_mv,
331
                         int ind);
332
    /** computes the Shannon entropy of a set of heads
333
     *
334
     * The entropy depends on how many positive and negative heads are in the
335
     * set and in their distribution. The polarity of the evaluation heads is
336
     * queried from their model values in hd_mv.
337
     *
338
     * ind is the current level of indentation (for debugging)
339
     */
340
    double getEntropy(const std::vector<Node>& hds,
341
                      std::map<Node, Node>& hd_mv,
342
                      int ind);
343
    /** evaluates a condition on a set of points
344
     *
345
     * The result is two sets of points: those on which the condition holds
346
     * and those on which it does not
347
     */
348
    std::pair<std::vector<Node>, std::vector<Node>> evaluateCond(
349
        std::vector<Node>& pts, Node cond);
350
    /** Classifies evaluation points according to enumerated condition values
351
     *
352
     * Maintains the invariant that points evaluated in the same way in the
353
     * current condition values are kept in the same "separation class."
354
     */
355
2376652
    class PointSeparator : public LazyTrieEvaluator
356
    {
357
     public:
358
17
      PointSeparator() : d_dt(nullptr) {}
359
      /** initializes this class */
360
      void initialize(DecisionTreeInfo* dt);
361
      /**
362
       * evaluates the respective evaluation point of the head n on the index-th
363
       * condition
364
       */
365
      Node evaluate(Node n, unsigned index) override;
366
367
      /** the lazy trie for building the separation classes */
368
      LazyTrieMulti d_trie;
369
      /** extracts solution from decision tree built */
370
      Node extractSol(Node cons, std::map<Node, Node>& hd_mv);
371
      /** computes the result of applying cond on the respective point of hd
372
       *
373
       * If for example cond is (\lambda xy. x < y) and hd is an evaluation head
374
       * in point (hd 0 1) this function will result in true, since
375
       *   (\lambda xy. x < y) 0 1 evaluates to true
376
       */
377
      Node computeCond(Node cond, Node hd);
378
379
     private:
380
      /** reference to parent unif util */
381
      DecisionTreeInfo* d_dt;
382
      /** cache of conditions evaluations on heads
383
       *
384
       * If for example cond is (\lambda xy. x < y) and hd is an evaluation head
385
       * in point (hd 0 1), then after invoking computeCond(cond, hd) this map
386
       * will contain d_eval_cond_hd[<cond, hd>] = true, since
387
       *
388
       *   (\lambda xy. x < y) 0 1 evaluates to true
389
       */
390
      std::map<std::pair<Node, Node>, Node> d_eval_cond_hd;
391
    };
392
    /**
393
     * Utility for determining how evaluation points are separated by currently
394
     * enumerated condiotion values
395
     */
396
    PointSeparator d_pt_sep;
397
  };
398
  /** maps strategy points in the strategy tree to the above data */
399
  std::map<Node, DecisionTreeInfo> d_stratpt_to_dt;
400
  /** maps conditional enumerators to strategy points in which they occur */
401
  std::map<Node, std::vector<Node>> d_cenum_to_stratpt;
402
  /** maps unif candidates to their conditional enumerators */
403
  std::map<Node, std::vector<Node>> d_cand_cenums;
404
  /** all conditional enumerators */
405
  std::vector<Node> d_cond_enums;
406
  /** register strategy
407
   *
408
   * Initialize the above data for the relevant enumerators in the strategy tree
409
   * of candidate variable f. For each strategy point e which there is a
410
   * decision tree strategy, we add e to enums. For each strategy with index
411
   * i in an strategy point e, if we are not using the strategy, we add i to
412
   * unused_strats[e]. This map is later passed to
413
   * SygusUnifStrategy::staticLearnRedundantOps.
414
   */
415
  void registerStrategy(
416
      Node f,
417
      std::vector<Node>& enums,
418
      std::map<Node, std::unordered_set<unsigned>>& unused_strats);
419
  /** register strategy node
420
   *
421
   * Called while traversing the strategy tree of f. The arguments e and nrole
422
   * indicate the current node in the tree we are traversing, and visited
423
   * indicates the nodes we have already visited. The arguments enums and
424
   * unused_strats are modified as described above.
425
   */
426
  void registerStrategyNode(
427
      Node f,
428
      Node e,
429
      NodeRole nrole,
430
      std::map<Node, std::map<NodeRole, bool>>& visited,
431
      std::vector<Node>& enums,
432
      std::map<Node, std::unordered_set<unsigned>>& unused_strats);
433
  /** register conditional enumerator
434
   *
435
   * Registers that cond is a conditional enumerator for building a (recursive)
436
   * decision tree at strategy node e within the strategy tree of f.
437
   */
438
  void registerConditionalEnumerator(Node f,
439
                                     Node e,
440
                                     Node cond,
441
                                     unsigned strategy_index);
442
};
443
444
}  // namespace quantifiers
445
}  // namespace theory
446
}  // namespace CVC4
447
448
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */