diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-18 13:13:14 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-18 13:13:14 -0600 |
commit | 357e81dfc393d9e2ea80f66cddc837564494a34c (patch) | |
tree | a4a09139ae7942907a75efcb895b7e3bc3e7f77a /src/expr | |
parent | 11bc0e4c3147b0fce3033b6a4290d8730aa401ad (diff) |
Improve interface for sygus datatype, fix utilities (#3473)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/sygus_datatype.cpp | 44 | ||||
-rw-r--r-- | src/expr/sygus_datatype.h | 54 |
2 files changed, 64 insertions, 34 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<TypeNode>& consTypes, + const std::vector<TypeNode>& argTypes, std::shared_ptr<SygusPrintCallback> 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<TypeNode>& consTypes, + const std::vector<TypeNode>& argTypes, std::shared_ptr<SygusPrintCallback> 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<Type> 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 @@ -33,6 +33,25 @@ struct SygusAnyConstAttributeId typedef expr::Attribute<SygusAnyConstAttributeId, bool> 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<TypeNode> d_argTypes; + /** Print callback of the constructor. */ + std::shared_ptr<SygusPrintCallback> 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 * for each constructor. @@ -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<TypeNode>& consTypes, + const std::vector<TypeNode>& argTypes, std::shared_ptr<SygusPrintCallback> 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<TypeNode>& consTypes, + const std::vector<TypeNode>& argTypes, std::shared_ptr<SygusPrintCallback> 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<Node> d_ops; - /** Names for each constructor. */ - std::vector<std::string> d_cons_names; - /** Print callbacks for each constructor */ - std::vector<std::shared_ptr<SygusPrintCallback>> d_pc; - /** Weights for each constructor */ - std::vector<int> d_weight; - /** List of argument types for each constructor */ - std::vector<std::vector<TypeNode>> d_consArgs; + /** Information for each constructor. */ + std::vector<SygusDatatypeConstructor> d_cons; /** Datatype to represent type's structure */ Datatype d_dt; }; |