diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-09 12:50:31 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-09 17:50:31 +0000 |
commit | 9dc6deed6147b7a53a65d727cc7afd7b1b6c2c19 (patch) | |
tree | 2aa8ff76f1900764d4d8a680b564ad193c729f69 /src/printer/smt2/smt2_printer.cpp | |
parent | cd34574f476827c11e1f0d9a33141a04b5175696 (diff) |
Fixes related to printing tuples, define-fun commands in smt2 (#6679)
This PR fixes some initial issues with printing datatypes in smt2.
It does not yet address further issues on printing define-fun as a result of dump=raw-benchmark, which requires deeper refactoring of the implementation of the API / SmtEngine.
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 04a57e0e9..1f64bd23d 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 << "(...)"; } |