diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-16 11:56:39 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-16 09:56:39 -0800 |
| commit | c101a6b42d1f14bc750fb2328ddd83261148d7ae (patch) | |
| tree | 3155d3edd7c26690088cbc9a223de5c854941475 /src/printer/smt2/smt2_printer.cpp | |
| parent | d15d44b3c91b5be2c19adac292f137d2a67eb848 (diff) | |
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.
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 006895df7..f0a1e740f 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -21,6 +21,7 @@ #include <typeinfo> #include <vector> +#include "expr/dtype.h" #include "expr/node_manager_attributes.h" #include "options/bv_options.h" #include "options/language.h" @@ -246,7 +247,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::DATATYPE_TYPE: { - const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( + const DType& dt = (NodeManager::currentNM()->getDTypeForIndex( n.getConst<DatatypeIndexConstant>().getIndex())); if (dt.isTuple()) { |