Z3Seq

public class Z3Seq<Element> : AnyZ3Ast where Element : SortKind

An AST class for Z3 sequence sorts with a given base element sort.

  • Gets the statically-typed Z3Sort associated with this Z3Seq.

    Declaration

    Swift

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

Functions and members

  • Returns the AST for this sequence’s length.

    Declaration

    Swift

    var length: Z3Int { get }

  • Retrieve from this sequence the the element positioned at position index.

    Declaration

    Swift

    subscript(index: Z3Int) -> Z3Ast<Element> { get }

  • Return index of the first occurrence of search in this sequence starting from offset.

    If this sequence does not contain search, then the value is -1, if offset is the length of this sequence, then the value is -1 as well. The value is -1 if offset is negative or larger than the length of this sequence.

    Declaration

    Swift

    func index(of search: Z3Seq<Element>, offset: Z3Int) -> Z3Int

  • Return index of the last occurrence of search in this sequence.

    If this sequence does not contain search, then the value is -1.

    Declaration

    Swift

    func lastIndex(of search: Z3Seq<Element>) -> Z3Int

  • Check if subsequence is a subsequence of this sequence.

    Declaration

    Swift

    func contains(search: Z3Seq<Element>) -> Z3Bool

  • Extract a subsequence starting at offset of length.

    Declaration

    Swift

    func extract(offset: Z3Int, length: Z3Int) -> Z3Seq

  • Replace the first occurrence of src with dst in this sequence.

    Declaration

    Swift

    func replace(source: Z3Seq, dest: Z3Seq) -> Z3Seq

  • Retrieve from this sequence the unit sequence positioned at position index.

    Declaration

    Swift

    func at(index: Z3Int) -> Z3Seq

  • Create a regular expression that accepts this sequence.

    Declaration

    Swift

    func toRegularExp() -> Z3RegularExp<Element>

  • Check for regular expression membership.

    Declaration

    Swift

    func inRegExp(_ re: Z3RegularExp<Element>) -> Z3Bool