From cf6bc6c57dd579b8f75b7d20922eda0eaa92b2f7 Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Wed, 3 Dec 2014 21:29:43 -0500 Subject: Floating point infrastructure. Signed-off-by: Morgan Deters --- src/printer/smt2/smt2_printer.cpp | 158 +++++++++++++++++++++++++++++++++++++- 1 file changed, 157 insertions(+), 1 deletion(-) (limited to 'src/printer') diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4f12ed012..b3b548450 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -42,6 +42,7 @@ namespace smt2 { static string smtKindString(Kind k) throw(); static void printBvParameterizedOp(std::ostream& out, TNode n) throw(); +static void printFpParameterizedOp(std::ostream& out, TNode n) throw(); void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw() { @@ -140,6 +141,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case REAL_TYPE: out << "Real"; break; case INTEGER_TYPE: out << "Int"; break; case STRING_TYPE: out << "String"; break; + case ROUNDINGMODE_TYPE: out << "RoundingMode"; break; default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant @@ -149,6 +151,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BITVECTOR_TYPE: out << "(_ BitVec " << n.getConst().size << ")"; break; + case kind::FLOATINGPOINT_TYPE: + out << "(_ FloatingPoint " + << n.getConst().exponent() << " " + << n.getConst().significand() + << ")"; + break; case kind::CONST_BITVECTOR: { const BitVector& bv = n.getConst(); const Integer& x = bv.getValue(); @@ -163,6 +171,20 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // } break; } + case kind::CONST_FLOATINGPOINT: + out << n.getConst().getLiteral(); + break; + case kind::CONST_ROUNDINGMODE: + switch (n.getConst()) { + case roundNearestTiesToEven : out << "roundNearestTiesToEven"; break; + case roundNearestTiesToAway : out << "roundNearestTiesToAway"; break; + case roundTowardPositive : out << "roundTowardPositive"; break; + case roundTowardNegative : out << "roundTowardNegative"; break; + case roundTowardZero : out << "roundTowardZero"; break; + default : + Unreachable("Invalid value of rounding mode constant (%d)",n.getConst()); + } + break; case kind::CONST_BOOLEAN: // the default would print "1" or "0" for bool, that's not correct // for our purposes @@ -448,7 +470,49 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::SET_TYPE: case kind::SINGLETON: out << smtKindString(k) << " "; break; - // datatypes + // fp theory + case kind::FLOATINGPOINT_FP: + case kind::FLOATINGPOINT_EQ: + case kind::FLOATINGPOINT_ABS: + case kind::FLOATINGPOINT_NEG: + case kind::FLOATINGPOINT_PLUS: + case kind::FLOATINGPOINT_SUB: + case kind::FLOATINGPOINT_MULT: + case kind::FLOATINGPOINT_DIV: + case kind::FLOATINGPOINT_FMA: + case kind::FLOATINGPOINT_SQRT: + case kind::FLOATINGPOINT_REM: + case kind::FLOATINGPOINT_RTI: + case kind::FLOATINGPOINT_MIN: + case kind::FLOATINGPOINT_MAX: + case kind::FLOATINGPOINT_LEQ: + case kind::FLOATINGPOINT_LT: + case kind::FLOATINGPOINT_GEQ: + case kind::FLOATINGPOINT_GT: + case kind::FLOATINGPOINT_ISN: + case kind::FLOATINGPOINT_ISSN: + case kind::FLOATINGPOINT_ISZ: + case kind::FLOATINGPOINT_ISINF: + case kind::FLOATINGPOINT_ISNAN: + case kind::FLOATINGPOINT_ISNEG: + case kind::FLOATINGPOINT_ISPOS: + case kind::FLOATINGPOINT_TO_REAL: + out << smtKindString(k) << ' '; break; + + case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: + case kind::FLOATINGPOINT_TO_FP_REAL: + case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + case kind::FLOATINGPOINT_TO_FP_GENERIC: + case kind::FLOATINGPOINT_TO_UBV: + case kind::FLOATINGPOINT_TO_SBV: + printFpParameterizedOp(out, n); + out << ' '; + stillNeedToPrintParams = false; + break; + + // datatypes case kind::APPLY_TYPE_ASCRIPTION: { TypeNode t = TypeNode::fromType(n.getOperator().getConst().getType()); if(t.getKind() == kind::TYPE_CONSTANT && @@ -657,6 +721,46 @@ static string smtKindString(Kind k) throw() { case kind::SET_TYPE: return "Set"; case kind::SINGLETON: return "singleton"; case kind::INSERT: return "insert"; + + // fp theory + case kind::FLOATINGPOINT_FP: return "fp"; + case kind::FLOATINGPOINT_EQ: return "fp.eq"; + case kind::FLOATINGPOINT_ABS: return "fp.abs"; + case kind::FLOATINGPOINT_NEG: return "fp.neg"; + case kind::FLOATINGPOINT_PLUS: return "fp.add"; + case kind::FLOATINGPOINT_SUB: return "fp.sub"; + case kind::FLOATINGPOINT_MULT: return "fp.mul"; + case kind::FLOATINGPOINT_DIV: return "fp.div"; + case kind::FLOATINGPOINT_FMA: return "fp.fma"; + case kind::FLOATINGPOINT_SQRT: return "fp.sqrt"; + case kind::FLOATINGPOINT_REM: return "fp.rem"; + case kind::FLOATINGPOINT_RTI: return "fp.roundToIntegral"; + case kind::FLOATINGPOINT_MIN: return "fp.min"; + case kind::FLOATINGPOINT_MAX: return "fp.max"; + + case kind::FLOATINGPOINT_LEQ: return "fp.leq"; + case kind::FLOATINGPOINT_LT: return "fp.lt"; + case kind::FLOATINGPOINT_GEQ: return "fp.geq"; + case kind::FLOATINGPOINT_GT: return "fp.gt"; + + case kind::FLOATINGPOINT_ISN: return "fp.isNormal"; + case kind::FLOATINGPOINT_ISSN: return "fp.isSubnormal"; + case kind::FLOATINGPOINT_ISZ: return "fp.isZero"; + case kind::FLOATINGPOINT_ISINF: return "fp.isInfinite"; + case kind::FLOATINGPOINT_ISNAN: return "fp.isNaN"; + case kind::FLOATINGPOINT_ISNEG: return "fp.isNegative"; + case kind::FLOATINGPOINT_ISPOS: return "fp.isPositive"; + + case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "to_fp"; + case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "to_fp"; + case kind::FLOATINGPOINT_TO_FP_REAL: return "to_fp"; + case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "to_fp"; + 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_SBV: return "fp.to_sbv"; + case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real"; + default: ; /* fall through */ } @@ -703,6 +807,58 @@ static void printBvParameterizedOp(std::ostream& out, TNode n) throw() { out << ")"; } +static void printFpParameterizedOp(std::ostream& out, TNode n) throw() { + out << "(_ "; + switch(n.getKind()) { + case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + //out << "to_fp_bv " + out << "to_fp " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: + //out << "to_fp_fp " + out << "to_fp " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_FP_REAL: + //out << "to_fp_real " + out << "to_fp " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + //out << "to_fp_signed " + out << "to_fp " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + out << "to_fp_unsigned " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_FP_GENERIC: + out << "to_fp " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_UBV: + out << "fp.to_ubv " + << n.getOperator().getConst().bvs.size; + break; + case kind::FLOATINGPOINT_TO_SBV: + out << "fp.to_sbv " + << n.getOperator().getConst().bvs.size; + break; + default: + out << n.getKind(); + } + out << ")"; +} + + template static bool tryToStream(std::ostream& out, const Command* c) throw(); template -- cgit v1.2.3