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