From 6861f66d2e2b54fc31d9151b4dbeb2964ea07f94 Mon Sep 17 00:00:00 2001 From: Martin Date: Tue, 3 Oct 2017 01:41:24 +0100 Subject: 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 --- src/printer/smt2/smt2_printer.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/printer/smt2') 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().bvs.size; break; + case kind::FLOATINGPOINT_TO_UBV_TOTAL: + out << "fp.to_ubv_total " + << n.getOperator().getConst().bvs.size; + break; + case kind::FLOATINGPOINT_TO_SBV_TOTAL: + out << "fp.to_sbv_total " + << n.getOperator().getConst().bvs.size; + break; default: out << n.getKind(); } -- cgit v1.2.3