1 /********************* */
2 /*! \file sygus_enumerator.cpp
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 Implementation of sygus_enumerator
13 **/
14
15 #include "theory/quantifiers/sygus/sygus_enumerator.h"
16
17 #include "options/datatypes_options.h"
18 #include "options/quantifiers_options.h"
19 #include "theory/datatypes/datatypes_rewriter.h"
20
21 using namespace CVC4::kind;
22
23 namespace CVC4 {
24 namespace theory {
25 namespace quantifiers {
26
SygusEnumerator(TermDbSygus * tds,SynthConjecture * p)27 SygusEnumerator::SygusEnumerator(TermDbSygus* tds, SynthConjecture* p)
28 : d_tds(tds), d_parent(p), d_tlEnum(nullptr), d_abortSize(-1)
29 {
30 }
31
initialize(Node e)32 void SygusEnumerator::initialize(Node e)
33 {
34 Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl;
35 d_enum = e;
36 d_etype = d_enum.getType();
37 Assert(d_etype.isDatatype());
38 Assert(d_etype.getDatatype().isSygus());
39 d_tlEnum = getMasterEnumForType(d_etype);
40 d_abortSize = options::sygusAbortSize();
41
42 // Get the statically registered symmetry breaking clauses for e, see if they
43 // can be used for speeding up the enumeration.
44 NodeManager* nm = NodeManager::currentNM();
45 std::vector<Node> sbl;
46 d_tds->getSymBreakLemmas(e, sbl);
47 Node ag = d_tds->getActiveGuardForEnumerator(e);
48 Node truen = nm->mkConst(true);
49 // use TNode for substitute below
50 TNode agt = ag;
51 TNode truent = truen;
52 Assert(d_tcache.find(d_etype) != d_tcache.end());
53 const Datatype& dt = d_etype.getDatatype();
54 for (const Node& lem : sbl)
55 {
56 if (!d_tds->isSymBreakLemmaTemplate(lem))
57 {
58 // substitute its active guard by true and rewrite
59 Node slem = lem.substitute(agt, truent);
60 slem = Rewriter::rewrite(slem);
61 // break into conjuncts
62 std::vector<Node> sblc;
63 if (slem.getKind() == AND)
64 {
65 for (const Node& slemc : slem)
66 {
67 sblc.push_back(slemc);
68 }
69 }
70 else
71 {
72 sblc.push_back(slem);
73 }
74 for (const Node& sbl : sblc)
75 {
76 Trace("sygus-enum")
77 << " symmetry breaking lemma : " << sbl << std::endl;
78 // if its a negation of a unit top-level tester, then this specifies
79 // that we should not enumerate terms whose top symbol is that
80 // constructor
81 if (sbl.getKind() == NOT)
82 {
83 Node a;
84 int tst = datatypes::DatatypesRewriter::isTester(sbl[0], a);
85 if (tst >= 0)
86 {
87 if (a == e)
88 {
89 Node cons = Node::fromExpr(dt[tst].getConstructor());
90 Trace("sygus-enum") << " ...unit exclude constructor #" << tst
91 << ", constructor " << cons << std::endl;
92 d_sbExcTlCons.insert(cons);
93 }
94 }
95 }
96 // other symmetry breaking lemmas such as disjunctions are not used
97 }
98 }
99 }
100 }
101
addValue(Node v)102 void SygusEnumerator::addValue(Node v)
103 {
104 // do nothing
105 }
106
increment()107 bool SygusEnumerator::increment() { return d_tlEnum->increment(); }
getCurrent()108 Node SygusEnumerator::getCurrent()
109 {
110 if (d_abortSize >= 0)
111 {
112 int cs = static_cast<int>(d_tlEnum->getCurrentSize());
113 if (cs > d_abortSize)
114 {
115 std::stringstream ss;
116 ss << "Maximum term size (" << options::sygusAbortSize()
117 << ") for enumerative SyGuS exceeded.";
118 throw LogicException(ss.str());
119 }
120 }
121 Node ret = d_tlEnum->getCurrent();
122 if (!ret.isNull() && !d_sbExcTlCons.empty())
123 {
124 Assert(ret.hasOperator());
125 // might be excluded by an externally provided symmetry breaking clause
126 if (d_sbExcTlCons.find(ret.getOperator()) != d_sbExcTlCons.end())
127 {
128 Trace("sygus-enum-exc")
129 << "Exclude (external) : " << d_tds->sygusToBuiltin(ret) << std::endl;
130 ret = Node::null();
131 }
132 }
133 if (Trace.isOn("sygus-enum"))
134 {
135 Trace("sygus-enum") << "Enumerate : ";
136 TermDbSygus::toStreamSygus("sygus-enum", ret);
137 Trace("sygus-enum") << std::endl;
138 }
139 return ret;
140 }
141
TermCache()142 SygusEnumerator::TermCache::TermCache()
143 : d_tds(nullptr),
144 d_pbe(nullptr),
145 d_isSygusType(false),
146 d_numConClasses(0),
147 d_sizeEnum(0),
148 d_isComplete(false),
149 d_sampleRrVInit(false)
150 {
151 }
initialize(Node e,TypeNode tn,TermDbSygus * tds,SygusPbe * pbe)152 void SygusEnumerator::TermCache::initialize(Node e,
153 TypeNode tn,
154 TermDbSygus* tds,
155 SygusPbe* pbe)
156 {
157 Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl;
158 d_enum = e;
159 d_tn = tn;
160 d_tds = tds;
161 d_pbe = pbe;
162 d_sizeStartIndex[0] = 0;
163 d_isSygusType = false;
164
165 // compute static information about tn
166 if (!d_tn.isDatatype())
167 {
168 // not a datatype, finish
169 return;
170 }
171 const Datatype& dt = tn.getDatatype();
172 if (!dt.isSygus())
173 {
174 // not a sygus datatype, finish
175 return;
176 }
177
178 d_isSygusType = true;
179
180 // get argument types for all constructors
181 std::map<unsigned, std::vector<TypeNode>> argTypes;
182 // map weights to constructors
183 std::map<unsigned, std::vector<unsigned>> weightsToIndices;
184
185 // constructor class 0 is reserved for nullary operators with 0 weight
186 // this is an optimization so that we always skip them for sizes >= 1
187 d_ccToCons[0].clear();
188 d_ccToTypes[0].clear();
189 d_ccToWeight[0] = 0;
190 d_numConClasses = 1;
191 // we must indicate that we should process zero weight constructor classes
192 weightsToIndices[0].clear();
193 for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
194 {
195 // record weight information
196 unsigned w = dt[i].getWeight();
197 Trace("sygus-enum-debug") << "Weight " << dt[i].getSygusOp() << ": " << w
198 << std::endl;
199 weightsToIndices[w].push_back(i);
200 // record type information
201 for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
202 {
203 TypeNode tn = TypeNode::fromType(dt[i].getArgType(j));
204 argTypes[i].push_back(tn);
205 }
206 }
207 NodeManager* nm = NodeManager::currentNM();
208 for (std::pair<const unsigned, std::vector<unsigned>>& wp : weightsToIndices)
209 {
210 unsigned w = wp.first;
211
212 // assign constructors to constructor classes
213 TypeNodeIdTrie tnit;
214 std::map<Node, unsigned> nToC;
215 for (unsigned i : wp.second)
216 {
217 if (argTypes[i].empty() && w == 0)
218 {
219 d_ccToCons[0].push_back(i);
220 }
221 else
222 {
223 // we merge those whose argument types are the same
224 // We could, but choose not to, order these types, which would lead to
225 // more aggressive merging of constructor classes. On the negative side,
226 // this adds another level of indirection to remember which argument
227 // positions the argument types occur in, for each constructor.
228 Node n = nm->mkConst(Rational(i));
229 nToC[n] = i;
230 tnit.add(n, argTypes[i]);
231 }
232 }
233 std::map<Node, unsigned> assign;
234 tnit.assignIds(assign, d_numConClasses);
235 for (std::pair<const Node, unsigned>& cp : assign)
236 {
237 // determine which constructor class this goes into using tnit
238 unsigned cclassi = cp.second;
239 unsigned i = nToC[cp.first];
240 Trace("sygus-enum-debug") << "Constructor class for "
241 << dt[i].getSygusOp() << " is " << cclassi
242 << std::endl;
243 // initialize the constructor class
244 if (d_ccToWeight.find(cclassi) == d_ccToWeight.end())
245 {
246 d_ccToWeight[cclassi] = w;
247 d_ccToTypes[cclassi].insert(
248 d_ccToTypes[cclassi].end(), argTypes[i].begin(), argTypes[i].end());
249 }
250 // add to constructor class
251 d_ccToCons[cclassi].push_back(i);
252 }
253 Trace("sygus-enum-debug") << "#cons classes for weight <= " << w << " : "
254 << d_numConClasses << std::endl;
255 d_weightToCcIndex[w] = d_numConClasses;
256 }
257 Trace("sygus-enum-debug") << "...finish" << std::endl;
258 }
259
getLastConstructorClassIndexForWeight(unsigned w) const260 unsigned SygusEnumerator::TermCache::getLastConstructorClassIndexForWeight(
261 unsigned w) const
262 {
263 std::map<unsigned, unsigned>::const_iterator it = d_weightToCcIndex.find(w);
264 if (it == d_weightToCcIndex.end())
265 {
266 return d_numConClasses;
267 }
268 return it->second;
269 }
getNumConstructorClasses() const270 unsigned SygusEnumerator::TermCache::getNumConstructorClasses() const
271 {
272 return d_numConClasses;
273 }
getConstructorClass(unsigned i,std::vector<unsigned> & cclass) const274 void SygusEnumerator::TermCache::getConstructorClass(
275 unsigned i, std::vector<unsigned>& cclass) const
276 {
277 std::map<unsigned, std::vector<unsigned>>::const_iterator it =
278 d_ccToCons.find(i);
279 Assert(it != d_ccToCons.end());
280 cclass.insert(cclass.end(), it->second.begin(), it->second.end());
281 }
getTypesForConstructorClass(unsigned i,std::vector<TypeNode> & types) const282 void SygusEnumerator::TermCache::getTypesForConstructorClass(
283 unsigned i, std::vector<TypeNode>& types) const
284 {
285 std::map<unsigned, std::vector<TypeNode>>::const_iterator it =
286 d_ccToTypes.find(i);
287 Assert(it != d_ccToTypes.end());
288 types.insert(types.end(), it->second.begin(), it->second.end());
289 }
290
getWeightForConstructorClass(unsigned i) const291 unsigned SygusEnumerator::TermCache::getWeightForConstructorClass(
292 unsigned i) const
293 {
294 std::map<unsigned, unsigned>::const_iterator it = d_ccToWeight.find(i);
295 Assert(it != d_ccToWeight.end());
296 return it->second;
297 }
298
addTerm(Node n)299 bool SygusEnumerator::TermCache::addTerm(Node n)
300 {
301 if (!d_isSygusType)
302 {
303 // non-sygus terms generated by TermEnumMasterInterp/TermEnumMasterFv
304 // enumeration are unique by construction
305 Trace("sygus-enum-terms") << "tc(" << d_tn << "): term (builtin): " << n
306 << std::endl;
307 d_terms.push_back(n);
308 return true;
309 }
310 Assert(!n.isNull());
311 if (options::sygusSymBreakDynamic())
312 {
313 Node bn = d_tds->sygusToBuiltin(n);
314 Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn);
315 if (options::sygusRewVerify())
316 {
317 if (bn != bnr)
318 {
319 if (!d_sampleRrVInit)
320 {
321 d_sampleRrVInit = true;
322 d_samplerRrV.initializeSygus(
323 d_tds, d_enum, options::sygusSamples(), false);
324 }
325 d_samplerRrV.checkEquivalent(bn, bnr);
326 }
327 }
328 // must be unique up to rewriting
329 if (d_bterms.find(bnr) != d_bterms.end())
330 {
331 Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
332 return false;
333 }
334 // if we are doing PBE symmetry breaking
335 if (d_pbe != nullptr)
336 {
337 // Is it equivalent under examples?
338 Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr);
339 if (!bne.isNull())
340 {
341 if (bnr != bne)
342 {
343 Trace("sygus-enum-exc")
344 << "Exclude (by examples): " << bn << ", since we already have "
345 << bne << std::endl;
346 return false;
347 }
348 }
349 }
350 Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
351 d_bterms.insert(bnr);
352 }
353 d_terms.push_back(n);
354 return true;
355 }
pushEnumSizeIndex()356 void SygusEnumerator::TermCache::pushEnumSizeIndex()
357 {
358 d_sizeEnum++;
359 d_sizeStartIndex[d_sizeEnum] = d_terms.size();
360 Trace("sygus-enum-debug") << "tc(" << d_tn << "): size " << d_sizeEnum
361 << " terms start at index " << d_terms.size()
362 << std::endl;
363 }
getEnumSize() const364 unsigned SygusEnumerator::TermCache::getEnumSize() const { return d_sizeEnum; }
getIndexForSize(unsigned s) const365 unsigned SygusEnumerator::TermCache::getIndexForSize(unsigned s) const
366 {
367 Assert(s <= d_sizeEnum);
368 std::map<unsigned, unsigned>::const_iterator it = d_sizeStartIndex.find(s);
369 Assert(it != d_sizeStartIndex.end());
370 return it->second;
371 }
getTerm(unsigned index) const372 Node SygusEnumerator::TermCache::getTerm(unsigned index) const
373 {
374 Assert(index < d_terms.size());
375 return d_terms[index];
376 }
377
getNumTerms() const378 unsigned SygusEnumerator::TermCache::getNumTerms() const
379 {
380 return d_terms.size();
381 }
382
isComplete() const383 bool SygusEnumerator::TermCache::isComplete() const { return d_isComplete; }
setComplete()384 void SygusEnumerator::TermCache::setComplete() { d_isComplete = true; }
getCurrentSize()385 unsigned SygusEnumerator::TermEnum::getCurrentSize() { return d_currSize; }
TermEnum()386 SygusEnumerator::TermEnum::TermEnum() : d_se(nullptr), d_currSize(0) {}
TermEnumSlave()387 SygusEnumerator::TermEnumSlave::TermEnumSlave()
388 : TermEnum(),
389 d_sizeLim(0),
390 d_index(0),
391 d_indexNextEnd(0),
392 d_hasIndexNextEnd(false),
393 d_master(nullptr)
394 {
395 }
396
initialize(SygusEnumerator * se,TypeNode tn,unsigned sizeMin,unsigned sizeMax)397 bool SygusEnumerator::TermEnumSlave::initialize(SygusEnumerator* se,
398 TypeNode tn,
399 unsigned sizeMin,
400 unsigned sizeMax)
401 {
402 d_se = se;
403 d_tn = tn;
404 d_sizeLim = sizeMax;
405 Trace("sygus-enum-debug2") << "slave(" << d_tn
406 << "): init, min/max=" << sizeMin << "/" << sizeMax
407 << "...\n";
408
409 // must have pointer to the master
410 d_master = d_se->getMasterEnumForType(d_tn);
411
412 SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
413 // if the size is exact, we start at the limit
414 d_currSize = sizeMin;
415 // initialize the index
416 while (d_currSize > tc.getEnumSize())
417 {
418 Trace("sygus-enum-debug2") << "slave(" << d_tn
419 << "): init force increment master...\n";
420 // increment the master until we have enough terms
421 if (!d_master->increment())
422 {
423 Trace("sygus-enum-debug2") << "slave(" << d_tn
424 << "): ...fail init force master\n";
425 return false;
426 }
427 Trace("sygus-enum-debug2") << "slave(" << d_tn
428 << "): ...success init force master\n";
429 }
430 d_index = tc.getIndexForSize(d_currSize);
431 Trace("sygus-enum-debug2") << "slave(" << d_tn << "): validate indices...\n";
432 // initialize the next end index (marks where size increments)
433 validateIndexNextEnd();
434 Trace("sygus-enum-debug2")
435 << "slave(" << d_tn << "): validate init end: " << d_hasIndexNextEnd
436 << " " << d_indexNextEnd << " " << d_index << " " << d_currSize << "\n";
437 // ensure that indexNextEnd is valid (it must be greater than d_index)
438 bool ret = validateIndex();
439 Trace("sygus-enum-debug2")
440 << "slave(" << d_tn << "): ..." << (ret ? "success" : "fail")
441 << " init, now: " << d_hasIndexNextEnd << " " << d_indexNextEnd << " "
442 << d_index << " " << d_currSize << "\n";
443 return ret;
444 }
445
getCurrent()446 Node SygusEnumerator::TermEnumSlave::getCurrent()
447 {
448 SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
449 Node curr = tc.getTerm(d_index);
450 Trace("sygus-enum-debug2")
451 << "slave(" << d_tn
452 << "): current : " << d_se->d_tds->sygusToBuiltin(curr)
453 << ", sizes = " << d_se->d_tds->getSygusTermSize(curr) << " "
454 << getCurrentSize() << std::endl;
455 Trace("sygus-enum-debug2") << "slave(" << d_tn
456 << "): indices : " << d_hasIndexNextEnd << " "
457 << d_indexNextEnd << " " << d_index << std::endl;
458 // lookup in the cache
459 return tc.getTerm(d_index);
460 }
461
increment()462 bool SygusEnumerator::TermEnumSlave::increment()
463 {
464 // increment index
465 d_index++;
466 // ensure that index is valid
467 return validateIndex();
468 }
469
validateIndex()470 bool SygusEnumerator::TermEnumSlave::validateIndex()
471 {
472 Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : validate index...\n";
473 SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
474 // ensure that index is in the range
475 while (d_index >= tc.getNumTerms())
476 {
477 Assert(d_index == tc.getNumTerms());
478 Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n";
479 // if the size of the master is larger than the size limit, then
480 // there is no use continuing, since there are no more terms that this
481 // slave enumerator can return.
482 if (d_master->getCurrentSize() > d_sizeLim)
483 {
484 return false;
485 }
486 // must push the master index
487 if (!d_master->increment())
488 {
489 Trace("sygus-enum-debug2") << "slave(" << d_tn
490 << ") : ...fail force master\n";
491 return false;
492 }
493 Trace("sygus-enum-debug2") << "slave(" << d_tn
494 << ") : ...success force master\n";
495 }
496 // always validate the next index end here
497 validateIndexNextEnd();
498 Trace("sygus-enum-debug2") << "slave(" << d_tn
499 << ") : validate index end...\n";
500 // if we are at the beginning of the next size, increment current size
501 while (d_hasIndexNextEnd && d_index == d_indexNextEnd)
502 {
503 d_currSize++;
504 Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : size++ ("
505 << d_currSize << "/" << d_sizeLim << ")\n";
506 // if we've hit the size limit, return false
507 if (d_currSize > d_sizeLim)
508 {
509 Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : fail size\n";
510 return false;
511 }
512 validateIndexNextEnd();
513 }
514 Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : finished\n";
515 return true;
516 }
517
validateIndexNextEnd()518 void SygusEnumerator::TermEnumSlave::validateIndexNextEnd()
519 {
520 SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
521 // update the next end index
522 d_hasIndexNextEnd = d_currSize < tc.getEnumSize();
523 if (d_hasIndexNextEnd)
524 {
525 d_indexNextEnd = tc.getIndexForSize(d_currSize + 1);
526 }
527 }
528
initializeTermCache(TypeNode tn)529 void SygusEnumerator::initializeTermCache(TypeNode tn)
530 {
531 // initialize the term cache
532 // see if we use sygus PBE for symmetry breaking
533 SygusPbe* pbe = nullptr;
534 if (options::sygusSymBreakPbe())
535 {
536 pbe = d_parent->getPbe();
537 if (!pbe->hasExamples(d_enum))
538 {
539 pbe = nullptr;
540 }
541 }
542 d_tcache[tn].initialize(d_enum, tn, d_tds, pbe);
543 }
544
getMasterEnumForType(TypeNode tn)545 SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
546 {
547 if (tn.isDatatype() && tn.getDatatype().isSygus())
548 {
549 std::map<TypeNode, TermEnumMaster>::iterator it = d_masterEnum.find(tn);
550 if (it != d_masterEnum.end())
551 {
552 return &it->second;
553 }
554 initializeTermCache(tn);
555 // initialize the master enumerator
556 bool ret = d_masterEnum[tn].initialize(this, tn);
557 AlwaysAssert(ret);
558 return &d_masterEnum[tn];
559 }
560 if (options::sygusRepairConst())
561 {
562 std::map<TypeNode, TermEnumMasterFv>::iterator it = d_masterEnumFv.find(tn);
563 if (it != d_masterEnumFv.end())
564 {
565 return &it->second;
566 }
567 initializeTermCache(tn);
568 // initialize the master enumerator
569 bool ret = d_masterEnumFv[tn].initialize(this, tn);
570 AlwaysAssert(ret);
571 return &d_masterEnumFv[tn];
572 }
573 std::map<TypeNode, std::unique_ptr<TermEnumMasterInterp>>::iterator it =
574 d_masterEnumInt.find(tn);
575 if (it != d_masterEnumInt.end())
576 {
577 return it->second.get();
578 }
579 initializeTermCache(tn);
580 // create the master enumerator
581 d_masterEnumInt[tn].reset(new TermEnumMasterInterp(tn));
582 // initialize the master enumerator
583 TermEnumMasterInterp* temi = d_masterEnumInt[tn].get();
584 bool ret = temi->initialize(this, tn);
585 AlwaysAssert(ret);
586 return temi;
587 }
588
TermEnumMaster()589 SygusEnumerator::TermEnumMaster::TermEnumMaster()
590 : TermEnum(),
591 d_isIncrementing(false),
592 d_currTermSet(false),
593 d_consClassNum(0),
594 d_ccWeight(0),
595 d_consNum(0),
596 d_currChildSize(0),
597 d_childrenValid(0)
598 {
599 }
600
initialize(SygusEnumerator * se,TypeNode tn)601 bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se,
602 TypeNode tn)
603 {
604 Trace("sygus-enum-debug") << "master(" << tn << "): init...\n";
605 d_se = se;
606 d_tn = tn;
607
608 d_currSize = 0;
609 // we will start with constructor class zero
610 d_consClassNum = 0;
611 d_currChildSize = 0;
612 d_ccCons.clear();
613 d_isIncrementing = false;
614 d_currTermSet = false;
615 bool ret = increment();
616 Trace("sygus-enum-debug") << "master(" << tn
617 << "): finish init, ret = " << ret << "\n";
618 return ret;
619 }
620
getCurrent()621 Node SygusEnumerator::TermEnumMaster::getCurrent()
622 {
623 if (d_currTermSet)
624 {
625 return d_currTerm;
626 }
627 d_currTermSet = true;
628 // construct based on the children
629 std::vector<Node> children;
630 const Datatype& dt = d_tn.getDatatype();
631 Assert(d_consNum > 0 && d_consNum <= d_ccCons.size());
632 // get the current constructor number
633 unsigned cnum = d_ccCons[d_consNum - 1];
634 children.push_back(Node::fromExpr(dt[cnum].getConstructor()));
635 // add the current of each child to children
636 for (unsigned i = 0, nargs = dt[cnum].getNumArgs(); i < nargs; i++)
637 {
638 Assert(d_children.find(i) != d_children.end());
639 Node cc = d_children[i].getCurrent();
640 if (cc.isNull())
641 {
642 d_currTerm = cc;
643 return cc;
644 }
645 children.push_back(cc);
646 }
647 d_currTerm = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children);
648 return d_currTerm;
649 }
650
increment()651 bool SygusEnumerator::TermEnumMaster::increment()
652 {
653 // Am I already incrementing? If so, fail.
654 // This is to break infinite loops for slave enumerators who request an
655 // increment() from the master enumerator of their type that is also their
656 // parent. This ensures we do not loop on a grammar like:
657 // A -> -( A ) | B+B
658 // B -> x | y
659 // where we require the first term enumerated to be over B+B.
660 // Set that we are incrementing
661 if (d_isIncrementing)
662 {
663 return false;
664 }
665 Trace("sygus-enum-summary") << "SygusEnumerator::TermEnumMaster: increment "
666 << d_tn << "..." << std::endl;
667 d_isIncrementing = true;
668 bool ret = incrementInternal();
669 d_isIncrementing = false;
670 Trace("sygus-enum-summary")
671 << "SygusEnumerator::TermEnumMaster: finished increment " << d_tn
672 << std::endl;
673 return ret;
674 }
675
incrementInternal()676 bool SygusEnumerator::TermEnumMaster::incrementInternal()
677 {
678 SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
679 if (tc.isComplete())
680 {
681 return false;
682 }
683 Trace("sygus-enum-debug2") << "master(" << d_tn
684 << "): get last constructor class..." << std::endl;
685 // the maximum index of a constructor class to consider
686 unsigned ncc = tc.getLastConstructorClassIndexForWeight(d_currSize);
687 Trace("sygus-enum-debug2") << "Last constructor class " << d_currSize << ": "
688 << ncc << std::endl;
689
690 // have we initialized the current constructor class?
691 while (d_ccCons.empty() && d_consClassNum < ncc)
692 {
693 Assert(d_ccTypes.empty());
694 Trace("sygus-enum-debug2") << "master(" << d_tn
695 << "): try constructor class " << d_consClassNum
696 << std::endl;
697 // get the list of constructors in the constructor class
698 tc.getConstructorClass(d_consClassNum, d_ccCons);
699 // if there are any...
700 if (!d_ccCons.empty())
701 {
702 // successfully initialized the constructor class
703 d_consNum = 0;
704 // we will populate the children
705 Assert(d_children.empty());
706 Assert(d_ccTypes.empty());
707 tc.getTypesForConstructorClass(d_consClassNum, d_ccTypes);
708 d_ccWeight = tc.getWeightForConstructorClass(d_consClassNum);
709 d_childrenValid = 0;
710 // initialize the children into their initial state
711 if (!initializeChildren())
712 {
713 // didn't work (due to size), we will try the next class
714 d_ccCons.clear();
715 d_ccTypes.clear();
716 Trace("sygus-enum-debug2") << "master(" << d_tn
717 << "): failed due to init size\n";
718 }
719 }
720 else
721 {
722 // No constructors in constructor class. This can happen for class 0 if a
723 // type has no nullary constructors with weight 0.
724 Trace("sygus-enum-debug2") << "master(" << d_tn
725 << "): failed due to no cons\n";
726 }
727 // increment the next constructor class we will try
728 d_consClassNum++;
729 }
730
731 // have we run out of constructor classes for this size?
732 if (d_ccCons.empty())
733 {
734 // check whether we should terminate
735 if (d_tn.isInterpretedFinite())
736 {
737 if (ncc == tc.getNumConstructorClasses())
738 {
739 bool doTerminate = true;
740 for (unsigned i = 1; i < ncc; i++)
741 {
742 // The maximum size of terms from a constructor class can be
743 // determined if all of its argument types are finished enumerating.
744 // If this maximum size is less than or equal to d_currSize for
745 // each constructor class, we are done.
746 unsigned sum = tc.getWeightForConstructorClass(i);
747 std::vector<TypeNode> cctns;
748 tc.getTypesForConstructorClass(i, cctns);
749 for (unsigned j = 0, ntypes = cctns.size(); j < ntypes; j++)
750 {
751 TypeNode tnc = cctns[j];
752 SygusEnumerator::TermCache& tcc = d_se->d_tcache[tnc];
753 if (!tcc.isComplete())
754 {
755 // maximum size of this constructor class cannot be determined
756 doTerminate = false;
757 break;
758 }
759 else
760 {
761 sum += tcc.getEnumSize();
762 if (sum > d_currSize)
763 {
764 // maximum size of this constructor class is greater than size
765 doTerminate = false;
766 break;
767 }
768 }
769 }
770 if (!doTerminate)
771 {
772 break;
773 }
774 }
775 if (doTerminate)
776 {
777 Trace("cegqi-engine") << "master(" << d_tn << "): complete at size "
778 << d_currSize << std::endl;
779 tc.setComplete();
780 return false;
781 }
782 }
783 }
784
785 // increment the size bound
786 d_currSize++;
787 Trace("sygus-enum-debug2") << "master(" << d_tn
788 << "): size++ : " << d_currSize << "\n";
789 if (Trace.isOn("cegqi-engine"))
790 {
791 // am i the master enumerator? if so, print
792 if (d_se->d_tlEnum == this)
793 {
794 Trace("cegqi-engine") << "SygusEnumerator::size = " << d_currSize
795 << std::endl;
796 }
797 }
798
799 // push the bound
800 tc.pushEnumSizeIndex();
801
802 // restart with constructor class one (skip nullary constructors)
803 d_consClassNum = 1;
804
805 // We break for a round: return the null term when we cross a size
806 // boundary. This ensures that the necessary breaks are taken, e.g.
807 // in slave enumerators who may instead want to abandon this call to
808 // increment master when the size of the master makes their increment
809 // infeasible.
810 d_currTermSet = true;
811 d_currTerm = Node::null();
812 return true;
813 }
814
815 bool incSuccess = false;
816 do
817 {
818 Trace("sygus-enum-debug2") << "master(" << d_tn << "): check return "
819 << d_childrenValid << "/" << d_ccTypes.size()
820 << std::endl;
821 // the children should be initialized by here
822 Assert(d_childrenValid == d_ccTypes.size());
823
824 // do we have more constructors for the given children?
825 if (d_consNum < d_ccCons.size())
826 {
827 Trace("sygus-enum-debug2") << "master(" << d_tn << "): try constructor "
828 << d_consNum << std::endl;
829 // increment constructor index
830 // we will build for the current constructor and the given children
831 d_consNum++;
832 d_currTermSet = false;
833 d_currTerm = Node::null();
834 Node c = getCurrent();
835 if (!c.isNull())
836 {
837 if (!tc.addTerm(c))
838 {
839 // the term was not unique based on rewriting
840 Trace("sygus-enum-debug2") << "master(" << d_tn
841 << "): failed addTerm\n";
842 // we will return null (d_currTermSet is true at this point)
843 Assert(d_currTermSet);
844 d_currTerm = Node::null();
845 }
846 }
847 return true;
848 }
849
850 // finished constructors for this set of children, must increment children
851
852 // reset the constructor number
853 d_consNum = 0;
854
855 // try incrementing the last child until we find one that works
856 incSuccess = false;
857 while (!incSuccess && d_childrenValid > 0)
858 {
859 Trace("sygus-enum-debug2") << "master(" << d_tn << "): try incrementing "
860 << d_childrenValid << std::endl;
861 unsigned i = d_childrenValid - 1;
862 Assert(d_children[i].getCurrentSize() <= d_currChildSize);
863 // track the size
864 d_currChildSize -= d_children[i].getCurrentSize();
865 if (d_children[i].increment())
866 {
867 Trace("sygus-enum-debug2") << "master(" << d_tn
868 << "): increment success...\n";
869 d_currChildSize += d_children[i].getCurrentSize();
870 // must see if we can initialize the remaining children here
871 // if not, there is no use continuing.
872 if (initializeChildren())
873 {
874 Trace("sygus-enum-debug2") << "master(" << d_tn << "): success\n";
875 Assert(d_currChildSize + d_ccWeight <= d_currSize);
876 incSuccess = true;
877 }
878 }
879 else
880 {
881 Trace("sygus-enum-debug2") << "master(" << d_tn
882 << "): fail, backtrack...\n";
883 // current child is out of values
884 d_children.erase(i);
885 d_childrenValid--;
886 }
887 }
888 } while (incSuccess);
889 Trace("sygus-enum-debug2") << "master(" << d_tn
890 << "): failed increment children\n";
891 // restart with the next constructor class
892 d_ccCons.clear();
893 d_ccTypes.clear();
894 return incrementInternal();
895 }
896
initializeChildren()897 bool SygusEnumerator::TermEnumMaster::initializeChildren()
898 {
899 Trace("sygus-enum-debug2")
900 << "master(" << d_tn << "): init children, start = " << d_childrenValid
901 << ", #types=" << d_ccTypes.size() << ", sizes=" << d_currChildSize << "/"
902 << d_currSize << std::endl;
903 unsigned sizeMin = 0;
904 // while we need to initialize the current child
905 while (d_childrenValid < d_ccTypes.size())
906 {
907 if (!initializeChild(d_childrenValid, sizeMin))
908 {
909 if (d_childrenValid == 0)
910 {
911 Trace("sygus-enum-debug2") << "master(" << d_tn
912 << "): init children : failed, finished"
913 << std::endl;
914 return false;
915 }
916 Trace("sygus-enum-debug2") << "master(" << d_tn
917 << "): init children : failed" << std::endl;
918 // we failed in this size configuration
919 // reinitialize with the next size up
920 unsigned currSize = d_children[d_childrenValid - 1].getCurrentSize();
921 d_currChildSize -= currSize;
922 sizeMin = currSize + 1;
923 d_children.erase(d_childrenValid - 1);
924 d_childrenValid--;
925 }
926 else
927 {
928 sizeMin = 0;
929 d_childrenValid++;
930 }
931 }
932 Trace("sygus-enum-debug2") << "master(" << d_tn
933 << "): init children : success" << std::endl;
934 // initialized all children
935 return true;
936 }
937
initializeChild(unsigned i,unsigned sizeMin)938 bool SygusEnumerator::TermEnumMaster::initializeChild(unsigned i,
939 unsigned sizeMin)
940 {
941 Assert(d_ccWeight <= d_currSize);
942 Assert(d_currChildSize + d_ccWeight <= d_currSize);
943 unsigned sizeMax = (d_currSize - d_ccWeight) - d_currChildSize;
944 Trace("sygus-enum-debug2") << "master(" << d_tn << "): initializeChild " << i
945 << " (" << d_currSize << ", " << d_ccWeight << ", "
946 << d_currChildSize << ")\n";
947 if (sizeMin > sizeMax)
948 {
949 Trace("sygus-enum-debug2") << "master(" << d_tn << "): failed due to size "
950 << sizeMin << "/" << sizeMax << "\n";
951 return false;
952 }
953 // initialize the child to enumerate exactly the terms that sum to size
954 sizeMin = (i + 1 == d_ccTypes.size()) ? sizeMax : sizeMin;
955 TermEnumSlave& te = d_children[i];
956 bool init = te.initialize(d_se, d_ccTypes[i], sizeMin, sizeMax);
957 if (!init)
958 {
959 // failed to initialize
960 d_children.erase(i);
961 Trace("sygus-enum-debug2") << "master(" << d_tn
962 << "): failed due to child init\n";
963 return false;
964 }
965 unsigned teSize = te.getCurrentSize();
966 // fail if the initial children size does not fit d_currSize-d_ccWeight
967 if (teSize + d_currChildSize + d_ccWeight > d_currSize)
968 {
969 d_children.erase(i);
970 Trace("sygus-enum-debug2") << "master(" << d_tn
971 << "): failed due to child size\n";
972 return false;
973 }
974 d_currChildSize += teSize;
975 Trace("sygus-enum-debug2") << "master(" << d_tn
976 << "): success initializeChild " << i << "\n";
977 return true;
978 }
979
TermEnumMasterInterp(TypeNode tn)980 SygusEnumerator::TermEnumMasterInterp::TermEnumMasterInterp(TypeNode tn)
981 : TermEnum(), d_te(tn), d_currNumConsts(0), d_nextIndexEnd(0)
982 {
983 }
984
initialize(SygusEnumerator * se,TypeNode tn)985 bool SygusEnumerator::TermEnumMasterInterp::initialize(SygusEnumerator* se,
986 TypeNode tn)
987 {
988 d_se = se;
989 d_tn = tn;
990 d_currSize = 0;
991 d_currNumConsts = 1;
992 d_nextIndexEnd = 1;
993 return true;
994 }
995
getCurrent()996 Node SygusEnumerator::TermEnumMasterInterp::getCurrent() { return *d_te; }
increment()997 bool SygusEnumerator::TermEnumMasterInterp::increment()
998 {
999 SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
1000 Node curr = getCurrent();
1001 tc.addTerm(curr);
1002 if (tc.getNumTerms() == d_nextIndexEnd)
1003 {
1004 tc.pushEnumSizeIndex();
1005 d_currSize++;
1006 d_currNumConsts = d_currNumConsts * options::sygusActiveGenEnumConsts();
1007 d_nextIndexEnd = d_nextIndexEnd + d_currNumConsts;
1008 }
1009 ++d_te;
1010 return !d_te.isFinished();
1011 }
TermEnumMasterFv()1012 SygusEnumerator::TermEnumMasterFv::TermEnumMasterFv() : TermEnum() {}
initialize(SygusEnumerator * se,TypeNode tn)1013 bool SygusEnumerator::TermEnumMasterFv::initialize(SygusEnumerator* se,
1014 TypeNode tn)
1015 {
1016 d_se = se;
1017 d_tn = tn;
1018 d_currSize = 0;
1019 Node ret = getCurrent();
1020 AlwaysAssert(!ret.isNull());
1021 SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
1022 tc.addTerm(ret);
1023 return true;
1024 }
1025
getCurrent()1026 Node SygusEnumerator::TermEnumMasterFv::getCurrent()
1027 {
1028 Node ret = d_se->d_tds->getFreeVar(d_tn, d_currSize);
1029 Trace("sygus-enum-debug2") << "master_fv(" << d_tn << "): mk " << ret
1030 << std::endl;
1031 return ret;
1032 }
1033
increment()1034 bool SygusEnumerator::TermEnumMasterFv::increment()
1035 {
1036 SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
1037 // size increments at a constant rate
1038 d_currSize++;
1039 tc.pushEnumSizeIndex();
1040 Node curr = getCurrent();
1041 Trace("sygus-enum-debug2") << "master_fv(" << d_tn << "): increment, add "
1042 << curr << std::endl;
1043 bool ret = tc.addTerm(curr);
1044 AlwaysAssert(ret);
1045 return true;
1046 }
1047
1048 } // namespace quantifiers
1049 } // namespace theory
1050 } // namespace CVC4
1051