Add support for extra regular expression operators

Author: joaomhmpereira

src/smtml/bitwuzla_mappings.default.ml

@@ -81,6 +81,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let roundingMode = mk_rm_sort ()
 
+    let regexp = mk_bool_sort ()
+
     let ty t = Term.sort t
 
     let to_ety _ = Fmt.failwith "Bitwuzla_mappings: to_ety not implemented"
@@ -222,6 +224,12 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
   end
 
   module Re = struct
+    let allchar _ = Fmt.failwith "Bitwuzla_mappings: Re.allchar not implemented"
+
+    let all _ = Fmt.failwith "Bitwuzla_mappings: Re.all not implemented"
+
+    let none _ = Fmt.failwith "Bitwuzla_mappings: Re.none not implemented"
+
     let star _ = Fmt.failwith "Bitwuzla_mappings: Re.star not implemented"
 
     let plus _ = Fmt.failwith "Bitwuzla_mappings: Re.plus not implemented"
@@ -232,6 +240,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let range _ = Fmt.failwith "Bitwuzla_mappings: Re.range not implemented"
 
+    let inter _ = Fmt.failwith "Bitwuzla_mappings: Re.inter not implemented"
+
     let loop _ = Fmt.failwith "Bitwuzla_mappings: Re.loop not implemented"
 
     let union _ = Fmt.failwith "Bitwuzla_mappings: Re.union not implemented"

src/smtml/cvc5_mappings.default.ml

@@ -79,6 +79,8 @@ module Fresh_cvc5 () = struct
 
     let roundingMode = Sort.mk_rm_sort tm
 
+    let regexp = Sort.mk_bool_sort tm
+
     let ty t = Term.sort t
 
     let to_ety _ = assert false
@@ -204,6 +206,12 @@ module Fresh_cvc5 () = struct
   end
 
   module Re = struct
+    let allchar () = Term.mk_term tm Kind.Regexp_allchar [||]
+
+    let all () = Term.mk_term tm Kind.Regexp_all [||]
+
+    let none () = Term.mk_term tm Kind.Regexp_none [||]
+
     let star t = Term.mk_term tm Kind.Regexp_star [| t |]
 
     let plus t = Term.mk_term tm Kind.Regexp_plus [| t |]
@@ -214,6 +222,8 @@ module Fresh_cvc5 () = struct
 
     let range t1 t2 = Term.mk_term tm Kind.Regexp_range [| t1; t2 |]
 
+    let inter t1 t2 = Term.mk_term tm Kind.Regexp_inter [| t1; t2 |]
+
     let loop t i1 i2 =
       let op = Op.mk_op tm Kind.Regexp_loop [| i1; i2 |] in
       Term.mk_term_op tm op [| t |]

src/smtml/dolmenexpr_to_expr.ml

@@ -144,6 +144,8 @@ module DolmenIntf = struct
   module Types = struct
     include DTy
 
+    let regexp = DTy.string_reg_lang
+
     let ty = DTerm.ty
 
     let to_ety (ty : DTy.t) : Ty.t =
@@ -209,6 +211,12 @@ module DolmenIntf = struct
   end
 
   module Re = struct
+    let all () = DTerm.String.RegLan.all
+
+    let allchar () = DTerm.String.RegLan.allchar
+
+    let none () = DTerm.String.RegLan.empty
+
     let star = DTerm.String.RegLan.star
 
     let plus = DTerm.String.RegLan.cross
@@ -219,6 +227,8 @@ module DolmenIntf = struct
 
     let range = DTerm.String.RegLan.range
 
+    let inter = DTerm.String.RegLan.inter
+
     let loop t i1 i2 = DTerm.String.RegLan.loop i1 i2 t
 
     let union = nary_to_binary DTerm.Const.String.Reg_Lang.union

src/smtml/dolmenexpr_to_expr.mli

@@ -92,6 +92,8 @@ module DolmenIntf : sig
 
     val roundingMode : ty
 
+    val regexp : ty
+
     val ty : term -> ty
 
     val to_ety : ty -> Ty.t
@@ -186,6 +188,12 @@ module DolmenIntf : sig
   end
 
   module Re : sig
+    val allchar : unit -> term
+
+    val all : unit -> term
+
+    val none : unit -> term
+
     val star : term -> term
 
     val plus : term -> term
@@ -196,6 +204,8 @@ module DolmenIntf : sig
 
     val range : term -> term -> term
 
+    val inter : term -> term -> term
+
     val loop : term -> int -> int -> term
 
     val union : term list -> term

src/smtml/mappings.ml

@@ -66,7 +66,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty_fp 32 -> f32
       | Ty_fp 64 -> f64
       | Ty_roundingMode -> M.Types.roundingMode
-      | (Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) as ty ->
+      | Ty_regexp -> M.Types.regexp
+      | (Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none) as ty ->
         Fmt.failwith "Unsupported theory: %a@." Ty.pp ty
 
     let make_symbol (ctx : symbol_ctx) (s : Symbol.t) : symbol_ctx * M.term =
@@ -272,6 +273,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       let binop op e1 e2 =
         match op with
         | Binop.Regexp_range -> M.Re.range e1 e2
+        | Regexp_inter -> M.Re.inter e1 e2
         | op ->
           Fmt.failwith {|Regexp: Unsupported binop operator "%a"|} Binop.pp op
 
@@ -687,6 +689,9 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         let base' = v (Bitv (Bitvector.of_int32 base)) in
         let ctx, offset' = encode_expr ctx offset in
         (ctx, I32.binop Add base' offset')
+      | Symbol { name = Simple "re.all"; _ } -> (ctx, M.Re.all ())
+      | Symbol { name = Simple "re.none"; _ } -> (ctx, M.Re.none ())
+      | Symbol { name = Simple "re.allchar"; _ } -> (ctx, M.Re.allchar ())
       | Symbol sym -> make_symbol ctx sym
       (* FIXME: add a way to support building these expressions without apps *)
       | App ({ name = Simple "fp.add"; _ }, [ rm; a; b ]) ->

src/smtml/mappings.nop.ml

@@ -75,6 +75,8 @@ module Nop = struct
 
       let roundingMode = `Ty
 
+      let regexp = `Ty
+
       let ty _ = assert false
 
       let to_ety _ = assert false
@@ -183,6 +185,12 @@ module Nop = struct
     end
 
     module Re = struct
+      let allchar _ = assert false
+
+      let all _ = assert false
+
+      let none _ = assert false
+
       let star _ = assert false
 
       let plus _ = assert false
@@ -193,6 +201,8 @@ module Nop = struct
 
       let range _ = assert false
 
+      let inter _ = assert false
+
       let loop _ = assert false
 
       let union _ = assert false

src/smtml/mappings_intf.ml

@@ -122,6 +122,9 @@ module type M = sig
 
     val roundingMode : ty
 
+    (** [regexp] represents the regular expression type. *)
+    val regexp : ty
+
     (** [ty t] retrieves the type of the term [t]. *)
     val ty : term -> ty
 
@@ -318,6 +321,16 @@ module type M = sig
   (** {2 Regular Expression Operations} *)
 
   module Re : sig
+    (** [all] constructs the regular expression that matches all. *)
+    val all : unit -> term
+
+    (** [allchar] constructs the regular expression that matches any character.
+    *)
+    val allchar : unit -> term
+
+    (** [empty] constructs the empty regular expression. *)
+    val none : unit -> term
+
     (** [star t] constructs the Kleene star of the regular expression term [t].
     *)
     val star : term -> term
@@ -337,6 +350,10 @@ module type M = sig
         in the range from [t1] to [t2]. *)
     val range : term -> term -> term
 
+    (** [inter t1 t2] constructs the intersection of the regular expression
+        terms [t1] and [t2]. *)
+    val inter : term -> term -> term
+
     (** [loop t min max] constructs a regular expression term matching [t]
         repeated between [min] and [max] times. *)
     val loop : term -> int -> int -> term

src/smtml/smtlib.ml

@@ -72,6 +72,8 @@ module Term = struct
       | "roundTowardPositive" | "RTP" | "roundTowardNegative" | "RTN"
       | "roundTowardZero" | "RTZ" ->
         Expr.symbol { id with ty = Ty_roundingMode }
+      | "re.all" | "re.allchar" | "re.none" ->
+        Expr.symbol { id with ty = Ty_regexp }
       | _ -> Expr.symbol id
     end
     | Term, Indexed { basename = base; indices } -> begin
@@ -191,6 +193,7 @@ module Term = struct
       | "re.opt", [ a ] -> Expr.raw_unop Ty_regexp Regexp_opt a
       | "re.comp", [ a ] -> Expr.raw_unop Ty_regexp Regexp_comp a
       | "re.range", [ a; b ] -> Expr.raw_binop Ty_regexp Regexp_range a b
+      | "re.inter", [ a; b ] -> Expr.raw_binop Ty_regexp Regexp_inter a b
       | "re.union", n -> Expr.raw_naryop Ty_regexp Regexp_union n
       | "re.++", n -> Expr.raw_naryop Ty_regexp Concat n
       | "bvnot", [ a ] -> Expr.raw_unop Ty_none Not a

src/smtml/ty.ml

@@ -230,6 +230,7 @@ module Binop = struct
     | String_in_re
     (* Regexp *)
     | Regexp_range
+    | Regexp_inter
 
   let equal o1 o2 =
     match (o1, o2) with
@@ -261,12 +262,14 @@ module Binop = struct
     | String_contains, String_contains
     | String_last_index, String_last_index
     | String_in_re, String_in_re
-    | Regexp_range, Regexp_range ->
+    | Regexp_range, Regexp_range
+    | Regexp_inter, Regexp_inter ->
       true
     | ( ( Add | Sub | Mul | Div | DivU | Rem | RemU | Shl | ShrA | ShrL | And
         | Or | Xor | Implies | Pow | Min | Max | Copysign | Rotl | Rotr | At
         | List_cons | List_append | String_prefix | String_suffix
-        | String_contains | String_last_index | String_in_re | Regexp_range )
+        | String_contains | String_last_index | String_in_re | Regexp_range
+        | Regexp_inter )
       , _ ) ->
       false
 
@@ -300,6 +303,7 @@ module Binop = struct
     | String_last_index -> Fmt.string fmt "last_indexof"
     | String_in_re -> Fmt.string fmt "in_re"
     | Regexp_range -> Fmt.string fmt "range"
+    | Regexp_inter -> Fmt.string fmt "inter"
 end
 
 module Relop = struct

src/smtml/ty.mli

@@ -143,6 +143,7 @@ module Binop : sig
     | String_in_re  (** Check if a string matches a regular expression. *)
     (* Regexp operations *)
     | Regexp_range  (** Range of characters. *)
+    | Regexp_inter  (** Intersection of regular expressions. *)
 
   (** [equal op1 op2] checks if binary operations [op1] and [op2] are equal. *)
   val equal : t -> t -> bool