package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

String operations

Satisfy the required interface for the typing of smtlib's strings.

include Dolmen_intf.Term.Smtlib_String_String with type t := t

val of_ustring : string -> t

Create a string from a unicode UTF-8 encoded string (with escape sequences already interpreted as unicode characters).

val length : t -> t

Length of a string expression.

val at : t -> t -> t

Get the char at the given position.

val is_digit : t -> t

Is the string a singleton string with a single digit character ?

val to_code : t -> t

Returns the code point of the single character of the string, or (-1) is the string is not a singleton.

val of_code : t -> t

Returns the singleton string whose only character is the given code point.

val to_int : t -> t

Evaluates the string as a decimal natural number, or (-1) if it's not possible.

val of_int : t -> t

Convert an int expression to a string in decimal representation.

val concat : t -> t -> t

String concatenation.

val sub : t -> t -> t -> t

Substring extraction.

val index_of : t -> t -> t -> t

Index of the first occurrence of the second string in first one, starting at the position of the third argument.

val replace : t -> t -> t -> t

Replace the first occurrence.

val replace_all : t -> t -> t -> t

Replace all occurrences.

val replace_re : t -> t -> t -> t

Replace the leftmost, shortest re ocurrence.

val replace_re_all : t -> t -> t -> t

Replace left-to-right, each shortest non empty re occurrence.

val is_prefix : t -> t -> t

First string is a prefix of the second one.

val is_suffix : t -> t -> t

First string is a suffix of the second one.

val contains : t -> t -> t

First string contains the second one.

val lt : t -> t -> t

Lexicographic strict ordering.

val leq : t -> t -> t

Lexicographic large ordering.

val in_re : t -> t -> t

String Regular languager membership

module RegLan : Dolmen_intf.Term.Smtlib_String_RegLan with type t := t

Sub-module used for namespacing for the regular language part of the theory requirements.