diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-11 21:53:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-11 21:53:13 -0500 |
commit | 8b1f36ef24beaf3fa0708c28c53042a5c823c79c (patch) | |
tree | 81b5398a7c01b9936e0db883ff3684cc03ef5328 /src | |
parent | 1c06ccdb1228fc7ef14440e1f29cf016cf5756c9 (diff) |
Final preparations for changing API to use the Node-level datatype (#4863)
This includes all fixes encountered while fixing unit tests with the Term -> Node version of Datatypes in the API.
After all pending PRs are merged, the next step will be to convert the new API to use e.g. CVC4::DType instead of CVC4::Datatype everywhere.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/dtype.cpp | 22 | ||||
-rw-r--r-- | src/expr/dtype.h | 26 | ||||
-rw-r--r-- | src/expr/dtype_cons.cpp | 14 | ||||
-rw-r--r-- | src/expr/dtype_cons.h | 2 | ||||
-rw-r--r-- | src/expr/dtype_selector.cpp | 8 | ||||
-rw-r--r-- | src/expr/dtype_selector.h | 2 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 27 |
7 files changed, 94 insertions, 7 deletions
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 91ae9d158..bfc33ef87 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -220,6 +220,28 @@ void DType::addConstructor(std::shared_ptr<DTypeConstructor> c) d_constructors.push_back(c); } +void DType::addSygusConstructor(Node op, + const std::string& cname, + const std::vector<TypeNode>& cargs, + int weight) +{ + // avoid name clashes + std::stringstream ss; + ss << getName() << "_" << getNumConstructors() << "_" << cname; + std::string name = ss.str(); + unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1); + std::shared_ptr<DTypeConstructor> c = + std::make_shared<DTypeConstructor>(name, cweight); + c->setSygus(op); + for (size_t j = 0, nargs = cargs.size(); j < nargs; j++) + { + std::stringstream sname; + sname << name << "_" << j; + c->addArg(sname.str(), cargs[j]); + } + addConstructor(c); +} + void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll) { Assert(!d_resolved); diff --git a/src/expr/dtype.h b/src/expr/dtype.h index 1682614d0..f48997748 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -77,7 +77,6 @@ typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr; // ----------------------- end datatype attributes class NodeManager; - class Datatype; /** @@ -191,6 +190,31 @@ class DType * be unique; they are for convenience and pretty-printing only. */ void addConstructor(std::shared_ptr<DTypeConstructor> c); + /** add sygus constructor + * + * This adds a sygus constructor to this datatype, where + * this datatype should be currently unresolved. Note this method is + * syntactic sugar for adding a normal constructor and setting it to be a + * sygus constructor, and following a naming convention that avoids + * constructors with the same name. + * + * @param op : the builtin operator, constant, or variable that this + * constructor encodes + * @param cname the name of the constructor (for printing only) + * @param cargs the arguments of the constructor. + * It should be the case that cargs are sygus datatypes that + * encode the arguments of op. For example, a sygus constructor + * with op = PLUS should be such that cargs.size()>=2 and + * the sygus type of cargs[i] is Real/Int for each i. + * @param weight denotes the value added by the constructor when computing the + * size of datatype terms. Passing a value < 0 denotes the default weight for + * the constructor, which is 0 for nullary constructors and 1 for non-nullary + * constructors. + */ + void addSygusConstructor(Node op, + const std::string& cname, + const std::vector<TypeNode>& cargs, + int weight = -1); /** set sygus * diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index c64814ed6..05daae1b8 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -70,7 +70,7 @@ void DTypeConstructor::addArgSelf(std::string selectorName) addArg(a); } -std::string DTypeConstructor::getName() const { return d_name; } +const std::string& DTypeConstructor::getName() const { return d_name; } Node DTypeConstructor::getConstructor() const { @@ -115,7 +115,10 @@ TypeNode DTypeConstructor::getSpecializedConstructorType( TypeNode returnType) const { Assert(isResolved()); - Assert(returnType.isDatatype()); + Assert(returnType.isDatatype()) + << "DTypeConstructor::getSpecializedConstructorType: expected datatype, " + "got " + << returnType; const DType& dt = DType::datatypeOf(d_constructor); Assert(dt.isParametric()); TypeNode dtt = dt.getTypeNode(); @@ -577,6 +580,13 @@ bool DTypeConstructor::resolve( arg->d_selector.setAttribute(DTypeIndexAttr(), index++); arg->d_resolved = true; argTypes.push_back(range); + // We use \0 as a distinguished marker for unresolved selectors for doing + // name resolutions. We now can remove \0 from name if necessary. + const size_t nul = arg->d_name.find('\0'); + if (nul != std::string::npos) + { + arg->d_name.resize(nul); + } } Assert(index == getNumArgs()); diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h index 2553309f1..ee85d5f25 100644 --- a/src/expr/dtype_cons.h +++ b/src/expr/dtype_cons.h @@ -76,7 +76,7 @@ class DTypeConstructor void addArgSelf(std::string selectorName); /** Get the name of this constructor. */ - std::string getName() const; + const std::string& getName() const; /** * Get the constructor operator of this constructor. The diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp index 302e6c51f..e29d229af 100644 --- a/src/expr/dtype_selector.cpp +++ b/src/expr/dtype_selector.cpp @@ -26,7 +26,7 @@ DTypeSelector::DTypeSelector(std::string name, Node selector) Assert(name != ""); } -std::string DTypeSelector::getName() const { return d_name; } +const std::string& DTypeSelector::getName() const { return d_name; } Node DTypeSelector::getSelector() const { @@ -55,7 +55,11 @@ void DTypeSelector::toStream(std::ostream& out) const TypeNode t; if (d_resolved) { - t = getRangeType(); + // don't try to print the range type of null, instead we print null itself. + if (!getType().isNull()) + { + t = getRangeType(); + } } else if (d_selector.isNull()) { diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h index bd0271d90..6a3a7b268 100644 --- a/src/expr/dtype_selector.h +++ b/src/expr/dtype_selector.h @@ -41,7 +41,7 @@ class DTypeSelector DTypeSelector(std::string name, Node selector); /** Get the name of this constructor argument. */ - std::string getName() const; + const std::string& getName() const; /** * Get the selector for this constructor argument; this call is diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c72de9564..bcddc23f5 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -582,6 +582,33 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes( paramTypes, paramReplacements); } + // Check the datatype has been resolved properly. + for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + const DTypeConstructor& c = dt[i]; + TypeNode testerType CVC4_UNUSED = c.getTester().getType(); + Assert(c.isResolved() && testerType.isTester() && testerType[0] == ut) + << "malformed tester in datatype post-resolution"; + TypeNode ctorType CVC4_UNUSED = c.getConstructor().getType(); + Assert(ctorType.isConstructor() + && ctorType.getNumChildren() == c.getNumArgs() + 1 + && ctorType.getRangeType() == ut) + << "malformed constructor in datatype post-resolution"; + // for all selectors... + for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++) + { + const DTypeSelector& a = c[j]; + TypeNode selectorType = a.getType(); + Assert(a.isResolved() && selectorType.isSelector() + && selectorType[0] == ut) + << "malformed selector in datatype post-resolution"; + // This next one's a "hard" check, performed in non-debug builds + // as well; the other ones should all be guaranteed by the + // CVC4::DType class, but this actually needs to be checked. + AlwaysAssert(!selectorType.getRangeType().isFunctionLike()) + << "cannot put function-like things in datatypes"; + } + } } for (NodeManagerListener* nml : d_listeners) |