diff options
author | Martin <martin.brain@cs.ox.ac.uk> | 2017-10-03 01:41:24 +0100 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-10-02 17:41:24 -0700 |
commit | 6861f66d2e2b54fc31d9151b4dbeb2964ea07f94 (patch) | |
tree | 4b4e5fe368f5531f0b43045ac339c4b94124c7b1 /src/printer/smt2 | |
parent | fad765a539f8732461340980477ffe3f8c672fb2 (diff) |
Add 5 FP kinds for partial to total fn conversion (#1128)
- Add new kinds for partially defined functions
- Print the new kinds
- Type rules for the new total kinds
- Constant folding and rewrites for the new total kinds
Diffstat (limited to 'src/printer/smt2')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 105e2c0dd..c7d6b34ab 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -899,6 +899,8 @@ static string smtKindString(Kind k) throw() { case kind::FLOATINGPOINT_RTI: return "fp.roundToIntegral"; case kind::FLOATINGPOINT_MIN: return "fp.min"; case kind::FLOATINGPOINT_MAX: return "fp.max"; + case kind::FLOATINGPOINT_MIN_TOTAL: return "fp.min_total"; + case kind::FLOATINGPOINT_MAX_TOTAL: return "fp.max_total"; case kind::FLOATINGPOINT_LEQ: return "fp.leq"; case kind::FLOATINGPOINT_LT: return "fp.lt"; @@ -920,8 +922,11 @@ static string smtKindString(Kind k) throw() { case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "to_fp_unsigned"; case kind::FLOATINGPOINT_TO_FP_GENERIC: return "to_fp_unsigned"; case kind::FLOATINGPOINT_TO_UBV: return "fp.to_ubv"; + case kind::FLOATINGPOINT_TO_UBV_TOTAL: return "fp.to_ubv_total"; case kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv"; + case kind::FLOATINGPOINT_TO_SBV_TOTAL: return "fp.to_sbv_total"; case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real"; + case kind::FLOATINGPOINT_TO_REAL_TOTAL: return "fp.to_real_total"; //string theory case kind::STRING_CONCAT: return "str.++"; @@ -1043,6 +1048,14 @@ static void printFpParameterizedOp(std::ostream& out, TNode n) throw() { out << "fp.to_sbv " << n.getOperator().getConst<FloatingPointToSBV>().bvs.size; break; + case kind::FLOATINGPOINT_TO_UBV_TOTAL: + out << "fp.to_ubv_total " + << n.getOperator().getConst<FloatingPointToUBVTotal>().bvs.size; + break; + case kind::FLOATINGPOINT_TO_SBV_TOTAL: + out << "fp.to_sbv_total " + << n.getOperator().getConst<FloatingPointToSBVTotal>().bvs.size; + break; default: out << n.getKind(); } |