extend tests for new stubs

cvc5.ml

@@ -69,6 +69,9 @@ module Term = struct
 
   let mk_int = Cvc5_external.mk_int
 
+  let mk_string tm ?(useEscSequences = false) s =
+    Cvc5_external.mk_string tm s useEscSequences
+
   let mk_real_s = Cvc5_external.mk_real_s
 
   let mk_real_i = Cvc5_external.mk_real_i
@@ -104,7 +107,18 @@ module Term = struct
 
   let get_int t = int_of_string (Cvc5_external.term_get_int_val t)
 
-  let get_real t = float_of_string (Cvc5_external.term_get_real_val t)
+  let get_real t =
+    let real_str = Cvc5_external.term_get_real_val t in
+    (* cvc5 returns string o float in fraction format *)
+    let fraction_to_float str =
+      match String.split_on_char '/' str with
+      | [ numerator; denominator ] ->
+        let num = float_of_string numerator in
+        let denom = float_of_string denominator in
+        num /. denom
+      | _ -> assert false
+    in
+    fraction_to_float real_str
 
   let get_int32 = Cvc5_external.term_get_int32_val
 

cvc5.mli

@@ -66,6 +66,8 @@ module Term : sig
 
   val mk_int : TermManager.tm -> int -> term
 
+  val mk_string : TermManager.tm -> ?useEscSequences:bool -> string -> term
+
   val mk_real_s : TermManager.tm -> string -> term
 
   val mk_real_i : TermManager.tm -> int -> term

cvc5_external.ml

@@ -98,7 +98,7 @@ external mk_bv_s :
   term_manager -> (int[@untagged]) -> string -> (int[@untagged]) -> term
   = "ocaml_cvc5_stub_mk_bv_s" "native_cvc5_stub_mk_bv_s"
 
-external mk_string : term_manager -> string -> term
+external mk_string : term_manager -> string -> bool -> term
   = "ocaml_cvc5_stub_mk_string"
 
 external mk_term : term_manager -> int -> term array -> term
@@ -146,7 +146,8 @@ external term_get_uint64_val : term -> int64
 external term_is_bv_val : term -> bool = "ocaml_cvc5_stub_is_bv_value"
 [@@noalloc]
 
-external term_get_bv_val : term -> int32 -> string = "ocaml_cvc5_stub_get_bv_value"
+external term_get_bv_val : term -> int32 -> string
+  = "ocaml_cvc5_stub_get_bv_value"
 
 external term_is_rm_val : term -> bool = "ocaml_cvc5_stub_is_rm_value"
 [@@noalloc]

cvc5_stubs.cpp

@@ -353,11 +353,11 @@ CAMLprim value ocaml_cvc5_stub_term_to_string(value v){
   return caml_copy_string(Term_val(v)->toString().c_str());
 }
 
-CAMLprim value ocaml_cvc5_stub_mk_string(value v, value s){
+CAMLprim value ocaml_cvc5_stub_mk_string(value v, value s, value b){
   cvc5::TermManager* term_manager = TermManager_val(v);
   value custom = Val_unit;
   CVC5_TRY_CATCH_BEGIN;
-  new(&term_operations, &custom) Term(term_manager->mkString(String_val(s)));
+  new(&term_operations, &custom) Term(term_manager->mkString(String_val(s), Bool_val(b)));
   return custom;
   CVC5_TRY_CATCH_END;
 }

test/dune

@@ -1,3 +1,3 @@
 (tests
- (names test_trivial test_reset test_terms)
+ (names test_trivial test_reset test_terms test_val_interp)
  (libraries cvc5))

test/test_terms.ml

@@ -17,14 +17,14 @@ let () =
   let x_gt_zero_not = Term.mk_term tm Kind.Not [| x_gt_zero |] in
   let x_gt_zero_not_not = Term.mk_term tm Kind.Not [| x_gt_zero_not |] in
   let simplified = Solver.simplify solver x_gt_zero_not_not in
-  assert(Term.equal x_gt_zero simplified)
+  assert (Term.equal x_gt_zero simplified)
 
 (* Different terms should not be considered equal *)
 let () =
   let false_const = Term.mk_false tm in
-  assert(not (Term.equal false_const x_gt_zero))
+  assert (not (Term.equal false_const x_gt_zero))
 
 (* Term.kind returns the correct Kind of a term *)
 let () =
-  assert(Term.kind x_gt_zero = Kind.Geq);
-  assert(not (Term.kind x_gt_zero = Kind.Not))
+  assert (Term.kind x_gt_zero = Kind.Geq);
+  assert (not (Term.kind x_gt_zero = Kind.Not))

test/test_val_interp.ml

@@ -0,0 +1,41 @@
+open Cvc5
+
+let tm = TermManager.mk_tm ()
+
+(* Check int values construction and interpretation *)
+let () =
+  let one = Term.mk_int tm 1 in
+  assert (Term.is_int one);
+  assert (Term.get_int one = 1)
+
+(* Check real values contruction and interpretation *)
+let () =
+  let one_float_s = Term.mk_real_s tm "1.0" in
+  assert (Term.is_real one_float_s);
+  assert (Term.get_real one_float_s = 1.0);
+
+  let one_float_nd = Term.mk_real tm 1 2 in
+  assert (Term.is_real one_float_nd);
+  assert (Term.get_real one_float_nd = 0.5);
+
+  let one_float_i = Term.mk_real_i tm 1 in
+  assert (Term.is_real one_float_i);
+  assert (Term.get_real one_float_i = 1.0)
+
+(* Check boolean values construction and interpretation *)
+let () =
+  let true1 = Term.mk_bool tm true in
+  assert (Term.is_bool true1);
+  assert (Term.get_bool true1 = true);
+
+  let true2 = Term.mk_true tm in
+  assert (Term.is_bool true2);
+  assert (Term.get_bool true2 = true)
+
+(* Check string values construction and interpretation *)
+let () =
+  let str = Term.mk_string tm "abc" in
+  assert (Term.is_string str)
+
+(* Check bit-vector values construction and interpretation *)
+(* TODO *)