Move Datatype management to ExprManager (#3568)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 16 Dec 2019 17:56:39 +0000 (11:56 -0600)
committerAndres Noetzli <andres.noetzli@gmail.com>
Mon, 16 Dec 2019 17:56:39 +0000 (09:56 -0800)
commitc101a6b42d1f14bc750fb2328ddd83261148d7ae
tree3155d3edd7c26690088cbc9a223de5c854941475
parentd15d44b3c91b5be2c19adac292f137d2a67eb848
Move Datatype management to ExprManager (#3568)

This is further work towards decoupling the Expr layer from the Node layer.

This commit makes it so that ExprManager does memory management for Datatype while NodeManager maintains a list of DType.

As a reminder, the ownership policy (and level of indirection through DatatypeIndex) is necessary due to not being able to store Datatype within Node since this leads to circular dependencies in the Node AST.
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/node_manager.cpp
src/expr/node_manager.h
src/expr/type.cpp
src/printer/cvc/cvc_printer.cpp
src/printer/smt2/smt2_printer.cpp