Move dispatch of relational operators to their own dispatch functions.

So that top-level `convert_expr_to_smt` can be kept as clean as possible.

Author: NlightNFotis

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -556,6 +556,40 @@ convert_expr_to_smt(const count_trailing_zeros_exprt &count_trailing_zeros)
     count_trailing_zeros.pretty());
 }
 
+static smt_termt convert_expr_to_smt(const greater_than_exprt &greater_than)
+{
+  return convert_relational_to_smt(
+    greater_than,
+    smt_bit_vector_theoryt::unsigned_greater_than,
+    smt_bit_vector_theoryt::signed_greater_than);
+}
+
+static smt_termt
+convert_expr_to_smt(const greater_than_or_equal_exprt &greater_than_or_equal)
+{
+  return convert_relational_to_smt(
+    greater_than_or_equal,
+    smt_bit_vector_theoryt::unsigned_greater_than_or_equal,
+    smt_bit_vector_theoryt::signed_greater_than_or_equal);
+}
+
+static smt_termt convert_expr_to_smt(const less_than_exprt &less_than)
+{
+  return convert_relational_to_smt(
+    less_than,
+    smt_bit_vector_theoryt::unsigned_less_than,
+    smt_bit_vector_theoryt::signed_less_than);
+}
+
+static smt_termt
+convert_expr_to_smt(const less_than_or_equal_exprt &less_than_or_equal)
+{
+  return convert_relational_to_smt(
+    less_than_or_equal,
+    smt_bit_vector_theoryt::unsigned_less_than_or_equal,
+    smt_bit_vector_theoryt::signed_less_than_or_equal);
+}
+
 smt_termt convert_expr_to_smt(const exprt &expr)
 {
   if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
@@ -704,35 +738,23 @@ smt_termt convert_expr_to_smt(const exprt &expr)
 #endif
   if(const auto &greater_than = expr_try_dynamic_cast<greater_than_exprt>(expr))
   {
-    return convert_relational_to_smt(
-      *greater_than,
-      smt_bit_vector_theoryt::unsigned_greater_than,
-      smt_bit_vector_theoryt::signed_greater_than);
+    return convert_expr_to_smt(*greater_than);
   }
   if(
     const auto &greater_than_or_equal =
       expr_try_dynamic_cast<greater_than_or_equal_exprt>(expr))
   {
-    return convert_relational_to_smt(
-      *greater_than_or_equal,
-      smt_bit_vector_theoryt::unsigned_greater_than_or_equal,
-      smt_bit_vector_theoryt::signed_greater_than_or_equal);
+    return convert_expr_to_smt(*greater_than_or_equal);
   }
   if(const auto &less_than = expr_try_dynamic_cast<less_than_exprt>(expr))
   {
-    return convert_relational_to_smt(
-      *less_than,
-      smt_bit_vector_theoryt::unsigned_less_than,
-      smt_bit_vector_theoryt::signed_less_than);
+    return convert_expr_to_smt(*less_than);
   }
   if(
     const auto &less_than_or_equal =
       expr_try_dynamic_cast<less_than_or_equal_exprt>(expr))
   {
-    return convert_relational_to_smt(
-      *less_than_or_equal,
-      smt_bit_vector_theoryt::unsigned_less_than_or_equal,
-      smt_bit_vector_theoryt::signed_less_than_or_equal);
+    return convert_expr_to_smt(*less_than_or_equal);
   }
   if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
   {