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/cvc | |
| parent | c314b0162c7fa089c400e11bd72c4ca24a26c9d0 (diff) | |
Delete Expr layer. (#6117)
Diffstat (limited to 'src/printer/cvc')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 20 |
1 files changed, 10 insertions, 10 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: |