diff options
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); } |