diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 11 | ||||
| -rw-r--r-- | src/options/quantifiers_modes.h | 6 | ||||
| -rw-r--r-- | src/options/quantifiers_options.toml | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.cpp | 925 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.h | 442 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 6 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 14 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 27 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 82 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 26 |
11 files changed, 1491 insertions, 58 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 10db1dc86..9a1cfe9e7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -534,6 +534,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/cegis_unif.h theory/quantifiers/sygus/enum_stream_substitution.cpp theory/quantifiers/sygus/enum_stream_substitution.h + theory/quantifiers/sygus/sygus_enumerator.cpp + theory/quantifiers/sygus/sygus_enumerator.h theory/quantifiers/sygus/sygus_eval_unfold.cpp theory/quantifiers/sygus/sygus_eval_unfold.h theory/quantifiers/sygus/sygus_explain.cpp diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 46663ce7c..e4c0276ea 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -530,7 +530,10 @@ none \n\ + Do not use actively-generated sygus enumerators.\n\ \n\ basic \n\ -+ Use basic type enumerator as sygus enumerator.\n\ ++ Use basic type enumerator for actively-generated sygus enumerators.\n\ +\n\ +enum \n\ ++ Use optimized enumerator for actively-generated sygus enumerators.\n\ \n\ var-agnostic \n\ + Use sygus solver to enumerate terms that are agnostic to variables. \n\ @@ -974,7 +977,11 @@ OptionsHandler::stringToSygusActiveGenMode(std::string option, } else if (optarg == "basic") { - return theory::quantifiers::SYGUS_ACTIVE_GEN_BASIC; + return theory::quantifiers::SYGUS_ACTIVE_GEN_ENUM_BASIC; + } + else if (optarg == "enum") + { + return theory::quantifiers::SYGUS_ACTIVE_GEN_ENUM; } else if (optarg == "var-agnostic") { diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 42ab7bc06..392393a91 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -266,8 +266,10 @@ enum SygusActiveGenMode { /** do not use actively-generated enumerators */ SYGUS_ACTIVE_GEN_NONE, - /** use basic actively-generated enumerators */ - SYGUS_ACTIVE_GEN_BASIC, + /** use basic enumeration for actively-generated enumerators */ + SYGUS_ACTIVE_GEN_ENUM_BASIC, + /** use optimized enumeration actively-generated enumerators */ + SYGUS_ACTIVE_GEN_ENUM, /** use variable-agnostic enumerators */ SYGUS_ACTIVE_GEN_VAR_AGNOSTIC, }; diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 0762622f0..0b28c6a27 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1051,6 +1051,14 @@ header = "options/quantifiers_options.h" help = "mode for actively-generated sygus enumerators" [[option]] + name = "sygusActiveGenEnumConsts" + category = "regular" + long = "sygus-active-gen-cfactor=N" + type = "unsigned long" + default = "5" + help = "the branching factor for the number of interpreted constants to consider for each size when using --sygus-active-gen=enum" + +[[option]] name = "sygusMinGrammar" category = "regular" long = "sygus-min-grammar" diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp new file mode 100644 index 000000000..61ab9007a --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -0,0 +1,925 @@ +/********************* */ +/*! \file sygus_enumerator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sygus_enumerator + **/ + +#include "theory/quantifiers/sygus/sygus_enumerator.h" + +#include "options/datatypes_options.h" +#include "options/quantifiers_options.h" +#include "theory/datatypes/datatypes_rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SygusEnumerator::SygusEnumerator(TermDbSygus* tds, SynthConjecture* p) + : d_tds(tds), + d_parent(p), + d_tlEnum(nullptr), + d_abortSize(-1), + d_firstTime(false) +{ +} + +void SygusEnumerator::initialize(Node e) +{ + d_enum = e; + d_etype = d_enum.getType(); + d_tlEnum = getMasterEnumForType(d_etype); + d_abortSize = options::sygusAbortSize(); + d_firstTime = true; +} + +void SygusEnumerator::addValue(Node v) +{ + // do nothing +} + +Node SygusEnumerator::getNext() +{ + if (d_firstTime) + { + d_firstTime = false; + } + else if (!d_tlEnum->increment()) + { + // no more values + return Node::null(); + } + if (d_abortSize >= 0) + { + int cs = static_cast<int>(d_tlEnum->getCurrentSize()); + if (cs > d_abortSize) + { + std::stringstream ss; + ss << "Maximum term size (" << options::sygusAbortSize() + << ") for enumerative SyGuS exceeded."; + throw LogicException(ss.str()); + } + } + Node ret = d_tlEnum->getCurrent(); + Trace("sygus-enum") << "Enumerate : " << d_tds->sygusToBuiltin(ret) + << std::endl; + return ret; +} + +SygusEnumerator::TermCache::TermCache() + : d_tds(nullptr), + d_pbe(nullptr), + d_numConClasses(0), + d_sizeEnum(0), + d_isComplete(false) +{ +} +void SygusEnumerator::TermCache::initialize(Node e, + TypeNode tn, + TermDbSygus* tds, + SygusPbe* pbe) +{ + Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl; + d_enum = e; + d_tn = tn; + d_tds = tds; + d_pbe = pbe; + d_sizeStartIndex[0] = 0; + d_isSygusType = false; + + // compute static information about tn + if (!d_tn.isDatatype()) + { + // not a datatype, finish + return; + } + const Datatype& dt = tn.getDatatype(); + if (!dt.isSygus()) + { + // not a sygus datatype, finish + return; + } + + d_isSygusType = true; + + // get argument types for all constructors + std::map<unsigned, std::vector<TypeNode>> argTypes; + // map weights to constructors + std::map<unsigned, std::vector<unsigned>> weightsToIndices; + + // constructor class 0 is reserved for nullary operators with 0 weight + // this is an optimization so that we always skip them for sizes >= 1 + d_ccToCons[0].clear(); + d_ccToTypes[0].clear(); + d_ccToWeight[0] = 0; + d_numConClasses = 1; + // we must indicate that we should process zero weight constructor classes + weightsToIndices[0].clear(); + for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + // record weight information + unsigned w = dt[i].getWeight(); + Trace("sygus-enum-debug") << "Weight " << dt[i].getSygusOp() << ": " << w + << std::endl; + weightsToIndices[w].push_back(i); + // record type information + for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) + { + TypeNode tn = TypeNode::fromType(dt[i].getArgType(j)); + argTypes[i].push_back(tn); + } + } + NodeManager* nm = NodeManager::currentNM(); + for (std::pair<const unsigned, std::vector<unsigned>>& wp : weightsToIndices) + { + unsigned w = wp.first; + + // assign constructors to constructor classes + TypeNodeIdTrie tnit; + std::map<Node, unsigned> nToC; + for (unsigned i : wp.second) + { + if (argTypes[i].empty() && w == 0) + { + d_ccToCons[0].push_back(i); + } + else + { + // we merge those whose argument types are the same + // We could, but choose not to, order these types, which would lead to + // more aggressive merging of constructor classes. On the negative side, + // this adds another level of indirection to remember which argument + // positions the argument types occur in, for each constructor. + Node n = nm->mkConst(Rational(i)); + nToC[n] = i; + tnit.add(n, argTypes[i]); + } + } + std::map<Node, unsigned> assign; + tnit.assignIds(assign, d_numConClasses); + for (std::pair<const Node, unsigned>& cp : assign) + { + // determine which constructor class this goes into using tnit + unsigned cclassi = cp.second; + unsigned i = nToC[cp.first]; + Trace("sygus-enum-debug") << "Constructor class for " + << dt[i].getSygusOp() << " is " << cclassi + << std::endl; + // initialize the constructor class + if (d_ccToWeight.find(cclassi) == d_ccToWeight.end()) + { + d_ccToWeight[cclassi] = w; + d_ccToTypes[cclassi].insert( + d_ccToTypes[cclassi].end(), argTypes[i].begin(), argTypes[i].end()); + } + // add to constructor class + d_ccToCons[cclassi].push_back(i); + } + Trace("sygus-enum-debug") << "#cons classes for weight <= " << w << " : " + << d_numConClasses << std::endl; + d_weightToCcIndex[w] = d_numConClasses; + } + Trace("sygus-enum-debug") << "...finish" << std::endl; +} + +unsigned SygusEnumerator::TermCache::getLastConstructorClassIndexForWeight( + unsigned w) const +{ + std::map<unsigned, unsigned>::const_iterator it = d_weightToCcIndex.find(w); + if (it == d_weightToCcIndex.end()) + { + return d_numConClasses; + } + return it->second; +} +unsigned SygusEnumerator::TermCache::getNumConstructorClasses() const +{ + return d_numConClasses; +} +void SygusEnumerator::TermCache::getConstructorClass( + unsigned i, std::vector<unsigned>& cclass) const +{ + std::map<unsigned, std::vector<unsigned>>::const_iterator it = + d_ccToCons.find(i); + Assert(it != d_ccToCons.end()); + cclass.insert(cclass.end(), it->second.begin(), it->second.end()); +} +void SygusEnumerator::TermCache::getTypesForConstructorClass( + unsigned i, std::vector<TypeNode>& types) const +{ + std::map<unsigned, std::vector<TypeNode>>::const_iterator it = + d_ccToTypes.find(i); + Assert(it != d_ccToTypes.end()); + types.insert(types.end(), it->second.begin(), it->second.end()); +} + +unsigned SygusEnumerator::TermCache::getWeightForConstructorClass( + unsigned i) const +{ + std::map<unsigned, unsigned>::const_iterator it = d_ccToWeight.find(i); + Assert(it != d_ccToWeight.end()); + return it->second; +} + +bool SygusEnumerator::TermCache::addTerm(Node n) +{ + if (!d_isSygusType) + { + // non-sygus terms generated by TermEnumMasterInterp/TermEnumMasterFv + // enumeration are unique by construction + Trace("sygus-enum-terms") << "tc(" << d_tn << "): term (builtin): " << n + << std::endl; + d_terms.push_back(n); + return true; + } + Node bn = d_tds->sygusToBuiltin(n); + Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn); + // must be unique up to rewriting + if (d_bterms.find(bnr) != d_bterms.end()) + { + Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl; + return false; + } + // if we are doing PBE symmetry breaking + if (d_pbe != nullptr) + { + // Is it equivalent under examples? + Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr); + if (!bne.isNull()) + { + if (bnr != bne) + { + Trace("sygus-enum-exc") << "Exclude (by examples): " << bn + << ", since we already have " << bne + << "!=" << bnr << std::endl; + return false; + } + } + } + Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl; + d_terms.push_back(n); + d_bterms.insert(bnr); + return true; +} +void SygusEnumerator::TermCache::pushEnumSizeIndex() +{ + d_sizeEnum++; + d_sizeStartIndex[d_sizeEnum] = d_terms.size(); + Trace("sygus-enum-debug") << "tc(" << d_tn << "): size " << d_sizeEnum + << " terms start at index " << d_terms.size() + << std::endl; +} +unsigned SygusEnumerator::TermCache::getEnumSize() const { return d_sizeEnum; } +unsigned SygusEnumerator::TermCache::getIndexForSize(unsigned s) const +{ + Assert(s <= d_sizeEnum); + std::map<unsigned, unsigned>::const_iterator it = d_sizeStartIndex.find(s); + Assert(it != d_sizeStartIndex.end()); + return it->second; +} +Node SygusEnumerator::TermCache::getTerm(unsigned index) const +{ + Assert(index < d_terms.size()); + return d_terms[index]; +} + +unsigned SygusEnumerator::TermCache::getNumTerms() const +{ + return d_terms.size(); +} + +bool SygusEnumerator::TermCache::isComplete() const { return d_isComplete; } +void SygusEnumerator::TermCache::setComplete() { d_isComplete = true; } +unsigned SygusEnumerator::TermEnum::getCurrentSize() { return d_currSize; } +SygusEnumerator::TermEnum::TermEnum() : d_se(nullptr), d_currSize(0) {} +SygusEnumerator::TermEnumSlave::TermEnumSlave() + : TermEnum(), d_sizeLim(0), d_index(0), d_indexNextEnd(0), d_master(nullptr) +{ +} + +bool SygusEnumerator::TermEnumSlave::initialize(SygusEnumerator* se, + TypeNode tn, + unsigned sizeMin, + unsigned sizeMax) +{ + d_se = se; + d_tn = tn; + d_sizeLim = sizeMax; + Trace("sygus-enum-debug2") << "slave(" << d_tn + << "): init, min/max=" << sizeMin << "/" << sizeMax + << "...\n"; + + // must have pointer to the master + d_master = d_se->getMasterEnumForType(d_tn); + + SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn]; + // if the size is exact, we start at the limit + d_currSize = sizeMin; + // initialize the index + while (d_currSize > tc.getEnumSize()) + { + Trace("sygus-enum-debug2") << "slave(" << d_tn + << "): init force increment master...\n"; + // increment the master until we have enough terms + if (!d_master->increment()) + { + Trace("sygus-enum-debug2") << "slave(" << d_tn + << "): ...fail init force master\n"; + return false; + } + Trace("sygus-enum-debug2") << "slave(" << d_tn + << "): ...success init force master\n"; + } + d_index = tc.getIndexForSize(d_currSize); + Trace("sygus-enum-debug2") << "slave(" << d_tn << "): validate indices...\n"; + // initialize the next end index (marks where size increments) + validateIndexNextEnd(); + Trace("sygus-enum-debug2") + << "slave(" << d_tn << "): validate init end: " << d_hasIndexNextEnd + << " " << d_indexNextEnd << " " << d_index << " " << d_currSize << "\n"; + // ensure that indexNextEnd is valid (it must be greater than d_index) + bool ret = validateIndex(); + Trace("sygus-enum-debug2") + << "slave(" << d_tn << "): ..." << (ret ? "success" : "fail") + << " init, now: " << d_hasIndexNextEnd << " " << d_indexNextEnd << " " + << d_index << " " << d_currSize << "\n"; + return ret; +} + +Node SygusEnumerator::TermEnumSlave::getCurrent() +{ + SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn]; + Node curr = tc.getTerm(d_index); + Trace("sygus-enum-debug2") + << "slave(" << d_tn + << "): current : " << d_se->d_tds->sygusToBuiltin(curr) + << ", sizes = " << d_se->d_tds->getSygusTermSize(curr) << " " + << getCurrentSize() << std::endl; + Trace("sygus-enum-debug2") << "slave(" << d_tn + << "): indices : " << d_hasIndexNextEnd << " " + << d_indexNextEnd << " " << d_index << std::endl; + // lookup in the cache + return tc.getTerm(d_index); +} + +bool SygusEnumerator::TermEnumSlave::increment() +{ + // increment index + d_index++; + // ensure that index is valid + return validateIndex(); +} + +bool SygusEnumerator::TermEnumSlave::validateIndex() +{ + Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : validate index...\n"; + SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn]; + // ensure that index is in the range + if (d_index >= tc.getNumTerms()) + { + Assert(d_index == tc.getNumTerms()); + Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n"; + // must push the master index + if (!d_master->increment()) + { + Trace("sygus-enum-debug2") << "slave(" << d_tn + << ") : ...fail force master\n"; + return false; + } + Trace("sygus-enum-debug2") << "slave(" << d_tn + << ") : ...success force master\n"; + } + // always validate the next index end here + validateIndexNextEnd(); + Trace("sygus-enum-debug2") << "slave(" << d_tn + << ") : validate index end...\n"; + // if we are at the beginning of the next size, increment current size + while (d_hasIndexNextEnd && d_index == d_indexNextEnd) + { + d_currSize++; + Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : size++ (" + << d_currSize << "/" << d_sizeLim << ")\n"; + // if we've hit the size limit, return false + if (d_currSize > d_sizeLim) + { + Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : fail size\n"; + return false; + } + validateIndexNextEnd(); + } + Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : finished\n"; + return true; +} + +void SygusEnumerator::TermEnumSlave::validateIndexNextEnd() +{ + SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn]; + // update the next end index + d_hasIndexNextEnd = d_currSize < tc.getEnumSize(); + if (d_hasIndexNextEnd) + { + d_indexNextEnd = tc.getIndexForSize(d_currSize + 1); + } +} + +void SygusEnumerator::initializeTermCache(TypeNode tn) +{ + // initialize the term cache + // see if we use sygus PBE for symmetry breaking + SygusPbe* pbe = nullptr; + if (options::sygusSymBreakPbe()) + { + pbe = d_parent->getPbe(); + if (!pbe->hasExamples(d_enum)) + { + pbe = nullptr; + } + } + d_tcache[tn].initialize(d_enum, tn, d_tds, pbe); +} + +SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) +{ + if (tn.isDatatype() && tn.getDatatype().isSygus()) + { + std::map<TypeNode, TermEnumMaster>::iterator it = d_masterEnum.find(tn); + if (it != d_masterEnum.end()) + { + return &it->second; + } + initializeTermCache(tn); + // initialize the master enumerator + bool ret = d_masterEnum[tn].initialize(this, tn); + AlwaysAssert(ret); + return &d_masterEnum[tn]; + } + if (options::sygusRepairConst()) + { + std::map<TypeNode, TermEnumMasterFv>::iterator it = d_masterEnumFv.find(tn); + if (it != d_masterEnumFv.end()) + { + return &it->second; + } + initializeTermCache(tn); + // initialize the master enumerator + bool ret = d_masterEnumFv[tn].initialize(this, tn); + AlwaysAssert(ret); + return &d_masterEnumFv[tn]; + } + std::map<TypeNode, std::unique_ptr<TermEnumMasterInterp>>::iterator it = + d_masterEnumInt.find(tn); + if (it != d_masterEnumInt.end()) + { + return it->second.get(); + } + initializeTermCache(tn); + // create the master enumerator + d_masterEnumInt[tn].reset(new TermEnumMasterInterp(tn)); + // initialize the master enumerator + TermEnumMasterInterp* temi = d_masterEnumInt[tn].get(); + bool ret = temi->initialize(this, tn); + AlwaysAssert(ret); + return temi; +} + +SygusEnumerator::TermEnumMaster::TermEnumMaster() + : TermEnum(), + d_isIncrementing(false), + d_consClassNum(0), + d_ccWeight(0), + d_consNum(0), + d_currChildSize(0), + d_childrenValid(0) +{ +} + +bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se, + TypeNode tn) +{ + Trace("sygus-enum-debug") << "master(" << tn << "): init...\n"; + d_se = se; + d_tn = tn; + + d_currSize = 0; + // we will start with constructor class zero + d_consClassNum = 0; + d_currChildSize = 0; + d_ccCons.clear(); + d_isIncrementing = false; + bool ret = increment(); + Trace("sygus-enum-debug") << "master(" << tn + << "): finish init, ret = " << ret << "\n"; + return ret; +} + +Node SygusEnumerator::TermEnumMaster::getCurrent() +{ + if (!d_currTerm.isNull()) + { + return d_currTerm; + } + // construct based on the children + std::vector<Node> children; + const Datatype& dt = d_tn.getDatatype(); + Assert(d_consNum > 0 && d_consNum <= d_ccCons.size()); + // get the current constructor number + unsigned cnum = d_ccCons[d_consNum - 1]; + children.push_back(Node::fromExpr(dt[cnum].getConstructor())); + // add the current of each child to children + for (unsigned i = 0, nargs = dt[cnum].getNumArgs(); i < nargs; i++) + { + Assert(d_children.find(i) != d_children.end()); + children.push_back(d_children[i].getCurrent()); + } + d_currTerm = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children); + return d_currTerm; +} + +bool SygusEnumerator::TermEnumMaster::increment() +{ + // Am I already incrementing? If so, fail. + // This is to break infinite loops for slave enumerators who request an + // increment() from the master enumerator of their type that is also their + // parent. This ensures we do not loop on a grammar like: + // A -> -( A ) | B+B + // B -> x | y + // where we require the first term enumerated to be over B+B. + // Set that we are incrementing + if (d_isIncrementing) + { + return false; + } + d_isIncrementing = true; + bool ret = incrementInternal(); + d_isIncrementing = false; + return ret; +} + +bool SygusEnumerator::TermEnumMaster::incrementInternal() +{ + SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn]; + if (tc.isComplete()) + { + return false; + } + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): get last constructor class..." << std::endl; + // the maximum index of a constructor class to consider + unsigned ncc = tc.getLastConstructorClassIndexForWeight(d_currSize); + Trace("sygus-enum-debug2") << "Last constructor class " << d_currSize << ": " + << ncc << std::endl; + + // have we initialized the current constructor class? + while (d_ccCons.empty() && d_consClassNum < ncc) + { + Assert(d_ccTypes.empty()); + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): try constructor class " << d_consClassNum + << std::endl; + // get the list of constructors in the constructor class + tc.getConstructorClass(d_consClassNum, d_ccCons); + // if there are any... + if (!d_ccCons.empty()) + { + // successfully initialized the constructor class + d_consNum = 0; + // we will populate the children + Assert(d_children.empty()); + Assert(d_ccTypes.empty()); + tc.getTypesForConstructorClass(d_consClassNum, d_ccTypes); + d_ccWeight = tc.getWeightForConstructorClass(d_consClassNum); + d_childrenValid = 0; + // initialize the children into their initial state + if (!initializeChildren()) + { + // didn't work (due to size), we will try the next class + d_ccCons.clear(); + d_ccTypes.clear(); + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): failed due to init size\n"; + } + } + else + { + // No constructors in constructor class. This can happen for class 0 if a + // type has no nullary constructors with weight 0. + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): failed due to no cons\n"; + } + // increment the next constructor class we will try + d_consClassNum++; + } + + // have we run out of constructor classes for this size? + if (d_ccCons.empty()) + { + // check whether we should terminate + if (d_tn.isInterpretedFinite()) + { + if (ncc == tc.getNumConstructorClasses()) + { + bool doTerminate = true; + for (unsigned i = 1; i < ncc; i++) + { + // The maximum size of terms from a constructor class can be + // determined if all of its argument types are finished enumerating. + // If this maximum size is less than or equal to d_currSize for + // each constructor class, we are done. + unsigned sum = tc.getWeightForConstructorClass(i); + std::vector<TypeNode> cctns; + tc.getTypesForConstructorClass(i, cctns); + for (unsigned j = 0, ntypes = cctns.size(); j < ntypes; j++) + { + TypeNode tnc = cctns[j]; + SygusEnumerator::TermCache& tcc = d_se->d_tcache[tnc]; + if (!tcc.isComplete()) + { + // maximum size of this constructor class cannot be determined + doTerminate = false; + break; + } + else + { + sum += tcc.getEnumSize(); + if (sum > d_currSize) + { + // maximum size of this constructor class is greater than size + doTerminate = false; + break; + } + } + } + if (!doTerminate) + { + break; + } + } + if (doTerminate) + { + Trace("cegqi-engine") << "master(" << d_tn << "): complete at size " + << d_currSize << std::endl; + tc.setComplete(); + return false; + } + } + } + + // increment the size bound + d_currSize++; + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): size++ : " << d_currSize << "\n"; + if (Trace.isOn("cegqi-engine")) + { + // am i the master enumerator? if so, print + if (d_se->d_tlEnum == this) + { + Trace("cegqi-engine") << "SygusEnumerator::size = " << d_currSize + << std::endl; + } + } + + // push the bound + tc.pushEnumSizeIndex(); + + // restart with constructor class one (skip nullary constructors) + d_consClassNum = 1; + return incrementInternal(); + } + + bool incSuccess = false; + do + { + Trace("sygus-enum-debug2") << "master(" << d_tn << "): check return " + << d_childrenValid << "/" << d_ccTypes.size() + << std::endl; + // the children should be initialized by here + Assert(d_childrenValid == d_ccTypes.size()); + + // do we have more constructors for the given children? + while (d_consNum < d_ccCons.size()) + { + Trace("sygus-enum-debug2") << "master(" << d_tn << "): try constructor " + << d_consNum << std::endl; + // increment constructor index + // we will build for the current constructor and the given children + d_consNum++; + d_currTerm = Node::null(); + Node c = getCurrent(); + if (tc.addTerm(c)) + { + return true; + } + Trace("sygus-enum-debug2") << "master(" << d_tn << "): failed addTerm\n"; + // the term was not unique based on rewriting + } + + // finished constructors for this set of children, must increment children + + // reset the constructor number + d_consNum = 0; + + // try incrementing the last child until we find one that works + incSuccess = false; + while (!incSuccess && d_childrenValid > 0) + { + Trace("sygus-enum-debug2") << "master(" << d_tn << "): try incrementing " + << d_childrenValid << std::endl; + unsigned i = d_childrenValid - 1; + Assert(d_children[i].getCurrentSize() <= d_currChildSize); + // track the size + d_currChildSize -= d_children[i].getCurrentSize(); + if (d_children[i].increment()) + { + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): increment success...\n"; + d_currChildSize += d_children[i].getCurrentSize(); + // must see if we can initialize the remaining children here + // if not, there is no use continuing. + if (initializeChildren()) + { + Trace("sygus-enum-debug2") << "master(" << d_tn << "): success\n"; + Assert(d_currChildSize + d_ccWeight <= d_currSize); + incSuccess = true; + } + } + else + { + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): fail, backtrack...\n"; + // current child is out of values + d_children.erase(i); + d_childrenValid--; + } + } + } while (incSuccess); + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): failed increment children\n"; + // restart with the next constructor class + d_ccCons.clear(); + d_ccTypes.clear(); + return incrementInternal(); +} + +bool SygusEnumerator::TermEnumMaster::initializeChildren() +{ + Trace("sygus-enum-debug2") + << "master(" << d_tn << "): init children, start = " << d_childrenValid + << ", #types=" << d_ccTypes.size() << ", sizes=" << d_currChildSize << "/" + << d_currSize << std::endl; + 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) + { + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): init children : failed, finished" + << std::endl; + return false; + } + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): init children : failed" << std::endl; + // we failed in this size configuration + // reinitialize with the next size up + unsigned currSize = d_children[d_childrenValid - 1].getCurrentSize(); + d_currChildSize -= currSize; + sizeMin = currSize + 1; + d_children.erase(d_childrenValid - 1); + d_childrenValid--; + } + else + { + sizeMin = 0; + d_childrenValid++; + } + } + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): init children : success" << std::endl; + // initialized all children + return true; +} + +bool SygusEnumerator::TermEnumMaster::initializeChild(unsigned i, + unsigned sizeMin) +{ + Assert(d_ccWeight <= d_currSize); + Assert(d_currChildSize + d_ccWeight <= d_currSize); + unsigned sizeMax = (d_currSize - d_ccWeight) - d_currChildSize; + Trace("sygus-enum-debug2") << "master(" << d_tn << "): initializeChild " << i + << " (" << d_currSize << ", " << d_ccWeight << ", " + << d_currChildSize << ")\n"; + if (sizeMin > sizeMax) + { + Trace("sygus-enum-debug2") << "master(" << d_tn << "): failed due to size " + << sizeMin << "/" << sizeMax << "\n"; + return false; + } + // initialize the child to enumerate exactly the terms that sum to size + sizeMin = (i + 1 == d_ccTypes.size()) ? sizeMax : sizeMin; + TermEnumSlave& te = d_children[i]; + bool init = te.initialize(d_se, d_ccTypes[i], sizeMin, sizeMax); + if (!init) + { + // failed to initialize + d_children.erase(i); + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): failed due to child init\n"; + return false; + } + unsigned teSize = te.getCurrentSize(); + // fail if the initial children size does not fit d_currSize-d_ccWeight + if (teSize + d_currChildSize + d_ccWeight > d_currSize) + { + d_children.erase(i); + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): failed due to child size\n"; + return false; + } + d_currChildSize += teSize; + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): success initializeChild " << i << "\n"; + return true; +} + +SygusEnumerator::TermEnumMasterInterp::TermEnumMasterInterp(TypeNode tn) + : TermEnum(), d_te(tn), d_currNumConsts(0), d_nextIndexEnd(0) +{ +} + +bool SygusEnumerator::TermEnumMasterInterp::initialize(SygusEnumerator* se, + TypeNode tn) +{ + d_se = se; + d_tn = tn; + d_currSize = 0; + d_currNumConsts = 1; + d_nextIndexEnd = 1; + return true; +} + +Node SygusEnumerator::TermEnumMasterInterp::getCurrent() { return *d_te; } +bool SygusEnumerator::TermEnumMasterInterp::increment() +{ + SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn]; + Node curr = getCurrent(); + tc.addTerm(curr); + if (tc.getNumTerms() == d_nextIndexEnd) + { + tc.pushEnumSizeIndex(); + d_currSize++; + d_currNumConsts = d_currNumConsts * options::sygusActiveGenEnumConsts(); + d_nextIndexEnd = d_nextIndexEnd + d_currNumConsts; + } + ++d_te; + return !d_te.isFinished(); +} +SygusEnumerator::TermEnumMasterFv::TermEnumMasterFv() : TermEnum() {} +bool SygusEnumerator::TermEnumMasterFv::initialize(SygusEnumerator* se, + TypeNode tn) +{ + d_se = se; + d_tn = tn; + d_currSize = 0; + Node ret = getCurrent(); + AlwaysAssert(!ret.isNull()); + SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn]; + tc.addTerm(ret); + return true; +} + +Node SygusEnumerator::TermEnumMasterFv::getCurrent() +{ + Node ret = d_se->d_tds->getFreeVar(d_tn, d_currSize); + Trace("sygus-enum-debug2") << "master_fv(" << d_tn << "): mk " << ret + << std::endl; + return ret; +} + +bool SygusEnumerator::TermEnumMasterFv::increment() +{ + SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn]; + // size increments at a constant rate + d_currSize++; + tc.pushEnumSizeIndex(); + Node curr = getCurrent(); + Trace("sygus-enum-debug2") << "master_fv(" << d_tn << "): increment, add " + << curr << std::endl; + bool ret = tc.addTerm(curr); + AlwaysAssert(ret); + return true; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h new file mode 100644 index 000000000..10a44da03 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -0,0 +1,442 @@ +/******************** */ +/*! \file sygus_enumerator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief sygus_enumerator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H + +#include <map> +#include <unordered_set> +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class SynthConjecture; +class SygusPbe; + +/** SygusEnumerator + * + * This class is used for enumerating all terms of a sygus datatype type. At + * a high level, it is used as an alternative approach to sygus datatypes + * solver as a candidate generator in a synthesis loop. It filters terms based + * on redundancy criteria, for instance, it does not generate two terms whose + * builtin terms (TermDb::sygusToBuiltin) can be shown to be equivalent via + * rewriting. It enumerates terms in order of sygus term size + * (TermDb::getSygusTermSize). + */ +class SygusEnumerator : public EnumValGenerator +{ + public: + SygusEnumerator(TermDbSygus* tds, SynthConjecture* p); + ~SygusEnumerator() {} + /** initialize this class with enumerator e */ + void initialize(Node e) override; + /** Inform this generator that abstract value v was enumerated. */ + void addValue(Node v) override; + /** Get the next concrete value generated by this class. */ + Node getNext() override; + + private: + /** pointer to term database sygus */ + TermDbSygus* d_tds; + /** pointer to the synth conjecture that owns this enumerator */ + SynthConjecture* d_parent; + /** Term cache + * + * This stores a list of terms for a given sygus type. The key features of + * this data structure are that terms are stored in order of size, + * indices can be recorded that indicate where terms of size n begin for each + * natural number n, and redundancy criteria are used for discarding terms + * that are not relevant. This includes discarding terms whose builtin version + * is the same up to T-rewriting with another, or is equivalent under + * examples, if the conjecture in question is in PBE form and sygusSymBreakPbe + * is enabled. + * + * This class also computes static information about sygus types that is + * relevant for enumeration. Primarily, this includes mapping constructors + * to "constructor classes". Two sygus constructors can be placed in the same + * constructor class if their constructor weight is equal, and the tuple + * of their argument types are the same. For example, for: + * A -> A+B | A-B | A*B | A+A | A | x + * The first three constructors above can be placed in the same constructor + * class, assuming they have identical weights. Constructor classes are used + * as an optimization when enumerating terms, since they expect the same + * tuple of argument terms for constructing a term of a fixed size. + * + * Constructor classes are allocated such that the constructor weights are + * in ascending order. This allows us to avoid constructors whose weight + * is greater than n while we are trying to enumerate terms of sizes strictly + * less than n. + * + * Constructor class 0 is reserved for nullary operators with weight 0. This + * is an optimization so that such constructors can be skipped for sizes + * greater than 0, since we know all terms generated by these constructors + * have size 0. + */ + class TermCache + { + public: + TermCache(); + /** initialize this cache */ + void initialize(Node e, + TypeNode tn, + TermDbSygus* tds, + SygusPbe* pbe = nullptr); + /** get last constructor class index for weight + * + * This returns a minimal index n such that all constructor classes at + * index < n have weight at most w. + */ + unsigned getLastConstructorClassIndexForWeight(unsigned w) const; + /** get num constructor classes */ + unsigned getNumConstructorClasses() const; + /** get the constructor indices for constructor class i */ + void getConstructorClass(unsigned i, std::vector<unsigned>& cclass) const; + /** get argument types for constructor class i */ + void getTypesForConstructorClass(unsigned i, + std::vector<TypeNode>& types) const; + /** get constructor weight for constructor class i */ + unsigned getWeightForConstructorClass(unsigned i) const; + + /** + * Add sygus term n to this cache, return true if the term was unique based + * on the redundancy criteria used by this class. + */ + bool addTerm(Node n); + /** + * Indicate to this cache that we are finished enumerating terms of the + * current size. + */ + void pushEnumSizeIndex(); + /** Get the current size of terms that we are enumerating */ + unsigned getEnumSize() const; + /** get the index at which size s terms start, where s <= getEnumSize() */ + unsigned getIndexForSize(unsigned s) const; + /** get the index^th term successfully added to this cache */ + Node getTerm(unsigned index) const; + /** get the number of terms successfully added to this cache */ + unsigned getNumTerms() const; + /** are we finished enumerating terms? */ + bool isComplete() const; + /** set that we are finished enumerating terms */ + void setComplete(); + + private: + /** the enumerator this cache is for */ + Node d_enum; + /** the sygus type of terms in this cache */ + TypeNode d_tn; + /** pointer to term database sygus */ + TermDbSygus* d_tds; + /** pointer to the PBE utility (used for symmetry breaking) */ + SygusPbe* d_pbe; + //-------------------------static information about type + /** is d_tn a sygus type? */ + bool d_isSygusType; + /** number of constructor classes */ + unsigned d_numConClasses; + /** Map from weights to the starting constructor class for that weight. */ + std::map<unsigned, unsigned> d_weightToCcIndex; + /** constructor classes */ + std::map<unsigned, std::vector<unsigned>> d_ccToCons; + /** maps constructor classes to children types */ + std::map<unsigned, std::vector<TypeNode>> d_ccToTypes; + /** maps constructor classes to constructor weight */ + std::map<unsigned, unsigned> d_ccToWeight; + /** constructor to indices */ + std::map<unsigned, std::vector<unsigned>> d_cToCIndices; + //-------------------------end static information about type + + /** the list of sygus terms we have enumerated */ + std::vector<Node> d_terms; + /** the set of builtin terms corresponding to the above list */ + std::unordered_set<Node, NodeHashFunction> d_bterms; + /** + * The index of first term whose size is greater than or equal to that size, + * if it exists. + */ + std::map<unsigned, unsigned> d_sizeStartIndex; + /** the maximum size of terms we have stored in this cache so far */ + unsigned d_sizeEnum; + /** whether this term cache is complete */ + bool d_isComplete; + }; + /** above cache for each sygus type */ + std::map<TypeNode, TermCache> d_tcache; + /** initialize term cache for type tn */ + void initializeTermCache(TypeNode tn); + + /** virtual class for term enumerators */ + class TermEnum + { + public: + TermEnum(); + virtual ~TermEnum() {} + /** get the current size of terms we are enumerating */ + unsigned getCurrentSize(); + /** get the current term of the enumerator */ + virtual Node getCurrent() = 0; + /** increment the enumerator, return false if the enumerator is finished */ + virtual bool increment() = 0; + + protected: + /** pointer to the sygus enumerator class */ + SygusEnumerator* d_se; + /** the (sygus) type of terms we are enumerating */ + TypeNode d_tn; + /** the current size of terms we are enumerating */ + unsigned d_currSize; + }; + class TermEnumMaster; + /** A "slave" enumerator + * + * A slave enumerator simply iterates over an index in a given term cache, + * and relies on a pointer to a "master" enumerator to generate new terms + * whenever necessary. + * + * This class maintains the following invariants, for tc=d_se->d_tcache[d_tn]: + * (1) d_index < tc.getNumTerms(), + * (2) d_currSize is the term size of tc.getTerm( d_index ), + * (3) d_hasIndexNextEnd is (d_currSize < tc.getEnumSize()), + * (4) If d_hasIndexNextEnd is true, then + * d_indexNextEnd = tc.getIndexForSize(d_currSize+1), and + * d_indexNextEnd > d_index. + * + * Intuitively, these invariants say (1) d_index is a valid index in the + * term cache, (2) d_currSize is the sygus term size of getCurrent(), (3) + * d_hasIndexNextEnd indicates whether d_indexNextEnd is valid, and (4) + * d_indexNextEnd is the index in the term cache where terms of the current + * size end, if such an index exists. + */ + class TermEnumSlave : public TermEnum + { + public: + TermEnumSlave(); + /** + * Initialize this enumerator to enumerate terms of type tn whose size is in + * the range [sizeMin, sizeMax], inclusive. If this function returns true, + * then getCurrent() will return the first term in the stream, which is + * non-empty. Further terms are generated by increment()/getCurrent(). + */ + bool initialize(SygusEnumerator* se, + TypeNode tn, + unsigned sizeMin, + unsigned sizeMax); + /** get the current term of the enumerator */ + Node getCurrent() override; + /** increment the enumerator */ + bool increment() override; + + private: + /** the maximum size of terms this enumerator should enumerate */ + unsigned d_sizeLim; + /** the current index in the term cache we are considering */ + unsigned d_index; + /** the index in the term cache where terms of the current size end */ + unsigned d_indexNextEnd; + /** whether d_indexNextEnd refers to a valid index */ + bool d_hasIndexNextEnd; + /** pointer to the master enumerator of type d_tn */ + TermEnum* d_master; + /** validate invariants on d_index, d_indexNextEnd, d_hasIndexNextEnd */ + bool validateIndex(); + /** validate invariants on d_indexNextEnd, d_hasIndexNextEnd */ + void validateIndexNextEnd(); + }; + /** Class for "master" enumerators + * + * This enumerator is used to generate new terms of a given type d_tn. It + * generates all terms of type d_tn that are not redundant based on the + * current criteria. + * + * To enumerate terms, this class performs the following steps as necessary + * during a call to increment(): + * - Fix the size of terms "d_currSize" we are currently enumerating, + * - Set the constructor class "d_consClassNum" whose constructors are the top + * symbol of the current term we are constructing. All constructors from this + * class have the same weight, which we store in d_ccWeight, + * - Initialize the current children "d_children" so that the sum of their + * current sizes is exactly (d_currSize - d_ccWeight), + * - Increment the current set of children until a new tuple of terms is + * considered, + * - Set the constructor "d_consNum" from within the constructor class, + * - Build the current term and check whether it is not redundant according + * to the term cache of its type. + * + * We say this enumerator is active if initialize(...) returns true, and the + * last call (if any) to increment returned true. + * + * This class maintains the following invariants, for tc=d_se->d_tcache[d_tn], + * if it is active: + * (1) getCurrent() is tc.getTerm(tc.getNumTerms()-1), + * (2) tc.pushEnumSizeIndex() has been called by this class exactly + * getCurrentSize() times. + * In other words, (1) getCurrent() is always the last term in the term cache + * of the type of this enumerator tc, and (2) the size counter of tc is in + * sync with the current size of this enumerator, that is, the master + * enumerator is responsible for communicating size boundaries to its term + * cache. + */ + class TermEnumMaster : public TermEnum + { + public: + TermEnumMaster(); + /** + * Initialize this enumerator to enumerate (all) terms of type tn, modulo + * the redundancy criteria used by this class. + */ + bool initialize(SygusEnumerator* se, TypeNode tn); + /** get the current term of the enumerator */ + Node getCurrent() override; + /** increment the enumerator + * + * Returns true if there are more terms to enumerate, in which case a + * subsequent call to getCurrent() returns the next enumerated term. This + * method returns false if the last call to increment() has yet to + * terminate. This can happen for recursive datatypes where a slave + * enumerator may request that this class increment the next term. We avoid + * an infinite loop by guarding this with the d_isIncrementing flag and + * return false. + */ + bool increment() override; + + private: + /** are we currently inside a increment() call? */ + bool d_isIncrementing; + /** cache for getCurrent() */ + Node d_currTerm; + //----------------------------- current constructor class information + /** the next constructor class we are using */ + unsigned d_consClassNum; + /** the constructors in the current constructor class */ + std::vector<unsigned> d_ccCons; + /** the types of the current constructor class */ + std::vector<TypeNode> d_ccTypes; + /** the operator weight for the constructor class */ + unsigned d_ccWeight; + //----------------------------- end current constructor class information + /** If >0, 1 + the index in d_ccCons we are considering */ + unsigned d_consNum; + /** the child enumerators for this enumerator */ + std::map<unsigned, TermEnumSlave> d_children; + /** the current sum of current sizes of the enumerators in d_children */ + unsigned d_currChildSize; + /** + * The number of indices, starting from zero, in d_children that point to + * initialized slave enumerators. + */ + 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 + * 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. + */ + bool initializeChildren(); + /** initialize child + * + * Initialize child i to enumerate terms whose size is at least sizeMin, + * and whose maximum size is the largest size such that we can still + * construct terms for the given constructor class and the current children + * whose size is not more than the current size d_currSize. Additionally, + * if i is the last child, we modify sizeMin such that it is exactly the + * size of terms needed for the children to sum up to size d_currSize. + */ + bool initializeChild(unsigned i, unsigned sizeMin); + /** increment internal, helper for increment() */ + bool incrementInternal(); + }; + /** an interpreted value enumerator + * + * This enumerator uses the builtin type enumerator for a given type. It + * is used to fill in concrete holes into "any constant" constructors + * when sygus-repair-const is not enabled. The number of terms of size n + * is m^n, where m is configurable via --sygus-active-gen-enum-cfactor=m. + */ + class TermEnumMasterInterp : public TermEnum + { + public: + TermEnumMasterInterp(TypeNode tn); + /** initialize this enumerator */ + bool initialize(SygusEnumerator* se, TypeNode tn); + /** get the current term of the enumerator */ + Node getCurrent() override; + /** increment the enumerator */ + bool increment() override; + + private: + /** the type enumerator */ + TypeEnumerator d_te; + /** the current number of terms we are enumerating for the given size */ + unsigned d_currNumConsts; + /** the next end threshold */ + unsigned d_nextIndexEnd; + }; + /** a free variable enumerator + * + * This enumerator enumerates canonical free variables for a given type. + * The n^th variable in this stream is assigned size n. This enumerator is + * used in conjunction with sygus-repair-const to generate solutions with + * constant holes. In this approach, free variables are arguments to + * any-constant constructors. This is required so that terms with holes are + * unique up to rewriting when appropriate. + */ + class TermEnumMasterFv : public TermEnum + { + public: + TermEnumMasterFv(); + /** initialize this enumerator */ + bool initialize(SygusEnumerator* se, TypeNode tn); + /** get the current term of the enumerator */ + Node getCurrent() override; + /** increment the enumerator */ + bool increment() override; + }; + /** the master enumerator for each sygus type */ + std::map<TypeNode, TermEnumMaster> d_masterEnum; + /** the master enumerator for each non-sygus type */ + std::map<TypeNode, TermEnumMasterFv> d_masterEnumFv; + /** the master enumerator for each non-sygus type */ + std::map<TypeNode, std::unique_ptr<TermEnumMasterInterp>> d_masterEnumInt; + /** the sygus enumerator this class is for */ + Node d_enum; + /** the type of d_enum */ + TypeNode d_etype; + /** pointer to the master enumerator of type d_etype */ + TermEnum* d_tlEnum; + /** the abort size, caches the value of --sygus-abort-size */ + int d_abortSize; + /** this flag is true for the first time to getNext() after initialize(e) */ + bool d_firstTime; + /** get master enumerator for type tn */ + TermEnum* getMasterEnumForType(TypeNode tn); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index ac8b56ee4..b49c29c53 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -356,10 +356,10 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr) { Assert(isPbe()); Assert(!e.isNull()); - if (!d_tds->isPassiveEnumerator(e)) + if (d_tds->isVariableAgnosticEnumerator(e)) { - // we cannot apply conjecture-specific symmetry breaking on enumerators that - // are not passive + // we cannot apply conjecture-specific symmetry breaking on variable + // agnostic enumerators return Node::null(); } Node ee = d_tds->getSynthFunForEnumerator(e); diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index bd9274f91..78892aac8 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -564,13 +564,15 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) std::vector<Node> exp_exc_vec; Assert(d_tds->isEnumerator(e)); bool isPassive = d_tds->isPassiveEnumerator(e); - if (isPassive - && getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec)) + if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec)) { - Assert(!exp_exc_vec.empty()); - exp_exc = exp_exc_vec.size() == 1 - ? exp_exc_vec[0] - : NodeManager::currentNM()->mkNode(AND, exp_exc_vec); + if (isPassive) + { + Assert(!exp_exc_vec.empty()); + exp_exc = exp_exc_vec.size() == 1 + ? exp_exc_vec[0] + : NodeManager::currentNM()->mkNode(AND, exp_exc_vec); + } Trace("sygus-sui-enum") << " ...fail : term is excluded (domain-specific)" << std::endl; } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index b95af719e..21079aedc 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -28,6 +28,7 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/enum_stream_substitution.h" +#include "theory/quantifiers/sygus/sygus_enumerator.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -759,7 +760,17 @@ Node SynthConjecture::getEnumeratedValue(Node e) } else { - d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); + // Actively-generated enumerators are currently either variable agnostic + // or basic. + Assert(d_tds->isBasicEnumerator(e)); + if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM) + { + d_evg[e].reset(new SygusEnumerator(d_tds, this)); + } + else + { + d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); + } } Trace("sygus-active-gen") << "Active-gen: initialize for " << e << std::endl; @@ -800,12 +811,18 @@ Node SynthConjecture::getEnumeratedValue(Node e) // No more concrete values generated from absE. NodeManager* nm = NodeManager::currentNM(); d_ev_curr_active_gen[e] = Node::null(); - // We must block e = absE. std::vector<Node> exp; - d_tds->getExplain()->getExplanationForEquality(e, absE, exp); - for (unsigned i = 0, size = exp.size(); i < size; i++) + // If we are a basic enumerator, a single abstract value maps to *all* + // concrete values of its type, thus we don't depend on the current + // solution. + if (!d_tds->isBasicEnumerator(e)) { - exp[i] = exp[i].negate(); + // We must block e = absE + d_tds->getExplain()->getExplanationForEquality(e, absE, exp); + for (unsigned i = 0, size = exp.size(); i < size; i++) + { + exp[i] = exp[i].negate(); + } } Node g = d_tds->getActiveGuardForEnumerator(e); if (!g.isNull()) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index d5b7bc51c..435e1a00f 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -31,6 +31,33 @@ namespace CVC4 { namespace theory { namespace quantifiers { +void TypeNodeIdTrie::add(Node v, std::vector<TypeNode>& types) +{ + TypeNodeIdTrie* tnt = this; + for (unsigned i = 0, size = types.size(); i < size; i++) + { + tnt = &tnt->d_children[types[i]]; + } + tnt->d_data.push_back(v); +} + +void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign, + unsigned& idCount) +{ + if (!d_data.empty()) + { + for (const Node& v : d_data) + { + assign[v] = idCount; + } + idCount++; + } + for (std::pair<const TypeNode, TypeNodeIdTrie>& c : d_children) + { + c.second.assignIds(assign, idCount); + } +} + TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe) : d_quantEngine(qe), d_syexp(new SygusExplain(this)), @@ -424,45 +451,6 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { } } -/** A trie indexed by types that assigns unique identifiers to nodes. */ -class TypeNodeIdTrie -{ - public: - /** children of this node */ - std::map<TypeNode, TypeNodeIdTrie> d_children; - /** the data stored at this node */ - std::vector<Node> d_data; - /** add v to this trie, indexed by types */ - void add(Node v, std::vector<TypeNode>& types) - { - TypeNodeIdTrie* tnt = this; - for (unsigned i = 0, size = types.size(); i < size; i++) - { - tnt = &tnt->d_children[types[i]]; - } - tnt->d_data.push_back(v); - } - /** - * Assign each node in this trie an identifier such that - * assign[v1] = assign[v2] iff v1 and v2 are indexed by the same values. - */ - void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount) - { - if (!d_data.empty()) - { - for (const Node& v : d_data) - { - assign[v] = idCount; - } - idCount++; - } - for (std::pair<const TypeNode, TypeNodeIdTrie>& c : d_children) - { - c.second.assignIds(assign, idCount); - } - } -}; - void TermDbSygus::registerEnumerator(Node e, Node f, SynthConjecture* conj, @@ -566,7 +554,8 @@ void TermDbSygus::registerEnumerator(Node e, } Trace("sygus-db") << " ...finished" << std::endl; - d_enum_active_gen[e] = isActiveGen; + // Currently, actively-generated enumerators are either basic or variable + // agnostic. bool isVarAgnostic = isActiveGen && options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_VAR_AGNOSTIC; @@ -613,8 +602,11 @@ void TermDbSygus::registerEnumerator(Node e, << " since it has no subclass with more than one variable." << std::endl; d_enum_var_agnostic[e] = false; + isActiveGen = false; } } + d_enum_active_gen[e] = isActiveGen; + d_enum_basic[e] = isActiveGen && !isVarAgnostic; } bool TermDbSygus::isEnumerator(Node e) const @@ -671,6 +663,16 @@ bool TermDbSygus::isVariableAgnosticEnumerator(Node e) const return false; } +bool TermDbSygus::isBasicEnumerator(Node e) const +{ + std::map<Node, bool>::const_iterator itus = d_enum_basic.find(e); + if (itus != d_enum_basic.end()) + { + return itus->second; + } + return false; +} + bool TermDbSygus::isPassiveEnumerator(Node e) const { std::map<Node, bool>::const_iterator itus = d_enum_active_gen.find(e); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 56ed68e76..713e322a4 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -31,6 +31,23 @@ namespace quantifiers { class SynthConjecture; +/** A trie indexed by types that assigns unique identifiers to nodes. */ +class TypeNodeIdTrie +{ + public: + /** children of this node */ + std::map<TypeNode, TypeNodeIdTrie> d_children; + /** the data stored at this node */ + std::vector<Node> d_data; + /** add v to this trie, indexed by types */ + void add(Node v, std::vector<TypeNode>& types); + /** + * Assign each node in this trie an identifier such that + * assign[v1] = assign[v2] iff v1 and v2 are indexed by the same values. + */ + void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount); +}; + // TODO :issue #1235 split and document this class class TermDbSygus { public: @@ -98,6 +115,13 @@ class TermDbSygus { bool usingSymbolicConsForEnumerator(Node e) const; /** is this enumerator agnostic to variables? */ bool isVariableAgnosticEnumerator(Node e) const; + /** is this enumerator a "basic" enumerator. + * + * A basic enumerator is one that does not rely on the sygus extension of the + * datatypes solver. Basic enumerators enumerate all concrete terms for their + * type for a single abstract value. + */ + bool isBasicEnumerator(Node e) const; /** is this a "passively-generated" enumerator? * * A "passively-generated" enumerator is one for which the terms it enumerates @@ -304,6 +328,8 @@ class TermDbSygus { std::map<Node, bool> d_enum_active_gen; /** enumerators to whether they are variable agnostic */ std::map<Node, bool> d_enum_var_agnostic; + /** enumerators to whether they are basic */ + std::map<Node, bool> d_enum_basic; //------------------------------end enumerators //-----------------------------conversion from sygus to builtin |