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