From 4874e4f9566b5e536e6c66b559574d2df97e20ec Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 1 Nov 2019 07:09:35 -0500 Subject: [PATCH] Eagerly beta reduce during sygus to builtin term conversion (#3418) --- .../datatypes/theory_datatypes_utils.cpp | 37 ++++++++++++++----- src/theory/datatypes/theory_datatypes_utils.h | 6 ++- .../quantifiers/sygus/sygus_grammar_red.cpp | 6 ++- .../quantifiers/sygus/term_database_sygus.cpp | 21 ++++++++--- .../quantifiers/sygus/term_database_sygus.h | 12 ++++-- src/theory/quantifiers/sygus/type_info.cpp | 2 + 6 files changed, 63 insertions(+), 21 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index c3b145b15..bb62ab8ae 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -116,7 +116,8 @@ Kind getOperatorKindForSygusBuiltin(Node op) Node mkSygusTerm(const Datatype& dt, unsigned i, - const std::vector& children) + const std::vector& children, + bool doBetaReduction) { Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i << "] with children: " << children << std::endl; @@ -138,26 +139,44 @@ Node mkSygusTerm(const Datatype& dt, Assert(children.size() == 1); return children[0]; } - if (op.getKind() != BUILTIN) + // get the kind of the operator + Kind ok = op.getKind(); + if (ok != BUILTIN) { - schildren.push_back(op); + if (ok == LAMBDA && doBetaReduction) + { + // Do immediate beta reduction. It suffices to use a normal substitution + // since neither op nor children have quantifiers, since they are + // generated by sygus grammars. + std::vector vars{op[0].begin(), op[0].end()}; + Assert(vars.size() == children.size()); + Node ret = op[1].substitute( + vars.begin(), vars.end(), children.begin(), children.end()); + Trace("dt-sygus-util") << "...return (beta-reduce) " << ret << std::endl; + return ret; + } + else + { + schildren.push_back(op); + } } schildren.insert(schildren.end(), children.begin(), children.end()); Node ret; - if (op.getKind() == BUILTIN) + if (ok == BUILTIN) { ret = NodeManager::currentNM()->mkNode(op, schildren); Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl; return ret; } - Kind ok = NodeManager::operatorToKind(op); - Trace("dt-sygus-util") << "operator kind is " << ok << std::endl; - if (ok != UNDEFINED_KIND) + // get the kind used for applying op + Kind otk = NodeManager::operatorToKind(op); + Trace("dt-sygus-util") << "operator kind is " << otk << std::endl; + if (otk != UNDEFINED_KIND) { // If it is an APPLY_UF operator, we should have at least an operator and // a child. - Assert(ok != APPLY_UF || schildren.size() != 1); - ret = NodeManager::currentNM()->mkNode(ok, schildren); + Assert(otk != APPLY_UF || schildren.size() != 1); + ret = NodeManager::currentNM()->mkNode(otk, schildren); Trace("dt-sygus-util") << "...return (op) " << ret << std::endl; return ret; } diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index ba0643567..92783c2f7 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -146,11 +146,13 @@ Kind getOperatorKindForSygusBuiltin(Node op); * * This function returns a builtin term f( children[0], ..., children[n] ) * where f is the builtin op that the i^th constructor of sygus datatype dt - * encodes. + * encodes. If doBetaReduction is true, then lambdas are eagerly eliminated + * via beta reduction. */ Node mkSygusTerm(const Datatype& dt, unsigned i, - const std::vector& children); + const std::vector& children, + bool doBetaReduction = true); /** * n is a builtin term that is an application of operator op. * diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index a566ebfff..6bf8c56fb 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -42,7 +42,9 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn) Trace("sygus-red") << " Is " << dt[i].getName() << " a redundant operator?" << std::endl; std::map pre; - Node g = tds->mkGeneric(dt, i, pre); + // We do not do beta reduction, since we want the arguments to match the + // the types of the datatype. + Node g = tds->mkGeneric(dt, i, pre, false); Trace("sygus-red-debug") << " ...pre-rewrite : " << g << std::endl; d_gen_terms[i] = g; for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) @@ -73,6 +75,8 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn) } d_sygus_red_status.push_back(red ? 1 : 0); } + Trace("sygus-red") << "Compute redundant cons for " << tn << " finished" + << std::endl; } void SygusRedundantCons::getRedundant(std::vector& indices) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 7fb54f14e..d4ee11453 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -162,7 +162,8 @@ TypeNode TermDbSygus::getSygusTypeForVar( Node v ) { Node TermDbSygus::mkGeneric(const Datatype& dt, unsigned c, std::map& var_count, - std::map& pre) + std::map& pre, + bool doBetaRed) { Assert(c < dt.getNumConstructors()); Assert(dt.isSygus()); @@ -176,6 +177,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, std::map< int, Node >::iterator it = pre.find( i ); if( it!=pre.end() ){ a = it->second; + Trace("sygus-db-debug") << "From pre: " << a << std::endl; }else{ TypeNode tna = TypeNode::fromType(dt[c].getArgType(i)); a = getFreeVarInc( tna, var_count, true ); @@ -185,19 +187,24 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, Assert(!a.isNull()); children.push_back( a ); } - return datatypes::utils::mkSygusTerm(dt, c, children); + Node ret = datatypes::utils::mkSygusTerm(dt, c, children, doBetaRed); + Trace("sygus-db-debug") << "mkGeneric returns " << ret << std::endl; + return ret; } -Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map& pre) +Node TermDbSygus::mkGeneric(const Datatype& dt, + int c, + std::map& pre, + bool doBetaRed) { std::map var_count; - return mkGeneric(dt, c, var_count, pre); + return mkGeneric(dt, c, var_count, pre, doBetaRed); } -Node TermDbSygus::mkGeneric(const Datatype& dt, int c) +Node TermDbSygus::mkGeneric(const Datatype& dt, int c, bool doBetaRed) { std::map pre; - return mkGeneric(dt, c, pre); + return mkGeneric(dt, c, pre, doBetaRed); } struct CanonizeBuiltinAttributeId @@ -293,6 +300,8 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn) for (unsigned j = 0, size = n.getNumChildren(); j < size; j++) { pre[j] = sygusToBuiltin(n[j], TypeNode::fromType(dt[i].getArgType(j))); + Trace("sygus-db-debug") + << "sygus to builtin " << n[j] << " is " << pre[j] << std::endl; } Node ret = mkGeneric(dt, i, pre); Trace("sygus-db-debug") diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 6c62d7a1b..68381fb2a 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -223,15 +223,21 @@ class TermDbSygus { * If i is in the domain of pre, then ti = pre[i]. * If i is not in the domain of pre, then ti = d_fv[1][ var_count[Ti ] ], * and var_count[Ti] is incremented. + * If doBetaRed is true, then lambda operators are eagerly eliminated via + * beta reduction. */ Node mkGeneric(const Datatype& dt, unsigned c, std::map& var_count, - std::map& pre); + std::map& pre, + bool doBetaRed = true); /** same as above, but with empty var_count */ - Node mkGeneric(const Datatype& dt, int c, std::map& pre); + Node mkGeneric(const Datatype& dt, + int c, + std::map& pre, + bool doBetaRed = true); /** same as above, but with empty pre */ - Node mkGeneric(const Datatype& dt, int c); + Node mkGeneric(const Datatype& dt, int c, bool doBetaRed = true); /** makes a symbolic term concrete * * Given a sygus datatype term n of type tn with holes (symbolic constructor diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 8f280c587..5f51d8dec 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -187,6 +187,8 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) } d_min_cons_term_size[i] = csize; } + Trace("sygus-db") << "Register type " << dt.getName() << " finished" + << std::endl; } void SygusTypeInfo::initializeVarSubclasses() -- 2.30.2