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