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

Line Exec Source
1
/*********************                                                        */
2
/*! \file synth_conjecture.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 Class that encapsulates techniques for a single (SyGuS) synthesis
13
 ** conjecture.
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
19
#define CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
20
21
#include <memory>
22
23
#include "theory/quantifiers/expr_miner_manager.h"
24
#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
25
#include "theory/quantifiers/sygus/cegis.h"
26
#include "theory/quantifiers/sygus/cegis_core_connective.h"
27
#include "theory/quantifiers/sygus/cegis_unif.h"
28
#include "theory/quantifiers/sygus/example_eval_cache.h"
29
#include "theory/quantifiers/sygus/example_infer.h"
30
#include "theory/quantifiers/sygus/sygus_process_conj.h"
31
#include "theory/quantifiers/sygus/sygus_repair_const.h"
32
#include "theory/quantifiers/sygus/sygus_stats.h"
33
#include "theory/quantifiers/sygus/template_infer.h"
34
35
namespace CVC4 {
36
namespace theory {
37
namespace quantifiers {
38
39
class CegGrammarConstructor;
40
class SygusPbe;
41
class SygusStatistics;
42
43
/**
44
 * A base class for generating values for actively-generated enumerators.
45
 * At a high level, the job of this class is to accept a stream of "abstract
46
 * values" a1, ..., an, ..., and generate a (possibly larger) stream of
47
 * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, ....
48
 */
49
195
class EnumValGenerator
50
{
51
 public:
52
195
  virtual ~EnumValGenerator() {}
53
  /** initialize this class with enumerator e */
54
  virtual void initialize(Node e) = 0;
55
  /** Inform this generator that abstract value v was enumerated. */
56
  virtual void addValue(Node v) = 0;
57
  /**
58
   * Increment this value generator. If this returns false, then we are out of
59
   * values. If this returns true, getCurrent(), if non-null, returns the
60
   * current term.
61
   *
62
   * Notice that increment() may return true and afterwards it may be the case
63
   * getCurrent() is null. We do this so that increment() does not take too
64
   * much time per call, which can be the case for grammars where it is
65
   * difficult to find the next (non-redundant) term. Returning true with
66
   * a null current term gives the caller the chance to interleave other
67
   * reasoning.
68
   */
69
  virtual bool increment() = 0;
70
  /** Get the current concrete value generated by this class. */
71
  virtual Node getCurrent() = 0;
72
};
73
74
/** a synthesis conjecture
75
 * This class implements approaches for a synthesis conjecture, given by data
76
 * member d_quant.
77
 * This includes both approaches for synthesis in Reynolds et al CAV 2015. It
78
 * determines which approach and optimizations are applicable to the
79
 * conjecture, and has interfaces for implementing them.
80
 */
81
class SynthConjecture
82
{
83
 public:
84
  SynthConjecture(QuantifiersEngine* qe,
85
                  QuantifiersState& qs,
86
                  QuantifiersInferenceManager& qim,
87
                  QuantifiersRegistry& qr,
88
                  SygusStatistics& s);
89
  ~SynthConjecture();
90
  /** presolve */
91
  void presolve();
92
  /** get original version of conjecture */
93
8539
  Node getConjecture() const { return d_quant; }
94
  /** get deep embedding version of conjecture */
95
  Node getEmbeddedConjecture() const { return d_embed_quant; }
96
  //-------------------------------for counterexample-guided check/refine
97
  /** whether the conjecture is waiting for a call to doCheck below */
98
  bool needsCheck();
99
  /** whether the conjecture is waiting for a call to doRefine below */
100
  bool needsRefinement() const;
101
  /** do syntax-guided enumerative check
102
   *
103
   * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
104
   *
105
   * The method returns true if this conjecture is finished trying solutions
106
   * for the given call to SynthEngine::check.
107
   *
108
   * Notice that we make multiple calls to doCheck on one call to
109
   * SynthEngine::check. For example, if we are using an actively-generated
110
   * enumerator, one enumerated (abstract) term may correspond to multiple
111
   * concrete terms t1, ..., tn to check, where we make up to n calls to doCheck
112
   * when each of t1, ..., tn fails to satisfy the current refinement lemmas.
113
   */
114
  bool doCheck(std::vector<Node>& lems);
115
  /** do refinement
116
   *
117
   * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
118
   *
119
   * This method is run when needsRefinement() returns true, indicating that
120
   * the last call to doCheck found a counterexample to the last candidate.
121
   *
122
   * This method adds a refinement lemma on the output channel of quantifiers
123
   * engine. If the refinement lemma is a duplicate, then we manually
124
   * exclude the current candidate via excludeCurrentSolution. This should
125
   * only occur when the synthesis conjecture for the current candidate fails
126
   * to evaluate to false for a given counterexample point, but regardless its
127
   * negation is satisfiable for the current candidate and that point. This is
128
   * exclusive to theories with partial functions, e.g. (non-linear) division.
129
   *
130
   * This method returns true if a lemma was added on the output channel, and
131
   * false otherwise.
132
   */
133
  bool doRefine();
134
  //-------------------------------end for counterexample-guided check/refine
135
  /**
136
   * Prints the synthesis solution to output stream out. This invokes solution
137
   * reconstruction if the conjecture is single invocation. Otherwise, it
138
   * returns the solution found by sygus enumeration.
139
   */
140
  void printSynthSolution(std::ostream& out);
141
  /** get synth solutions
142
   *
143
   * This method returns true if this class has a solution available to the
144
   * conjecture that it was assigned.
145
   *
146
   * Let q be the synthesis conjecture assigned to this class.
147
   * This method adds entries to sol_map[q] that map functions-to-synthesize to
148
   * their builtin solution, which has the same type. For example, for synthesis
149
   * conjecture exists f. forall x. f( x )>x, this function will update
150
   * sol_map[q] to contain the entry:
151
   *   f -> (lambda x. x+1)
152
   */
153
  bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
154
  /**
155
   * The feasible guard whose semantics are "this conjecture is feasiable".
156
   * This is "G" in Figure 3 of Reynolds et al CAV 2015.
157
   */
158
  Node getGuard() const;
159
  /** is ground */
160
  bool isGround() { return d_inner_vars.empty(); }
161
  /** are we using single invocation techniques */
162
  bool isSingleInvocation() const;
163
  /** preregister conjecture
164
   * This is used as a heuristic for solution reconstruction, so that we
165
   * remember expressions in the conjecture before preprocessing, since they
166
   * may be helpful during solution reconstruction (Figure 5 of Reynolds et al
167
   * CAV 2015)
168
   */
169
  void preregisterConjecture(Node q);
170
  /** assign conjecture q to this class */
171
  void assign(Node q);
172
  /** has a conjecture been assigned to this class */
173
760
  bool isAssigned() { return !d_embed_quant.isNull(); }
174
  /**
175
   * Get model value for term n.
176
   */
177
  Node getModelValue(Node n);
178
179
  /** get utility for static preprocessing and analysis of conjectures */
180
454
  SynthConjectureProcess* getProcess() { return d_ceg_proc.get(); }
181
  /** get constant repair utility */
182
239
  SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); }
183
  /** get example inference utility */
184
15312
  ExampleInfer* getExampleInfer() { return d_exampleInfer.get(); }
185
  /** get the example evaluation cache utility for enumerator e */
186
  ExampleEvalCache* getExampleEvalCache(Node e);
187
  /** get program by examples module */
188
  SygusPbe* getPbe() { return d_ceg_pbe.get(); }
189
  /** get the symmetry breaking predicate for type */
190
  Node getSymmetryBreakingPredicate(
191
      Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
192
  /** print out debug information about this conjecture */
193
  void debugPrint(const char* c);
194
  /** check side condition
195
   *
196
   * This returns false if the solution { d_candidates -> cvals } does not
197
   * satisfy the side condition of the conjecture maintained by this class,
198
   * if it exists, and true otherwise.
199
   */
200
  bool checkSideCondition(const std::vector<Node>& cvals) const;
201
202
 private:
203
  /** reference to quantifier engine */
204
  QuantifiersEngine* d_qe;
205
  /** Reference to the quantifiers state */
206
  QuantifiersState& d_qstate;
207
  /** Reference to the quantifiers inference manager */
208
  QuantifiersInferenceManager& d_qim;
209
  /** The quantifiers registry */
210
  QuantifiersRegistry& d_qreg;
211
  /** reference to the statistics of parent */
212
  SygusStatistics& d_stats;
213
  /** term database sygus of d_qe */
214
  TermDbSygus* d_tds;
215
  /** The feasible guard. */
216
  Node d_feasible_guard;
217
  /**
218
   * Do we have a solution in this solve context? This flag is reset to false
219
   * on every call to presolve.
220
   */
221
  bool d_hasSolution;
222
  /** the decision strategy for the feasible guard */
223
  std::unique_ptr<DecisionStrategy> d_feasible_strategy;
224
  /** single invocation utility */
225
  std::unique_ptr<CegSingleInv> d_ceg_si;
226
  /** template inference utility */
227
  std::unique_ptr<SygusTemplateInfer> d_templInfer;
228
  /** utility for static preprocessing and analysis of conjectures */
229
  std::unique_ptr<SynthConjectureProcess> d_ceg_proc;
230
  /** grammar utility */
231
  std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
232
  /** repair constant utility */
233
  std::unique_ptr<SygusRepairConst> d_sygus_rconst;
234
  /** example inference utility */
235
  std::unique_ptr<ExampleInfer> d_exampleInfer;
236
  /** example evaluation cache utility for each enumerator */
237
  std::map<Node, std::unique_ptr<ExampleEvalCache> > d_exampleEvalCache;
238
239
  //------------------------modules
240
  /** program by examples module */
241
  std::unique_ptr<SygusPbe> d_ceg_pbe;
242
  /** CEGIS module */
243
  std::unique_ptr<Cegis> d_ceg_cegis;
244
  /** CEGIS UNIF module */
245
  std::unique_ptr<CegisUnif> d_ceg_cegisUnif;
246
  /** connective core utility */
247
  std::unique_ptr<CegisCoreConnective> d_sygus_ccore;
248
  /** the set of active modules (subset of the above list) */
249
  std::vector<SygusModule*> d_modules;
250
  /** master module
251
   *
252
   * This is the module (one of those above) that takes sole responsibility
253
   * for this conjecture, determined during assign(...).
254
   */
255
  SygusModule* d_master;
256
  //------------------------end modules
257
258
  //------------------------enumerators
259
  /**
260
   * Get model values for terms n, store in vector v. This method returns true
261
   * if and only if all values added to v are non-null.
262
   *
263
   * The argument activeIncomplete indicates whether n contains an active
264
   * enumerator that is currently not finished enumerating values, but returned
265
   * null on a call to getEnumeratedValue. This value is used for determining
266
   * whether we should call getEnumeratedValues again within a call to
267
   * SynthConjecture::check.
268
   *
269
   * It removes terms from n that correspond to "inactive" enumerators, that
270
   * is, enumerators whose values have been exhausted.
271
   */
272
  bool getEnumeratedValues(std::vector<Node>& n,
273
                           std::vector<Node>& v,
274
                           bool& activeIncomplete);
275
  /**
276
   * Get model value for term n. If n has a value that was excluded by
277
   * datatypes sygus symmetry breaking, this method returns null. It sets
278
   * activeIncomplete to true if there is an actively-generated enumerator whose
279
   * current value is null but it has not finished generating values.
280
   */
281
  Node getEnumeratedValue(Node n, bool& activeIncomplete);
282
  /** enumerator generators for each actively-generated enumerator */
283
  std::map<Node, std::unique_ptr<EnumValGenerator> > d_evg;
284
  /**
285
   * Map from enumerators to whether they are currently being
286
   * "actively-generated". That is, we are in a state where we have called
287
   * d_evg[e].addValue(v) for some v, and d_evg[e].getNext() has not yet
288
   * returned null. The range of this map stores the abstract value that
289
   * we are currently generating values from.
290
   */
291
  std::map<Node, Node> d_ev_curr_active_gen;
292
  /** the current waiting value of each actively-generated enumerator, if any
293
   *
294
   * This caches values that are actively generated and that we have not yet
295
   * passed to a call to SygusModule::constructCandidates. An example of when
296
   * this may occur is when there are two actively-generated enumerators e1 and
297
   * e2. Say on some iteration we actively-generate v1 for e1, the value
298
   * of e2 was excluded by symmetry breaking, and say the current master sygus
299
   * module does not handle partial models. Hence, we abort the current check.
300
   * We remember that the value of e1 was v1 by storing it here, so that on
301
   * a future check when v2 has a proper value, it is returned.
302
   */
303
  std::map<Node, Node> d_ev_active_gen_waiting;
304
  /** the first value enumerated for each actively-generated enumerator
305
   *
306
   * This is to implement an optimization that only guards the blocking lemma
307
   * for the first value of an actively-generated enumerator.
308
   */
309
  std::map<Node, Node> d_ev_active_gen_first_val;
310
  //------------------------end enumerators
311
312
  /** list of constants for quantified formula
313
   * The outer Skolems for the negation of d_embed_quant.
314
   */
315
  std::vector<Node> d_candidates;
316
  /** base instantiation
317
   * If d_embed_quant is forall d. exists y. P( d, y ), then
318
   * this is the formula  exists y. P( d_candidates, y ). Notice that
319
   * (exists y. F) is shorthand above for ~( forall y. ~F ).
320
   */
321
  Node d_base_inst;
322
  /** list of variables on inner quantification */
323
  std::vector<Node> d_inner_vars;
324
  /**
325
   * The set of skolems for the current "verification" lemma, if one exists.
326
   * This may be added to during calls to doCheck(). The model values for these
327
   * skolems are analyzed during doRefine().
328
   */
329
  std::vector<Node> d_ce_sk_vars;
330
  /**
331
   * If we have already tested the satisfiability of the current verification
332
   * lemma, this stores the model values of d_ce_sk_vars in the current
333
   * (satisfiable, failed) verification lemma.
334
   */
335
  std::vector<Node> d_ce_sk_var_mvs;
336
  /**
337
   * Whether the above vector has been set. We have this flag since the above
338
   * vector may be set to empty (e.g. for ground synthesis conjectures).
339
   */
340
  bool d_set_ce_sk_vars;
341
342
  /** the asserted (negated) conjecture */
343
  Node d_quant;
344
  /**
345
   * The side condition for solving the conjecture, after conversion to deep
346
   * embedding.
347
   */
348
  Node d_embedSideCondition;
349
  /** (negated) conjecture after simplification */
350
  Node d_simp_quant;
351
  /** (negated) conjecture after simplification, conversion to deep embedding */
352
  Node d_embed_quant;
353
  /** candidate information */
354
2738
  class CandidateInfo
355
  {
356
   public:
357
2738
    CandidateInfo() {}
358
    /** list of terms we have instantiated candidates with */
359
    std::vector<Node> d_inst;
360
  };
361
  std::map<Node, CandidateInfo> d_cinfo;
362
  /**
363
   * The first index of an instantiation in CandidateInfo::d_inst that we have
364
   * not yet tried to repair.
365
   */
366
  unsigned d_repair_index;
367
  /** number of times we have called doRefine */
368
  unsigned d_refine_count;
369
  /** record solution (this is used to construct solutions later) */
370
  void recordSolution(std::vector<Node>& vs);
371
  /** get synth solutions internal
372
   *
373
   * This function constructs the body of solutions for all
374
   * functions-to-synthesize in this conjecture and stores them in sols, in
375
   * order. For each solution added to sols, we add an integer indicating what
376
   * kind of solution n is, where if sols[i] = n, then
377
   *   if status[i] = 0: n is the (builtin term) corresponding to the solution,
378
   *   if status[i] = 1: n is the sygus representation of the solution.
379
   * We store builtin versions under some conditions (such as when the sygus
380
   * grammar is being ignored).
381
   *
382
   * This consults the single invocation module to get synthesis solutions if
383
   * isSingleInvocation() returns true.
384
   *
385
   * For example, for conjecture exists fg. forall x. f(x)>g(x), this function
386
   * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is
387
   * the sygus datatype constructor corresponding to variable x.
388
   */
389
  bool getSynthSolutionsInternal(std::vector<Node>& sols,
390
                                 std::vector<int>& status);
391
  //-------------------------------- sygus stream
392
  /**
393
   * Prints the current synthesis solution to the output stream indicated by
394
   * the Options object, send a lemma blocking the current solution to the
395
   * output channel, which we refer to as a "stream exclusion lemma".
396
   *
397
   * The argument enums is the set of enumerators that comprise the current
398
   * solution, and values is their current values.
399
   */
400
  void printAndContinueStream(const std::vector<Node>& enums,
401
                              const std::vector<Node>& values);
402
  /** exclude the current solution { enums -> values } */
403
  void excludeCurrentSolution(const std::vector<Node>& enums,
404
                              const std::vector<Node>& values);
405
  /**
406
   * Whether we have guarded a stream exclusion lemma when using sygusStream.
407
   * This is an optimization that allows us to guard only the first stream
408
   * exclusion lemma.
409
   */
410
  bool d_guarded_stream_exc;
411
  //-------------------------------- end sygus stream
412
  /** expression miner managers for each function-to-synthesize
413
   *
414
   * Notice that for each function-to-synthesize, we enumerate a stream of
415
   * candidate solutions, where each of these streams is independent. Thus,
416
   * we maintain separate expression miner managers for each of them.
417
   *
418
   * This is used for the sygusRewSynth() option to synthesize new candidate
419
   * rewrite rules.
420
   */
421
  std::map<Node, ExpressionMinerManager> d_exprm;
422
};
423
424
}  // namespace quantifiers
425
}  // namespace theory
426
} /* namespace CVC4 */
427
428
#endif