diff options
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 191 |
1 files changed, 84 insertions, 107 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8473d684d..b71e9d4c4 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -50,9 +50,6 @@ bool isVariant_2_6(Variant v) return v == smt2_6_variant || v == smt2_6_1_variant; } -static void printBvParameterizedOp(std::ostream& out, TNode n); -static void printFpParameterizedOp(std::ostream& out, TNode n); - static void toStreamRational(std::ostream& out, const Rational& r, bool decimal, @@ -276,7 +273,88 @@ void Smt2Printer::toStream(std::ostream& out, case kind::EMPTYSET: out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")"; break; - + case kind::BITVECTOR_EXTRACT_OP: + { + BitVectorExtract p = n.getConst<BitVectorExtract>(); + out << "(_ extract " << p.high << ' ' << p.low << ")"; + break; + } + case kind::BITVECTOR_REPEAT_OP: + out << "(_ repeat " << n.getConst<BitVectorRepeat>().repeatAmount << ")"; + break; + case kind::BITVECTOR_ZERO_EXTEND_OP: + out << "(_ zero_extend " + << n.getConst<BitVectorZeroExtend>().zeroExtendAmount << ")"; + break; + case kind::BITVECTOR_SIGN_EXTEND_OP: + out << "(_ sign_extend " + << n.getConst<BitVectorSignExtend>().signExtendAmount << ")"; + break; + case kind::BITVECTOR_ROTATE_LEFT_OP: + out << "(_ rotate_left " + << n.getConst<BitVectorRotateLeft>().rotateLeftAmount << ")"; + break; + case kind::BITVECTOR_ROTATE_RIGHT_OP: + out << "(_ rotate_right " + << n.getConst<BitVectorRotateRight>().rotateRightAmount << ")"; + break; + case kind::INT_TO_BITVECTOR_OP: + out << "(_ int2bv " << n.getConst<IntToBitVector>().size << ")"; + break; + case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: + // out << "to_fp_bv " + out << "(_ to_fp " + << n.getConst<FloatingPointToFPIEEEBitVector>().t.exponent() << ' ' + << n.getConst<FloatingPointToFPIEEEBitVector>().t.significand() + << ")"; + break; + case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: + // out << "to_fp_fp " + out << "(_ to_fp " + << n.getConst<FloatingPointToFPFloatingPoint>().t.exponent() << ' ' + << n.getConst<FloatingPointToFPFloatingPoint>().t.significand() + << ")"; + break; + case kind::FLOATINGPOINT_TO_FP_REAL_OP: + // out << "to_fp_real " + out << "(_ to_fp " << n.getConst<FloatingPointToFPReal>().t.exponent() + << ' ' << n.getConst<FloatingPointToFPReal>().t.significand() << ")"; + break; + case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: + // out << "to_fp_signed " + out << "(_ to_fp " + << n.getConst<FloatingPointToFPSignedBitVector>().t.exponent() << ' ' + << n.getConst<FloatingPointToFPSignedBitVector>().t.significand() + << ")"; + break; + case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: + out << "(_ to_fp_unsigned " + << n.getConst<FloatingPointToFPUnsignedBitVector>().t.exponent() + << ' ' + << n.getConst<FloatingPointToFPUnsignedBitVector>().t.significand() + << ")"; + break; + case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: + out << "(_ to_fp " << n.getConst<FloatingPointToFPGeneric>().t.exponent() + << ' ' << n.getConst<FloatingPointToFPGeneric>().t.significand() + << ")"; + break; + case kind::FLOATINGPOINT_TO_UBV_OP: + out << "(_ fp.to_ubv " << n.getConst<FloatingPointToUBV>().bvs.size + << ")"; + break; + case kind::FLOATINGPOINT_TO_SBV_OP: + out << "(_ fp.to_sbv " << n.getConst<FloatingPointToSBV>().bvs.size + << ")"; + break; + case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP: + out << "(_ fp.to_ubv_total " + << n.getConst<FloatingPointToUBVTotal>().bvs.size << ")"; + break; + case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP: + out << "(_ fp.to_sbv_total " + << n.getConst<FloatingPointToSBVTotal>().bvs.size << ")"; + break; default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant @@ -592,8 +670,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::BITVECTOR_ROTATE_LEFT: case kind::BITVECTOR_ROTATE_RIGHT: case kind::INT_TO_BITVECTOR: - printBvParameterizedOp(out, n); - out << ' '; + out << n.getOperator() << ' '; stillNeedToPrintParams = false; break; @@ -662,8 +739,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::FLOATINGPOINT_TO_FP_GENERIC: case kind::FLOATINGPOINT_TO_UBV: case kind::FLOATINGPOINT_TO_SBV: - printFpParameterizedOp(out, n); - out << ' '; + out << n.getOperator() << ' '; stillNeedToPrintParams = false; break; @@ -1105,105 +1181,6 @@ static string smtKindString(Kind k, Variant v) return kind::kindToString(k); } -static void printBvParameterizedOp(std::ostream& out, TNode n) -{ - out << "(_ "; - switch(n.getKind()) { - case kind::BITVECTOR_EXTRACT: { - BitVectorExtract p = n.getOperator().getConst<BitVectorExtract>(); - out << "extract " << p.high << ' ' << p.low; - break; - } - case kind::BITVECTOR_REPEAT: - out << "repeat " - << n.getOperator().getConst<BitVectorRepeat>().repeatAmount; - break; - case kind::BITVECTOR_ZERO_EXTEND: - out << "zero_extend " - << n.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount; - break; - case kind::BITVECTOR_SIGN_EXTEND: - out << "sign_extend " - << n.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; - break; - case kind::BITVECTOR_ROTATE_LEFT: - out << "rotate_left " - << n.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount; - break; - case kind::BITVECTOR_ROTATE_RIGHT: - out << "rotate_right " - << n.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount; - break; - case kind::INT_TO_BITVECTOR: - out << "int2bv " - << n.getOperator().getConst<IntToBitVector>().size; - break; - default: - out << n.getKind(); - } - out << ")"; -} - -static void printFpParameterizedOp(std::ostream& out, TNode n) -{ - out << "(_ "; - switch(n.getKind()) { - case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: - //out << "to_fp_bv " - out << "to_fp " - << n.getOperator().getConst<FloatingPointToFPIEEEBitVector>().t.exponent() << ' ' - << n.getOperator().getConst<FloatingPointToFPIEEEBitVector>().t.significand(); - break; - case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: - //out << "to_fp_fp " - out << "to_fp " - << n.getOperator().getConst<FloatingPointToFPFloatingPoint>().t.exponent() << ' ' - << n.getOperator().getConst<FloatingPointToFPFloatingPoint>().t.significand(); - break; - case kind::FLOATINGPOINT_TO_FP_REAL: - //out << "to_fp_real " - out << "to_fp " - << n.getOperator().getConst<FloatingPointToFPReal>().t.exponent() << ' ' - << n.getOperator().getConst<FloatingPointToFPReal>().t.significand(); - break; - case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: - //out << "to_fp_signed " - out << "to_fp " - << n.getOperator().getConst<FloatingPointToFPSignedBitVector>().t.exponent() << ' ' - << n.getOperator().getConst<FloatingPointToFPSignedBitVector>().t.significand(); - break; - case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: - out << "to_fp_unsigned " - << n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>().t.exponent() << ' ' - << n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>().t.significand(); - break; - case kind::FLOATINGPOINT_TO_FP_GENERIC: - out << "to_fp " - << n.getOperator().getConst<FloatingPointToFPGeneric>().t.exponent() << ' ' - << n.getOperator().getConst<FloatingPointToFPGeneric>().t.significand(); - break; - case kind::FLOATINGPOINT_TO_UBV: - out << "fp.to_ubv " - << n.getOperator().getConst<FloatingPointToUBV>().bvs.size; - break; - case kind::FLOATINGPOINT_TO_SBV: - 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(); - } - out << ")"; -} - template <class T> static bool tryToStream(std::ostream& out, const Command* c); template <class T> |