diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-20 07:47:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-20 07:47:24 -0500 |
commit | 6ae3e7167132e9060257d4f3d876f4e49e67b2a8 (patch) | |
tree | 59c18c32abcded14e6694468f2dae0b4c486203c /src | |
parent | c3620b97ea7fac5dd16f5bd99f8dd10226c60d92 (diff) |
Fix parametric datatype instantiation (#4493)
A bug was introduced when adding the Node-level datatype implementation in d803e7f. The code did not probably get the arity of a sort constructor. This adds TypeNode::getSortConstructorArity and uses it during parametric datatype type resolution.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/dtype_cons.cpp | 15 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 7 | ||||
-rw-r--r-- | src/expr/type_node.h | 3 |
3 files changed, 24 insertions, 1 deletions
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 428097d54..8923667b1 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -480,6 +480,7 @@ bool DTypeConstructor::resolve( NodeManager* nm = NodeManager::currentNM(); size_t index = 0; std::vector<TypeNode> argTypes; + Trace("datatypes-init") << "Initialize constructor " << d_name << std::endl; for (std::shared_ptr<DTypeSelector> arg : d_args) { std::string argName = arg->d_name; @@ -488,9 +489,12 @@ bool DTypeConstructor::resolve( { // the unresolved type wasn't created here; do name resolution std::string typeName = argName.substr(argName.find('\0') + 1); + Trace("datatypes-init") + << " - selector, typeName is " << typeName << std::endl; argName.resize(argName.find('\0')); if (typeName == "") { + Trace("datatypes-init") << " ...self selector" << std::endl; range = self; arg->d_selector = nm->mkSkolem( argName, @@ -504,11 +508,14 @@ bool DTypeConstructor::resolve( resolutions.find(typeName); if (j == resolutions.end()) { + Trace("datatypes-init") + << " ...failed to resolve selector" << std::endl; // failed to resolve selector return false; } else { + Trace("datatypes-init") << " ...resolved selector" << std::endl; range = (*j).second; arg->d_selector = nm->mkSkolem( argName, @@ -523,6 +530,8 @@ bool DTypeConstructor::resolve( // the type for the selector already exists; may need // complex-type substitution range = arg->d_selector.getType(); + Trace("datatypes-init") + << " - null selector, range = " << range << std::endl; if (!placeholders.empty()) { range = range.substitute(placeholders.begin(), @@ -530,10 +539,14 @@ bool DTypeConstructor::resolve( replacements.begin(), replacements.end()); } + Trace("datatypes-init") + << " ...range after placeholder replacement " << range << std::endl; if (!paramTypes.empty()) { range = doParametricSubstitution(range, paramTypes, paramReplacements); } + Trace("datatypes-init") + << " ...range after parametric substitution " << range << std::endl; arg->d_selector = nm->mkSkolem( argName, nm->mkSelectorType(self, range), @@ -597,7 +610,7 @@ TypeNode DTypeConstructor::doParametricSubstitution( } for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i) { - if (paramTypes[i].getNumChildren() + 1 == origChildren.size()) + if (paramTypes[i].getSortConstructorArity() == origChildren.size()) { TypeNode tn = paramTypes[i].instantiateSortConstructor(origChildren); if (range == tn) diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index e6c695dd6..110db6162 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -459,9 +459,16 @@ TypeNode TypeNode::instantiateParametricDatatype( return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes); } +uint64_t TypeNode::getSortConstructorArity() const +{ + Assert(isSortConstructor() && hasAttribute(expr::SortArityAttr())); + return getAttribute(expr::SortArityAttr()); +} + TypeNode TypeNode::instantiateSortConstructor( const std::vector<TypeNode>& params) const { + Assert(isSortConstructor()); return NodeManager::currentNM()->mkSort(*this, params); } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 6de4a0271..70392fb01 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -674,6 +674,9 @@ public: /** Is this a sort constructor kind */ bool isSortConstructor() const; + /** Get sort constructor arity */ + uint64_t getSortConstructorArity() const; + /** * Instantiate a sort constructor type. The type on which this method is * called should be a sort constructor type whose parameter list is the |