Z3RegularExp Class Reference


                    
                    
                    getSort(_:)

Gets the statically-typed Z3Sort associated with this Z3RegularExp.

Declaration

Swift

static func getSort(_ context: Z3Context) -> Z3Sort


                    
                    
                    plus()

Create a regular expression language self+.

Declaration

Swift

func plus() -> Z3RegularExp


                    
                    
                    star()

Create a regular expression language self*.

Declaration

Swift

func star() -> Z3RegularExp


                    
                    
                    option()

Create a regular expression language [self].

Declaration

Swift

func option() -> Z3RegularExp


                    
                    
                    union(_:)

Create the union of this regular language and every other in others.

Declaration

Swift

func union(_ others: [Z3RegularExp]) -> Z3RegularExp


                    
                    
                    concat(_:)

Create the concatenation of this regular language and every other in others.

Declaration

Swift

func concat(_ others: [Z3RegularExp]) -> Z3RegularExp


                    
                    
                    range(low:high:)

Create the range regular expression over two sequences of length 1.

Declaration

Swift

func range(low: Z3Seq<Element>, high: Z3Seq<Element>) -> Z3RegularExp


                    
                    
                    loop(low:high:)

Create a regular expression loop.

The supplied regular expression self is repeated between low and high times. The low should be below high with one exception: when supplying the value high as 0, the meaning is to repeat the argument self at least low number of times, and with an unbounded upper bound.

Declaration

Swift

func loop(low: UInt32, high: UInt32) -> Z3RegularExp


                    
                    
                    power(count:)

Create a power regular expression.

Declaration

Swift

func power(count: UInt32) -> Z3RegularExp


                    
                    
                    intersect(_:)

Create the intersection of the regular languages.

Declaration

Swift

func intersect(_ others: [Z3RegularExp]) -> Z3RegularExp


                    
                    
                    complement()

Create the complement of the regular language self.

Declaration

Swift

func complement() -> Z3RegularExp


                    
                    
                    difference(_:)

Create the difference of this regular expression and other.

Declaration

Swift

func difference(_ other: Z3RegularExp) -> Z3RegularExp