projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c3620b9) | patch
Fix parametric datatype instantiation (#4493)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 May 2020 12:47:24 +0000 (07:47 -0500)
committerGitHub <noreply@github.com>
Wed, 20 May 2020 12:47:24 +0000 (07:47 -0500)
commit6ae3e7167132e9060257d4f3d876f4e49e67b2a8
tree59c18c32abcded14e6694468f2dae0b4c486203ctree
parentc3620b97ea7fac5dd16f5bd99f8dd10226c60d92commit | 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.
src/expr/dtype_cons.cpp diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/expr/type_node.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/datatypes/parametric-alt-list.cvc [new file with mode: 0644] blob