Z3 |

Public Member Functions
SeqSortRef Class Reference

Strings, Sequences and Regular expressions. More...

Inheritance diagram for SeqSortRef:

## Public Member Functions
def | is_string (self)
def | basis (self)
Public Member Functions inherited from SortRef
def | as_ast (self)
def | get_id (self)
def | kind (self)
def | subsort (self, other)
def | cast (self, val)
def | name (self)
def | __eq__ (self, other)
def | __ne__ (self, other)
def | __hash__ (self)
Public Member Functions inherited from AstRef
def | __init__ (self, ast, ctx=None)
def | __del__ (self)
def | __deepcopy__ (self, memo={})
def | __str__ (self)
def | __repr__ (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __nonzero__ (self)
def | __bool__ (self)
def | sexpr (self)
def | as_ast (self)
def | get_id (self)
def | ctx_ref (self)
def | eq (self, other)
def | translate (self, target)
def | __copy__ (self)
def | hash (self)
Public Member Functions inherited from Z3PPObject
def | use_pp (self)

## Additional Inherited Members
Data Fields inherited from AstRef
| ast
| ctx

## Detailed Description

Strings, Sequences and Regular expressions.

    Sequence sort.

Definition at line 10551 of file z3py.py.

## Member Function Documentation

## ◆ basis()

def basis | ( |  | self | ) |

Definition at line 10565 of file z3py.py.

10565 def basis(self):
10566 return _to_sort_ref(Z3_get_seq_sort_basis(self.ctx_ref(), self.ast), self.ctx)
10567
10568
Z3_get_seq_sort_basis
Z3_sort Z3_API Z3_get_seq_sort_basis(Z3_context c, Z3_sort s)
Retrieve basis sort for sequence sort.

## ◆ is_string()

def is_string | ( |  | self | ) |

    Determine if sort is a string
    >>> s = StringSort()
    >>> s.is_string()
    True
    >>> s = SeqSort(IntSort())
    >>> s.is_string()
    False

Definition at line 10554 of file z3py.py.

10554 def is_string(self):
10555 """Determine if sort is a string
10556 >>> s = StringSort()
10557 >>> s.is_string()
10558 True
10559 >>> s = SeqSort(IntSort())
10560 >>> s.is_string()
10561 False
10562 """
10563 return Z3_is_string_sort(self.ctx_ref(), self.ast)
10564
z3py.IntSort
def IntSort(ctx=None)
Definition: z3py.py:3100
z3py.SeqSort
def SeqSort(s)
Definition: z3py.py:10579
z3py.StringSort
def StringSort(ctx=None)
Definition: z3py.py:10569
z3py.is_string
def is_string(a)
Definition: z3py.py:10668
Z3_is_string_sort
bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s)
Check if s is a string sort.