diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-22 13:26:26 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-22 13:26:41 -0600 |
| commit | 92d78a10ac24962efad4daf240acf5c5fb265a59 (patch) | |
| tree | 90911f825d9844ea7447993790a76e5f5c68513b /src/printer/cvc/cvc_printer.cpp | |
| parent | 9c14d7c0ccdd220b8ae3d4a39cb5b5810bc28c01 (diff) | |
Fix smt2 and cvc printers for testers when output and input languages are different.
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index b7e1520b7..4f0d4b664 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -398,8 +398,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } } break; - case kind::APPLY_TESTER: - toStream(op, n.getOperator(), depth, types, false); + case kind::APPLY_TESTER: { + Assert( !n.getType().isTuple() && !n.getType().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); + } break; case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: |