From 357e81dfc393d9e2ea80f66cddc837564494a34c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 18 Nov 2019 13:13:14 -0600 Subject: [PATCH] Improve interface for sygus datatype, fix utilities (#3473) --- src/expr/sygus_datatype.cpp | 44 +++++++++------ src/expr/sygus_datatype.h | 54 ++++++++++++------- .../quantifiers/sygus/sygus_grammar_norm.cpp | 14 ++++- .../quantifiers/sygus/sygus_grammar_red.cpp | 28 ++++++++-- 4 files changed, 101 insertions(+), 39 deletions(-) diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp index d8ee2e1ea..73f7c5769 100644 --- a/src/expr/sygus_datatype.cpp +++ b/src/expr/sygus_datatype.cpp @@ -26,15 +26,16 @@ std::string SygusDatatype::getName() const { return d_dt.getName(); } void SygusDatatype::addConstructor(Node op, const std::string& name, - const std::vector& consTypes, + const std::vector& argTypes, std::shared_ptr spc, int weight) { - d_ops.push_back(op); - d_cons_names.push_back(std::string(name)); - d_pc.push_back(spc); - d_weight.push_back(weight); - d_consArgs.push_back(consTypes); + d_cons.push_back(SygusDatatypeConstructor()); + d_cons.back().d_op = op; + d_cons.back().d_name = name; + d_cons.back().d_argTypes = argTypes; + d_cons.back().d_pc = spc; + d_cons.back().d_weight = weight; } void SygusDatatype::addAnyConstantConstructor(TypeNode tn) @@ -53,15 +54,21 @@ void SygusDatatype::addAnyConstantConstructor(TypeNode tn) av, cname, builtinArg, printer::SygusEmptyPrintCallback::getEmptyPC(), 0); } void SygusDatatype::addConstructor(Kind k, - const std::vector& consTypes, + const std::vector& argTypes, std::shared_ptr spc, int weight) { NodeManager* nm = NodeManager::currentNM(); - addConstructor(nm->operatorOf(k), kindToString(k), consTypes, spc, weight); + addConstructor(nm->operatorOf(k), kindToString(k), argTypes, spc, weight); } -size_t SygusDatatype::getNumConstructors() const { return d_ops.size(); } +size_t SygusDatatype::getNumConstructors() const { return d_cons.size(); } + +const SygusDatatypeConstructor& SygusDatatype::getConstructor(unsigned i) const +{ + Assert(i < d_cons.size()); + return d_cons[i]; +} void SygusDatatype::initializeDatatype(TypeNode sygusType, Node sygusVars, @@ -69,21 +76,26 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType, bool allowAll) { // should not have initialized (set sygus) yet - Assert(!d_dt.isSygus()); + Assert(!isInitialized()); + // should have added a constructor + Assert(!d_cons.empty()); /* Use the sygus type to not lose reference to the original types (Bool, * Int, etc) */ d_dt.setSygus(sygusType.toType(), sygusVars.toExpr(), allowConst, allowAll); - for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i) + for (unsigned i = 0, ncons = d_cons.size(); i < ncons; ++i) { // must convert to type now std::vector cargs; - for (TypeNode& ct : d_consArgs[i]) + for (TypeNode& ct : d_cons[i].d_argTypes) { cargs.push_back(ct.toType()); } // add (sygus) constructor - d_dt.addSygusConstructor( - d_ops[i].toExpr(), d_cons_names[i], cargs, d_pc[i], d_weight[i]); + d_dt.addSygusConstructor(d_cons[i].d_op.toExpr(), + d_cons[i].d_name, + cargs, + d_cons[i].d_pc, + d_cons[i].d_weight); } Trace("sygus-type-cons") << "...built datatype " << d_dt << " "; } @@ -91,8 +103,10 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType, const Datatype& SygusDatatype::getDatatype() const { // should have initialized by this point - Assert(d_dt.isSygus()); + Assert(isInitialized()); return d_dt; } +bool SygusDatatype::isInitialized() const { return d_dt.isSygus(); } + } // namespace CVC4 diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h index 132406c69..e7b60f3a3 100644 --- a/src/expr/sygus_datatype.h +++ b/src/expr/sygus_datatype.h @@ -32,6 +32,25 @@ struct SygusAnyConstAttributeId }; typedef expr::Attribute SygusAnyConstAttribute; +/** + * Information necessary to specify a sygus constructor. Further detail on these + * fields can be found in SygusDatatype below. + */ +class SygusDatatypeConstructor +{ + public: + /** The operator that the constructor encodes. */ + Node d_op; + /** Name of the constructor. */ + std::string d_name; + /** List of argument types. */ + std::vector d_argTypes; + /** Print callback of the constructor. */ + std::shared_ptr d_pc; + /** Weight of the constructor. */ + int d_weight; +}; + /** * Keeps the necessary information for initializing a sygus datatype, which * includes the operators, names, print callbacks and list of argument types @@ -57,28 +76,28 @@ class SygusDatatype * * op: the builtin operator, * name: the name of the constructor, - * spc: the print callback (for custom printing of this node), - * weight: the weight of this constructor, - * consTypes: the argument types of the constructor (typically other sygus + * argTypes: the argument types of the constructor (typically other sygus * datatype types). + * spc: the print callback (for custom printing of this node), + * weight: the weight of this constructor. * - * It should be the case that consTypes are sygus datatype types (possibly + * It should be the case that argTypes are sygus datatype types (possibly * unresolved) that encode the arguments of the builtin operator. That is, - * if op is the builtin PLUS operator, then consTypes could contain 2+ + * if op is the builtin PLUS operator, then argTypes could contain 2+ * sygus datatype types that encode integer. */ void addConstructor(Node op, const std::string& name, - const std::vector& consTypes, + const std::vector& argTypes, std::shared_ptr spc = nullptr, int weight = -1); /** * Add constructor that encodes an application of builtin kind k. Like above, - * the arguments consTypes should correspond to sygus datatypes that encode + * the arguments argTypes should correspond to sygus datatypes that encode * the types of the arguments of the kind. */ void addConstructor(Kind k, - const std::vector& consTypes, + const std::vector& argTypes, std::shared_ptr spc = nullptr, int weight = -1); /** @@ -90,6 +109,9 @@ class SygusDatatype /** Get the number of constructors added to this class so far */ size_t getNumConstructors() const; + /** Get constructor at index i */ + const SygusDatatypeConstructor& getConstructor(unsigned i) const; + /** builds a datatype with the information in the type object * * sygusType: the builtin type that this datatype encodes, @@ -106,18 +128,12 @@ class SygusDatatype /** Get the sygus datatype initialized by this class */ const Datatype& getDatatype() const; + /** is initialized */ + bool isInitialized() const; + private: - //---------- information to build normalized type node - /** Operators for each constructor. */ - std::vector d_ops; - /** Names for each constructor. */ - std::vector d_cons_names; - /** Print callbacks for each constructor */ - std::vector> d_pc; - /** Weights for each constructor */ - std::vector d_weight; - /** List of argument types for each constructor */ - std::vector> d_consArgs; + /** Information for each constructor. */ + std::vector d_cons; /** Datatype to represent type's structure */ Datatype d_dt; }; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 40046ef15..019abc28a 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -495,6 +495,7 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, const Datatype& dt, std::vector& op_pos) { + Assert(tn.isDatatype()); /* Corresponding type node to tn with the given operator positions. To be * retrieved (if cached) or defined (otherwise) */ TypeNode unres_tn; @@ -591,8 +592,19 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn) { + if (!tn.isDatatype()) + { + // Might not be a sygus datatype, e.g. if the input grammar had the + // any constant constructor. + return tn; + } /* Collect all operators for normalization */ - const Datatype& dt = static_cast(tn.toType()).getDatatype(); + const Datatype& dt = tn.getDatatype(); + if (!dt.isSygus()) + { + // datatype but not sygus datatype case + return tn; + } std::vector op_pos(dt.getNumConstructors()); std::iota(op_pos.begin(), op_pos.end(), 0); return normalizeSygusRec(tn, dt, op_pos); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 6bf8c56fb..b1b1ea62c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/sygus_grammar_red.h" +#include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -41,18 +42,37 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn) { Trace("sygus-red") << " Is " << dt[i].getName() << " a redundant operator?" << std::endl; + Node sop = Node::fromExpr(dt[i].getSygusOp()); + if (sop.getAttribute(SygusAnyConstAttribute())) + { + // the any constant constructor is never redundant + d_sygus_red_status.push_back(0); + continue; + } std::map 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++) + // a list of variants of the generic term (see getGenericList). + std::vector glist; + if (sop.isConst() || sop.getKind() == LAMBDA) + { + Assert(g.getNumChildren() == dt[i].getNumArgs()); + for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) + { + pre[j] = g[j]; + } + getGenericList(tds, dt, i, 0, pre, glist); + } + else { - pre[j] = g[j]; + // It is a builtin (possibly) ground term. Its children do not correspond + // one-to-one with the arugments of the constructor. Hence, we consider + // only g itself as a variant. + glist.push_back(g); } - std::vector glist; - getGenericList(tds, dt, i, 0, pre, glist); // call the extended rewriter bool red = false; for (const Node& gr : glist) -- 2.30.2