Add floating point support to incremental SMT2 solver via bit-blasting

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -14,6 +14,7 @@
 #include <util/std_expr.h>
 #include <util/string_constant.h>
 
+#include <solvers/floatbv/float_bv.h>
 #include <solvers/prop/literal_expr.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/theories/smt_array_theory.h>
@@ -96,6 +97,12 @@ static smt_sortt convert_type_to_smt_sort(const array_typet &type)
     convert_type_to_smt_sort(type.element_type())};
 }
 
+static smt_sortt convert_type_to_smt_sort(const floatbv_typet &type)
+{
+  // Convert floating-point to bitvector for bit-blasting
+  return smt_bit_vector_sortt{type.get_width()};
+}
+
 smt_sortt convert_type_to_smt_sort(const typet &type)
 {
   if(const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
@@ -104,6 +111,10 @@ smt_sortt convert_type_to_smt_sort(const typet &type)
   }
   if(const auto bitvector_type = type_try_dynamic_cast<bitvector_typet>(type))
   {
+    if(const auto floatbv_type = type_try_dynamic_cast<floatbv_typet>(type))
+    {
+      return convert_type_to_smt_sort(*floatbv_type);
+    }
     return convert_type_to_smt_sort(*bitvector_type);
   }
   if(const auto array_type = type_try_dynamic_cast<array_typet>(type))
@@ -184,9 +195,9 @@ static smt_termt make_bitvector_resize_cast(
   }
   if(type_try_dynamic_cast<floatbv_typet>(to_type))
   {
-    UNIMPLEMENTED_FEATURE(
-      "Generation of SMT formula for type cast to floating-point bitvector "
-      "type: " +
+    UNREACHABLE_BECAUSE(
+      "Type cast to floating-point bitvector should have been lowered to "
+      "bitvector operations. Target type: " +
       to_type.pretty());
   }
   const std::size_t from_width = from_type.get_width();
@@ -272,8 +283,11 @@ static smt_termt convert_expr_to_smt(
   const floatbv_typecast_exprt &float_cast,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for floating point type cast expression: " +
+  // Floating-point operations should be lowered to bitvector operations
+  // before reaching this point. If we get here, it means the lowering failed.
+  UNREACHABLE_BECAUSE(
+    "Floating point type cast expression should have been lowered to "
+    "bitvector operations: " +
     float_cast.pretty());
 }
 
@@ -535,17 +549,19 @@ static smt_termt convert_expr_to_smt(
   const ieee_float_equal_exprt &float_equal,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for floating point equality expression: " +
+  UNREACHABLE_BECAUSE(
+    "Floating point equality expression should have been lowered to "
+    "bitvector operations: " +
     float_equal.pretty());
 }
 
 static smt_termt convert_expr_to_smt(
   const ieee_float_notequal_exprt &float_not_equal,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for floating point not equal expression: " +
+  UNREACHABLE_BECAUSE(
+    "Floating point not equal expression should have been lowered to "
+    "bitvector operations: " +
     float_not_equal.pretty());
 }
 
@@ -785,8 +801,9 @@ static smt_termt convert_expr_to_smt(
 {
   // This case includes the floating point plus, minus, division and
   // multiplication operations.
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for floating point operation expression: " +
+  UNREACHABLE_BECAUSE(
+    "Floating point operation expression should have been lowered to "
+    "bitvector operations: " +
     float_operation.pretty());
 }
 
@@ -1158,35 +1175,39 @@ static smt_termt convert_expr_to_smt(
   const isnan_exprt &is_nan_expr,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is not a number expression: " +
+  UNREACHABLE_BECAUSE(
+    "Is not a number expression should have been lowered to "
+    "bitvector operations: " +
     is_nan_expr.pretty());
 }
 
 static smt_termt convert_expr_to_smt(
   const isfinite_exprt &is_finite_expr,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is finite expression: " +
+  UNREACHABLE_BECAUSE(
+    "Is finite expression should have been lowered to "
+    "bitvector operations: " +
     is_finite_expr.pretty());
 }
 
 static smt_termt convert_expr_to_smt(
   const isinf_exprt &is_infinite_expr,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is infinite expression: " +
+  UNREACHABLE_BECAUSE(
+    "Is infinite expression should have been lowered to "
+    "bitvector operations: " +
     is_infinite_expr.pretty());
 }
 
 static smt_termt convert_expr_to_smt(
   const isnormal_exprt &is_normal_expr,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is infinite expression: " +
+  UNREACHABLE_BECAUSE(
+    "Is normal expression should have been lowered to "
+    "bitvector operations: " +
     is_normal_expr.pretty());
 }
 

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -6,11 +6,13 @@
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/floatbv_expr.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string_constant.h>
 
+#include <solvers/floatbv/float_bv.h>
 #include <solvers/smt2_incremental/ast/smt_commands.h>
 #include <solvers/smt2_incremental/ast/smt_responses.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>
@@ -308,6 +310,12 @@ static exprt lower_zero_extend(exprt expr, const namespacet &ns)
   return expr;
 }
 
+static exprt lower_floatbv(exprt expr, const namespacet &ns)
+{
+  const float_bvt float_bv;
+  return float_bv.convert(expr);
+}
+
 void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
   const exprt &in_expr)
 {
@@ -688,7 +696,8 @@ exprt smt2_incremental_decision_proceduret::lower(exprt expression) const
 {
   const exprt lowered = struct_encoding.encode(lower_zero_extend(
     lower_enum(
-      lower_byte_operators(lower_rw_ok_pointer_in_range(expression, ns), ns),
+      lower_byte_operators(
+        lower_floatbv(lower_rw_ok_pointer_in_range(expression, ns), ns), ns),
       ns),
     ns));
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {