From c07b98af8fb866e54b2dcf29adf3853d94ab4da0 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 21 May 2026 11:57:47 +0100 Subject: [PATCH] [z3] add implement `Re.allchar` and `Re.diff` using native API Since these aren't yet available in the API we can use the native function and leverage `Obj.magic` to implement `Re.allchar` and `Re.diff`. --- src/smtml/z3_mappings.default.ml | 11 +++++---- test/integration/test_solver.ml | 39 ++++++++++++++++++++++++++++---- 2 files changed, 42 insertions(+), 8 deletions(-) diff --git a/src/smtml/z3_mappings.default.ml b/src/smtml/z3_mappings.default.ml index 20a2085f..7189c75f 100644 --- a/src/smtml/z3_mappings.default.ml +++ b/src/smtml/z3_mappings.default.ml @@ -273,7 +273,10 @@ module M = struct end module Re = struct - let allchar () = assert false + let allchar () = + Z3native.mk_re_allchar (Obj.magic ctx) + (Obj.magic (Z3.Seq.mk_re_sort ctx Types.string)) + |> Obj.magic let all () = Z3.Seq.mk_re_full ctx (Z3.Seq.mk_re_sort ctx Types.string) @@ -289,9 +292,9 @@ module M = struct let range e1 e2 = Z3.Seq.mk_re_range ctx e1 e2 - let diff _ = - Fmt.failwith "%s:%d: %s not implemented" __MODULE__ __LINE__ - __FUNCTION__ + let diff e1 e2 = + Z3native.mk_re_diff (Obj.magic ctx) (Obj.magic e1) (Obj.magic e2) + |> Obj.magic let inter e1 e2 = Z3.Seq.mk_re_intersect ctx [ e1; e2 ] diff --git a/test/integration/test_solver.ml b/test/integration/test_solver.ml index b34456d4..6ee6a83c 100644 --- a/test/integration/test_solver.ml +++ b/test/integration/test_solver.ml @@ -291,13 +291,13 @@ module Make (M : Mappings_intf.S_with_fresh) = struct ; "test_to_ieee_bv" >:: with_solver test_to_ieee_bv ] - let test_regexp solver_module = + let test_regexp_allchar solver_module = let open Typed in let module Solver = (val solver_module : Solver_intf.S) in let solver = Solver.create () in let s = symbol Types.string "s" in - let any_char = String.(Re.range (v "a") (v "z")) in - Solver.add solver [ (String.in_re s any_char :> Expr.t) ]; + let allchar = String.Re.allchar in + Solver.add solver [ (String.in_re s allchar :> Expr.t) ]; assert_sat ~f:"test_re_allchar" (Solver.check solver []); let model = Solver.model solver in let val_s = @@ -306,6 +306,35 @@ module Make (M : Mappings_intf.S_with_fresh) = struct assert ( match val_s with Some (Str s) -> Stdlib.String.length s = 1 | _ -> false ) + let test_regexp_diff solver_module = + let open Typed in + let module Solver = (val solver_module : Solver_intf.S) in + let solver = Solver.create () in + let s = symbol Types.string "s" in + let re_az = String.(Re.range (v "a") (v "z")) in + let re_a = String.(to_re (v "a")) in + let re_not_a = String.Re.diff re_az re_a in + Solver.add solver [ (String.in_re s re_not_a :> Expr.t) ]; + assert_sat ~f:"test_re_diff" (Solver.check solver []); + let model = Solver.model solver in + let val_s = + Option.bind model (fun m -> Model.evaluate m (Symbol.make Ty_str "s")) + in + assert ( + match val_s with + | Some (Str s) -> Stdlib.String.length s = 1 && s <> "a" + | _ -> false ) + + let test_regexp_diff_unsat solver_module = + let open Typed in + let module Solver = (val solver_module : Solver_intf.S) in + let solver = Solver.create () in + let s = symbol Types.string "s" in + let re_a = String.(to_re (v "a")) in + let re_diff_a_a = String.Re.diff re_a re_a in + Solver.add solver [ (String.in_re s re_diff_a_a :> Expr.t) ]; + assert_unsat ~f:"test_re_diff_unsat" (Solver.check solver []) + let test_regexp_concat solver_module = let open Typed in let module Solver = (val solver_module : Solver_intf.S) in @@ -406,7 +435,9 @@ module Make (M : Mappings_intf.S_with_fresh) = struct let test_regexp = "test_regexp" - >::: [ "test_re" >:: with_solver test_regexp + >::: [ "test_re_allchar" >:: with_solver test_regexp_allchar + ; "test_re_diff" >:: with_solver test_regexp_diff + ; "test_re_diff_unsat" >:: with_solver test_regexp_diff_unsat ; "test_re_concat" >:: with_solver test_regexp_concat ; "test_re_union" >:: with_solver test_regexp_union ; "test_re_star" >:: with_solver test_regexp_star