1 /********************* */ 2 /*! \file sygus_unif_strat.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 sygus_unif_strat 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H 18 #define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H 19 20 #include <map> 21 #include "expr/node.h" 22 #include "theory/quantifiers_engine.h" 23 24 namespace CVC4 { 25 namespace theory { 26 namespace quantifiers { 27 28 /** roles for enumerators 29 * 30 * This indicates the role of an enumerator that is allocated by approaches 31 * for synthesis-by-unification (see details below). 32 * io : the enumerator should enumerate values that are overall solutions 33 * for the function-to-synthesize, 34 * ite_condition : the enumerator should enumerate values that are useful 35 * in ite conditions in the ITE strategy, 36 * concat_term : the enumerator should enumerate values that are used as 37 * components of string concatenation solutions. 38 */ 39 enum EnumRole 40 { 41 enum_invalid, 42 enum_io, 43 enum_ite_condition, 44 enum_concat_term, 45 }; 46 std::ostream& operator<<(std::ostream& os, EnumRole r); 47 48 /** roles for strategy nodes 49 * 50 * This indicates the role of a strategy node, which is a subprocedure of 51 * SygusUnif::constructSolution (see details below). 52 * equal : the node constructed must be equal to the overall solution for 53 * the function-to-synthesize, 54 * string_prefix/suffix : the node constructed must be a prefix/suffix 55 * of the function-to-synthesize, 56 * ite_condition : the node constructed must be a condition that makes some 57 * active input examples true and some input examples false. 58 */ 59 enum NodeRole 60 { 61 role_invalid, 62 role_equal, 63 role_string_prefix, 64 role_string_suffix, 65 role_ite_condition, 66 }; 67 std::ostream& operator<<(std::ostream& os, NodeRole r); 68 69 /** enumerator role for node role */ 70 EnumRole getEnumeratorRoleForNodeRole(NodeRole r); 71 72 /** strategy types 73 * 74 * This indicates a strategy for synthesis-by-unification (see details below). 75 * ITE : strategy for constructing if-then-else solutions via decision 76 * tree learning techniques, 77 * CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation 78 * solutions via a divide and conquer approach, 79 * ID : identity strategy used for calling strategies on child type through 80 * an identity function. 81 */ 82 enum StrategyType 83 { 84 strat_INVALID, 85 strat_ITE, 86 strat_CONCAT_PREFIX, 87 strat_CONCAT_SUFFIX, 88 strat_ID, 89 }; 90 std::ostream& operator<<(std::ostream& os, StrategyType st); 91 92 /** virtual base class for context in synthesis-by-unification approaches */ 93 class UnifContext 94 { 95 public: ~UnifContext()96 virtual ~UnifContext() {} 97 98 /** Get the current role 99 * 100 * In a particular context when constructing solutions in synthesis by 101 * unification, we may be solving based on a modified role. For example, 102 * if we are currently synthesizing x in a solution ("a" ++ x), we are 103 * synthesizing the string suffix of the overall solution. In this case, this 104 * function returns role_string_suffix. 105 */ 106 virtual NodeRole getCurrentRole() = 0; 107 /** is return value modified? 108 * 109 * This returns true if we are currently in a state where the return value 110 * of the solution has been modified, e.g. by a previous node that solved 111 * for a string prefix. 112 */ isReturnValueModified()113 bool isReturnValueModified() { return getCurrentRole() != role_equal; } 114 }; 115 116 /** 117 * This class stores information regarding an enumerator, including 118 * information regarding the role of this enumerator (see EnumRole), its 119 * parent, whether it is templated, its slave enumerators, and so on. 120 * 121 * We say an enumerator is a master enumerator if it is the variable that 122 * we use to enumerate values for its sort. Master enumerators may have 123 * (possibly multiple) slave enumerators, stored in d_enum_slave. When 124 * constructing a sygus unifciation strategy, we make the first enumerator for 125 * each type a master enumerator, and any additional ones slaves of it. 126 */ 127 class EnumInfo 128 { 129 public: EnumInfo()130 EnumInfo() : d_role(enum_io), d_is_conditional(false) {} 131 /** initialize this class 132 * 133 * role is the "role" the enumerator plays in the high-level strategy, 134 * which is one of enum_* above. 135 */ 136 void initialize(EnumRole role); 137 /** is this enumerator associated with a template? */ isTemplated()138 bool isTemplated() { return !d_template.isNull(); } 139 /** set conditional 140 * 141 * This flag is set to true if this enumerator may not apply to all 142 * input/output examples. For example, if this enumerator is used 143 * as an output value beneath a conditional in an instance of strat_ITE, 144 * then this enumerator is conditional. 145 */ setConditional()146 void setConditional() { d_is_conditional = true; } 147 /** returns if this enumerator is conditional */ isConditional()148 bool isConditional() { return d_is_conditional; } 149 /** get the role of this enumerator */ getRole()150 EnumRole getRole() { return d_role; } 151 /** enumerator template 152 * 153 * If d_template non-null, enumerated values V are immediately transformed to 154 * d_template { d_template_arg -> V }. 155 */ 156 Node d_template; 157 Node d_template_arg; 158 /** 159 * Slave enumerators of this enumerator. These are other enumerators that 160 * have the same type, but a different role in the strategy tree. We 161 * generally 162 * only use one enumerator per type, and hence these slaves are notified when 163 * values are enumerated for this enumerator. 164 */ 165 std::vector<Node> d_enum_slave; 166 167 private: 168 /** the role of this enumerator (one of enum_* above). */ 169 EnumRole d_role; 170 /** is this enumerator conditional */ 171 bool d_is_conditional; 172 }; 173 174 class EnumTypeInfoStrat; 175 176 /** represents a node in the strategy graph 177 * 178 * It contains a list of possible strategies which are tried during calls 179 * to constructSolution. 180 */ 181 class StrategyNode 182 { 183 public: StrategyNode()184 StrategyNode() {} 185 ~StrategyNode(); 186 /** the set of strategies to try at this node in the strategy graph */ 187 std::vector<EnumTypeInfoStrat*> d_strats; 188 }; 189 190 /** 191 * Stores all enumerators and strategies for a SyGuS datatype type. 192 */ 193 class EnumTypeInfo 194 { 195 public: EnumTypeInfo()196 EnumTypeInfo() {} 197 /** the type that this information is for */ 198 TypeNode d_this_type; 199 /** map from enum roles to enumerators for this type */ 200 std::map<EnumRole, Node> d_enum; 201 /** map from node roles to strategy nodes */ 202 std::map<NodeRole, StrategyNode> d_snodes; 203 /** get strategy node for node role */ 204 StrategyNode& getStrategyNode(NodeRole nrole); 205 }; 206 207 /** represents a strategy for a SyGuS datatype type 208 * 209 * This represents a possible strategy to apply when processing a strategy 210 * node in constructSolution. When applying the strategy represented by this 211 * class, we may make recursive calls to the children of the strategy, 212 * given in d_cenum. If all recursive calls to constructSolution for these 213 * children are successful, say: 214 * constructSolution( d_cenum[1], ... ) = t1, 215 * ..., 216 * constructSolution( d_cenum[n], ... ) = tn, 217 * Then, the solution returned by this strategy is 218 * d_sol_templ * { d_sol_templ_args -> (t1,...,tn) } 219 * where * is application of substitution. 220 */ 221 class EnumTypeInfoStrat 222 { 223 public: 224 /** the type of strategy this represents */ 225 StrategyType d_this; 226 /** the sygus datatype constructor that induced this strategy 227 * 228 * For example, this may be a sygus datatype whose sygus operator is ITE, 229 * if the strategy type above is strat_ITE. 230 */ 231 Node d_cons; 232 /** children of this strategy */ 233 std::vector<std::pair<Node, NodeRole> > d_cenum; 234 /** the arguments for the (templated) solution */ 235 std::vector<Node> d_sol_templ_args; 236 /** the template for the solution */ 237 Node d_sol_templ; 238 /** Returns true if argument is valid strategy in unification context x */ 239 bool isValid(UnifContext& x); 240 }; 241 242 /** 243 * flags for extra restrictions to be inferred during redundant operators 244 * learning 245 */ 246 struct StrategyRestrictions 247 { StrategyRestrictionsStrategyRestrictions248 StrategyRestrictions() : d_iteReturnBoolConst(false), d_iteCondOnlyAtoms(true) 249 { 250 } 251 /** 252 * if this flag is true then staticLearnRedundantOps will also try to make 253 * the return value of boolean ITEs to be restricted to constants 254 */ 255 bool d_iteReturnBoolConst; 256 /** 257 * if this flag is true then staticLearnRedundantOps will also try to make 258 * the condition values of ITEs to be restricted to atoms 259 */ 260 bool d_iteCondOnlyAtoms; 261 /** 262 * A list of unused strategies. This maps strategy points to the indices 263 * in StrategyNode::d_strats that are not used by the caller of 264 * staticLearnRedundantOps, and hence should not be taken into account 265 * when doing redundant operator learning. 266 */ 267 std::map<Node, std::unordered_set<unsigned>> d_unused_strategies; 268 }; 269 270 /** 271 * Stores strategy and enumeration information for a function-to-synthesize. 272 * 273 * When this class is initialized, we construct a "strategy tree" based on 274 * the grammar of the function to synthesize f. This tree is represented by 275 * the above classes. 276 */ 277 class SygusUnifStrategy 278 { 279 public: SygusUnifStrategy()280 SygusUnifStrategy() : d_qe(nullptr) {} 281 /** initialize 282 * 283 * This initializes this class with function-to-synthesize f. We also call 284 * f the candidate variable. 285 * 286 * This call constructs a set of enumerators for the relevant subfields of 287 * the grammar of f and adds them to enums. 288 */ 289 void initialize(QuantifiersEngine* qe, Node f, std::vector<Node>& enums); 290 /** Get the root enumerator for this class */ 291 Node getRootEnumerator() const; 292 /** 293 * Get the enumerator info for enumerator e, where e must be an enumerator 294 * initialized by this class (in enums after a call to initialize). 295 */ 296 EnumInfo& getEnumInfo(Node e); 297 /** 298 * Get the enumerator type info for sygus type t, where t must be the type 299 * of some enumerator initialized by this class 300 */ 301 EnumTypeInfo& getEnumTypeInfo(TypeNode tn); 302 303 /** static learn redundant operators 304 * 305 * This learns static lemmas for pruning enumerative space based on the 306 * strategy for the function-to-synthesize of this class, and stores these 307 * into strategy_lemmas. 308 * 309 * These may correspond to static symmetry breaking predicates (for example, 310 * those that exclude ITE from enumerators whose role is enum_io when the 311 * strategy is ITE_strat). 312 * 313 * then the module may also try to apply the given pruning restrictions (see 314 * StrategyRestrictions for more details) 315 */ 316 void staticLearnRedundantOps( 317 std::map<Node, std::vector<Node>>& strategy_lemmas, 318 StrategyRestrictions& restrictions); 319 /** 320 * creates the default restrictions when they are not given and calls the 321 * above function 322 */ 323 void staticLearnRedundantOps( 324 std::map<Node, std::vector<Node>>& strategy_lemmas); 325 326 /** debug print this strategy on Trace c */ 327 void debugPrint(const char* c); 328 329 private: 330 /** reference to quantifier engine */ 331 QuantifiersEngine* d_qe; 332 /** The candidate variable this strategy is for */ 333 Node d_candidate; 334 /** maps enumerators to relevant information */ 335 std::map<Node, EnumInfo> d_einfo; 336 /** list of all enumerators for the function-to-synthesize */ 337 std::vector<Node> d_esym_list; 338 /** Info for sygus datatype type occurring in a field of d_root */ 339 std::map<TypeNode, EnumTypeInfo> d_tinfo; 340 /** 341 * The root sygus datatype for the function-to-synthesize, 342 * which encodes the overall syntactic restrictions on the space 343 * of solutions. 344 */ 345 TypeNode d_root; 346 /** 347 * Maps sygus datatypes to their master enumerator. This is the (single) 348 * enumerator of that type that we enumerate values for. 349 */ 350 std::map<TypeNode, Node> d_master_enum; 351 /** Initialize necessary information for (sygus) type tn */ 352 void initializeType(TypeNode tn); 353 354 //-----------------------debug printing 355 /** print ind indentations on trace c */ 356 static void indent(const char* c, int ind); 357 //-----------------------end debug printing 358 359 //------------------------------ strategy registration 360 /** build strategy graph 361 * 362 * This builds the strategy for enumerated values of type tn for the given 363 * role of nrole, for solutions to function-to-synthesize of this class. 364 */ 365 void buildStrategyGraph(TypeNode tn, NodeRole nrole); 366 /** register enumerator 367 * 368 * This registers that et is an enumerator of type tn, having enumerator 369 * role enum_role. 370 * 371 * inSearch is whether we will enumerate values based on this enumerator. 372 * A strategy node is represented by a (enumerator, node role) pair. Hence, 373 * we may use enumerators for which this flag is false to represent strategy 374 * nodes that have child strategies. 375 */ 376 void registerStrategyPoint(Node et, 377 TypeNode tn, 378 EnumRole enum_role, 379 bool inSearch); 380 /** infer template */ 381 bool inferTemplate(unsigned k, 382 Node n, 383 std::map<Node, unsigned>& templ_var_index, 384 std::map<unsigned, unsigned>& templ_injection); 385 /** helper for static learn redundant operators 386 * 387 * (e, nrole) specify the strategy node in the graph we are currently 388 * analyzing, visited stores the nodes we have already visited. 389 * 390 * This method builds the mapping needs_cons, which maps (master) enumerators 391 * to a map from the constructors that it needs. 392 */ 393 void staticLearnRedundantOps( 394 Node e, 395 NodeRole nrole, 396 std::map<Node, std::map<NodeRole, bool>>& visited, 397 std::map<Node, std::map<unsigned, bool>>& needs_cons, 398 StrategyRestrictions& restrictions); 399 /** finish initialization of the strategy tree 400 * 401 * (e, nrole) specify the strategy node in the graph we are currently 402 * analyzing, visited stores the nodes we have already visited. 403 * 404 * isCond is whether the current enumerator is conditional (beneath a 405 * conditional of an strat_ITE strategy). 406 */ 407 void finishInit(Node e, 408 NodeRole nrole, 409 std::map<Node, std::map<NodeRole, bool> >& visited, 410 bool isCond); 411 /** helper for debug print 412 * 413 * Prints the node e with role nrole on Trace(c). 414 * 415 * (e, nrole) specify the strategy node in the graph we are currently 416 * analyzing, visited stores the nodes we have already visited. 417 * 418 * ind is the current level of indentation (for debugging) 419 */ 420 void debugPrint(const char* c, 421 Node e, 422 NodeRole nrole, 423 std::map<Node, std::map<NodeRole, bool> >& visited, 424 int ind); 425 //------------------------------ end strategy registration 426 }; 427 428 } /* CVC4::theory::quantifiers namespace */ 429 } /* CVC4::theory namespace */ 430 } /* CVC4 namespace */ 431 432 #endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ 433