Adds Term.{is_fp, get_fp}

cvc5.ml

@@ -116,7 +116,8 @@ module Term = struct
   let mk_term_2 (tm : TermManager.tm) (k : Kind.t) (t1 : term) (t2 : term) =
     Cvc5_external.mk_term_2 tm (Kind.to_cpp k) t1 t2
 
-  let mk_term_3 (tm : TermManager.tm) (k : Kind.t) (t1 : term) (t2 : term) (t3 : term) =
+  let mk_term_3 (tm : TermManager.tm) (k : Kind.t) (t1 : term) (t2 : term)
+    (t3 : term) =
     Cvc5_external.mk_term_3 tm (Kind.to_cpp k) t1 t2 t3
 
   let mk_term_op (tm : TermManager.tm) (op : Op.op) (terms : term array) =
@@ -178,6 +179,8 @@ module Term = struct
 
   let is_rm = Cvc5_external.term_is_rm_val
 
+  let is_fp = Cvc5_external.term_is_fp_val
+
   let is_bool = Cvc5_external.term_is_bool_val
 
   let get_int t = int_of_string (Cvc5_external.term_get_int_val t)
@@ -209,6 +212,8 @@ module Term = struct
 
   let get_rm t = RoundingMode.of_cpp @@ Cvc5_external.term_get_rm_val t
 
+  let get_fp = Cvc5_external.term_get_fp_val
+
   let get_bool = Cvc5_external.term_get_bool_val
 end
 

cvc5.mli

@@ -171,6 +171,9 @@ module Term : sig
 
   val is_rm : term -> bool
 
+  (** Determine if a given term is a floating-point value. *)
+  val is_fp : term -> bool
+
   val get_int : term -> int
 
   val get_real : term -> float
@@ -190,6 +193,10 @@ module Term : sig
   val get_bv : term -> int -> string
 
   val get_rm : term -> RoundingMode.t
+
+  (** Get the representation of a floating-point value as a tuple of its
+      exponent width, significand width and a bit-vector value term. *)
+  val get_fp : term -> int * int * term
 end
 
 module Result : sig

cvc5_external.ml

@@ -23,57 +23,57 @@
 
 type ptr
 
-and result = ptr
+type result = ptr
 
-and synth_result = ptr
+type synth_result = ptr
 
-and sort = ptr
+type sort = ptr
 
-and term = ptr
+type term = ptr
 
-and op = ptr
+type op = ptr
 
-and datatype = ptr
+type datatype = ptr
 
-and datatype_constructor_decl = ptr
+type datatype_constructor_decl = ptr
 
-and datatype_decl = ptr
+type datatype_decl = ptr
 
-and datatype_selector = ptr
+type datatype_selector = ptr
 
-and datatype_constructor = ptr
+type datatype_constructor = ptr
 
-and grammar = ptr
+type grammar = ptr
 
-and solver = ptr
+type solver = ptr
 
-and term_manager = ptr
+type term_manager = ptr
 
-and option_info = ptr
+type option_info = ptr
 
-and proof = ptr
+type proof = ptr
 
-and proof_rule = ptr
+type proof_rule = ptr
 
-and statistics = ptr
+type statistics = ptr
 
-and unknown_explanation = ptr
+type unknown_explanation = ptr
 
-and sort_kind = ptr
+type sort_kind = ptr
 
-and kind = ptr
+type kind = ptr
 
-and rounding_mode = ptr
+type rounding_mode = ptr
 
-and proof_format = ptr
+type proof_format = ptr
 
-and proof_component = ptr
+type proof_component = ptr
 
-and learned_lit_type = ptr
+type learned_lit_type = ptr
 
-and block_model_mode = ptr
+type block_model_mode = ptr
 
-and find_synth_target = ptr
+type find_synth_target = ptr
 
 external result_is_sat : result -> bool = "ocaml_cvc5_stub_result_is_sat"
 
@@ -102,7 +102,8 @@ external mk_real_s : term_manager -> string -> term
 external mk_real_i : term_manager -> (int64[@unboxed]) -> term
   = "ocaml_cvc5_stub_mk_real_i" "native_cvc5_stub_mk_real_i"
 
-external mk_real : term_manager -> (int64[@unboxed]) -> (int64[@unboxed]) -> term
+external mk_real :
+  term_manager -> (int64[@unboxed]) -> (int64[@unboxed]) -> term
   = "ocaml_cvc5_stub_mk_real" "native_cvc5_stub_mk_real"
 
 external mk_bv : term_manager -> (int[@untagged]) -> (int64[@unboxed]) -> term
@@ -186,6 +187,11 @@ external term_is_rm_val : term -> bool = "ocaml_cvc5_stub_is_rm_value"
 
 external term_get_rm_val : term -> int = "ocaml_cvc5_stub_get_rm_value"
 
+external term_is_fp_val : term -> bool = "ocaml_cvc5_stub_is_fp_value"
+
+external term_get_fp_val : term -> int * int * term
+  = "ocaml_cvc5_stub_get_fp_value"
+
 external term_is_bool_val : term -> bool = "ocaml_cvc5_stub_is_bool_value"
 
 external term_get_bool_val : term -> bool = "ocaml_cvc5_stub_get_bool_value"
@@ -330,8 +336,7 @@ external mk_term_1 : term_manager -> int -> term -> term
 external mk_term_2 : term_manager -> int -> term -> term -> term
   = "ocaml_cvc5_stub_mk_term_2"
 
-external mk_term_3 :
-  term_manager -> int -> term -> term -> term -> term
+external mk_term_3 : term_manager -> int -> term -> term -> term -> term
   = "ocaml_cvc5_stub_mk_term_3"
 
 (**/**)

cvc5_stubs.cpp

@@ -26,6 +26,7 @@
 #include <string.h>
 #include <iostream>
 #include <algorithm>
+#include <tuple>
 
 #include <cvc5/cvc5.h>
 
@@ -743,11 +744,35 @@ CAMLprim value ocaml_cvc5_stub_is_rm_value(value t){
   CVC5_TRY_CATCH_END;
 }
 
+CAMLprim value ocaml_cvc5_stub_is_fp_value(value t) {
+  CAMLparam1(t);
+  CVC5_TRY_CATCH_BEGIN;
+  CAMLreturn(Val_bool(Term_val(t)->isFloatingPointValue()));
+  CVC5_TRY_CATCH_END;
+}
+
+CAMLprim value ocaml_cvc5_stub_get_fp_value(value t) {
+  CAMLparam1(t);
+  CAMLlocal2(custom, term);
+  TermManager *tm = TermManager_val(t);
+  const auto fp = Term_val(t)->getFloatingPointValue();
+  int ebits = std::get<0>(fp);
+  int sbits = std::get<1>(fp);
+  CVC5_TRY_CATCH_BEGIN;
+  new(&term_operations, &term) Term(std::get<2>(fp), tm);
+  custom = caml_alloc_tuple(3);
+  Store_field (custom, 0, Val_int(ebits));
+  Store_field (custom, 1, Val_int(sbits));
+  Store_field (custom, 2, term);
+  CAMLreturn(custom);
+  CVC5_TRY_CATCH_END;
+}
+
 CAMLprim value ocaml_cvc5_stub_is_bool_value(value t){
   CAMLparam1(t);
   CVC5_TRY_CATCH_BEGIN;
   CAMLreturn(Val_bool(Term_val(t)->isBooleanValue()));
-  CVC5_TRY_CATCH_END
+  CVC5_TRY_CATCH_END;
 }
 
 CAMLprim value ocaml_cvc5_stub_get_bool_value(value t){

dune

@@ -16,7 +16,6 @@
      (progn
       (bash "./configure")
       (bash "make -j $(opam var jobs)")))
-
     (copy vendor/cadical/build/libcadical.a libcadical.a)
     (chdir
      vendor/libpoly