1 /********************* */ 2 /*! \file sygus_enumerator.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds 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_enumerator 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H 18 #define __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H 19 20 #include <map> 21 #include <unordered_set> 22 #include "expr/node.h" 23 #include "expr/type_node.h" 24 #include "theory/quantifiers/sygus/synth_conjecture.h" 25 #include "theory/quantifiers/sygus/term_database_sygus.h" 26 27 namespace CVC4 { 28 namespace theory { 29 namespace quantifiers { 30 31 class SynthConjecture; 32 class SygusPbe; 33 34 /** SygusEnumerator 35 * 36 * This class is used for enumerating all terms of a sygus datatype type. At 37 * a high level, it is used as an alternative approach to sygus datatypes 38 * solver as a candidate generator in a synthesis loop. It filters terms based 39 * on redundancy criteria, for instance, it does not generate two terms whose 40 * builtin terms (TermDb::sygusToBuiltin) can be shown to be equivalent via 41 * rewriting. It enumerates terms in order of sygus term size 42 * (TermDb::getSygusTermSize). 43 */ 44 class SygusEnumerator : public EnumValGenerator 45 { 46 public: 47 SygusEnumerator(TermDbSygus* tds, SynthConjecture* p); ~SygusEnumerator()48 ~SygusEnumerator() {} 49 /** initialize this class with enumerator e */ 50 void initialize(Node e) override; 51 /** Inform this generator that abstract value v was enumerated. */ 52 void addValue(Node v) override; 53 /** increment */ 54 bool increment() override; 55 /** Get the next concrete value generated by this class. */ 56 Node getCurrent() override; 57 58 private: 59 /** pointer to term database sygus */ 60 TermDbSygus* d_tds; 61 /** pointer to the synth conjecture that owns this enumerator */ 62 SynthConjecture* d_parent; 63 /** Term cache 64 * 65 * This stores a list of terms for a given sygus type. The key features of 66 * this data structure are that terms are stored in order of size, 67 * indices can be recorded that indicate where terms of size n begin for each 68 * natural number n, and redundancy criteria are used for discarding terms 69 * that are not relevant. This includes discarding terms whose builtin version 70 * is the same up to T-rewriting with another, or is equivalent under 71 * examples, if the conjecture in question is in PBE form and sygusSymBreakPbe 72 * is enabled. 73 * 74 * This class also computes static information about sygus types that is 75 * relevant for enumeration. Primarily, this includes mapping constructors 76 * to "constructor classes". Two sygus constructors can be placed in the same 77 * constructor class if their constructor weight is equal, and the tuple 78 * of their argument types are the same. For example, for: 79 * A -> A+B | A-B | A*B | A+A | A | x 80 * The first three constructors above can be placed in the same constructor 81 * class, assuming they have identical weights. Constructor classes are used 82 * as an optimization when enumerating terms, since they expect the same 83 * tuple of argument terms for constructing a term of a fixed size. 84 * 85 * Constructor classes are allocated such that the constructor weights are 86 * in ascending order. This allows us to avoid constructors whose weight 87 * is greater than n while we are trying to enumerate terms of sizes strictly 88 * less than n. 89 * 90 * Constructor class 0 is reserved for nullary operators with weight 0. This 91 * is an optimization so that such constructors can be skipped for sizes 92 * greater than 0, since we know all terms generated by these constructors 93 * have size 0. 94 */ 95 class TermCache 96 { 97 public: 98 TermCache(); 99 /** initialize this cache */ 100 void initialize(Node e, 101 TypeNode tn, 102 TermDbSygus* tds, 103 SygusPbe* pbe = nullptr); 104 /** get last constructor class index for weight 105 * 106 * This returns a minimal index n such that all constructor classes at 107 * index < n have weight at most w. 108 */ 109 unsigned getLastConstructorClassIndexForWeight(unsigned w) const; 110 /** get num constructor classes */ 111 unsigned getNumConstructorClasses() const; 112 /** get the constructor indices for constructor class i */ 113 void getConstructorClass(unsigned i, std::vector<unsigned>& cclass) const; 114 /** get argument types for constructor class i */ 115 void getTypesForConstructorClass(unsigned i, 116 std::vector<TypeNode>& types) const; 117 /** get constructor weight for constructor class i */ 118 unsigned getWeightForConstructorClass(unsigned i) const; 119 120 /** 121 * Add sygus term n to this cache, return true if the term was unique based 122 * on the redundancy criteria used by this class. 123 */ 124 bool addTerm(Node n); 125 /** 126 * Indicate to this cache that we are finished enumerating terms of the 127 * current size. 128 */ 129 void pushEnumSizeIndex(); 130 /** Get the current size of terms that we are enumerating */ 131 unsigned getEnumSize() const; 132 /** get the index at which size s terms start, where s <= getEnumSize() */ 133 unsigned getIndexForSize(unsigned s) const; 134 /** get the index^th term successfully added to this cache */ 135 Node getTerm(unsigned index) const; 136 /** get the number of terms successfully added to this cache */ 137 unsigned getNumTerms() const; 138 /** are we finished enumerating terms? */ 139 bool isComplete() const; 140 /** set that we are finished enumerating terms */ 141 void setComplete(); 142 143 private: 144 /** the enumerator this cache is for */ 145 Node d_enum; 146 /** the sygus type of terms in this cache */ 147 TypeNode d_tn; 148 /** pointer to term database sygus */ 149 TermDbSygus* d_tds; 150 /** pointer to the PBE utility (used for symmetry breaking) */ 151 SygusPbe* d_pbe; 152 //-------------------------static information about type 153 /** is d_tn a sygus type? */ 154 bool d_isSygusType; 155 /** number of constructor classes */ 156 unsigned d_numConClasses; 157 /** Map from weights to the starting constructor class for that weight. */ 158 std::map<unsigned, unsigned> d_weightToCcIndex; 159 /** constructor classes */ 160 std::map<unsigned, std::vector<unsigned>> d_ccToCons; 161 /** maps constructor classes to children types */ 162 std::map<unsigned, std::vector<TypeNode>> d_ccToTypes; 163 /** maps constructor classes to constructor weight */ 164 std::map<unsigned, unsigned> d_ccToWeight; 165 /** constructor to indices */ 166 std::map<unsigned, std::vector<unsigned>> d_cToCIndices; 167 //-------------------------end static information about type 168 169 /** the list of sygus terms we have enumerated */ 170 std::vector<Node> d_terms; 171 /** the set of builtin terms corresponding to the above list */ 172 std::unordered_set<Node, NodeHashFunction> d_bterms; 173 /** 174 * The index of first term whose size is greater than or equal to that size, 175 * if it exists. 176 */ 177 std::map<unsigned, unsigned> d_sizeStartIndex; 178 /** the maximum size of terms we have stored in this cache so far */ 179 unsigned d_sizeEnum; 180 /** whether this term cache is complete */ 181 bool d_isComplete; 182 /** sampler (for --sygus-rr-verify) */ 183 quantifiers::SygusSampler d_samplerRrV; 184 /** is the above sampler initialized? */ 185 bool d_sampleRrVInit; 186 }; 187 /** above cache for each sygus type */ 188 std::map<TypeNode, TermCache> d_tcache; 189 /** initialize term cache for type tn */ 190 void initializeTermCache(TypeNode tn); 191 192 /** virtual class for term enumerators */ 193 class TermEnum 194 { 195 public: 196 TermEnum(); ~TermEnum()197 virtual ~TermEnum() {} 198 /** get the current size of terms we are enumerating */ 199 unsigned getCurrentSize(); 200 /** get the current term of the enumerator */ 201 virtual Node getCurrent() = 0; 202 /** increment the enumerator, return false if the enumerator is finished */ 203 virtual bool increment() = 0; 204 205 protected: 206 /** pointer to the sygus enumerator class */ 207 SygusEnumerator* d_se; 208 /** the (sygus) type of terms we are enumerating */ 209 TypeNode d_tn; 210 /** the current size of terms we are enumerating */ 211 unsigned d_currSize; 212 }; 213 class TermEnumMaster; 214 /** A "slave" enumerator 215 * 216 * A slave enumerator simply iterates over an index in a given term cache, 217 * and relies on a pointer to a "master" enumerator to generate new terms 218 * whenever necessary. 219 * 220 * This class maintains the following invariants, for tc=d_se->d_tcache[d_tn]: 221 * (1) d_index < tc.getNumTerms(), 222 * (2) d_currSize is the term size of tc.getTerm( d_index ), 223 * (3) d_hasIndexNextEnd is (d_currSize < tc.getEnumSize()), 224 * (4) If d_hasIndexNextEnd is true, then 225 * d_indexNextEnd = tc.getIndexForSize(d_currSize+1), and 226 * d_indexNextEnd > d_index. 227 * 228 * Intuitively, these invariants say (1) d_index is a valid index in the 229 * term cache, (2) d_currSize is the sygus term size of getCurrent(), (3) 230 * d_hasIndexNextEnd indicates whether d_indexNextEnd is valid, and (4) 231 * d_indexNextEnd is the index in the term cache where terms of the current 232 * size end, if such an index exists. 233 */ 234 class TermEnumSlave : public TermEnum 235 { 236 public: 237 TermEnumSlave(); 238 /** 239 * Initialize this enumerator to enumerate terms of type tn whose size is in 240 * the range [sizeMin, sizeMax], inclusive. If this function returns true, 241 * then getCurrent() will return the first term in the stream, which is 242 * non-empty. Further terms are generated by increment()/getCurrent(). 243 */ 244 bool initialize(SygusEnumerator* se, 245 TypeNode tn, 246 unsigned sizeMin, 247 unsigned sizeMax); 248 /** get the current term of the enumerator */ 249 Node getCurrent() override; 250 /** increment the enumerator */ 251 bool increment() override; 252 253 private: 254 /** the maximum size of terms this enumerator should enumerate */ 255 unsigned d_sizeLim; 256 /** the current index in the term cache we are considering */ 257 unsigned d_index; 258 /** the index in the term cache where terms of the current size end */ 259 unsigned d_indexNextEnd; 260 /** whether d_indexNextEnd refers to a valid index */ 261 bool d_hasIndexNextEnd; 262 /** pointer to the master enumerator of type d_tn */ 263 TermEnum* d_master; 264 /** validate invariants on d_index, d_indexNextEnd, d_hasIndexNextEnd */ 265 bool validateIndex(); 266 /** validate invariants on d_indexNextEnd, d_hasIndexNextEnd */ 267 void validateIndexNextEnd(); 268 }; 269 /** Class for "master" enumerators 270 * 271 * This enumerator is used to generate new terms of a given type d_tn. It 272 * generates all terms of type d_tn that are not redundant based on the 273 * current criteria. 274 * 275 * To enumerate terms, this class performs the following steps as necessary 276 * during a call to increment(): 277 * - Fix the size of terms "d_currSize" we are currently enumerating, 278 * - Set the constructor class "d_consClassNum" whose constructors are the top 279 * symbol of the current term we are constructing. All constructors from this 280 * class have the same weight, which we store in d_ccWeight, 281 * - Initialize the current children "d_children" so that the sum of their 282 * current sizes is exactly (d_currSize - d_ccWeight), 283 * - Increment the current set of children until a new tuple of terms is 284 * considered, 285 * - Set the constructor "d_consNum" from within the constructor class, 286 * - Build the current term and check whether it is not redundant according 287 * to the term cache of its type. 288 * 289 * We say this enumerator is active if initialize(...) returns true, and the 290 * last call (if any) to increment returned true. 291 * 292 * This class maintains the following invariants, for tc=d_se->d_tcache[d_tn], 293 * if it is active: 294 * (1) getCurrent() is tc.getTerm(tc.getNumTerms()-1), 295 * (2) tc.pushEnumSizeIndex() has been called by this class exactly 296 * getCurrentSize() times. 297 * In other words, (1) getCurrent() is always the last term in the term cache 298 * of the type of this enumerator tc, and (2) the size counter of tc is in 299 * sync with the current size of this enumerator, that is, the master 300 * enumerator is responsible for communicating size boundaries to its term 301 * cache. 302 */ 303 class TermEnumMaster : public TermEnum 304 { 305 public: 306 TermEnumMaster(); 307 /** 308 * Initialize this enumerator to enumerate (all) terms of type tn, modulo 309 * the redundancy criteria used by this class. 310 */ 311 bool initialize(SygusEnumerator* se, TypeNode tn); 312 /** get the current term of the enumerator */ 313 Node getCurrent() override; 314 /** increment the enumerator 315 * 316 * Returns true if there are more terms to enumerate, in which case a 317 * subsequent call to getCurrent() returns the next enumerated term. This 318 * method returns false if the last call to increment() has yet to 319 * terminate. This can happen for recursive datatypes where a slave 320 * enumerator may request that this class increment the next term. We avoid 321 * an infinite loop by guarding this with the d_isIncrementing flag and 322 * return false. 323 */ 324 bool increment() override; 325 326 private: 327 /** are we currently inside a increment() call? */ 328 bool d_isIncrementing; 329 /** cache for getCurrent() */ 330 Node d_currTerm; 331 /** is d_currTerm set */ 332 bool d_currTermSet; 333 //----------------------------- current constructor class information 334 /** the next constructor class we are using */ 335 unsigned d_consClassNum; 336 /** the constructors in the current constructor class */ 337 std::vector<unsigned> d_ccCons; 338 /** the types of the current constructor class */ 339 std::vector<TypeNode> d_ccTypes; 340 /** the operator weight for the constructor class */ 341 unsigned d_ccWeight; 342 //----------------------------- end current constructor class information 343 /** If >0, 1 + the index in d_ccCons we are considering */ 344 unsigned d_consNum; 345 /** the child enumerators for this enumerator */ 346 std::map<unsigned, TermEnumSlave> d_children; 347 /** the current sum of current sizes of the enumerators in d_children */ 348 unsigned d_currChildSize; 349 /** 350 * The number of indices, starting from zero, in d_children that point to 351 * initialized slave enumerators. 352 */ 353 unsigned d_childrenValid; 354 /** initialize children 355 * 356 * Initialize all the uninitialized children of this enumerator. If this 357 * method returns true, then all children d_children are successfully 358 * initialized to be slave enumerators of the argument types indicated by 359 * d_ccTypes, and the sum of their current sizes (d_currChildSize) is 360 * exactly (d_currSize - d_ccWeight). If this method returns false, then 361 * it was not possible to initialize the children such that they meet the 362 * size requirements, and such that the assignments from children to size 363 * has not already been considered. In this case, d_children is cleared 364 * and d_currChildSize and d_childrenValid are reset. 365 */ 366 bool initializeChildren(); 367 /** initialize child 368 * 369 * Initialize child i to enumerate terms whose size is at least sizeMin, 370 * and whose maximum size is the largest size such that we can still 371 * construct terms for the given constructor class and the current children 372 * whose size is not more than the current size d_currSize. Additionally, 373 * if i is the last child, we modify sizeMin such that it is exactly the 374 * size of terms needed for the children to sum up to size d_currSize. 375 */ 376 bool initializeChild(unsigned i, unsigned sizeMin); 377 /** increment internal, helper for increment() */ 378 bool incrementInternal(); 379 }; 380 /** an interpreted value enumerator 381 * 382 * This enumerator uses the builtin type enumerator for a given type. It 383 * is used to fill in concrete holes into "any constant" constructors 384 * when sygus-repair-const is not enabled. The number of terms of size n 385 * is m^n, where m is configurable via --sygus-active-gen-enum-cfactor=m. 386 */ 387 class TermEnumMasterInterp : public TermEnum 388 { 389 public: 390 TermEnumMasterInterp(TypeNode tn); 391 /** initialize this enumerator */ 392 bool initialize(SygusEnumerator* se, TypeNode tn); 393 /** get the current term of the enumerator */ 394 Node getCurrent() override; 395 /** increment the enumerator */ 396 bool increment() override; 397 398 private: 399 /** the type enumerator */ 400 TypeEnumerator d_te; 401 /** the current number of terms we are enumerating for the given size */ 402 unsigned d_currNumConsts; 403 /** the next end threshold */ 404 unsigned d_nextIndexEnd; 405 }; 406 /** a free variable enumerator 407 * 408 * This enumerator enumerates canonical free variables for a given type. 409 * The n^th variable in this stream is assigned size n. This enumerator is 410 * used in conjunction with sygus-repair-const to generate solutions with 411 * constant holes. In this approach, free variables are arguments to 412 * any-constant constructors. This is required so that terms with holes are 413 * unique up to rewriting when appropriate. 414 */ 415 class TermEnumMasterFv : public TermEnum 416 { 417 public: 418 TermEnumMasterFv(); 419 /** initialize this enumerator */ 420 bool initialize(SygusEnumerator* se, TypeNode tn); 421 /** get the current term of the enumerator */ 422 Node getCurrent() override; 423 /** increment the enumerator */ 424 bool increment() override; 425 }; 426 /** the master enumerator for each sygus type */ 427 std::map<TypeNode, TermEnumMaster> d_masterEnum; 428 /** the master enumerator for each non-sygus type */ 429 std::map<TypeNode, TermEnumMasterFv> d_masterEnumFv; 430 /** the master enumerator for each non-sygus type */ 431 std::map<TypeNode, std::unique_ptr<TermEnumMasterInterp>> d_masterEnumInt; 432 /** the sygus enumerator this class is for */ 433 Node d_enum; 434 /** the type of d_enum */ 435 TypeNode d_etype; 436 /** pointer to the master enumerator of type d_etype */ 437 TermEnum* d_tlEnum; 438 /** the abort size, caches the value of --sygus-abort-size */ 439 int d_abortSize; 440 /** get master enumerator for type tn */ 441 TermEnum* getMasterEnumForType(TypeNode tn); 442 //-------------------------------- externally specified symmetry breaking 443 /** set of constructors we disallow at top level 444 * 445 * A constructor C is disallowed at the top level if a symmetry breaking 446 * lemma that entails ~is-C( d_enum ) was registered to 447 * TermDbSygus::registerSymBreakLemma. 448 */ 449 std::unordered_set<Node, NodeHashFunction> d_sbExcTlCons; 450 //-------------------------------- end externally specified symmetry breaking 451 }; 452 453 } // namespace quantifiers 454 } // namespace theory 455 } // namespace CVC4 456 457 #endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */ 458