From 03ac764e0131c209633588e685fdc1f82dba263e Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 21 Dec 2024 21:44:14 +0000
Subject: [PATCH] SMT2 parser: add abbreviated versions of the rounding modes

This adds RNE, RNA, RTP, RTN, RTZ as abbreviated versions of the rounding
modes.
---
 src/solvers/smt2/smt2_parser.cpp | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
index add14229d3f..c952506111f 100644
--- a/src/solvers/smt2/smt2_parser.cpp
+++ b/src/solvers/smt2/smt2_parser.cpp
@@ -1088,25 +1088,49 @@ void smt2_parsert::setup_expressions()
     return from_integer(ieee_floatt::ROUND_TO_EVEN, unsignedbv_typet(32));
   };
 
+  expressions["RNE"] = [] {
+    // we encode as 32-bit unsignedbv
+    return from_integer(ieee_floatt::ROUND_TO_EVEN, unsignedbv_typet(32));
+  };
+
   expressions["roundNearestTiesToAway"] = [this]() -> exprt {
     throw error("unsupported rounding mode");
   };
 
+  expressions["RNA"] = [this]() -> exprt {
+    throw error("unsupported rounding mode");
+  };
+
   expressions["roundTowardPositive"] = [] {
     // we encode as 32-bit unsignedbv
     return from_integer(ieee_floatt::ROUND_TO_PLUS_INF, unsignedbv_typet(32));
   };
 
+  expressions["RTP"] = [] {
+    // we encode as 32-bit unsignedbv
+    return from_integer(ieee_floatt::ROUND_TO_PLUS_INF, unsignedbv_typet(32));
+  };
+
   expressions["roundTowardNegative"] = [] {
     // we encode as 32-bit unsignedbv
     return from_integer(ieee_floatt::ROUND_TO_MINUS_INF, unsignedbv_typet(32));
   };
 
+  expressions["RTN"] = [] {
+    // we encode as 32-bit unsignedbv
+    return from_integer(ieee_floatt::ROUND_TO_MINUS_INF, unsignedbv_typet(32));
+  };
+
   expressions["roundTowardZero"] = [] {
     // we encode as 32-bit unsignedbv
     return from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32));
   };
 
+  expressions["RTZ"] = [] {
+    // we encode as 32-bit unsignedbv
+    return from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32));
+  };
+
   expressions["lambda"] = [this] { return lambda_expression(); };
   expressions["let"] = [this] { return let_expression(); };
   expressions["exists"] = [this] { return quantifier_expression(ID_exists); };