Module String.Reg_Lang

A module for regular language constant symbols that occur in terms.

val empty : t

The empty regular language.

val all : t

The language that contains all strings.

val allchar : t

The language that contains all strings of length 1.

val of_string : t

Singleton language containing a single string.

val range : t

range s1 s2 is the language containing all singleton strings (i.e. string of length 1) that are lexicographically beetween s1 and s2, **assuming s1 and s2 are singleton strings**. Else it is the empty language.

val concat : t

Language concatenation.

val union : t

Language union.

val inter : t

Language intersection.

val diff : t

Language difference.

val star : t

Kleene closure.

val cross : t

Kleene cross. cross e abbreviates concat e (star e).

val complement : t

Language complement.

val option : t

Option. option e abbreviates union e (of_string "").

val power : int -> t

power n e is n-th power of e.

val loop : (int * int) -> t

Loop. See SMTLIb documentation.