1 /*********************                                                        */
2 /*! \file cegis_unif.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Andrew Reynolds, Haniel Barbosa, Andres Noetzli
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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 with unification techinques
13  **/
14 #include "cvc4_private.h"
15 
16 #ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
17 #define __CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
18 
19 #include <map>
20 #include <vector>
21 
22 #include "theory/quantifiers/sygus/cegis.h"
23 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
24 
25 namespace CVC4 {
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(QuantifiersEngine* qe, SynthConjecture* parent);
51   /** Make the n^th literal of this strategy (G_uq_n).
52    *
53    * This call may add new lemmas of the form described above
54    * registerEvalPtAtValue on the output channel of d_qe.
55    */
56   Node mkLiteral(unsigned n) override;
57   /** identify */
identify()58   std::string identify() const override
59   {
60     return std::string("cegis_unif_num_enums");
61   }
62 
63   /** initialize candidates
64    *
65    * Notify this class that it will be managing enumerators for the vector
66    * of strategy points es. This function should only be called once.
67    *
68    * Each strategy point in es should be such that we are using a
69    * synthesis-by-unification approach for its candidate.
70    */
71   void initialize(const std::vector<Node>& es,
72                   const std::map<Node, Node>& e_to_cond,
73                   const std::map<Node, std::vector<Node>>& strategy_lemmas);
74 
75   /*
76    * Do not hide the zero-argument version of initialize() inherited from the
77    * base class
78    */
79   using DecisionStrategy::initialize;
80 
81   /** get the current set of enumerators for strategy point e
82    *
83    * Index 0 adds the set of return value enumerators to es, index 1 adds the
84    * set of condition enumerators to es.
85    */
86   void getEnumeratorsForStrategyPt(Node e,
87                                    std::vector<Node>& es,
88                                    unsigned index) const;
89   /** register evaluation point for candidate
90    *
91    * This notifies this class that eis is a set of heads of evaluation points
92    * for strategy point e, where e was passed to initialize in the vector es.
93    *
94    * This may add new lemmas of the form described above
95    * registerEvalPtAtSize on the output channel of d_qe.
96    */
97   void registerEvalPts(const std::vector<Node>& eis, Node e);
98 
99  private:
100   /** reference to quantifier engine */
101   QuantifiersEngine* d_qe;
102   /** sygus term database of d_qe */
103   TermDbSygus* d_tds;
104   /** reference to the parent conjecture */
105   SynthConjecture* d_parent;
106   /** whether this module has been initialized */
107   bool d_initialized;
108   /** null node */
109   Node d_null;
110   /** information per initialized type */
111   class StrategyPtInfo
112   {
113    public:
StrategyPtInfo()114     StrategyPtInfo() {}
115     /** strategy point for this type */
116     Node d_pt;
117     /** the set of enumerators we have allocated for this strategy point
118      *
119      * Index 0 stores the return value enumerators, and index 1 stores the
120      * conditional enumerators. We have that
121      *   d_enums[0].size()==d_enums[1].size()+1.
122      */
123     std::vector<Node> d_enums[2];
124     /** the type of conditional enumerators for this strategy point  */
125     TypeNode d_ce_type;
126     /**
127      * The set of evaluation points of this type. In models, we ensure that
128      * each of these are equal to one of d_enums[0].
129      */
130     std::vector<Node> d_eval_points;
131     /** symmetry breaking lemma template for this strategy point
132      *
133      * Each pair stores (the symmetry breaking lemma template, argument (to be
134      * instantiated) of symmetry breaking lemma template).
135      *
136      * Index 0 stores the symmetry breaking lemma template for return values,
137      * index 1 stores the template for conditions.
138      */
139     std::pair<Node, Node> d_sbt_lemma_tmpl[2];
140   };
141   /** map strategy points to the above info */
142   std::map<Node, StrategyPtInfo> d_ce_info;
143   /** the "virtual" enumerator
144    *
145    * This enumerator is used for enforcing fairness. In particular, we relate
146    * its size to the number of conditions allocated by this class such that:
147    *    ~G_uq_i => size(d_virtual_enum) >= floor( log2( i-1 ) )
148    * In other words, if we are using (i-1) conditions in our solution,
149    * the size of the virtual enumerator is at least the floor of the log (base
150    * two) of (i-1). Due to the default fairness scheme in the quantifier-free
151    * datatypes solver (if --sygus-fair-max is enabled), this ensures that other
152    * enumerators are allowed to have at least this size. This affect other
153    * fairness schemes in an analogous fashion. In particular, we enumerate
154    * based on the tuples for (term size, #conditions):
155    *   (0,0), (0,1)                                             [size 0]
156    *   (0,2), (0,3), (1,1), (1,2), (1,3)                        [size 1]
157    *   (0,4), ..., (0,7), (1,4), ..., (1,7), (2,0), ..., (2,7)  [size 2]
158    *   (0,8), ..., (0,15), (1,8), ..., (1,15), ...              [size 3]
159    */
160   Node d_virtual_enum;
161   /** Registers an enumerator and adds symmetry breaking lemmas
162    *
163    * The symmetry breaking lemmas are generated according to the stored
164    * information from the enumerator's respective strategy point and whether it
165    * is a condition or return value enumerator. For the latter we add symmetry
166    * breaking lemmas that force enumerators to consider values in an increasing
167    * order of size.
168    */
169   void setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index);
170   /** register evaluation point at size
171    *
172    * This sends a lemma of the form:
173    *   G_uq_n => ei = d1 V ... V ei = dn
174    * on the output channel of d_qe, where d1...dn are sygus enumerators of the
175    * same type as e and ei, and ei is an evaluation point of strategy point e.
176    */
177   void registerEvalPtAtSize(Node e, Node ei, Node guq_lit, unsigned n);
178 };
179 
180 /** Synthesizes functions in a data-driven SyGuS approach
181  *
182  * Data is derived from refinement lemmas generated through the regular CEGIS
183  * approach. SyGuS is used to generate terms for classifying the data
184  * (e.g. using decision tree learning) and thus generate a candidates for
185  * functions-to-synthesize.
186  *
187  * This approach is inspired by the divide and conquer synthesis through
188  * unification approach by Alur et al. TACAS 2017, by ICE-based invariant
189  * synthesis from Garg et al. CAV 2014 and POPL 2016, and Padhi et al. PLDI 2016
190  *
191  * This module mantains a set of functions-to-synthesize and a set of term
192  * enumerators. When new terms are enumerated it tries to learn new candidate
193  * solutions, which are verified outside this module. If verification fails a
194  * refinement lemma is generated, which this module sends to the utility that
195  * learns candidates.
196  */
197 class CegisUnif : public Cegis
198 {
199  public:
200   CegisUnif(QuantifiersEngine* qe, SynthConjecture* p);
201   ~CegisUnif() override;
202   /** Retrieves enumerators for constructing solutions
203    *
204    * Non-unification candidates have themselves as enumerators, while for
205    * unification candidates we add their conditonal enumerators to enums if
206    * their respective guards are set in the current model
207    */
208   void getTermList(const std::vector<Node>& candidates,
209                    std::vector<Node>& enums) override;
210 
211   /** Communicates refinement lemma to unification utility and external modules
212    *
213    * For the lemma to be sent to the external modules it adds a guard from the
214    * parent conjecture which establishes that if the conjecture has a solution
215    * then it must satisfy this refinement lemma
216    *
217    * For the lemma to be sent to the unification utility it purifies the
218    * arguments of the function-to-synthensize such that all of its applications
219    * are over concrete values. E.g.:
220    *   f(f(f(0))) > 1
221    * becomes
222    *   f(0) != c1 v f(c1) != c2 v f(c2) > 1
223    * in which c1 and c2 are concrete integer values
224    *
225    * Note that the lemma is in the deep embedding, which means that the above
226    * example would actually correspond to
227    *   eval(d, 0) != c1 v eval(d, c1) != c2 v eval(d, c2) > 1
228    * in which d is the deep embedding of the function-to-synthesize f
229    */
230   void registerRefinementLemma(const std::vector<Node>& vars,
231                                Node lem,
232                                std::vector<Node>& lems) override;
233 
234  private:
235   /** do cegis-implementation-specific initialization for this class */
236   bool processInitialize(Node n,
237                          const std::vector<Node>& candidates,
238                          std::vector<Node>& lemmas) override;
239   /** Tries to build new candidate solutions with new enumerated expressions
240    *
241    * This function relies on a data-driven unification-based approach for
242    * constructing solutions for the functions-to-synthesize. See SygusUnifRl for
243    * more details.
244    *
245    * Calls to this function are such that terms is the list of active
246    * enumerators (returned by getTermList), and term_values are their current
247    * model values. This function registers { terms -> terms_values } in
248    * the database of values that have been enumerated, which are in turn used
249    * for constructing candidate solutions when possible.
250    *
251    * This function also excludes models where (terms = terms_values) by adding
252    * blocking clauses to lems. For example, for grammar:
253    *   A -> A+A | x | 1 | 0
254    * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
255    *   ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
256    * to lems, where G is active guard of the enumerator d (see
257    * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
258    * indicates that d should not be given the model value +( x, 1 ) anymore,
259    * since { d -> +( x, 1 ) } has now been added to the database of this class.
260    */
261   bool processConstructCandidates(const std::vector<Node>& enums,
262                                   const std::vector<Node>& enum_values,
263                                   const std::vector<Node>& candidates,
264                                   std::vector<Node>& candidate_values,
265                                   bool satisfiedRl,
266                                   std::vector<Node>& lems) override;
267   /** communicate condition values to solution building utility
268    *
269    * for each unification candidate and for each strategy point associated with
270    * it, set in d_sygus_unif the condition values (unif_cvalues) for respective
271    * condition enumerators (unif_cenums)
272    */
273   void setConditions(const std::map<Node, std::vector<Node>>& unif_cenums,
274                      const std::map<Node, std::vector<Node>>& unif_cvalues,
275                      std::vector<Node>& lems);
276   /** set values of condition enumerators based on current enumerator assignment
277    *
278    * enums and enum_values are the enumerators registered in getTermList and
279    * their values retrieved by the parent SynthConjecture module, respectively.
280    *
281    * unif_cenums and unif_cvalues associate the conditional enumerators of each
282    * strategy point of each unification candidate with their respective model
283    * values
284    *
285    * This function also generates inter-enumerator symmetry breaking for return
286    * values, such that their model values are ordered by size
287    *
288    * returns true if no symmetry breaking lemmas were generated for the return
289    * value enumerators, false otherwise
290    */
291   bool getEnumValues(const std::vector<Node>& enums,
292                      const std::vector<Node>& enum_values,
293                      std::map<Node, std::vector<Node>>& unif_cenums,
294                      std::map<Node, std::vector<Node>>& unif_cvalues,
295                      std::vector<Node>& lems);
296   /**
297    * Sygus unif utility. This class implements the core algorithm (e.g. decision
298    * tree learning) that this module relies upon.
299    */
300   SygusUnifRl d_sygus_unif;
301   /** enumerator manager utility */
302   CegisUnifEnumDecisionStrategy d_u_enum_manager;
303   /* The null node */
304   Node d_null;
305   /** the unification candidates */
306   std::vector<Node> d_unif_candidates;
307   /** the non-unification candidates */
308   std::vector<Node> d_non_unif_candidates;
309   /** list of strategy points per candidate */
310   std::map<Node, std::vector<Node>> d_cand_to_strat_pt;
311   /** map from conditional enumerators to their strategy point */
312   std::map<Node, Node> d_cenum_to_strat_pt;
313 }; /* class CegisUnif */
314 
315 }  // namespace quantifiers
316 }  // namespace theory
317 }  // namespace CVC4
318 
319 #endif
320