diff options
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/sygus_datatype.cpp | 25 | ||||
| -rw-r--r-- | src/expr/sygus_datatype.h | 23 |
2 files changed, 41 insertions, 7 deletions
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp index be2b04402..d8ee2e1ea 100644 --- a/src/expr/sygus_datatype.cpp +++ b/src/expr/sygus_datatype.cpp @@ -26,9 +26,9 @@ std::string SygusDatatype::getName() const { return d_dt.getName(); } void SygusDatatype::addConstructor(Node op, const std::string& name, + const std::vector<TypeNode>& consTypes, std::shared_ptr<SygusPrintCallback> spc, - int weight, - const std::vector<TypeNode>& consTypes) + int weight) { d_ops.push_back(op); d_cons_names.push_back(std::string(name)); @@ -50,14 +50,26 @@ void SygusDatatype::addAnyConstantConstructor(TypeNode tn) std::vector<TypeNode> builtinArg; builtinArg.push_back(tn); addConstructor( - av, cname, printer::SygusEmptyPrintCallback::getEmptyPC(), 0, builtinArg); + av, cname, builtinArg, printer::SygusEmptyPrintCallback::getEmptyPC(), 0); +} +void SygusDatatype::addConstructor(Kind k, + const std::vector<TypeNode>& consTypes, + std::shared_ptr<SygusPrintCallback> spc, + int weight) +{ + NodeManager* nm = NodeManager::currentNM(); + addConstructor(nm->operatorOf(k), kindToString(k), consTypes, spc, weight); } +size_t SygusDatatype::getNumConstructors() const { return d_ops.size(); } + void SygusDatatype::initializeDatatype(TypeNode sygusType, Node sygusVars, bool allowConst, bool allowAll) { + // should not have initialized (set sygus) yet + Assert(!d_dt.isSygus()); /* Use the sygus type to not lose reference to the original types (Bool, * Int, etc) */ d_dt.setSygus(sygusType.toType(), sygusVars.toExpr(), allowConst, allowAll); @@ -76,6 +88,11 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType, Trace("sygus-type-cons") << "...built datatype " << d_dt << " "; } -const Datatype& SygusDatatype::getDatatype() const { return d_dt; } +const Datatype& SygusDatatype::getDatatype() const +{ + // should have initialized by this point + Assert(d_dt.isSygus()); + return d_dt; +} } // namespace CVC4 diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h index d7b18644a..132406c69 100644 --- a/src/expr/sygus_datatype.h +++ b/src/expr/sygus_datatype.h @@ -61,18 +61,35 @@ class SygusDatatype * weight: the weight of this constructor, * consTypes: the argument types of the constructor (typically other sygus * datatype types). + * + * It should be the case that consTypes 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+ + * sygus datatype types that encode integer. */ void addConstructor(Node op, const std::string& name, - std::shared_ptr<SygusPrintCallback> spc, - int weight, - const std::vector<TypeNode>& consTypes); + const std::vector<TypeNode>& consTypes, + 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 types of the arguments of the kind. + */ + void addConstructor(Kind k, + const std::vector<TypeNode>& consTypes, + std::shared_ptr<SygusPrintCallback> spc = nullptr, + int weight = -1); /** * This adds a constructor that corresponds to the any constant constructor * for the given (builtin) type tn. */ void addAnyConstantConstructor(TypeNode tn); + /** Get the number of constructors added to this class so far */ + size_t getNumConstructors() const; + /** builds a datatype with the information in the type object * * sygusType: the builtin type that this datatype encodes, |