diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-11 11:05:58 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-11 19:05:58 +0000 |
commit | dc679ed380aabc62aadfbb4033c02c5a27ae903c (patch) | |
tree | eae38a0bcbd56104c4e381e84d7f8c724104d365 /src/printer | |
parent | c314b0162c7fa089c400e11bd72c4ca24a26c9d0 (diff) |
Delete Expr layer. (#6117)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 20 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 4 |
2 files changed, 12 insertions, 12 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 715f74c43..280dc7047 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -401,7 +401,7 @@ void CvcPrinter::toStreamNode(std::ostream& out, out << "TUPLE"; } } - else if (t.toType().isRecord()) + else if (t.isRecord()) { const DType& dt = t.getDType(); const DTypeConstructor& recCons = dt[0]; @@ -448,11 +448,11 @@ void CvcPrinter::toStreamNode(std::ostream& out, int sindex; if (n.getKind() == kind::APPLY_SELECTOR) { - sindex = DType::indexOf(opn.toExpr()); + sindex = DType::indexOf(opn); } else { - sindex = dt[0].getSelectorIndexInternal(opn.toExpr()); + sindex = dt[0].getSelectorIndexInternal(opn); } Assert(sindex >= 0); out << sindex; @@ -468,7 +468,7 @@ void CvcPrinter::toStreamNode(std::ostream& out, } break; case kind::APPLY_TESTER: { - Assert(!n.getType().isTuple() && !n.getType().toType().isRecord()); + Assert(!n.getType().isTuple() && !n.getType().isRecord()); op << "is_"; unsigned cindex = DType::indexOf(n.getOperator()); const DType& dt = DType::datatypeOf(n.getOperator()); @@ -733,14 +733,14 @@ void CvcPrinter::toStreamNode(std::ostream& out, unsigned child = 0; while (child < numc) { out << "BVPLUS("; - out << BitVectorType(n.getType().toType()).getSize(); + out << n.getType().getBitVectorSize(); out << ','; toStreamNode(out, n[child], depth, false, lbind); out << ','; ++child; } out << "BVPLUS("; - out << BitVectorType(n.getType().toType()).getSize(); + out << n.getType().getBitVectorSize(); out << ','; toStreamNode(out, n[child], depth, false, lbind); out << ','; @@ -756,7 +756,7 @@ void CvcPrinter::toStreamNode(std::ostream& out, case kind::BITVECTOR_SUB: out << "BVSUB("; Assert(n.getType().isBitVector()); - out << BitVectorType(n.getType().toType()).getSize(); + out << n.getType().getBitVectorSize(); out << ','; toStreamNode(out, n[0], depth, false, lbind); out << ','; @@ -770,14 +770,14 @@ void CvcPrinter::toStreamNode(std::ostream& out, unsigned child = 0; while (child < numc) { out << "BVMULT("; - out << BitVectorType(n.getType().toType()).getSize(); + out << n.getType().getBitVectorSize(); out << ','; toStreamNode(out, n[child], depth, false, lbind); out << ','; ++child; } out << "BVMULT("; - out << BitVectorType(n.getType().toType()).getSize(); + out << n.getType().getBitVectorSize(); out << ','; toStreamNode(out, n[child], depth, false, lbind); out << ','; @@ -813,7 +813,7 @@ void CvcPrinter::toStreamNode(std::ostream& out, case kind::BITVECTOR_SIGN_EXTEND: out << "SX("; toStreamNode(out, n[0], depth, false, lbind); - out << ", " << BitVectorType(n.getType().toType()).getSize() << ')'; + out << ", " << n.getType().getBitVectorSize() << ')'; return; break; case kind::BITVECTOR_ROTATE_LEFT: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index f21683525..7a27794e6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -995,8 +995,8 @@ void Smt2Printer::toStream(std::ostream& out, if(toDepth != 0) { if (n.getKind() == kind::APPLY_TESTER) { - unsigned cindex = DType::indexOf(n.getOperator().toExpr()); - const DType& dt = DType::datatypeOf(n.getOperator().toExpr()); + unsigned cindex = DType::indexOf(n.getOperator()); + const DType& dt = DType::datatypeOf(n.getOperator()); out << "(_ is "; toStream(out, dt[cindex].getConstructor(), |