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

Line Exec Source
1
/*********************                                                        */
2
/*! \file cegis.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, 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 cegis
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_H
18
#define CVC4__THEORY__QUANTIFIERS__CEGIS_H
19
20
#include <map>
21
#include "theory/quantifiers/sygus/sygus_module.h"
22
#include "theory/quantifiers/sygus_sampler.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
/** Cegis
29
 *
30
 * The default sygus module for synthesis, counterexample-guided inductive
31
 * synthesis (CEGIS).
32
 *
33
 * It initializes a list of sygus enumerators that are one-to-one with
34
 * candidates, and returns a list of candidates that are the model values
35
 * of these enumerators on calls to constructCandidates.
36
 *
37
 * It implements an optimization (getRefinementEvalLemmas) that evaluates all
38
 * previous refinement lemmas for a term before returning it as a candidate
39
 * in calls to constructCandidates.
40
 */
41
class Cegis : public SygusModule
42
{
43
 public:
44
  Cegis(QuantifiersEngine* qe,
45
        QuantifiersInferenceManager& qim,
46
        SynthConjecture* p);
47
8752
  ~Cegis() override {}
48
  /** initialize */
49
  virtual bool initialize(Node conj,
50
                          Node n,
51
                          const std::vector<Node>& candidates,
52
                          std::vector<Node>& lemmas) override;
53
  /** get term list */
54
  virtual void getTermList(const std::vector<Node>& candidates,
55
                           std::vector<Node>& enums) override;
56
  /** construct candidate */
57
  virtual bool constructCandidates(const std::vector<Node>& enums,
58
                                   const std::vector<Node>& enum_values,
59
                                   const std::vector<Node>& candidates,
60
                                   std::vector<Node>& candidate_values,
61
                                   std::vector<Node>& lems) override;
62
  /** register refinement lemma
63
   *
64
   * This function stores lem as a refinement lemma, and adds it to lems.
65
   */
66
  virtual void registerRefinementLemma(const std::vector<Node>& vars,
67
                                       Node lem,
68
                                       std::vector<Node>& lems) override;
69
  /** using repair const */
70
  virtual bool usingRepairConst() override;
71
72
 protected:
73
  /** the evaluation unfold utility of d_tds */
74
  SygusEvalUnfold* d_eval_unfold;
75
  /** If SynthConjecture::d_base_inst is exists y. P( d, y ), then this is y. */
76
  std::vector<Node> d_base_vars;
77
  /**
78
   * If SynthConjecture::d_base_inst is exists y. P( d, y ), then this is the
79
   * formula P( SynthConjecture::d_candidates, y ).
80
   */
81
  Node d_base_body;
82
  //----------------------------------cegis-implementation-specific
83
  /**
84
   * Do cegis-implementation-specific initialization for this class. The return
85
   * value and behavior of this function is the same as initialize(...) above.
86
   */
87
  virtual bool processInitialize(Node conj,
88
                                 Node n,
89
                                 const std::vector<Node>& candidates,
90
                                 std::vector<Node>& lemmas);
91
  /** do cegis-implementation-specific post-processing for construct candidate
92
   *
93
   * satisfiedRl is whether all refinement lemmas are satisfied under the
94
   * substitution { enums -> enum_values }.
95
   *
96
   * The return value and behavior of this function is the same as
97
   * constructCandidates(...) above.
98
   */
99
  virtual bool processConstructCandidates(const std::vector<Node>& enums,
100
                                          const std::vector<Node>& enum_values,
101
                                          const std::vector<Node>& candidates,
102
                                          std::vector<Node>& candidate_values,
103
                                          bool satisfiedRl,
104
                                          std::vector<Node>& lems);
105
  //----------------------------------end cegis-implementation-specific
106
107
  //-----------------------------------refinement lemmas
108
  /** refinement lemmas */
109
  std::vector<Node> d_refinement_lemmas;
110
  /** (processed) conjunctions of refinement lemmas that are not unit */
111
  std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_conj;
112
  /** (processed) conjunctions of refinement lemmas that are unit */
113
  std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_unit;
114
  /** substitution entailed by d_refinement_lemma_unit */
115
  std::vector<Node> d_rl_eval_hds;
116
  std::vector<Node> d_rl_vals;
117
  /** all variables appearing in refinement lemmas */
118
  std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_vars;
119
120
  /** adds lem as a refinement lemma */
121
  void addRefinementLemma(Node lem);
122
  /** add refinement lemma conjunct
123
   *
124
   * This is a helper function for addRefinementLemma.
125
   *
126
   * This adds waiting[wcounter] to the proper vector (d_refinement_lemma_conj
127
   * or d_refinement_lemma_unit). In the case that waiting[wcounter] corresponds
128
   * to a value propagation, e.g. it is of the form:
129
   *   (eval x c1...cn) = c
130
   * then it is added to d_refinement_lemma_unit, (eval x c1...cn) -> c is added
131
   * as a substitution in d_rl_eval_hds/d_rl_eval_vals, and applied to previous
132
   * lemmas in d_refinement_lemma_conj and lemmas waiting[k] for k>wcounter.
133
   * Each lemma in d_refinement_lemma_conj that is modifed in this process is
134
   * moved to the vector waiting.
135
   */
136
  void addRefinementLemmaConjunct(unsigned wcounter,
137
                                  std::vector<Node>& waiting);
138
  /** sample add refinement lemma
139
   *
140
   * This function will check if there is a sample point in d_sampler that
141
   * refutes the candidate solution (d_quant_vars->vals). If so, it adds a
142
   * refinement lemma to the lists d_refinement_lemmas that corresponds to that
143
   * sample point, and adds a lemma to lems if cegisSample mode is not trust.
144
   */
145
  bool sampleAddRefinementLemma(const std::vector<Node>& candidates,
146
                                const std::vector<Node>& vals,
147
                                std::vector<Node>& lems);
148
149
  /** evaluates candidate values on current refinement lemmas
150
   *
151
   * This method performs techniques that ensure that
152
   * { candidates -> candidate_values } is a candidate solution that should
153
   * be checked by the solution verifier of the CEGIS loop. This method
154
   * invokes two sub-methods which may reject the current solution.
155
   * The first is "refinement evaluation", described above the method
156
   * getRefinementEvalLemmas below. The second is "evaluation unfolding",
157
   * which eagerly unfolds applications of evaluation functions (see
158
   * sygus_eval_unfold.h for details).
159
   *
160
   * If this method returns true, then { candidates -> candidate_values }
161
   * is not ready to be tried as a candidate solution. In this case, it may add
162
   * lemmas to lems.
163
   *
164
   * Notice that this method may return true without adding any lemmas to
165
   * lems, in the case that terms from candidates are "actively-generated
166
   * enumerators", since the model values of such terms are managed
167
   * explicitly within getEnumeratedValue. In this case, the owner of the
168
   * actively-generated enumerators (e.g. SynthConjecture) is responsible for
169
   * blocking the current value of candidates.
170
   */
171
  bool addEvalLemmas(const std::vector<Node>& candidates,
172
                     const std::vector<Node>& candidate_values,
173
                     std::vector<Node>& lems);
174
  /** Get the node corresponding to the conjunction of all refinement lemmas. */
175
  Node getRefinementLemmaFormula();
176
  //-----------------------------------end refinement lemmas
177
178
  /** Get refinement evaluation lemmas
179
   *
180
   * This method performs "refinement evaluation", that is, it tests
181
   * whether the current solution, given by { vs -> ms },
182
   * satisfies all current refinement lemmas. If it does not, it may add
183
   * blocking lemmas L to lems which exclude (a generalization of) the current
184
   * solution.
185
   *
186
   * Given a candidate solution ms for candidates vs, this function adds lemmas
187
   * to lems based on evaluating the conjecture, instantiated for ms, on lemmas
188
   * for previous refinements (d_refinement_lemmas).
189
   *
190
   * Returns true if any such lemma exists.
191
   */
192
  bool getRefinementEvalLemmas(const std::vector<Node>& vs,
193
                               const std::vector<Node>& ms,
194
                               std::vector<Node>& lems);
195
  /** Check refinement evaluation lemmas
196
   *
197
   * This method is similar to above, but does not perform any generalization
198
   * techniques. It is used when we are using only fast enumerators for
199
   * all functions-to-synthesize.
200
   *
201
   * Returns true if a refinement lemma is false for the solution
202
   * { vs -> ms }.
203
   */
204
  bool checkRefinementEvalLemmas(const std::vector<Node>& vs,
205
                                 const std::vector<Node>& ms);
206
  /** sampler object for the option cegisSample()
207
   *
208
   * This samples points of the type of the inner variables of the synthesis
209
   * conjecture (d_base_vars).
210
   */
211
  SygusSampler d_cegis_sampler;
212
  /** cegis sample refine points
213
   *
214
   * Stores the list of indices of sample points in d_cegis_sampler we have
215
   * added as refinement lemmas.
216
   */
217
  std::unordered_set<unsigned> d_cegis_sample_refine;
218
219
  //---------------------------------for symbolic constructors
220
  /** are we using symbolic constants?
221
   *
222
   * This flag is set ot true if at least one of the enumerators allocated
223
   * by this class has been configured to allow model values with symbolic
224
   * constructors, such as the "any constant" constructor.
225
   */
226
  bool d_usingSymCons;
227
  //---------------------------------end for symbolic constructors
228
};
229
230
} /* CVC4::theory::quantifiers namespace */
231
} /* CVC4::theory namespace */
232
} /* CVC4 namespace */
233
234
#endif /* CVC4__THEORY__QUANTIFIERS__CEGIS_H */