From f79e1db3a3055f9e0daa259b9d5e3dc7afd8e4ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Recoules?= Date: Fri, 8 Mar 2024 11:58:02 +0100 Subject: [PATCH] Add a test for OCaml 5 --- examples/unsatassumptions.ml | 4 +- test/dune | 11 ++ test/t_bitwuzla_cxx_5.ml | 257 +++++++++++++++++++++++++++++++++++ 3 files changed, 270 insertions(+), 2 deletions(-) create mode 100644 test/t_bitwuzla_cxx_5.ml diff --git a/examples/unsatassumptions.ml b/examples/unsatassumptions.ml index 7da9f37..393725c 100644 --- a/examples/unsatassumptions.ml +++ b/examples/unsatassumptions.ml @@ -87,9 +87,9 @@ let () = Format.printf "Bitwuzla: %s@," (Result.to_string result); (* (get-unsat-assumptions) *) - let unsat_core = Solver.get_unsat_core bitwuzla in + let unsat_assumptions = Solver.get_unsat_assumptions bitwuzla in Format.printf "Unsat Assumptions:@,@[{"; - Array.iter (Format.printf "@,%a" Term.pp) unsat_core; + Array.iter (Format.printf "@,%a" Term.pp) unsat_assumptions; Format.printf "@]@,}@,"; Format.close_box () diff --git a/test/dune b/test/dune index e7a9ecb..571f14c 100644 --- a/test/dune +++ b/test/dune @@ -6,3 +6,14 @@ (preprocess (pps ppx_expect ppx_inline_test)) (libraries bitwuzla-cxx)) + +(library + (name t_bitwuzla_cxx_5) + (optional) + (enabled_if + (> %{ocaml_version} 5)) + (modules t_bitwuzla_cxx_5) + (inline_tests) + (preprocess + (pps ppx_expect ppx_inline_test)) + (libraries unix bitwuzla-cxx)) diff --git a/test/t_bitwuzla_cxx_5.ml b/test/t_bitwuzla_cxx_5.ml new file mode 100644 index 0000000..a7007de --- /dev/null +++ b/test/t_bitwuzla_cxx_5.ml @@ -0,0 +1,257 @@ +(**************************************************************************) +(* Bitwuzla: Satisfiability Modulo Theories (SMT) solver. *) +(* *) +(* Copyright (C) 2023 by the authors listed in the AUTHORS file at *) +(* https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS *) +(* *) +(* This file is part of Bitwuzla under the MIT license. *) +(* See COPYING for more information at *) +(* https://github.com/bitwuzla/bitwuzla/blob/main/COPYING *) +(**************************************************************************) + +(* The inline tests were moved here to avoid depending on ppx outside tests. *) +(* The goal of these tests are to catch errors in the function and constant *) +(* mappings. They do not try to catch functional errors in Bitwuzla. *) + +let timeout time_limit = + let start = Unix.gettimeofday () in + fun () -> Float.compare (Unix.gettimeofday () -. start) time_limit >= 0 + +module Options = Bitwuzla_cxx.Options + +let quickstart (m : (module Bitwuzla_cxx.S)) : bool = + let open (val m) in + let options = Options.default () in + Options.set options Produce_models true; + let bitwuzla = Solver.create options in + let sortbv4 = mk_bv_sort 4 and sortbv8 = mk_bv_sort 8 in + let sortfun = mk_fun_sort [| sortbv8; sortbv4 |] sortbv8 in + let sortarr = mk_array_sort sortbv8 sortbv8 in + let x = mk_const sortbv8 ~symbol:"x" and y = mk_const sortbv8 ~symbol:"y" in + let f = mk_const sortfun ~symbol:"f" in + let a = mk_const sortarr ~symbol:"a" in + let one = mk_bv_one sortbv8 in + let two = mk_bv_value_int sortbv8 2 in + let sdiv = mk_term2 Bv_sdiv x two in + let ashr = mk_term2 Bv_ashr y one in + let sdive = mk_term1_indexed2 Bv_extract sdiv 3 0 in + let ashre = mk_term1_indexed2 Bv_extract ashr 3 0 in + Solver.assert_formula bitwuzla (mk_term2 Distinct sdive ashre); + Solver.assert_formula bitwuzla + (mk_term2 Equal (mk_term3 Apply f x (mk_term1_indexed2 Bv_extract x 6 3)) y); + Solver.assert_formula bitwuzla (mk_term2 Equal (mk_term2 Select a x) y); + let result = Solver.check_sat bitwuzla in + result = Sat + && Term.value Z (Solver.get_value bitwuzla x) = Z.of_int 0b10011111 + && Term.value Z (Solver.get_value bitwuzla y) = Z.of_int 0b11111111 + && Term.value Z (Solver.get_value bitwuzla (mk_term2 Bv_mul x x)) + = Z.of_int 0b11000001 + +let pushpop (m : (module Bitwuzla_cxx.S)) : bool = + let open (val m) in + let options = Options.default () in + let bitwuzla = Solver.create options in + let sortbv1 = mk_bv_sort 1 in + let sortbv2 = mk_bv_sort 2 in + let o0 = mk_const sortbv1 ~symbol:"o0" in + let o1 = mk_const sortbv1 ~symbol:"o1" in + let s0 = mk_const sortbv2 ~symbol:"s0" in + let s1 = mk_const sortbv2 ~symbol:"s1" in + let s2 = mk_const sortbv2 ~symbol:"s1" in + let goal = mk_const sortbv2 ~symbol:"goal" in + let zero = mk_bv_zero sortbv2 + and one1 = mk_bv_one sortbv1 + and one2 = mk_bv_one sortbv2 + and three = mk_bv_value_int sortbv2 3 in + Solver.assert_formula bitwuzla (mk_term2 Equal s0 zero); + Solver.assert_formula bitwuzla (mk_term2 Equal goal three); + Solver.push bitwuzla 1; + Solver.assert_formula bitwuzla (mk_term2 Equal s0 goal); + let result = Solver.check_sat bitwuzla in + result = Unsat + && (Solver.pop bitwuzla 1; + Solver.assert_formula bitwuzla + (mk_term2 Equal s1 + (mk_term3 Ite (mk_term2 Equal o0 one1) (mk_term2 Bv_add s0 one2) s0)); + Solver.push bitwuzla 1; + Solver.assert_formula bitwuzla (mk_term2 Equal s1 goal); + let result = Solver.check_sat bitwuzla in + result = Unsat) + && + (Solver.pop bitwuzla 1; + Solver.assert_formula bitwuzla + (mk_term2 Equal s2 + (mk_term3 Ite (mk_term2 Equal o1 one1) (mk_term2 Bv_add s1 one2) s1)); + Solver.push bitwuzla 1; + Solver.assert_formula bitwuzla (mk_term2 Equal s2 goal); + let result = Solver.check_sat bitwuzla in + result = Unsat) + +let checksatassuming (m : (module Bitwuzla_cxx.S)) : bool = + let open (val m) in + let options = Options.default () in + let bitwuzla = Solver.create options in + let sortbv1 = mk_bv_sort 1 in + let sortbv2 = mk_bv_sort 2 in + let o0 = mk_const sortbv1 ~symbol:"o0" in + let o1 = mk_const sortbv1 ~symbol:"o1" in + let s0 = mk_const sortbv2 ~symbol:"s0" in + let s1 = mk_const sortbv2 ~symbol:"s1" in + let s2 = mk_const sortbv2 ~symbol:"s1" in + let goal = mk_const sortbv2 ~symbol:"goal" in + let zero = mk_bv_zero sortbv2 + and one1 = mk_bv_one sortbv1 + and one2 = mk_bv_one sortbv2 + and three = mk_bv_value_int sortbv2 3 in + Solver.assert_formula bitwuzla (mk_term2 Equal s0 zero); + Solver.assert_formula bitwuzla (mk_term2 Equal goal three); + let result = + Solver.check_sat bitwuzla ~assumptions:[| mk_term2 Equal s0 goal |] + in + result = Unsat + && (Solver.assert_formula bitwuzla + (mk_term2 Equal s1 + (mk_term3 Ite (mk_term2 Equal o0 one1) (mk_term2 Bv_add s0 one2) s0)); + let result = + Solver.check_sat bitwuzla ~assumptions:[| mk_term2 Equal s1 goal |] + in + result = Unsat) + && + (Solver.assert_formula bitwuzla + (mk_term2 Equal s2 + (mk_term3 Ite (mk_term2 Equal o1 one1) (mk_term2 Bv_add s1 one2) s1)); + let result = + Solver.check_sat bitwuzla ~assumptions:[| mk_term2 Equal s2 goal |] + in + result = Unsat) + +let unsatassumptions (m : (module Bitwuzla_cxx.S)) : bool = + let open (val m) in + let options = Options.default () in + Options.set options Produce_unsat_assumptions true; + let bitwuzla = Solver.create options in + let sortbool = mk_bool_sort () in + let sortbv2 = mk_bv_sort 2 in + let sortbv4 = mk_bv_sort 4 in + let sortfp16 = mk_fp_sort 5 11 in + let x0 = mk_const sortbv4 ~symbol:"x0" in + let x1 = mk_const sortbv2 ~symbol:"x1" in + let x2 = mk_const sortbv2 ~symbol:"x2" in + let x3 = mk_const sortbv2 ~symbol:"x3" in + let x4 = mk_const sortfp16 ~symbol:"x4" in + let fpzero = mk_fp_pos_zero sortfp16 in + let bvzero = mk_bv_zero sortbv4 in + let a_f0 = mk_var sortfp16 ~symbol:"a_f0" in + let f0 = mk_term2 Lambda a_f0 (mk_term2 Fp_gt a_f0 fpzero) in + let a_f1 = mk_var sortfp16 ~symbol:"a_f1" in + let f1 = + mk_term2 Lambda a_f1 (mk_term3 Ite (mk_term2 Apply f0 a_f1) x0 bvzero) + in + let a_f2 = mk_var sortfp16 ~symbol:"a_f2" in + let f2 = + mk_term2 Lambda a_f2 + (mk_term1_indexed2 Bv_extract (mk_term2 Apply f1 a_f2) 1 0) + in + let a0 = mk_const sortbool ~symbol:"a0" in + let assumption0 = mk_term2 Bv_ult x2 (mk_term2 Apply f2 fpzero) in + Solver.assert_formula bitwuzla (mk_term2 Equal a0 assumption0); + let a1 = mk_const sortbool ~symbol:"a1" in + let assumption1 = mk_term Equal [| x1; x2; x3 |] in + Solver.assert_formula bitwuzla (mk_term2 Equal a1 assumption1); + let a2 = mk_const sortbool ~symbol:"a2" in + let assumption2 = + mk_term2 Equal x4 + (mk_term2_indexed2 Fp_to_fp_from_ubv (mk_rm_value Rne) x3 5 11) + in + Solver.assert_formula bitwuzla (mk_term2 Equal a2 assumption2); + let result = Solver.check_sat bitwuzla ~assumptions:[| a0; a1; a2 |] in + result = Unsat + && + let unsat_assumptions = Solver.get_unsat_core bitwuzla in + Array.mem a0 unsat_assumptions + +let unsatcore (m : (module Bitwuzla_cxx.S)) : bool = + let open (val m) in + let options = Options.default () in + Options.set options Produce_unsat_cores true; + let bitwuzla = Solver.create options in + let sortbv2 = mk_bv_sort 2 in + let sortbv4 = mk_bv_sort 4 in + let sortfp16 = mk_fp_sort 5 11 in + let x0 = mk_const sortbv4 ~symbol:"x0" in + let x1 = mk_const sortbv2 ~symbol:"x1" in + let x2 = mk_const sortbv2 ~symbol:"x2" in + let x3 = mk_const sortbv2 ~symbol:"x3" in + let x4 = mk_const sortfp16 ~symbol:"x4" in + let fpzero = mk_fp_pos_zero sortfp16 in + let bvzero = mk_bv_zero sortbv4 in + let a_f0 = mk_var sortfp16 ~symbol:"a_f0" in + let f0 = mk_term2 Lambda a_f0 (mk_term2 Fp_gt a_f0 fpzero) in + let a_f1 = mk_var sortfp16 ~symbol:"a_f1" in + let f1 = + mk_term2 Lambda a_f1 (mk_term3 Ite (mk_term2 Apply f0 a_f1) x0 bvzero) + in + let a_f2 = mk_var sortfp16 ~symbol:"a_f2" in + let f2 = + mk_term2 Lambda a_f2 + (mk_term1_indexed2 Bv_extract (mk_term2 Apply f1 a_f2) 1 0) + in + let a0 = mk_term2 Bv_ult x2 (mk_term2 Apply f2 fpzero) in + Solver.assert_formula bitwuzla a0; + let a1 = mk_term Equal [| x1; x2; x3 |] in + Solver.assert_formula bitwuzla a1; + let a2 = + mk_term2 Equal x4 + (mk_term2_indexed2 Fp_to_fp_from_ubv (mk_rm_value Rne) x3 5 11) + in + Solver.assert_formula bitwuzla a2; + let result = Solver.check_sat bitwuzla in + result = Unsat + && + let unsat_core = Solver.get_unsat_core bitwuzla in + Array.mem a0 unsat_core + +let terminator (m : (module Bitwuzla_cxx.S)) : bool = + let open (val m) in + let options = Options.default () in + let bitwuzla = Solver.create options in + let bv = mk_bv_sort 32 in + let x = mk_const bv and s = mk_const bv and t = mk_const bv in + let a = + mk_term2 Distinct + (mk_term2 Bv_mul s (mk_term2 Bv_mul x t)) + (mk_term2 Bv_mul (mk_term2 Bv_mul s x) t) + in + Solver.check_sat bitwuzla ~assumptions:[| a |] = Unsat + && + (Options.set options Preprocess false; + let bitwuzla2 = Solver.create options in + let terminator = timeout 1. in + Solver.configure_terminator bitwuzla2 (Some terminator); + Solver.check_sat bitwuzla2 ~assumptions:[| a |] = Unknown) + +let examples = + [| + quickstart; + pushpop; + checksatassuming; + unsatassumptions; + unsatcore; + terminator; + |] + +let n = Array.length examples + +let run i () = + let module M = Bitwuzla_cxx.Make () in + try + Array.for_all + (fun f -> f (module M : Bitwuzla_cxx.S)) + (Array.init n (fun j -> Array.get examples ((i + j) mod n))) + with _ -> false + +let%test "domains" = + Array.for_all Fun.id + (Array.map Domain.join + (Array.init (Domain.recommended_domain_count ()) (fun i -> + Domain.spawn (run i))))