From 4125891ca0228501775282f6cf15028ab46d24ca Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 4 Dec 2019 15:52:28 -0600 Subject: [PATCH] Fixes for SyGuS PBE + templated string concatenations + datatypes (#3492) --- src/theory/evaluator.h | 3 +++ src/theory/quantifiers/sygus/sygus_unif_io.cpp | 14 ++++++++++---- src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 8 +++++++- 3 files changed, 20 insertions(+), 5 deletions(-) diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index 5c0e9b944..ce19a1f67 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -88,6 +88,9 @@ class Evaluator * `args` and the corresponding values `vals`. The function returns a null * node if there is a subterm that is not constant under the substitution or * if an operator is not supported by the evaluator. + * + * The nodes in the vals must be constant values, that is, they must return + * true for isConst(). */ Node eval(TNode n, const std::vector& args, diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 72091c0cf..d423b1777 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -594,12 +594,18 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) for (const Node& res : base_results) { TNode tres = res; - std::vector vals; - vals.push_back(tres); Node sres; - if (tryEval) + // It may not be constant, e.g. if we involve a partial operator + // like datatype selectors. In this case, we avoid using the evaluator, + // which expects a constant substitution. + if (tres.isConst()) { - sres = ev->eval(templ, args, vals); + std::vector vals; + vals.push_back(tres); + if (tryEval) + { + sres = ev->eval(templ, args, vals); + } } if (sres.isNull()) { diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 07997221f..f87b906e1 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -101,6 +101,8 @@ void SygusUnifStrategy::initialize(QuantifiersEngine* qe, void SygusUnifStrategy::initializeType(TypeNode tn) { + Trace("sygus-unif") << "SygusUnifStrategy: initialize : " << tn << " for " + << d_candidate << std::endl; d_tinfo[tn].d_this_type = tn; } @@ -123,6 +125,8 @@ EnumInfo& SygusUnifStrategy::getEnumInfo(Node e) EnumTypeInfo& SygusUnifStrategy::getEnumTypeInfo(TypeNode tn) { + Trace("sygus-unif") << "SygusUnifStrategy: get : " << tn << " for " + << d_candidate << std::endl; std::map::iterator it = d_tinfo.find(tn); Assert(it != d_tinfo.end()); return it->second; @@ -567,6 +571,9 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) EnumRole erole_c = getEnumeratorRoleForNodeRole(nrole_c); // make the enumerator Node et; + // Build the strategy recursively, regardless of whether the + // enumerator is templated. + buildStrategyGraph(ct, nrole_c); if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end()) { // it is templated, allocate a fresh variable @@ -591,7 +598,6 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) << "...child type enumerate " << ((DatatypeType)ct.toType()).getDatatype().getName() << ", node role = " << nrole_c << std::endl; - buildStrategyGraph(ct, nrole_c); // otherwise use the previous Assert(d_tinfo[ct].d_enum.find(erole_c) != d_tinfo[ct].d_enum.end()); -- 2.30.2