Implement arity and string conversions to FP operations

Author: augustomafra

src/ops.cpp

@@ -106,7 +106,39 @@ const std::unordered_map<PrimOp, std::string> primop2str(
       { Exists, "exists" },
       { Apply_Selector, "apply_selector" },
       { Apply_Tester, "apply_tester" },
-      { Apply_Constructor, "apply_constructor" } });
+      { Apply_Constructor, "apply_constructor" },
+      { FPEq, "fp.eq" },
+      { FPAbs, "fp.abs" },
+      { FPNeg, "fp.neg" },
+      { FPAdd, "fp.add" },
+      { FPSub, "fp.sub" },
+      { FPMul, "fp.mul" },
+      { FPDiv, "fp.div" },
+      { FPFma, "fp.fma" },
+      { FPSqrt, "fp.sqrt" },
+      { FPRem, "fp.rem" },
+      { FPRti, "fp.roundToIntegral" },
+      { FPMin, "fp.min" },
+      { FPMax, "fp.max" },
+      { FPLeq, "fp.leq" },
+      { FPLt, "fp.lt" },
+      { FPGeq, "fp.geq" },
+      { FPGt, "fp.gt" },
+      { FPIsNormal, "fp.isNormal" },
+      { FPIsSubNormal, "fp.isSubnormal" },
+      { FPIsZero, "fp.isZero" },
+      { FPIsInf, "fp.isInfinite" },
+      { FPIsNan, "fp.isNaN" },
+      { FPIsNeg, "fp.isNegative" },
+      { FPIsPos, "fp.isPositive" },
+      { IEEEBV_To_FP, "to_fp" },
+      { FP_To_FP, "to_fp" },
+      { Real_To_FP, "to_fp" },
+      { SBV_To_FP, "to_fp" },
+      { UBV_To_FP, "to_fp_unsigned" },
+      { FP_To_UBV, "fp.to_ubv" },
+      { FP_To_SBV, "fp.to_sbv" },
+      { FP_To_REAL, "fp.to_real" } });      
 
 // a map from PrimOp to <minimum arity, maximum arity>
 // TODO: support INT_MAX arity for those that allow it in SMT-LIB
@@ -207,7 +239,39 @@ const std::unordered_map<PrimOp, std::pair<size_t, size_t>> primop2arity(
       { Exists, { 2, 2 } },
       { Apply_Selector, { 2, 2 } },
       { Apply_Tester, { 2, 2 } },
-      { Apply_Constructor, { 2, INT_MAX } } });
+      { Apply_Constructor, { 2, INT_MAX } },
+      { FPEq, {2, 2} },
+      { FPAbs, {1, 1} },
+      { FPNeg, {1, 1} },
+      { FPAdd, {3, 3} },
+      { FPSub, {3, 3} },
+      { FPMul, {3, 3} },
+      { FPDiv, {3, 3} },
+      { FPFma, {4, 4} },
+      { FPSqrt, {2, 2} },
+      { FPRem, {2, 2} },
+      { FPRti, {2, 2} },
+      { FPMin, {2, 2} },
+      { FPMax, {2, 2} },
+      { FPLeq, {2, 2} },
+      { FPLt, {2, 2} },
+      { FPGeq, {2, 2} },
+      { FPGt, {2, 2} },
+      { FPIsNormal, {1, 1} },
+      { FPIsSubNormal, {1, 1} },
+      { FPIsZero, {1, 1} },
+      { FPIsInf, {1, 1} },
+      { FPIsNan, {1, 1} },
+      { FPIsNeg, {1, 1} },
+      { FPIsPos, {1, 1} },
+      { IEEEBV_To_FP, {2, 2} },
+      { FP_To_FP, {2, 2} },
+      { Real_To_FP, {2, 2} },
+      { SBV_To_FP, {2, 2} },
+      { UBV_To_FP, {2, 2} },
+      { FP_To_UBV, {2, 2} },
+      { FP_To_SBV, {2, 2} },
+      { FP_To_REAL, {1, 1} } });
 
 std::string to_string(PrimOp op)
 {