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