package dolmen

  1. Overview
  2. Docs

Module String.Reg_LangSource

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

Sourceval empty : t

The empty regular language.

Sourceval all : t

The language that contains all strings.

Sourceval allchar : t

The language that contains all strings of length 1.

Sourceval of_string : t

Singleton language containing a single string.

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

Sourceval concat : t

Language concatenation.

Sourceval union : t

Language union.

Sourceval inter : t

Language intersection.

Sourceval diff : t

Language difference.

Sourceval star : t

Kleene closure.

Sourceval cross : t

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

Sourceval complement : t

Language complement.

Sourceval option : t

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

Sourceval power : int -> t

power n e is n-th power of e.

Sourceval loop : (int * int) -> t

Loop. See SMTLIb documentation.