1 /********************* */ 2 /*! \file sygus_unif.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Haniel Barbosa 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 sygus_unif 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H 18 #define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H 19 20 #include <map> 21 #include "expr/node.h" 22 #include "theory/quantifiers/sygus/sygus_unif_strat.h" 23 #include "theory/quantifiers_engine.h" 24 25 namespace CVC4 { 26 namespace theory { 27 namespace quantifiers { 28 29 /** Sygus unification utility 30 * 31 * This utility implements synthesis-by-unification style approaches for a 32 * set of functions-to-synthesize. These approaches include a combination of: 33 * (1) Decision tree learning, inspired by Alur et al TACAS 2017, 34 * (2) Divide-and-conquer via string concatenation. 35 * 36 * This class maintains, for each function-to-synthesize f: 37 * (1) A "strategy tree" based on the syntactic restrictions for f that is 38 * constructed during initialize (d_strategy), 39 * 40 * Based on the above, solutions can be constructed via calls to 41 * constructSolution. 42 */ 43 class SygusUnif 44 { 45 public: 46 SygusUnif(); 47 virtual ~SygusUnif(); 48 49 /** initialize candidate 50 * 51 * This initializes this class with functions-to-synthesize f. We also call 52 * this a "candidate variable". This function can be called more than once 53 * for different functions-to-synthesize in the same conjecture. 54 * 55 * This call constructs a set of enumerators for the relevant subfields of 56 * the grammar of f and adds them to enums. These enumerators are those that 57 * should be later given to calls to notifyEnumeration below. 58 * 59 * This also may result in lemmas being added to strategy_lemmas, 60 * which correspond to static symmetry breaking predicates (for example, 61 * those that exclude ITE from enumerators whose role is enum_io when the 62 * strategy is ITE_strat). The lemmas are associated with a strategy point of 63 * the respective function-to-synthesize. 64 */ 65 virtual void initializeCandidate( 66 QuantifiersEngine* qe, 67 Node f, 68 std::vector<Node>& enums, 69 std::map<Node, std::vector<Node>>& strategy_lemmas); 70 71 /** 72 * Notify that the value v has been enumerated for enumerator e. This call 73 * will add lemmas L to lemmas such that L entails e^M != v for all future 74 * models M. 75 */ 76 virtual void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) = 0; 77 /** construct solution 78 * 79 * This attempts to construct a solution for each function-to-synthesize 80 * based on the current set of enumerated values. Returns null if it cannot 81 * for some function (for example, if the set of enumerated values is 82 * insufficient, or if a non-deterministic strategy aborts). 83 * 84 * This call may add lemmas to lemmas that should be sent out on an output 85 * channel by the caller. 86 */ 87 virtual bool constructSolution(std::vector<Node>& sols, 88 std::vector<Node>& lemmas) = 0; 89 90 protected: 91 /** reference to quantifier engine */ 92 QuantifiersEngine* d_qe; 93 /** sygus term database of d_qe */ 94 quantifiers::TermDbSygus* d_tds; 95 96 //-----------------------debug printing 97 /** print ind indentations on trace c */ 98 static void indent(const char* c, int ind); 99 /** print (pol ? vals : !vals) as a bit-string on trace c */ 100 static void print_val(const char* c, 101 std::vector<Node>& vals, 102 bool pol = true); 103 //-----------------------end debug printing 104 /** the candidates for this class */ 105 std::vector<Node> d_candidates; 106 /** maps a function-to-synthesize to the above information */ 107 std::map<Node, SygusUnifStrategy> d_strategy; 108 109 /** domain-specific enumerator exclusion techniques 110 * 111 * Returns true if the value v for e can be excluded based on a 112 * domain-specific exclusion technique like the ones below. 113 * 114 * results : the values of v under the input examples, 115 * exp : if this function returns true, then exp contains a (possibly 116 * generalize) explanation for why v can be excluded. 117 */ 118 bool getExplanationForEnumeratorExclude(Node e, 119 Node v, 120 std::vector<Node>& results, 121 std::vector<Node>& exp); 122 /** returns true if we can exlude values of e based on negative str.contains 123 * 124 * Values v for e may be excluded if we realize that the value of v under the 125 * substitution for some input example will never be contained in some output 126 * example. For details on this technique, see NegContainsSygusInvarianceTest 127 * in sygus_invariance.h. 128 * 129 * This function depends on whether e is being used to enumerate values 130 * for any node that is conditional in the strategy graph. For example, 131 * nodes that are children of ITE strategy nodes are conditional. If any node 132 * is conditional, then this function returns false. 133 */ 134 bool useStrContainsEnumeratorExclude(Node e); 135 /** cache for the above function */ 136 std::map<Node, bool> d_use_str_contains_eexc; 137 138 //------------------------------ constructing solutions 139 /** implementation-dependent initialize construct solution 140 * 141 * Called once before each attempt to construct solutions. 142 */ 143 virtual void initializeConstructSol() = 0; 144 /** implementation-dependent initialize construct solution 145 * 146 * Called once before each attempt to construct solution for a 147 * function-to-synthesize f. 148 */ 149 virtual void initializeConstructSolFor(Node f) = 0; 150 /** implementation-dependent function for construct solution. 151 * 152 * Construct a solution based on enumerator e for function-to-synthesize of 153 * this class with node role nrole in context x. 154 * 155 * ind is the term depth of the context (for debugging). 156 */ 157 virtual Node constructSol( 158 Node f, Node e, NodeRole nrole, int ind, std::vector<Node>& lemmas) = 0; 159 /** 160 * Heuristically choose the best solved term for enumerator e, 161 * currently return the first by default. A solved term is one that 162 * suffices to form part of the solution for the given context. For example, 163 * x is a solved term in the context "ite(x>0, _, 0)" for PBE problem 164 * with I/O pairs { 1 -> 1, 4 -> 4, -1 -> 0 }. 165 */ 166 virtual Node constructBestSolvedTerm(Node e, const std::vector<Node>& solved); 167 /** 168 * Heuristically choose the best conditional term from conds for condition 169 * enumerator ce, random by default. 170 */ 171 virtual Node constructBestConditional(Node ce, 172 const std::vector<Node>& conds); 173 /** Heuristically choose the best string to concatenate from strs to the 174 * solution in context x, currently random 175 * incr stores the vector of indices that are incremented by this solution in 176 * example outputs. 177 * total_inc[x] is the sum of incr[x] for each x in strs. 178 */ 179 virtual Node constructBestStringToConcat( 180 const std::vector<Node>& strs, 181 const std::map<Node, unsigned>& total_inc, 182 const std::map<Node, std::vector<unsigned> >& incr); 183 //------------------------------ end constructing solutions 184 /** map terms to their sygus size */ 185 std::map<Node, unsigned> d_termToSize; 186 /** 187 * Whether to ensure terms selected by the above methods lead to minimal 188 * solutions. 189 */ 190 bool d_enableMinimality; 191 /** returns the term whose sygus size is minimal among those in terms */ 192 Node getMinimalTerm(const std::vector<Node>& terms); 193 }; 194 195 } /* CVC4::theory::quantifiers namespace */ 196 } /* CVC4::theory namespace */ 197 } /* CVC4 namespace */ 198 199 #endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ 200