diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-06 13:41:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-06 13:41:24 -0500 |
commit | 816d5e7624c9d088c469f7e23d11394f5b385b84 (patch) | |
tree | bbb39e63a6b00c45be028d9be51b5a22cc640ddb /src/printer/cvc | |
parent | 956ffda5632b388a887003a5e030696091339bd2 (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.
Diffstat (limited to 'src/printer/cvc')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 68 |
1 files changed, 33 insertions, 35 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 9ec522141..243592456 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -214,23 +214,26 @@ void CvcPrinter::toStream( const Datatype& dt = NodeManager::currentNM()->toExprManager()->getDatatypeForIndex( n.getConst<DatatypeIndexConstant>().getIndex()); + if( dt.isTuple() ){ out << '['; for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { if (i > 0) { out << ", "; } - Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType(); + Type t = dt[0][i].getRangeType(); out << t; } out << ']'; - }else if( dt.isRecord() ){ + } + else if (dt.isRecord()) + { out << "[# "; for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { if (i > 0) { out << ", "; } - Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType(); + Type t = dt[0][i].getRangeType(); out << dt[0][i].getSelector() << ":" << t; } out << " #]"; @@ -414,18 +417,17 @@ void CvcPrinter::toStream( } else if (t.toType().isRecord()) { - const Record& rec = static_cast<DatatypeType>(t.toType()).getRecord(); + const DType& dt = t.getDType(); + const DTypeConstructor& recCons = dt[0]; out << "(# "; - TNode::iterator i = n.begin(); - bool first = true; - const Record::FieldVector& fields = rec.getFields(); - for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) { - if(!first) { + for (size_t i = 0, nargs = recCons.getNumArgs(); i < nargs; i++) + { + if (i != 0) + { out << ", "; } - out << (*j).first << " := "; - toStream(out, *i, depth, types, false); - first = false; + out << recCons[i].getName() << " := "; + toStream(out, n[i], depth, types, false); } out << " #)"; return; @@ -450,18 +452,17 @@ void CvcPrinter::toStream( { toStream(op, opn, depth, types, false); } - else if (t.isTuple() - || DatatypeType(t.toType()).isRecord()) + else if (t.isTuple() || t.isRecord()) { toStream(out, n[0], depth, types, true); out << '.'; - const Datatype& dt = ((DatatypeType)t.toType()).getDatatype(); + const DType& dt = t.getDType(); if (t.isTuple()) { int sindex; if (n.getKind() == kind::APPLY_SELECTOR) { - sindex = Datatype::indexOf(opn.toExpr()); + sindex = DType::indexOf(opn.toExpr()); } else { @@ -483,9 +484,9 @@ void CvcPrinter::toStream( case kind::APPLY_TESTER: { Assert(!n.getType().isTuple() && !n.getType().toType().isRecord()); op << "is_"; - unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); - const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); - toStream(op, Node::fromExpr(dt[cindex].getConstructor()), depth, types, false); + unsigned cindex = DType::indexOf(n.getOperator()); + const DType& dt = DType::datatypeOf(n.getOperator()); + toStream(op, dt[cindex].getConstructor(), depth, types, false); } break; case kind::CONSTRUCTOR_TYPE: @@ -1515,7 +1516,7 @@ static void toStream(std::ostream& out, { const vector<Type>& datatypes = c->getDatatypes(); Assert(!datatypes.empty() && datatypes[0].isDatatype()); - const Datatype& dt0 = DatatypeType(datatypes[0]).getDatatype(); + const DType& dt0 = TypeNode::fromType(datatypes[0]).getDType(); //do not print tuple/datatype internal declarations if (datatypes.size() != 1 || (!dt0.isTuple() && !dt0.isRecord())) { @@ -1526,7 +1527,7 @@ static void toStream(std::ostream& out, if(! firstDatatype) { out << ',' << endl; } - const Datatype& dt = DatatypeType(t).getDatatype(); + const DType& dt = TypeNode::fromType(t).getDType(); out << " " << dt.getName(); if(dt.isParametric()) { out << '['; @@ -1539,31 +1540,28 @@ static void toStream(std::ostream& out, out << ']'; } out << " = "; - bool firstConstructor = true; - for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) { - if(! firstConstructor) { + for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) + { + const DTypeConstructor& cons = dt[j]; + if (j != 0) + { out << " | "; } - firstConstructor = false; - const DatatypeConstructor& cons = *j; out << cons.getName(); if (cons.getNumArgs() > 0) { out << '('; - bool firstSelector = true; - for (DatatypeConstructor::const_iterator k = cons.begin(); - k != cons.end(); - ++k) + for (size_t k = 0, nargs = cons.getNumArgs(); k < nargs; k++) { - if(! firstSelector) { + if (k != 0) + { out << ", "; } - firstSelector = false; - const DatatypeConstructorArg& selector = *k; - Type tr = SelectorType(selector.getType()).getRangeType(); + const DTypeSelector& selector = cons[k]; + TypeNode tr = selector.getRangeType(); if (tr.isDatatype()) { - const Datatype& sdt = DatatypeType(tr).getDatatype(); + const DType& sdt = tr.getDType(); out << selector.getName() << ": " << sdt.getName(); } else |