diff options
Diffstat (limited to 'src/printer/smt2')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6fdbd4adb..13a64a2c3 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -138,9 +138,9 @@ void Smt2Printer::toStream(std::ostream& out, break; case kind::BITVECTOR_TYPE: if(d_variant == sygus_variant ){ - out << "(BitVec " << n.getConst<BitVectorSize>().size << ")"; + out << "(BitVec " << n.getConst<BitVectorSize>().d_size << ")"; }else{ - out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")"; + out << "(_ BitVec " << n.getConst<BitVectorSize>().d_size << ")"; } break; case kind::FLOATINGPOINT_TYPE: @@ -270,30 +270,31 @@ void Smt2Printer::toStream(std::ostream& out, case kind::BITVECTOR_EXTRACT_OP: { BitVectorExtract p = n.getConst<BitVectorExtract>(); - out << "(_ extract " << p.high << ' ' << p.low << ")"; + out << "(_ extract " << p.d_high << ' ' << p.d_low << ")"; break; } case kind::BITVECTOR_REPEAT_OP: - out << "(_ repeat " << n.getConst<BitVectorRepeat>().repeatAmount << ")"; + out << "(_ repeat " << n.getConst<BitVectorRepeat>().d_repeatAmount + << ")"; break; case kind::BITVECTOR_ZERO_EXTEND_OP: out << "(_ zero_extend " - << n.getConst<BitVectorZeroExtend>().zeroExtendAmount << ")"; + << n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount << ")"; break; case kind::BITVECTOR_SIGN_EXTEND_OP: out << "(_ sign_extend " - << n.getConst<BitVectorSignExtend>().signExtendAmount << ")"; + << n.getConst<BitVectorSignExtend>().d_signExtendAmount << ")"; break; case kind::BITVECTOR_ROTATE_LEFT_OP: out << "(_ rotate_left " - << n.getConst<BitVectorRotateLeft>().rotateLeftAmount << ")"; + << n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount << ")"; break; case kind::BITVECTOR_ROTATE_RIGHT_OP: out << "(_ rotate_right " - << n.getConst<BitVectorRotateRight>().rotateRightAmount << ")"; + << n.getConst<BitVectorRotateRight>().d_rotateRightAmount << ")"; break; case kind::INT_TO_BITVECTOR_OP: - out << "(_ int2bv " << n.getConst<IntToBitVector>().size << ")"; + out << "(_ int2bv " << n.getConst<IntToBitVector>().d_size << ")"; break; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: // out << "to_fp_bv " @@ -334,20 +335,20 @@ void Smt2Printer::toStream(std::ostream& out, << ")"; break; case kind::FLOATINGPOINT_TO_UBV_OP: - out << "(_ fp.to_ubv " << n.getConst<FloatingPointToUBV>().bvs.size + out << "(_ fp.to_ubv " << n.getConst<FloatingPointToUBV>().bvs.d_size << ")"; break; case kind::FLOATINGPOINT_TO_SBV_OP: - out << "(_ fp.to_sbv " << n.getConst<FloatingPointToSBV>().bvs.size + out << "(_ fp.to_sbv " << n.getConst<FloatingPointToSBV>().bvs.d_size << ")"; break; case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP: out << "(_ fp.to_ubv_total " - << n.getConst<FloatingPointToUBVTotal>().bvs.size << ")"; + << n.getConst<FloatingPointToUBVTotal>().bvs.d_size << ")"; break; case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP: out << "(_ fp.to_sbv_total " - << n.getConst<FloatingPointToSBVTotal>().bvs.size << ")"; + << n.getConst<FloatingPointToSBVTotal>().bvs.d_size << ")"; break; default: // fall back on whatever operator<< does on underlying type; we |