projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2b364e0) | patch
Simplify representation of datatypes at the TypeNode level (#8702)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 3 May 2022 03:03:51 +0000 (22:03 -0500)
committerGitHub <noreply@github.com>
Tue, 3 May 2022 03:03:51 +0000 (03:03 +0000)
commit0f2b2170adbf22f1541ed5be0eebd3fde7b80ba3
treead77f928062c8376a366f30a44dd625d2e6ed0eetree
parent2b364e03e54e06ca00b47812b7abbcedb6165409commit | diff
Simplify representation of datatypes at the TypeNode level (#8702)

They previously were TYPE_CONSTANTs hashed by the index of their DType in the NodeManager. Now they are variables having an attribute that is their index.

This makes datatypes more analogous to uninterpreted sorts, and eliminates the need for an auxiliary DatatypeIndexConstant class.
src/expr/CMakeLists.txt diff | blob | history
src/expr/datatype_index.cpp [deleted file] blob | history
src/expr/datatype_index.h [deleted file] blob | history
src/expr/dtype.cpp diff | blob | history
src/expr/dtype.h diff | blob | history
src/expr/node_manager_attributes.h diff | blob | history
src/expr/node_manager_template.cpp diff | blob | history
src/expr/node_manager_template.h diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/datatypes/kinds diff | blob | history