From d926bb3eab29a966ca2e6070271b05fa65f3c1be Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 11 Oct 2018 20:34:16 -0500
Subject: [PATCH]  Refactor printing of parameterized operators in smt2 (#2609)

---
 src/printer/smt2/smt2_printer.cpp | 191 +++++++++++++-----------------
 1 file 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>
-- 
2.30.2