diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/enum_stream_substitution.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/enum_stream_substitution.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.cpp | 183 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.h | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 378 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 88 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 26 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 128 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 61 |
13 files changed, 644 insertions, 324 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 79bec60ee..6aca71ca3 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -69,17 +69,10 @@ bool Cegis::processInitialize(Node n, { Trace("cegis") << "Initialize cegis..." << std::endl; unsigned csize = candidates.size(); - // We only can use actively-generated enumerators if there is only one - // function-to-synthesize. Otherwise, we would have to generate a "product" of - // two actively-generated enumerators. That is, given a conjecture with two - // functions-to-synthesize with enumerators e_f and e_g, if: - // e_f -> t1, ..., tn - // e_g -> s1, ..., sm - // This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj) - // for each i,j. We do not do this and revert to the default behavior of - // this module instead. - bool isActiveGen = - options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1; + // The role of enumerators is to be either the single solution or part of + // a solution involving multiple enumerators. + EnumeratorRole erole = + csize == 1 ? ROLE_ENUM_SINGLE_SOLUTION : ROLE_ENUM_MULTI_SOLUTION; // initialize an enumerator for each candidate for (unsigned i = 0; i < csize; i++) { @@ -98,13 +91,8 @@ bool Cegis::processInitialize(Node n, } } Trace("cegis") << std::endl; - // variable agnostic enumerators require an active guard - d_tds->registerEnumerator(candidates[i], - candidates[i], - d_parent, - isActiveGen, - do_repair_const, - isActiveGen); + d_tds->registerEnumerator( + candidates[i], candidates[i], d_parent, erole, do_repair_const); } return true; } diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index dbde79aae..18e313bf0 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -44,7 +44,12 @@ bool CegisUnif::processInitialize(Node n, std::map<Node, Node> pt_to_cond; // strategy lemmas for each strategy point std::map<Node, std::vector<Node>> strategy_lemmas; - // Initialize strategies for all functions-to-synhesize + // Initialize strategies for all functions-to-synthesize + // The role of non-unification enumerators is to be either the single solution + // or part of a solution involving multiple enumerators. + EnumeratorRole eroleNonUnif = candidates.size() == 1 + ? ROLE_ENUM_SINGLE_SOLUTION + : ROLE_ENUM_MULTI_SOLUTION; for (const Node& f : candidates) { // Init UNIF util for this candidate @@ -53,7 +58,7 @@ bool CegisUnif::processInitialize(Node n, if (!d_sygus_unif.usingUnif(f)) { Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl; - d_tds->registerEnumerator(f, f, d_parent); + d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif); d_non_unif_candidates.push_back(f); } else @@ -462,7 +467,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) exclude_cons, term_irrelevant); d_virtual_enum = nm->mkSkolem("_ve", vtn); - d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent); + d_tds->registerEnumerator( + d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED); } // if new_size is a power of two, then isPow2 returns log2(new_size)+1 // otherwise, this returns 0. In the case it returns 0, we don't care @@ -606,20 +612,17 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, } // register the enumerator si.d_enums[index].push_back(e); - bool mkActiveGuard = false; - bool isActiveGen = false; + EnumeratorRole erole = ROLE_ENUM_CONSTRAINED; // if we are using a single independent enumerator for conditions, then we // allocate an active guard, and are eligible to use variable-agnostic // enumeration. if (options::sygusUnifCondIndependent() && index == 1) { - mkActiveGuard = true; - isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; + erole = ROLE_ENUM_POOL; } Trace("cegis-unif-enum") << "* Registering new enumerator " << e << " to strategy point " << si.d_pt << "\n"; - d_tds->registerEnumerator( - e, si.d_pt, d_parent, mkActiveGuard, false, isActiveGen); + d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, false); } void CegisUnifEnumDecisionStrategy::registerEvalPts( diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 24770ade0..e8daa4256 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -608,8 +608,17 @@ bool EnumStreamSubstitution::CombinationState::getNextCombination() } void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); } -void EnumStreamConcrete::addValue(Node v) { d_ess.resetValue(v); } -Node EnumStreamConcrete::getNext() { return d_ess.getNext(); } +void EnumStreamConcrete::addValue(Node v) +{ + d_ess.resetValue(v); + d_currTerm = d_ess.getNext(); +} +bool EnumStreamConcrete::increment() +{ + d_currTerm = d_ess.getNext(); + return !d_currTerm.isNull(); +} +Node EnumStreamConcrete::getCurrent() { return d_currTerm; } } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 38fa0627b..476a364ea 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -286,12 +286,16 @@ class EnumStreamConcrete : public EnumValGenerator void initialize(Node e) override; /** get that value v was enumerated */ void addValue(Node v) override; - /** get the next value enumerated by this class */ - Node getNext() override; + /** increment */ + bool increment() override; + /** get the current value enumerated by this class */ + Node getCurrent() override; private: /** stream substitution utility */ EnumStreamSubstitution d_ess; + /** the current term generated by this class */ + Node d_currTerm; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 61ab9007a..5c3e44a33 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -25,21 +25,78 @@ 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) + : d_tds(tds), d_parent(p), d_tlEnum(nullptr), d_abortSize(-1) { } void SygusEnumerator::initialize(Node e) { + Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl; d_enum = e; d_etype = d_enum.getType(); + Assert(d_etype.isDatatype()); + Assert(d_etype.getDatatype().isSygus()); d_tlEnum = getMasterEnumForType(d_etype); d_abortSize = options::sygusAbortSize(); - d_firstTime = true; + + // Get the statically registered symmetry breaking clauses for e, see if they + // can be used for speeding up the enumeration. + NodeManager* nm = NodeManager::currentNM(); + std::vector<Node> sbl; + d_tds->getSymBreakLemmas(e, sbl); + Node ag = d_tds->getActiveGuardForEnumerator(e); + Node truen = nm->mkConst(true); + // use TNode for substitute below + TNode agt = ag; + TNode truent = truen; + Assert(d_tcache.find(d_etype) != d_tcache.end()); + const Datatype& dt = d_etype.getDatatype(); + for (const Node& lem : sbl) + { + if (!d_tds->isSymBreakLemmaTemplate(lem)) + { + // substitute its active guard by true and rewrite + Node slem = lem.substitute(agt, truent); + slem = Rewriter::rewrite(slem); + // break into conjuncts + std::vector<Node> sblc; + if (slem.getKind() == AND) + { + for (const Node& slemc : slem) + { + sblc.push_back(slemc); + } + } + else + { + sblc.push_back(slem); + } + for (const Node& sbl : sblc) + { + Trace("sygus-enum") + << " symmetry breaking lemma : " << sbl << std::endl; + // if its a negation of a unit top-level tester, then this specifies + // that we should not enumerate terms whose top symbol is that + // constructor + if (sbl.getKind() == NOT) + { + Node a; + int tst = datatypes::DatatypesRewriter::isTester(sbl[0], a); + if (tst >= 0) + { + if (a == e) + { + Node cons = Node::fromExpr(dt[tst].getConstructor()); + Trace("sygus-enum") << " ...unit exclude constructor #" << tst + << ", constructor " << cons << std::endl; + d_sbExcTlCons.insert(cons); + } + } + } + // other symmetry breaking lemmas such as disjunctions are not used + } + } + } } void SygusEnumerator::addValue(Node v) @@ -47,17 +104,9 @@ void SygusEnumerator::addValue(Node v) // do nothing } -Node SygusEnumerator::getNext() +bool SygusEnumerator::increment() { return d_tlEnum->increment(); } +Node SygusEnumerator::getCurrent() { - 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()); @@ -70,14 +119,30 @@ Node SygusEnumerator::getNext() } } Node ret = d_tlEnum->getCurrent(); - Trace("sygus-enum") << "Enumerate : " << d_tds->sygusToBuiltin(ret) - << std::endl; + if (!ret.isNull() && !d_sbExcTlCons.empty()) + { + Assert(ret.hasOperator()); + // might be excluded by an externally provided symmetry breaking clause + if (d_sbExcTlCons.find(ret.getOperator()) != d_sbExcTlCons.end()) + { + Trace("sygus-enum-exc") + << "Exclude (external) : " << d_tds->sygusToBuiltin(ret) << std::endl; + ret = Node::null(); + } + } + if (Trace.isOn("sygus-enum")) + { + Trace("sygus-enum") << "Enumerate : "; + TermDbSygus::toStreamSygus("sygus-enum", ret); + Trace("sygus-enum") << std::endl; + } return ret; } SygusEnumerator::TermCache::TermCache() : d_tds(nullptr), d_pbe(nullptr), + d_isSygusType(false), d_numConClasses(0), d_sizeEnum(0), d_isComplete(false) @@ -241,33 +306,37 @@ bool SygusEnumerator::TermCache::addTerm(Node n) 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) + Assert(!n.isNull()); + if (options::sygusSymBreakDynamic()) { - // Is it equivalent under examples? - Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr); - if (!bne.isNull()) + 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()) { - if (bnr != bne) + 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()) { - Trace("sygus-enum-exc") << "Exclude (by examples): " << bn - << ", since we already have " << bne - << "!=" << bnr << std::endl; - return false; + 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_bterms.insert(bnr); } - 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() @@ -302,7 +371,12 @@ 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) + : TermEnum(), + d_sizeLim(0), + d_index(0), + d_indexNextEnd(0), + d_hasIndexNextEnd(false), + d_master(nullptr) { } @@ -384,7 +458,7 @@ 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()) + while (d_index >= tc.getNumTerms()) { Assert(d_index == tc.getNumTerms()); Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n"; @@ -494,6 +568,7 @@ SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) SygusEnumerator::TermEnumMaster::TermEnumMaster() : TermEnum(), d_isIncrementing(false), + d_currTermSet(false), d_consClassNum(0), d_ccWeight(0), d_consNum(0), @@ -515,6 +590,7 @@ bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se, d_currChildSize = 0; d_ccCons.clear(); d_isIncrementing = false; + d_currTermSet = false; bool ret = increment(); Trace("sygus-enum-debug") << "master(" << tn << "): finish init, ret = " << ret << "\n"; @@ -523,10 +599,11 @@ bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se, Node SygusEnumerator::TermEnumMaster::getCurrent() { - if (!d_currTerm.isNull()) + if (d_currTermSet) { return d_currTerm; } + d_currTermSet = true; // construct based on the children std::vector<Node> children; const Datatype& dt = d_tn.getDatatype(); @@ -538,7 +615,13 @@ Node SygusEnumerator::TermEnumMaster::getCurrent() 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()); + Node cc = d_children[i].getCurrent(); + if (cc.isNull()) + { + d_currTerm = cc; + return cc; + } + children.push_back(cc); } d_currTerm = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children); return d_currTerm; @@ -705,21 +788,27 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() Assert(d_childrenValid == d_ccTypes.size()); // do we have more constructors for the given children? - while (d_consNum < d_ccCons.size()) + if (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_currTermSet = false; d_currTerm = Node::null(); Node c = getCurrent(); - if (tc.addTerm(c)) + if (!c.isNull()) { - return true; + if (!tc.addTerm(c)) + { + // the term was not unique based on rewriting + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): failed addTerm\n"; + d_currTerm = Node::null(); + } } - Trace("sygus-enum-debug2") << "master(" << d_tn << "): failed addTerm\n"; - // the term was not unique based on rewriting + return true; } // finished constructors for this set of children, must increment children diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 10a44da03..af6bb03f0 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -50,8 +50,10 @@ class SygusEnumerator : public EnumValGenerator void initialize(Node e) override; /** Inform this generator that abstract value v was enumerated. */ void addValue(Node v) override; + /** increment */ + bool increment() override; /** Get the next concrete value generated by this class. */ - Node getNext() override; + Node getCurrent() override; private: /** pointer to term database sygus */ @@ -322,6 +324,8 @@ class SygusEnumerator : public EnumValGenerator bool d_isIncrementing; /** cache for getCurrent() */ Node d_currTerm; + /** is d_currTerm set */ + bool d_currTermSet; //----------------------------- current constructor class information /** the next constructor class we are using */ unsigned d_consClassNum; @@ -429,10 +433,17 @@ class SygusEnumerator : public EnumValGenerator 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); + //-------------------------------- externally specified symmetry breaking + /** set of constructors we disallow at top level + * + * A constructor C is disallowed at the top level if a symmetry breaking + * lemma that entails ~is-C( d_enum ) was registered to + * TermDbSygus::registerSymBreakLemma. + */ + std::unordered_set<Node, NodeHashFunction> d_sbExcTlCons; + //-------------------------------- end externally specified symmetry breaking }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 47c701cf6..d6dfb3d26 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -374,18 +374,24 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, // TODO #1178 : add other missing types } -void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ){ +void CegGrammarConstructor::collectSygusGrammarTypesFor( + TypeNode range, std::vector<TypeNode>& types) +{ if( !range.isBoolean() ){ if( std::find( types.begin(), types.end(), range )==types.end() ){ Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl; types.push_back( range ); if( range.isDatatype() ){ - const Datatype& dt = ((DatatypeType)range.toType()).getDatatype(); - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ - TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() ); - sels[crange].push_back( dt[i][j] ); - collectSygusGrammarTypesFor( crange, types, sels ); + const Datatype& dt = range.getDatatype(); + for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i) + { + for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args; + ++j) + { + collectSygusGrammarTypesFor( + TypeNode::fromType(static_cast<SelectorType>(dt[i][j].getType()) + .getRangeType()), + types); } } } @@ -408,76 +414,87 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( << range << std::endl; // collect the variables std::vector<Node> sygus_vars; - if( !bvl.isNull() ){ - for( unsigned i=0; i<bvl.getNumChildren(); i++ ){ + if (!bvl.isNull()) + { + for (unsigned i = 0, size = bvl.getNumChildren(); i < size; ++i) + { if (term_irrelevant.find(bvl[i]) == term_irrelevant.end()) { sygus_vars.push_back(bvl[i]); } else { - Trace("sygus-grammar-def") << "...synth var " << bvl[i] - << " has been marked irrelevant." - << std::endl; + Trace("sygus-grammar-def") + << "...synth var " << bvl[i] << " has been marked irrelevant." + << std::endl; } } } - //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){ - // parseError("No default grammar for type."); - //} - std::vector< std::vector< Expr > > ops; + // operators for each constructor in type + std::vector<std::vector<Expr>> ops; + // names for the operators + std::vector<std::vector<std::string>> cnames; + // argument types of operators + std::vector<std::vector<std::vector<Type>>> cargs; + // set of callbacks for each constructor + std::vector<std::vector<std::shared_ptr<SygusPrintCallback>>> pcs; + // weights for each constructor + std::vector<std::vector<int>> weights; + // index of top datatype, i.e. the datatype for the range type int startIndex = -1; std::map< Type, Type > sygus_to_builtin; - std::vector< TypeNode > types; - std::map< TypeNode, std::vector< DatatypeConstructorArg > > sels; - //types for each of the variables of parametric sort - for( unsigned i=0; i<sygus_vars.size(); i++ ){ - collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels ); + std::vector<TypeNode> types; + // collect connected types for each of the variables + for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i) + { + collectSygusGrammarTypesFor(sygus_vars[i].getType(), types); } - //types connected to range - collectSygusGrammarTypesFor( range, types, sels ); + // collect connected types to range + collectSygusGrammarTypesFor(range, types); - //name of boolean sort + // create placeholder for boolean type (kept apart since not collected) std::stringstream ssb; ssb << fun << "_Bool"; std::string dbname = ssb.str(); Type unres_bt = mkUnresolvedType(ssb.str(), unres).toType(); + // create placeholders for collected types std::vector< Type > unres_types; std::map< TypeNode, Type > type_to_unres; - for( unsigned i=0; i<types.size(); i++ ){ + for (unsigned i = 0, size = types.size(); i < size; ++i) + { std::stringstream ss; ss << fun << "_" << types[i]; std::string dname = ss.str(); datatypes.push_back(Datatype(dname)); ops.push_back(std::vector< Expr >()); + cnames.push_back(std::vector<std::string>()); + cargs.push_back(std::vector<std::vector<Type>>()); + pcs.push_back(std::vector<std::shared_ptr<SygusPrintCallback>>()); + weights.push_back(std::vector<int>()); //make unresolved type Type unres_t = mkUnresolvedType(dname, unres).toType(); unres_types.push_back(unres_t); type_to_unres[types[i]] = unres_t; sygus_to_builtin[unres_t] = types[i].toType(); } - for( unsigned i=0; i<types.size(); i++ ){ + for (unsigned i = 0, size = types.size(); i < size; ++i) + { Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl; - std::vector<std::string> cnames; - std::vector<std::vector<CVC4::Type> > cargs; - /* Print callbacks for each constructor */ - std::vector<std::shared_ptr<SygusPrintCallback>> pcs; - /* Weights for each constructor */ - std::vector<int> weights; Type unres_t = unres_types[i]; //add variables - for( unsigned j=0; j<sygus_vars.size(); j++ ){ + for (unsigned j = 0, size_j = sygus_vars.size(); j < size_j; ++j) + { if( sygus_vars[j].getType()==types[i] ){ std::stringstream ss; ss << sygus_vars[j]; Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl; ops[i].push_back( sygus_vars[j].toExpr() ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(ss.str()); + cargs[i].push_back(std::vector<Type>()); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } } //add constants @@ -486,33 +503,35 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::map< TypeNode, std::vector< Node > >::iterator itec = extra_cons.find( types[i] ); if( itec!=extra_cons.end() ){ //consts.insert( consts.end(), itec->second.begin(), itec->second.end() ); - for( unsigned j=0; j<itec->second.size(); j++ ){ + for (unsigned j = 0, size_j = itec->second.size(); j < size_j; ++j) + { if( std::find( consts.begin(), consts.end(), itec->second[j] )==consts.end() ){ consts.push_back( itec->second[j] ); } } } - for( unsigned j=0; j<consts.size(); j++ ){ + for (unsigned j = 0, size_j = consts.size(); j < size_j; ++j) + { std::stringstream ss; ss << consts[j]; Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl; ops[i].push_back( consts[j].toExpr() ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(ss.str()); + cargs[i].push_back(std::vector<Type>()); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } - //ITE - CVC4::Kind k = kind::ITE; + // ITE + Kind k = ITE; Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames.push_back( kind::kindToString(k) ); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_bt); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_t); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(kindToString(k)); + cargs[i].push_back(std::vector<Type>()); + cargs[i].back().push_back(unres_bt); + cargs[i].back().push_back(unres_t); + cargs[i].back().push_back(unres_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); if (types[i].isReal()) { @@ -521,16 +540,17 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Kind k = j == 0 ? PLUS : MINUS; Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kind::kindToString(k)); - cargs.push_back(std::vector<CVC4::Type>()); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_t); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(kindToString(k)); + cargs[i].push_back(std::vector<Type>()); + cargs[i].back().push_back(unres_t); + cargs[i].back().push_back(unres_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } if (!types[i].isInteger()) { - Trace("sygus-grammar-def") << "...Dedicate to Real\n"; + Trace("sygus-grammar-def") + << " ...create auxiliary Positive Integers grammar\n"; /* Creating type for positive integers */ std::stringstream ss; ss << fun << "_PosInt"; @@ -546,7 +566,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( /* Add operator 1 */ Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n"; ops_pos_int.push_back(nm->mkConst(Rational(1)).toExpr()); - ss << "_1"; + ss.str(""); + ss << "1"; cnames_pos_int.push_back(ss.str()); cargs_pos_int.push_back(std::vector<Type>()); /* Add operator PLUS */ @@ -558,23 +579,23 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargs_pos_int.back().push_back(unres_pos_int_t); cargs_pos_int.back().push_back(unres_pos_int_t); datatypes.back().setSygus(types[i].toType(), bvl.toExpr(), true, true); - for (unsigned j = 0; j < ops_pos_int.size(); j++) + for (unsigned j = 0, size_j = ops_pos_int.size(); j < size_j; ++j) { datatypes.back().addSygusConstructor( ops_pos_int[j], cnames_pos_int[j], cargs_pos_int[j]); } Trace("sygus-grammar-def") - << "...built datatype " << datatypes.back() << " "; + << " ...built datatype " << datatypes.back() << " "; /* Adding division at root */ k = DIVISION; Trace("sygus-grammar-def") << "\t...add for " << k << std::endl; ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kindToString(k)); - cargs.push_back(std::vector<Type>()); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_pos_int_t); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(kindToString(k)); + cargs[i].push_back(std::vector<Type>()); + cargs[i].back().push_back(unres_t); + cargs[i].back().push_back(unres_pos_int_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } } else if (types[i].isBitVector()) @@ -585,11 +606,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kindToString(k)); - cargs.push_back(std::vector<Type>()); - cargs.back().push_back(unres_t); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(kindToString(k)); + cargs[i].push_back(std::vector<Type>()); + cargs[i].back().push_back(unres_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } // binary apps std::vector<Kind> bin_kinds = {BITVECTOR_AND, @@ -609,56 +630,65 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kindToString(k)); - cargs.push_back(std::vector<Type>()); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_t); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(kindToString(k)); + cargs[i].push_back(std::vector<Type>()); + cargs[i].back().push_back(unres_t); + cargs[i].back().push_back(unres_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } } else if (types[i].isDatatype()) { Trace("sygus-grammar-def") << "...add for constructors" << std::endl; - const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype(); - for( unsigned k=0; k<dt.getNumConstructors(); k++ ){ + const Datatype& dt = types[i].getDatatype(); + for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) + { Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl; ops[i].push_back( dt[k].getConstructor() ); - cnames.push_back( dt[k].getName() ); - cargs.push_back( std::vector< CVC4::Type >() ); - for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){ - TypeNode crange = TypeNode::fromType( ((SelectorType)dt[k][j].getType()).getRangeType() ); - //Assert( type_to_unres.find(crange)!=type_to_unres.end() ); - cargs.back().push_back( type_to_unres[crange] ); + cnames[i].push_back(dt[k].getName()); + cargs[i].push_back(std::vector<Type>()); + Trace("sygus-grammar-def") << "...add for selectors" << std::endl; + for (unsigned j = 0, size_j = dt[k].getNumArgs(); j < size_j; ++j) + { + Trace("sygus-grammar-def") + << "...for " << dt[k][j].getName() << std::endl; + TypeNode crange = TypeNode::fromType( + static_cast<SelectorType>(dt[k][j].getType()).getRangeType()); + Assert(type_to_unres.find(crange) != type_to_unres.end()); + cargs[i].back().push_back(type_to_unres[crange]); + // add to the selector type the selector operator + + Assert(std::find(types.begin(), types.end(), crange) != types.end()); + unsigned i_selType = std::distance( + types.begin(), std::find(types.begin(), types.end(), crange)); + TypeNode arg_type = TypeNode::fromType( + static_cast<SelectorType>(dt[k][j].getType()).getDomain()); + ops[i_selType].push_back(dt[k][j].getSelector()); + cnames[i_selType].push_back(dt[k][j].getName()); + cargs[i_selType].push_back(std::vector<Type>()); + Assert(type_to_unres.find(arg_type) != type_to_unres.end()); + cargs[i_selType].back().push_back(type_to_unres[arg_type]); + pcs[i_selType].push_back(nullptr); + weights[i_selType].push_back(-1); } - pcs.push_back(nullptr); - weights.push_back(-1); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } }else{ std::stringstream sserr; sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl; throw LogicException(sserr.str()); } - //add for all selectors to this type - if( !sels[types[i]].empty() ){ - Trace("sygus-grammar-def") << "...add for selectors" << std::endl; - for( unsigned j=0; j<sels[types[i]].size(); j++ ){ - Trace("sygus-grammar-def") << "...for " << sels[types[i]][j].getName() << std::endl; - TypeNode arg_type = TypeNode::fromType( ((SelectorType)sels[types[i]][j].getType()).getDomain() ); - ops[i].push_back( sels[types[i]][j].getSelector() ); - cnames.push_back( sels[types[i]][j].getName() ); - cargs.push_back( std::vector< CVC4::Type >() ); - //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() ); - cargs.back().push_back( type_to_unres[arg_type] ); - pcs.push_back(nullptr); - weights.push_back(-1); - } - } + } + // make datatypes + for (unsigned i = 0, size = types.size(); i < size; ++i) + { Trace("sygus-grammar-def") << "...make datatype " << datatypes[i] << std::endl; datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true ); std::map<TypeNode, std::vector<Node>>::iterator itexc = exc_cons.find(types[i]); - for (unsigned j = 0, size = ops[i].size(); j < size; j++) + for (unsigned j = 0, size = ops[i].size(); j < size; ++j) { // add the constructor if it is not excluded Node opn = Node::fromExpr(ops[i][j]); @@ -667,12 +697,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( == itexc->second.end()) { datatypes[i].addSygusConstructor( - ops[i][j], cnames[j], cargs[j], pcs[j], weights[j]); + ops[i][j], cnames[i][j], cargs[i][j], pcs[i][j], weights[i][j]); } } - Trace("sygus-grammar-def") - << "...built datatype " << datatypes[i] << " "; - //sorts.push_back( types[i] ); + Trace("sygus-grammar-def") << "...built datatype " << datatypes[i] << " "; //set start index if applicable if( types[i]==range ){ startIndex = i; @@ -683,94 +711,96 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode btype = nm->booleanType(); datatypes.push_back(Datatype(dbname)); ops.push_back(std::vector<Expr>()); - std::vector<std::string> cnames; - std::vector<std::vector< Type > > cargs; - /* Print callbacks for each constructor */ - std::vector<std::shared_ptr<SygusPrintCallback>> pcs; - /* Weights for each constructor */ - std::vector<int> weights; + cnames.push_back(std::vector<std::string>()); + cargs.push_back(std::vector<std::vector<Type>>()); + pcs.push_back(std::vector<std::shared_ptr<SygusPrintCallback>>()); + weights.push_back(std::vector<int>()); Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl; //add variables - for( unsigned i=0; i<sygus_vars.size(); i++ ){ + for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i) + { if( sygus_vars[i].getType().isBoolean() ){ std::stringstream ss; ss << sygus_vars[i]; Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl; ops.back().push_back( sygus_vars[i].toExpr() ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - pcs.push_back(nullptr); - weights.push_back(1); + cnames.back().push_back(ss.str()); + cargs.back().push_back(std::vector<Type>()); + pcs.back().push_back(nullptr); + // make boolean variables weight as non-nullary constructors + weights.back().push_back(1); } } - //add constants + // add constants std::vector<Node> consts; mkSygusConstantsForType(btype, consts); - for (unsigned j = 0; j < consts.size(); j++) + for (unsigned i = 0, size = consts.size(); i < size; ++i) { std::stringstream ss; - ss << consts[j]; + ss << consts[i]; Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl; - ops.back().push_back(consts[j].toExpr()); - cnames.push_back(ss.str()); - cargs.push_back(std::vector<CVC4::Type>()); - pcs.push_back(nullptr); - weights.push_back(-1); + ops.back().push_back(consts[i].toExpr()); + cnames.back().push_back(ss.str()); + cargs.back().push_back(std::vector<Type>()); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); } - //add predicates for types - for( unsigned i=0; i<types.size(); i++ ){ + // add predicates for types + for (unsigned i = 0, size = types.size(); i < size; ++i) + { Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl; //add equality per type - CVC4::Kind k = kind::EQUAL; + Kind k = EQUAL; Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops.back().push_back(nm->operatorOf(k).toExpr()); std::stringstream ss; - ss << kind::kindToString(k) << "_" << types[i]; - cnames.push_back(ss.str()); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - cargs.back().push_back(unres_types[i]); - pcs.push_back(nullptr); - weights.push_back(-1); - //type specific predicates + ss << kindToString(k) << "_" << types[i]; + cnames.back().push_back(ss.str()); + cargs.back().push_back(std::vector<Type>()); + cargs.back().back().push_back(unres_types[i]); + cargs.back().back().push_back(unres_types[i]); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); + // type specific predicates if (types[i].isReal()) { - CVC4::Kind k = kind::LEQ; + Kind k = LEQ; Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops.back().push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kind::kindToString(k)); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - cargs.back().push_back(unres_types[i]); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames.back().push_back(kindToString(k)); + cargs.back().push_back(std::vector<Type>()); + cargs.back().back().push_back(unres_types[i]); + cargs.back().back().push_back(unres_types[i]); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); } else if (types[i].isBitVector()) { Kind k = BITVECTOR_ULT; Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops.back().push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kindToString(k)); - cargs.push_back(std::vector<Type>()); - cargs.back().push_back(unres_types[i]); - cargs.back().push_back(unres_types[i]); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames.back().push_back(kindToString(k)); + cargs.back().push_back(std::vector<Type>()); + cargs.back().back().push_back(unres_types[i]); + cargs.back().back().push_back(unres_types[i]); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); } else if (types[i].isDatatype()) { //add for testers Trace("sygus-grammar-def") << "...add for testers" << std::endl; - const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype(); - for( unsigned k=0; k<dt.getNumConstructors(); k++ ){ + const Datatype& dt = types[i].getDatatype(); + for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) + { Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl; ops.back().push_back(dt[k].getTester()); - cnames.push_back(dt[k].getTesterName()); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames.back().push_back(dt[k].getTesterName()); + cargs.back().push_back(std::vector<Type>()); + cargs.back().back().push_back(unres_types[i]); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); } } } @@ -790,19 +820,19 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops.back().push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kindToString(k)); - cargs.push_back(std::vector<CVC4::Type>()); - cargs.back().push_back(unres_bt); + cnames.back().push_back(kindToString(k)); + cargs.back().push_back(std::vector<Type>()); + cargs.back().back().push_back(unres_bt); if (k != NOT) { - cargs.back().push_back(unres_bt); + cargs.back().back().push_back(unres_bt); if (k == ITE) { - cargs.back().push_back(unres_bt); + cargs.back().back().push_back(unres_bt); } } - pcs.push_back(nullptr); - weights.push_back(-1); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); } } if( range==btype ){ @@ -810,15 +840,19 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl; datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true ); - for( unsigned j=0; j<ops.back().size(); j++ ){ - datatypes.back().addSygusConstructor( - ops.back()[j], cnames[j], cargs[j], pcs[j], weights[j]); + for (unsigned i = 0, size = ops.back().size(); i < size; ++i) + { + datatypes.back().addSygusConstructor(ops.back()[i], + cnames.back()[i], + cargs.back()[i], + pcs.back()[i], + weights.back()[i]); } - //sorts.push_back( btype ); + Trace("sygus-grammar-def") << "...built datatype " << datatypes.back() << " "; Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl; - + // make first datatype be the top level datatype if( startIndex>0 ){ - CVC4::Datatype tmp_dt = datatypes[0]; + Datatype tmp_dt = datatypes[0]; datatypes[0] = datatypes[startIndex]; datatypes[startIndex] = tmp_dt; } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 0c5b67656..3afc4c689 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -131,7 +131,8 @@ public: // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres); // collect the list of types that depend on type range - static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ); + static void collectSygusGrammarTypesFor(TypeNode range, + std::vector<TypeNode>& types); /** helper function for function mkSygusDefaultType * Collects a set of mutually recursive datatypes "datatypes" corresponding to * encoding type "range" to SyGuS. diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index b49c29c53..ee7247121 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -179,7 +179,6 @@ bool SygusPbe::initialize(Node n, return false; } } - bool isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; for (const Node& c : candidates) { Assert(d_examples.find(c) != d_examples.end()); @@ -203,7 +202,7 @@ bool SygusPbe::initialize(Node n, for (const Node& e : d_candidate_to_enum[c]) { TypeNode etn = e.getType(); - d_tds->registerEnumerator(e, c, d_parent, true, false, isActiveGen); + d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL, false); d_enum_to_candidate[e] = c; TNode te = e; // initialize static symmetry breaking lemmas for it @@ -229,13 +228,24 @@ bool SygusPbe::initialize(Node n, { lem = lem.substitute(tsp, te); } - disj.push_back(lem); + if (std::find(disj.begin(), disj.end(), lem) == disj.end()) + { + disj.push_back(lem); + } } } + // add its active guard + Node ag = d_tds->getActiveGuardForEnumerator(e); + Assert(!ag.isNull()); + disj.push_back(ag.negate()); Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj); Trace("sygus-pbe") << " static redundant op lemma : " << lem << std::endl; - lemmas.push_back(lem); + // Register as a symmetry breaking lemma with the term database. + // This will either be processed via a lemma on the output channel + // of the sygus extension of the datatypes solver, or internally + // encoded as a constraint to an active enumerator. + d_tds->registerSymBreakLemma(e, lem, etn, 0, false); } } Trace("sygus-pbe") << "Initialize " << d_examples[c].size() diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 21079aedc..2bfde2d80 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -346,14 +346,17 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) { // get the model value of the relevant terms from the master module std::vector<Node> enum_values; - bool fullModel = getEnumeratedValues(terms, enum_values); + bool activeIncomplete = false; + bool fullModel = getEnumeratedValues(terms, enum_values, activeIncomplete); // if the master requires a full model and the model is partial, we fail if (!d_master->allowPartialModel() && !fullModel) { // we retain the values in d_ev_active_gen_waiting Trace("cegqi-engine") << "...partial model, fail." << std::endl; - return true; + // if we are partial due to an active enumerator, we may still succeed + // on the next call + return !activeIncomplete; } // the waiting values are passed to the module below, clear d_ev_active_gen_waiting.clear(); @@ -396,7 +399,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) if (emptyModel) { Trace("cegqi-engine") << "...empty model, fail." << std::endl; - return true; + return !activeIncomplete; } Assert(candidate_values.empty()); constructed_cand = d_master->constructCandidates( @@ -650,7 +653,8 @@ void SynthConjecture::preregisterConjecture(Node q) } bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n, - std::vector<Node>& v) + std::vector<Node>& v, + bool& activeIncomplete) { std::vector<Node> ncheck = n; n.clear(); @@ -670,7 +674,7 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n, continue; } } - Node nv = getEnumeratedValue(e); + Node nv = getEnumeratedValue(e, activeIncomplete); n.push_back(e); v.push_back(nv); ret = ret && !nv.isNull(); @@ -692,42 +696,50 @@ class EnumValGeneratorBasic : public EnumValGenerator /** initialize (do nothing) */ void initialize(Node e) override {} /** initialize (do nothing) */ - void addValue(Node v) override {} + void addValue(Node v) override { d_currTerm = *d_te; } /** * Get next returns the next (T-rewriter-unique) value based on the type * enumerator. */ - Node getNext() override + bool increment() override { + ++d_te; if (d_te.isFinished()) { - return Node::null(); + d_currTerm = Node::null(); + return false; } - Node next = *d_te; - ++d_te; - Node nextb = d_tds->sygusToBuiltin(next); + d_currTerm = *d_te; if (options::sygusSymBreakDynamic()) { + Node nextb = d_tds->sygusToBuiltin(d_currTerm); nextb = d_tds->getExtRewriter()->extendedRewrite(nextb); + if (d_cache.find(nextb) == d_cache.end()) + { + d_cache.insert(nextb); + // only return the current term if not unique + } + else + { + d_currTerm = Node::null(); + } } - if (d_cache.find(nextb) == d_cache.end()) - { - d_cache.insert(nextb); - return next; - } - return getNext(); + return true; } - + /** get the current term */ + Node getCurrent() override { return d_currTerm; } private: /** pointer to term database sygus */ TermDbSygus* d_tds; /** the type enumerator */ TypeEnumerator d_te; + /** the current term */ + Node d_currTerm; /** cache of (enumerated) builtin values we have enumerated so far */ std::unordered_set<Node, NodeHashFunction> d_cache; }; -Node SynthConjecture::getEnumeratedValue(Node e) +Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) { bool isEnum = d_tds->isEnumerator(e); @@ -761,15 +773,18 @@ Node SynthConjecture::getEnumeratedValue(Node e) else { // Actively-generated enumerators are currently either variable agnostic - // or basic. + // or basic. The auto mode always prefers the optimized enumerator over + // the basic one. Assert(d_tds->isBasicEnumerator(e)); - if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM) + if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM_BASIC) { - d_evg[e].reset(new SygusEnumerator(d_tds, this)); + d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); } else { - d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); + Assert(options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM + || options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO); + d_evg[e].reset(new SygusEnumerator(d_tds, this)); } } Trace("sygus-active-gen") @@ -790,6 +805,7 @@ Node SynthConjecture::getEnumeratedValue(Node e) // Check if there is an (abstract) value absE we were actively generating // values based on. Node absE = d_ev_curr_active_gen[e]; + bool firstTime = false; if (absE.isNull()) { // None currently exist. The next abstract value is the model value for e. @@ -804,9 +820,22 @@ Node SynthConjecture::getEnumeratedValue(Node e) } d_ev_curr_active_gen[e] = absE; iteg->second->addValue(absE); + firstTime = true; } - Node v = iteg->second->getNext(); - if (v.isNull()) + bool inc = true; + if (!firstTime) + { + inc = iteg->second->increment(); + } + Node v; + if (inc) + { + v = iteg->second->getCurrent(); + } + Trace("sygus-active-gen-debug") << "...generated " << v + << ", with increment success : " << inc + << std::endl; + if (!inc) { // No more concrete values generated from absE. NodeManager* nm = NodeManager::currentNM(); @@ -852,7 +881,14 @@ Node SynthConjecture::getEnumeratedValue(Node e) else { // We are waiting to send e -> v to the module that requested it. - d_ev_active_gen_waiting[e] = v; + if (v.isNull()) + { + activeIncomplete = true; + } + else + { + d_ev_active_gen_waiting[e] = v; + } if (Trace.isOn("sygus-active-gen")) { Trace("sygus-active-gen") << "Active-gen : " << e << " : "; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index ef1b4459f..3a43eb83d 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -49,8 +49,14 @@ class EnumValGenerator virtual void initialize(Node e) = 0; /** Inform this generator that abstract value v was enumerated. */ virtual void addValue(Node v) = 0; - /** Get the next concrete value generated by this class. */ - virtual Node getNext() = 0; + /** + * Increment this value generator. If this returns false, then we are out of + * values. If this returns true, getCurrent(), if non-null, returns the + * current term. + */ + virtual bool increment() = 0; + /** Get the current concrete value generated by this class. */ + virtual Node getCurrent() = 0; }; /** a synthesis conjecture @@ -193,15 +199,25 @@ class SynthConjecture * Get model values for terms n, store in vector v. This method returns true * if and only if all values added to v are non-null. * + * The argument activeIncomplete indicates whether n contains an active + * enumerator that is currently not finished enumerating values, but returned + * null on a call to getEnumeratedValue. This value is used for determining + * whether we should call getEnumeratedValues again within a call to + * SynthConjecture::check. + * * It removes terms from n that correspond to "inactive" enumerators, that * is, enumerators whose values have been exhausted. */ - bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v); + bool getEnumeratedValues(std::vector<Node>& n, + std::vector<Node>& v, + bool& activeIncomplete); /** * Get model value for term n. If n has a value that was excluded by - * datatypes sygus symmetry breaking, this method returns null. + * datatypes sygus symmetry breaking, this method returns null. It sets + * activeIncomplete to true if there is an actively-generated enumerator whose + * current value is null but it has not finished generating values. */ - Node getEnumeratedValue(Node n); + Node getEnumeratedValue(Node n, bool& activeIncomplete); /** enumerator generators for each actively-generated enumerator */ std::map<Node, std::unique_ptr<EnumValGenerator> > d_evg; /** diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 435e1a00f..9198f7e56 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -58,6 +58,19 @@ void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign, } } +std::ostream& operator<<(std::ostream& os, EnumeratorRole r) +{ + switch (r) + { + case ROLE_ENUM_POOL: os << "POOL"; break; + case ROLE_ENUM_SINGLE_SOLUTION: os << "SINGLE_SOLUTION"; break; + case ROLE_ENUM_MULTI_SOLUTION: os << "MULTI_SOLUTION"; break; + case ROLE_ENUM_CONSTRAINED: os << "CONSTRAINED"; break; + default: os << "enum_" << static_cast<unsigned>(r); break; + } + return os; +} + TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe) : d_quantEngine(qe), d_syexp(new SygusExplain(this)), @@ -454,9 +467,8 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { void TermDbSygus::registerEnumerator(Node e, Node f, SynthConjecture* conj, - bool mkActiveGuard, - bool useSymbolicCons, - bool isActiveGen) + EnumeratorRole erole, + bool useSymbolicCons) { if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end()) { @@ -470,13 +482,6 @@ void TermDbSygus::registerEnumerator(Node e, d_enum_to_conjecture[e] = conj; d_enum_to_synth_fun[e] = f; NodeManager* nm = NodeManager::currentNM(); - if( mkActiveGuard ){ - // make the guard - Node ag = nm->mkSkolem("eG", nm->booleanType()); - // must ensure it is a literal immediately here - ag = d_quantEngine->getValuation().ensureLiteral(ag); - d_enum_to_active_guard[e] = ag; - } Trace("sygus-db") << " registering symmetry breaking clauses..." << std::endl; @@ -554,6 +559,66 @@ void TermDbSygus::registerEnumerator(Node e, } Trace("sygus-db") << " ...finished" << std::endl; + // determine if we are actively-generated + bool isActiveGen = false; + if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE) + { + if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED) + { + // If the enumerator is a solution for a conjecture with multiple + // functions, we do not use active generation. If we did, we would have to + // generate a "product" of two actively-generated enumerators. That is, + // given a conjecture with two functions-to-synthesize with enumerators + // e_f and e_g, and if these enumerators generated: + // e_f -> t1, ..., tn + // e_g -> s1, ..., sm + // The sygus module in charge of this conjecture would expect + // constructCandidates calls of the form + // (e_f,e_g) -> (ti, sj) + // for each i,j. We instead use passive enumeration in this case. + // + // If the enumerator is constrained, it cannot be actively generated. + } + else if (erole == ROLE_ENUM_POOL) + { + // If the enumerator is used for generating a pool of values, we always + // use active generation. + isActiveGen = true; + } + else if (erole == ROLE_ENUM_SINGLE_SOLUTION) + { + // If the enumerator is the single function-to-synthesize, if auto is + // enabled, we infer whether it is better to enable active generation. + if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO) + { + // We use active generation if the grammar of the enumerator does not + // have ITE and is not Boolean. Experimentally, it is better to + // use passive generation for these cases since it enables useful + // search space pruning techniques, e.g. evaluation unfolding, + // conjecture-specific symmetry breaking. Also, if sygus-stream is + // enabled, we always use active generation, since the use cases of + // sygus stream are to find many solutions to an easy problem, where + // the bottleneck often becomes the large number of "exclude the current + // solution" clauses. + const Datatype& dt = et.getDatatype(); + if (options::sygusStream() + || (!hasKind(et, ITE) && !dt.getSygusType().isBoolean())) + { + isActiveGen = true; + } + } + else + { + isActiveGen = true; + } + } + else + { + Unreachable("Unknown enumerator mode in registerEnumerator"); + } + } + Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole + << " returned " << isActiveGen << std::endl; // Currently, actively-generated enumerators are either basic or variable // agnostic. bool isVarAgnostic = @@ -607,6 +672,22 @@ void TermDbSygus::registerEnumerator(Node e, } d_enum_active_gen[e] = isActiveGen; d_enum_basic[e] = isActiveGen && !isVarAgnostic; + + // We make an active guard if we will be explicitly blocking solutions for + // the enumerator. This is the case if the role of the enumerator is to + // populate a pool of terms, or (some cases) of when it is actively generated. + if (isActiveGen || erole == ROLE_ENUM_POOL) + { + // make the guard + Node ag = nm->mkSkolem("eG", nm->booleanType()); + // must ensure it is a literal immediately here + ag = d_quantEngine->getValuation().ensureLiteral(ag); + // must ensure that it is asserted as a literal before we begin solving + Node lem = nm->mkNode(OR, ag, ag.negate()); + d_quantEngine->getOutputChannel().requirePhase(ag, true); + d_quantEngine->getOutputChannel().lemma(lem); + d_enum_to_active_guard[e] = ag; + } } bool TermDbSygus::isEnumerator(Node e) const @@ -694,14 +775,13 @@ void TermDbSygus::getEnumerators(std::vector<Node>& mts) } } -void TermDbSygus::registerSymBreakLemma(Node e, - Node lem, - TypeNode tn, - unsigned sz) +void TermDbSygus::registerSymBreakLemma( + Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl) { d_enum_to_sb_lemmas[e].push_back(lem); d_sb_lemma_to_type[lem] = tn; d_sb_lemma_to_size[lem] = sz; + d_sb_lemma_to_isTempl[lem] = isTempl; } bool TermDbSygus::hasSymBreakLemmas(std::vector<Node>& enums) const @@ -740,6 +820,13 @@ unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const return it->second; } +bool TermDbSygus::isSymBreakLemmaTemplate(Node lem) const +{ + std::map<Node, bool>::const_iterator it = d_sb_lemma_to_isTempl.find(lem); + Assert(it != d_sb_lemma_to_isTempl.end()); + return it->second; +} + void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); } bool TermDbSygus::isRegistered(TypeNode tn) const @@ -756,9 +843,16 @@ void TermDbSygus::toStreamSygus(const char* c, Node n) { if (Trace.isOn(c)) { - std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n); - Trace(c) << ss.str(); + if (n.isNull()) + { + Trace(c) << n; + } + else + { + std::stringstream ss; + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n); + Trace(c) << ss.str(); + } } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 713e322a4..7a522ded6 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -48,6 +48,23 @@ class TypeNodeIdTrie void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount); }; +/** role for registering an enumerator */ +enum EnumeratorRole +{ + /** The enumerator populates a pool of terms (e.g. for PBE). */ + ROLE_ENUM_POOL, + /** The enumerator is the single solution of the problem. */ + ROLE_ENUM_SINGLE_SOLUTION, + /** + * The enumerator is part of the solution of the problem (e.g. multiple + * functions to synthesize). + */ + ROLE_ENUM_MULTI_SOLUTION, + /** The enumerator must satisfy some set of constraints */ + ROLE_ENUM_CONSTRAINED, +}; +std::ostream& operator<<(std::ostream& os, EnumeratorRole r); + // TODO :issue #1235 split and document this class class TermDbSygus { public: @@ -80,29 +97,32 @@ class TermDbSygus { //------------------------------enumerators /** * Register a variable e that we will do enumerative search on. + * * conj : the conjecture that the enumeration of e is for. - * f : the synth-fun that the enumeration of e is for. - * mkActiveGuard : whether we want to make an active guard for e - * (see d_enum_to_active_guard), - * useSymbolicCons : whether we want model values for e to include symbolic - * constructors like the "any constant" variable. - * isActiveGen : if this flag is true, the enumerator will be - * actively-generated based on the mode specified by --sygus-active-gen. + * + * f : the synth-fun that the enumeration of e is for.Notice that enumerator + * e may not be one-to-one with f in synthesis-through-unification approaches + * (e.g. decision tree construction for PBE synthesis). + * + * erole : the role of this enumerator (see definition of EnumeratorRole). + * Depending on this and the policy for actively-generated enumerators + * (--sygus-active-gen), the enumerator may be "actively-generated". * For example, if --sygus-active-gen=var-agnostic, then the enumerator will * only generate values whose variables are in canonical order (only x1-x2 * and not x2-x1 will be generated, assuming x1 and x2 are in the same * "subclass", see getSubclassForVar). * - * Notice that enumerator e may not be one-to-one with f in - * synthesis-through-unification approaches (e.g. decision tree construction - * for PBE synthesis). + * useSymbolicCons : whether we want model values for e to include symbolic + * constructors like the "any constant" variable. + * + * An "active guard" may be allocated by this method for e based on erole + * and the policies for active generation. */ void registerEnumerator(Node e, Node f, SynthConjecture* conj, - bool mkActiveGuard = false, - bool useSymbolicCons = false, - bool isActiveGen = false); + EnumeratorRole erole, + bool useSymbolicCons = false); /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ @@ -150,12 +170,13 @@ class TermDbSygus { * * tn : the (sygus datatype) type that lem applies to, i.e. the * type of terms that lem blocks models for, - * sz : the minimum size of terms that the lem blocks. - * - * Notice that the symmetry breaking lemma template should be relative to x, - * where x is returned by the call to getFreeVar( tn, 0 ) in this class. + * sz : the minimum size of terms that the lem blocks, + * isTempl : if this flag is false, then lem is a (concrete) lemma. + * If this flag is true, then lem is a symmetry breaking lemma template + * over x, where x is returned by the call to getFreeVar( tn, 0 ). */ - void registerSymBreakLemma(Node e, Node lem, TypeNode tn, unsigned sz); + void registerSymBreakLemma( + Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl = true); /** Has symmetry breaking lemmas been added for any enumerator? */ bool hasSymBreakLemmas(std::vector<Node>& enums) const; /** Get symmetry breaking lemmas @@ -168,6 +189,8 @@ class TermDbSygus { TypeNode getTypeForSymBreakLemma(Node lem) const; /** Get the minimum size of terms symmetry breaking lemma lem applies to */ unsigned getSizeForSymBreakLemma(Node lem) const; + /** Returns true if lem is a lemma template, false if lem is a lemma */ + bool isSymBreakLemmaTemplate(Node lem) const; /** Clear information about symmetry breaking lemmas for enumerator e */ void clearSymBreakLemmas(Node e); //------------------------------end enumerators @@ -324,6 +347,8 @@ class TermDbSygus { std::map<Node, TypeNode> d_sb_lemma_to_type; /** mapping from symmetry breaking lemmas to size */ std::map<Node, unsigned> d_sb_lemma_to_size; + /** mapping from symmetry breaking lemmas to whether they are templates */ + std::map<Node, bool> d_sb_lemma_to_isTempl; /** enumerators to whether they are actively-generated */ std::map<Node, bool> d_enum_active_gen; /** enumerators to whether they are variable agnostic */ |