diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-25 19:04:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-25 19:04:39 -0500 |
commit | 34eac85599875517732d53a5cc1acd3ab60479d1 (patch) | |
tree | ebfa9e493b32aba67d85d6d0bb7a6b468fac5fd4 /src/printer/cvc/cvc_printer.cpp | |
parent | c5eb77b96cd67b8d80ee8901a3f0b5ae7d54aab2 (diff) |
Replace Expr-level datatype with Node-level DType (#4875)
This PR makes two simultaneous changes:
The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API.
Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType.
This PR removes :
ExprManger::mkDatatypeType.
The Expr-level datatype itself. This PR removes all references to its include file.
It also updates one remaining unit test from Expr -> Node.
This PR will enable further removal of other datatype-specific things in the Expr layer.
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 8120d1d88..89b516511 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -211,17 +211,15 @@ void CvcPrinter::toStream( break; case kind::DATATYPE_TYPE: { - const Datatype& dt = - NodeManager::currentNM()->toExprManager()->getDatatypeForIndex( - n.getConst<DatatypeIndexConstant>().getIndex()); - + const DType& dt = NodeManager::currentNM()->getDTypeForIndex( + n.getConst<DatatypeIndexConstant>().getIndex()); if( dt.isTuple() ){ out << '['; for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { if (i > 0) { out << ", "; } - Type t = dt[0][i].getRangeType(); + TypeNode t = dt[0][i].getRangeType(); out << t; } out << ']'; @@ -233,7 +231,7 @@ void CvcPrinter::toStream( if (i > 0) { out << ", "; } - Type t = dt[0][i].getRangeType(); + TypeNode t = dt[0][i].getRangeType(); out << dt[0][i].getSelector() << ":" << t; } out << " #]"; |