diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.cpp | 17 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.h | 9 |
2 files changed, 19 insertions, 7 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index f6ec58f56..3a79a526a 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -871,12 +871,21 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() // if not, there is no use continuing. if (initializeChildren()) { - Trace("sygus-enum-debug2") << "master(" << d_tn << "): success\n"; + Trace("sygus-enum-debug2") + << "master(" << d_tn << "): success init children\n"; Assert(d_currChildSize + d_ccWeight <= d_currSize); incSuccess = true; } + else + { + // failed to initialize the remaining children (likely due to a + // child having a non-zero minimum size bound). + Trace("sygus-enum-debug2") + << "master(" << d_tn << "): fail init children\n"; + d_currChildSize -= d_children[i].getCurrentSize(); + } } - else + if (!incSuccess) { Trace("sygus-enum-debug2") << "master(" << d_tn << "): fail, backtrack...\n"; @@ -900,14 +909,16 @@ bool SygusEnumerator::TermEnumMaster::initializeChildren() << "master(" << d_tn << "): init children, start = " << d_childrenValid << ", #types=" << d_ccTypes.size() << ", sizes=" << d_currChildSize << "/" << d_currSize << std::endl; + unsigned currChildren = d_childrenValid; unsigned sizeMin = 0; // while we need to initialize the current child while (d_childrenValid < d_ccTypes.size()) { if (!initializeChild(d_childrenValid, sizeMin)) { - if (d_childrenValid == 0) + if (d_childrenValid == currChildren) { + // we are back to the child we started with, we terminate now. Trace("sygus-enum-debug2") << "master(" << d_tn << "): init children : failed, finished" << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index d4c466b03..c9d1d8fca 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -353,15 +353,16 @@ class SygusEnumerator : public EnumValGenerator unsigned d_childrenValid; /** initialize children * - * Initialize all the uninitialized children of this enumerator. If this - * method returns true, then all children d_children are successfully + * Initialize all the remaining uninitialized children of this enumerator. + * If this method returns true, then each of d_children are * initialized to be slave enumerators of the argument types indicated by * d_ccTypes, and the sum of their current sizes (d_currChildSize) is * exactly (d_currSize - d_ccWeight). If this method returns false, then * it was not possible to initialize the children such that they meet the * size requirements, and such that the assignments from children to size - * has not already been considered. In this case, d_children is cleared - * and d_currChildSize and d_childrenValid are reset. + * has not already been considered. In this case, all updates to d_children + * are reverted and d_currChildSize and d_childrenValid are reset to their + * values prior to this call. */ bool initializeChildren(); /** initialize child |