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/cvc | |
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/cvc')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 30 |
1 files changed, 18 insertions, 12 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 22a491af5..f8448f1e9 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -24,11 +24,12 @@ #include <typeinfo> #include <vector> -#include "expr/expr.h" // for ExprSetDepth etc.. -#include "expr/node_manager_attributes.h" // for VarNameAttr -#include "options/language.h" // for LANG_AST -#include "printer/dagification_visitor.h" +#include "expr/dtype.h" +#include "expr/expr.h" // for ExprSetDepth etc.. +#include "expr/node_manager_attributes.h" // for VarNameAttr +#include "options/language.h" // for LANG_AST #include "options/smt_options.h" +#include "printer/dagification_visitor.h" #include "smt/command.h" #include "smt/smt_engine.h" #include "smt_util/node_visitor.h" @@ -179,7 +180,9 @@ void CvcPrinter::toStream( break; case kind::DATATYPE_TYPE: { - const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() )); + const Datatype& dt = + NodeManager::currentNM()->toExprManager()->getDatatypeForIndex( + n.getConst<DatatypeIndexConstant>().getIndex()); if( dt.isTuple() ){ out << '['; for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { @@ -347,14 +350,17 @@ void CvcPrinter::toStream( // DATATYPES case kind::PARAMETRIC_DATATYPE: { - const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n[0].getConst< DatatypeIndexConstant >().getIndex() )); - out << dt.getName() << '['; - for(unsigned i = 1; i < n.getNumChildren(); ++i) { - if(i > 1) { - out << ','; - } - out << n[i]; + const DType& dt = NodeManager::currentNM()->getDTypeForIndex( + n[0].getConst<DatatypeIndexConstant>().getIndex()); + out << dt.getName() << '['; + for (unsigned i = 1; i < n.getNumChildren(); ++i) + { + if (i > 1) + { + out << ','; } + out << n[i]; + } out << ']'; } return; |