projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 956ffda) | patch
Updates not related to creation for eliminating Expr-level datatype (#4838)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 6 Aug 2020 18:41:24 +0000 (13:41 -0500)
committerGitHub <noreply@github.com>
Thu, 6 Aug 2020 18:41:24 +0000 (13:41 -0500)
commit816d5e7624c9d088c469f7e23d11394f5b385b84
treebbb39e63a6b00c45be028d9be51b5a22cc640ddbtree
parent956ffda5632b388a887003a5e030696091339bd2commit | diff
Updates not related to creation for eliminating Expr-level datatype (#4838)

This updates remaining uses of the Expr-level Datatype that are not related to their creation / memory management in ExprManager.

This required updating a unit test from Expr -> Node.
13 files changed:
src/expr/datatype.cpp diff | blob | history
src/expr/dtype_cons.cpp diff | blob | history
src/expr/symbol_table.cpp diff | blob | history
src/expr/type.cpp diff | blob | history
src/expr/type.h diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/expr/type_node.h diff | blob | history
src/preprocessing/passes/unconstrained_simplifier.cpp diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
test/unit/util/datatype_black.h diff | blob | history