Module Term.StringSource

String operations

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

include Dolmen_intf.Term.Smtlib_String_String with type t := t
Sourceval of_ustring : string -> t

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

Sourceval length : t -> t

Length of a string expression.

Sourceval at : t -> t -> t

Get the char at the given position.

Sourceval is_digit : t -> t

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

Sourceval to_code : t -> t

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

Sourceval of_code : t -> t

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

Sourceval to_int : t -> t

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

Sourceval of_int : t -> t

Convert an int expression to a string in decimal representation.

Sourceval concat : t -> t -> t

String concatenation.

Sourceval sub : t -> t -> t -> t

Substring extraction.

Sourceval 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.

Sourceval replace : t -> t -> t -> t

Replace the first occurrence.

Sourceval replace_all : t -> t -> t -> t

Replace all occurrences.

Sourceval replace_re : t -> t -> t -> t

Replace the leftmost, shortest re ocurrence.

Sourceval replace_re_all : t -> t -> t -> t

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

Sourceval is_prefix : t -> t -> t

First string is a prefix of the second one.

Sourceval is_suffix : t -> t -> t

First string is a suffix of the second one.

Sourceval contains : t -> t -> t

First string contains the second one.

Sourceval lt : t -> t -> t

Lexicographic strict ordering.

Sourceval leq : t -> t -> t

Lexicographic large ordering.

Sourceval in_re : t -> t -> t

String Regular languager membership

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