mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Remove size argument in OCaml's Z3.mk_re_intersect (#5383)

Browse source 
* Remove size argument in OCaml's `Z3.mk_re_intersect`

Passing the size as argument is unnecessary in OCaml, and that argument is abridged in all similar `Seq` functions. This applies the same pattern.

* Enable the ocaml documentation in Seq.

Turn all the comments into proper documentation comments.
This commit is contained in:
Gabriel Radanne 2021-07-06 10:21:04 +02:00 committed by GitHub
parent bdcfba1324
commit 0c7625cd26
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 39 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/ml/z3.ml
View file

@ -1272,7 +1272,7 @@ struct
let mk_re_concat ctx args = Z3native.mk_re_concat ctx (List.length args) args
let mk_re_range = Z3native.mk_re_range
let mk_re_loop = Z3native.mk_re_loop
let mk_re_intersect = Z3native.mk_re_intersect
let mk_re_intersect ctx args = Z3native.mk_re_intersect ctx (List.length args) args
let mk_re_complement = Z3native.mk_re_complement
let mk_re_empty = Z3native.mk_re_empty
let mk_re_full = Z3native.mk_re_full

76
src/api/ml/z3.mli
View file

@ -1850,115 +1850,115 @@ end
(** Sequences, Strings and Regular Expressions **)
module Seq :
sig
(* create a sequence sort *)
(** create a sequence sort *)
val mk_seq_sort : context -> Sort.sort -> Sort.sort
(* test if sort is a sequence sort *)
(** test if sort is a sequence sort *)
val is_seq_sort : context -> Sort.sort -> bool
(* create regular expression sorts over sequences of the argument sort *)
(** create regular expression sorts over sequences of the argument sort *)
val mk_re_sort : context -> Sort.sort -> Sort.sort
(* test if sort is a regular expression sort *)
(** test if sort is a regular expression sort *)
val is_re_sort : context -> Sort.sort -> bool
(* create string sort *)
(** create string sort *)
val mk_string_sort : context -> Sort.sort
(* test if sort is a string sort (a sequence of 8-bit bit-vectors) *)
(** test if sort is a string sort (a sequence of 8-bit bit-vectors) *)
val is_string_sort : context -> Sort.sort -> bool
(* create a string literal *)
(** create a string literal *)
val mk_string : context -> string -> Expr.expr
(* test if expression is a string *)
(** test if expression is a string *)
val is_string : context -> Expr.expr -> bool
(* retrieve string from string Expr.expr *)
(** retrieve string from string Expr.expr *)
val get_string : context -> Expr.expr -> string
(* the empty sequence over base sort *)
(** the empty sequence over base sort *)
val mk_seq_empty : context -> Sort.sort -> Expr.expr
(* a unit sequence *)
(** a unit sequence *)
val mk_seq_unit : context -> Expr.expr -> Expr.expr
(* sequence concatenation *)
(** sequence concatenation *)
val mk_seq_concat : context -> Expr.expr list -> Expr.expr
(* predicate if the first argument is a prefix of the second *)
(** predicate if the first argument is a prefix of the second *)
val mk_seq_prefix : context -> Expr.expr -> Expr.expr -> Expr.expr
(* predicate if the first argument is a suffix of the second *)
(** predicate if the first argument is a suffix of the second *)
val mk_seq_suffix : context -> Expr.expr -> Expr.expr -> Expr.expr
(* predicate if the first argument contains the second *)
(** predicate if the first argument contains the second *)
val mk_seq_contains : context -> Expr.expr -> Expr.expr -> Expr.expr
(* extract sub-sequence starting at index given by second argument and of length provided by third argument *)
(** extract sub-sequence starting at index given by second argument and of length provided by third argument *)
val mk_seq_extract : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
(* replace first occurrence of second argument by third *)
(** replace first occurrence of second argument by third *)
val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
(* a unit sequence at index provided by second argument *)
(** a unit sequence at index provided by second argument *)
val mk_seq_at : context -> Expr.expr -> Expr.expr -> Expr.expr
(* length of a sequence *)
(** length of a sequence *)
val mk_seq_length : context -> Expr.expr -> Expr.expr
(* index of the first occurrence of the second argument in the first *)
(** index of the first occurrence of the second argument in the first *)
val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
(* retrieve integer expression encoded in string *)
(** retrieve integer expression encoded in string *)
val mk_str_to_int : context -> Expr.expr -> Expr.expr
(* compare strings less-than-or-equal *)
(** compare strings less-than-or-equal *)
val mk_str_le : context -> Expr.expr -> Expr.expr -> Expr.expr
(* compare strings less-than *)
(** compare strings less-than *)
val mk_str_lt : context -> Expr.expr -> Expr.expr -> Expr.expr
(* convert an integer expression to a string *)
(** convert an integer expression to a string *)
val mk_int_to_str : context -> Expr.expr -> Expr.expr
(* create regular expression that accepts the argument sequence *)
(** create regular expression that accepts the argument sequence *)
val mk_seq_to_re : context -> Expr.expr -> Expr.expr
(* regular expression membership predicate *)
(** regular expression membership predicate *)
val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr
(* regular expression plus *)
(** regular expression plus *)
val mk_re_plus : context -> Expr.expr -> Expr.expr
(* regular expression star *)
(** regular expression star *)
val mk_re_star : context -> Expr.expr -> Expr.expr
(* optional regular expression *)
(** optional regular expression *)
val mk_re_option : context -> Expr.expr -> Expr.expr
(* union of regular expressions *)
(** union of regular expressions *)
val mk_re_union : context -> Expr.expr list -> Expr.expr
(* concatenation of regular expressions *)
(** concatenation of regular expressions *)
val mk_re_concat : context -> Expr.expr list -> Expr.expr
(* regular expression for the range between two characters *)
(** regular expression for the range between two characters *)
val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr
(* bounded loop regular expression *)
(** bounded loop regular expression *)
val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr
(* intersection of regular expressions *)
val mk_re_intersect : context -> int -> Expr.expr list -> Expr.expr
(** intersection of regular expressions *)
val mk_re_intersect : context -> Expr.expr list -> Expr.expr
(* the regular expression complement *)
(** the regular expression complement *)
val mk_re_complement : context -> Expr.expr -> Expr.expr
(* the regular expression that accepts no sequences *)
(** the regular expression that accepts no sequences *)
val mk_re_empty : context -> Sort.sort -> Expr.expr
(* the regular expression that accepts all sequences *)
(** the regular expression that accepts all sequences *)
val mk_re_full : context -> Sort.sort -> Expr.expr
end