Use TypeNode in UninterpretedConstant (#4748)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 15 Jul 2020 15:27:13 +0000 (08:27 -0700)
committerGitHub <noreply@github.com>
Wed, 15 Jul 2020 15:27:13 +0000 (10:27 -0500)
commit9975291763425e0aba9ae135ccd86d1fbc176d9d
tree9d8c1775df573fed99874dbea08273290c31ab35
parenta482635216017b0d558229f2339c663cf58f8d23
Use TypeNode in UninterpretedConstant (#4748)

This commit changes UninterpretedConstant to use TypeNode instead of
Type.
12 files changed:
src/api/cvc4cpp.cpp
src/expr/uninterpreted_constant.cpp
src/expr/uninterpreted_constant.h
src/theory/builtin/theory_builtin_type_rules.h
src/theory/builtin/type_enumerator.h
src/theory/datatypes/datatypes_rewriter.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/type_enumerator.cpp
src/theory/rewriter.cpp
test/unit/theory/theory_sets_type_enumerator_white.h
test/unit/theory/type_enumerator_white.h
test/unit/util/array_store_all_white.h