From bb5f9134fefd56eb46eebb1b4fabd8e77e201d24 Mon Sep 17 00:00:00 2001 From: joaomhmpereira Date: Mon, 8 Apr 2024 17:45:22 +0100 Subject: [PATCH] extend tests for new stubs --- cvc5.ml | 16 +++++++++++++++- cvc5.mli | 2 ++ cvc5_external.ml | 5 +++-- cvc5_stubs.cpp | 4 ++-- test/dune | 2 +- test/test_terms.ml | 8 ++++---- test/test_val_interp.ml | 41 +++++++++++++++++++++++++++++++++++++++++ 7 files changed, 68 insertions(+), 10 deletions(-) create mode 100644 test/test_val_interp.ml diff --git a/cvc5.ml b/cvc5.ml index a575495..829d121 100644 --- a/cvc5.ml +++ b/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 diff --git a/cvc5.mli b/cvc5.mli index bb004e7..80910d9 100644 --- a/cvc5.mli +++ b/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 diff --git a/cvc5_external.ml b/cvc5_external.ml index 13fd70f..db1e76b 100644 --- a/cvc5_external.ml +++ b/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] diff --git a/cvc5_stubs.cpp b/cvc5_stubs.cpp index c9fe59f..2af568d 100644 --- a/cvc5_stubs.cpp +++ b/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; } diff --git a/test/dune b/test/dune index a0cca98..d28c245 100644 --- a/test/dune +++ b/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)) diff --git a/test/test_terms.ml b/test/test_terms.ml index c3ab00d..5c9d089 100644 --- a/test/test_terms.ml +++ b/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)) \ No newline at end of file + assert (Term.kind x_gt_zero = Kind.Geq); + assert (not (Term.kind x_gt_zero = Kind.Not)) diff --git a/test/test_val_interp.ml b/test/test_val_interp.ml new file mode 100644 index 0000000..b5103d8 --- /dev/null +++ b/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 *)