Add support for str.replace_all operator

Author: joaomhmpereira

src/smtml/bitwuzla_mappings.default.ml

@@ -221,6 +221,9 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let replace _ ~pattern:_ ~with_:_ =
       Fmt.failwith "Bitwuzla_mappings: String.replace not implemented"
+
+    let replace_all _ ~pattern:_ ~with_:_ =
+      Fmt.failwith "Bitwuzla_mappings: String.replace_all not implemented"
   end
 
   module Re = struct

src/smtml/cvc5_mappings.default.ml

@@ -203,6 +203,9 @@ module Fresh_cvc5 () = struct
 
     let replace t1 ~pattern ~with_ =
       Term.mk_term tm Kind.String_replace [| t1; pattern; with_ |]
+
+    let replace_all t1 ~pattern ~with_ =
+      Term.mk_term tm Kind.String_replace_all [| t1; pattern; with_ |]
   end
 
   module Re = struct

src/smtml/dolmenexpr_to_expr.ml

@@ -208,6 +208,8 @@ module DolmenIntf = struct
     let index_of t ~sub ~pos = DTerm.String.index_of t sub pos
 
     let replace t ~pattern ~with_ = DTerm.String.replace t pattern with_
+
+    let replace_all t ~pattern ~with_ = DTerm.String.replace_all t pattern with_
   end
 
   module Re = struct

src/smtml/dolmenexpr_to_expr.mli

@@ -185,6 +185,8 @@ module DolmenIntf : sig
     val index_of : term -> sub:term -> pos:term -> term
 
     val replace : term -> pattern:term -> with_:term -> term
+
+    val replace_all : term -> pattern:term -> with_:term -> term
   end
 
   module Re : sig

src/smtml/mappings.ml

@@ -231,6 +231,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         | Triop.String_extract -> M.String.sub e1 ~pos:e2 ~len:e3
         | String_index -> M.String.index_of e1 ~sub:e2 ~pos:e3
         | String_replace -> M.String.replace e1 ~pattern:e2 ~with_:e3
+        | String_replace_all -> M.String.replace_all e1 ~pattern:e2 ~with_:e3
         | _ ->
           Fmt.failwith {|String: Unsupported triop operator "%a"|} Triop.pp op
 

src/smtml/mappings.nop.ml

@@ -182,6 +182,8 @@ module Nop = struct
       let index_of _ ~sub:_ ~pos:_ = assert false
 
       let replace _ ~pattern:_ ~with_:_ = assert false
+
+      let replace_all _ ~pattern:_ ~with_:_ = assert false
     end
 
     module Re = struct

src/smtml/mappings_intf.ml

@@ -316,6 +316,10 @@ module type M = sig
     (** [replace t ~pattern ~with_] constructs the string term resulting from
         replacing [pattern] with [with_] in [t]. *)
     val replace : term -> pattern:term -> with_:term -> term
+
+    (** [replace_all t ~pattern ~with_] constructs the string term resulting
+        from replacing all occurrences of [pattern] with [with_] in [t]. *)
+    val replace_all : term -> pattern:term -> with_:term -> term
   end
 
   (** {2 Regular Expression Operations} *)

src/smtml/smtlib.ml

@@ -180,6 +180,8 @@ module Term = struct
       | "str.substr", [ a; b; c ] -> Expr.triop Ty_str String_extract a b c
       | "str.indexof", [ a; b; c ] -> Expr.triop Ty_str String_index a b c
       | "str.replace", [ a; b; c ] -> Expr.triop Ty_str String_replace a b c
+      | "str.replace_all", [ a; b; c ] ->
+        Expr.triop Ty_str String_replace_all a b c
       | "str.++", n -> Expr.raw_naryop Ty_str Concat n
       | "str.<", [ a; b ] -> Expr.raw_relop Ty_str Lt a b
       | "str.<=", [ a; b ] -> Expr.raw_relop Ty_str Le a b

src/smtml/ty.ml

@@ -355,23 +355,28 @@ module Triop = struct
     | String_extract
     | String_replace
     | String_index
+    | String_replace_all
 
   let equal op1 op2 =
     match (op1, op2) with
     | Ite, Ite
     | List_set, List_set
     | String_extract, String_extract
     | String_replace, String_replace
-    | String_index, String_index ->
+    | String_index, String_index
+    | String_replace_all, String_replace_all ->
       true
-    | (Ite | List_set | String_extract | String_replace | String_index), _ ->
+    | ( ( Ite | List_set | String_extract | String_replace | String_index
+        | String_replace_all )
+      , _ ) ->
       false
 
   let pp fmt = function
     | Ite -> Fmt.string fmt "ite"
     | String_extract -> Fmt.string fmt "substr"
     | String_replace -> Fmt.string fmt "replace"
     | String_index -> Fmt.string fmt "indexof"
+    | String_replace_all -> Fmt.string fmt "replace_all"
     | List_set -> Fmt.string fmt "set"
 end
 

src/smtml/ty.mli

@@ -192,6 +192,9 @@ module Triop : sig
       (** Replace a substring. (str.replace String String String String) *)
     | String_index
       (** Find the index of a substring. (str.indexof String String Int Int) *)
+    | String_replace_all
+      (** Replace all occurrences of a substring. (str.replace_all String String
+          String String) *)
 
   (** [equal op1 op2] checks if ternary operations [op1] and [op2] are equal. *)
   val equal : t -> t -> bool