diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-01-22 15:48:48 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-22 15:48:48 -0600 |
commit | e5f4e2c0c1dc79f9940ddb4fcdbf04d6cffe98f5 (patch) | |
tree | ce24ee483caef8bf63ba33b2460f551d83925cc1 /src/printer | |
parent | af1714ddc446fe6e239852374f5f628302980488 (diff) |
Fix tuple and record CVC printing (#2818)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 26 |
1 files changed, 22 insertions, 4 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index e6ff02f10..36d2ddfb7 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -407,12 +407,30 @@ void CvcPrinter::toStream( case kind::APPLY_SELECTOR_TOTAL: { TypeNode t = n[0].getType(); Node opn = n.getOperator(); - if( t.isTuple() ){ + if (t.isTuple() || t.isRecord()) + { toStream(out, n[0], depth, types, true); + out << '.'; const Datatype& dt = ((DatatypeType)t.toType()).getDatatype(); - int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() ); - Assert( sindex>=0 ); - out << '.' << sindex; + if (t.isTuple()) + { + int sindex; + if (n.getKind() == kind::APPLY_SELECTOR) + { + sindex = Datatype::indexOf(opn.toExpr()); + } + else + { + sindex = dt[0].getSelectorIndexInternal(opn.toExpr()); + } + Assert(sindex >= 0); + out << sindex; + } + else + { + toStream(out, opn, depth, types, false); + } + return; }else{ toStream(op, opn, depth, types, false); } |