diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-13 11:07:16 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-13 11:07:16 -0600 |
commit | c0a7095f13547ac0c0d4c92670000ca875b7c349 (patch) | |
tree | 6a8eb67f79fb83b8e27e4837079c1df829c16e67 /src/printer | |
parent | 9acb8b8d0d529c4780191660f8ef2b51e4a92926 (diff) |
Eliminate Expr-level calls in TypeNode (#3562)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index b11ee77a7..22a491af5 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -373,8 +373,10 @@ void CvcPrinter::toStream( if( n.getNumChildren()==1 ){ out << "TUPLE"; } - }else if( t.isRecord() ){ - const Record& rec = t.getRecord(); + } + else if (t.toType().isRecord()) + { + const Record& rec = static_cast<DatatypeType>(t.toType()).getRecord(); out << "(# "; TNode::iterator i = n.begin(); bool first = true; @@ -389,7 +391,9 @@ void CvcPrinter::toStream( } out << " #)"; return; - }else{ + } + else + { toStream(op, n.getOperator(), depth, types, false); if (n.getNumChildren() == 0) { @@ -404,7 +408,12 @@ void CvcPrinter::toStream( case kind::APPLY_SELECTOR_TOTAL: { TypeNode t = n[0].getType(); Node opn = n.getOperator(); - if (t.isTuple() || t.isRecord()) + if (!t.isDatatype()) + { + toStream(op, opn, depth, types, false); + } + else if (t.isTuple() + || DatatypeType(t.toType()).isRecord()) { toStream(out, n[0], depth, types, true); out << '.'; @@ -434,7 +443,7 @@ void CvcPrinter::toStream( } break; case kind::APPLY_TESTER: { - Assert(!n.getType().isTuple() && !n.getType().isRecord()); + 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()); |