diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2021-06-11 10:52:53 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2021-06-11 10:52:53 -0500 |
commit | ee73990f8d383fc3848a44460b537667c4a2ce25 (patch) | |
tree | ba6413da7b93e882da73027c710f7f43d7dd8f76 /src/printer/smt2/smt2_printer.cpp | |
parent | 60007a036188c955d62de18c41be0b97f9b8413e (diff) | |
parent | f10087c3b347da6ef625a2ad92846551ad324d73 (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 52 |
1 files changed, 37 insertions, 15 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 426f60a60..076093bce 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -951,10 +951,43 @@ void Smt2Printer::toStream(std::ostream& out, return; break; } - case kind::APPLY_TESTER: case kind::APPLY_SELECTOR: - case kind::APPLY_SELECTOR_TOTAL: + { + Node op = n.getOperator(); + const DType& dt = DType::datatypeOf(op); + if (dt.isTuple()) + { + stillNeedToPrintParams = false; + out << "(_ tupSel " << DType::indexOf(op) << ") "; + } + } + break; + case kind::APPLY_TESTER: + { + stillNeedToPrintParams = false; + Node op = n.getOperator(); + size_t cindex = DType::indexOf(op); + const DType& dt = DType::datatypeOf(op); + out << "(_ is "; + toStream( + out, dt[cindex].getConstructor(), toDepth < 0 ? toDepth : toDepth - 1); + out << ") "; + } + break; case kind::APPLY_UPDATER: + { + Node op = n.getOperator(); + size_t index = DType::indexOf(op); + const DType& dt = DType::datatypeOf(op); + size_t cindex = DType::cindexOf(op); + out << "(_ update "; + toStream(out, + dt[cindex][index].getSelector(), + toDepth < 0 ? toDepth : toDepth - 1); + out << ") "; + } + break; + case kind::APPLY_SELECTOR_TOTAL: case kind::PARAMETRIC_DATATYPE: break; // separation logic @@ -1037,19 +1070,8 @@ void Smt2Printer::toStream(std::ostream& out, if( n.getMetaKind() == kind::metakind::PARAMETERIZED && stillNeedToPrintParams ) { if(toDepth != 0) { - if (n.getKind() == kind::APPLY_TESTER) - { - unsigned cindex = DType::indexOf(n.getOperator()); - const DType& dt = DType::datatypeOf(n.getOperator()); - out << "(_ is "; - toStream(out, - dt[cindex].getConstructor(), - toDepth < 0 ? toDepth : toDepth - 1); - out << ")"; - }else{ - toStream( - out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind); - } + toStream( + out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind); } else { out << "(...)"; } |