Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions
SeqRef Class Reference
+ Inheritance diagram for SeqRef:

Public Member Functions

def sort
 
def __add__
 
def __radd__
 
def __getitem__
 
def at
 
def is_string
 
def is_string_value
 
def as_string
 
- Public Member Functions inherited from ExprRef
def as_ast
 
def get_id
 
def sort
 
def sort_kind
 
def __eq__
 
def __hash__
 
def __ne__
 
def params
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
def hash
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Sequence expression.

Definition at line 9958 of file z3py.py.

Member Function Documentation

def __add__ (   self,
  other 
)

Definition at line 9964 of file z3py.py.

9965  def __add__(self, other):
9966  return Concat(self, other)
def __add__
Definition: z3py.py:9964
def Concat
Definition: z3py.py:3796
def __getitem__ (   self,
  i 
)

Definition at line 9970 of file z3py.py.

9971  def __getitem__(self, i):
9972  if _is_int(i):
9973  i = IntVal(i, self.ctx)
9974  return SeqRef(Z3_mk_seq_nth(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
def __getitem__
Definition: z3py.py:9970
Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the element positioned at position index. The function is under-specified if the inde...
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
def IntVal
Definition: z3py.py:2937
def __radd__ (   self,
  other 
)

Definition at line 9967 of file z3py.py.

9968  def __radd__(self, other):
9969  return Concat(other, self)
def __radd__
Definition: z3py.py:9967
def Concat
Definition: z3py.py:3796
def as_string (   self)
Return a string representation of sequence expression.

Definition at line 9986 of file z3py.py.

9987  def as_string(self):
9988  """Return a string representation of sequence expression."""
9989  if self.is_string_value():
9990  return Z3_get_string(self.ctx_ref(), self.as_ast())
9991  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
9992 
def as_string
Definition: z3py.py:9986
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
def is_string_value
Definition: z3py.py:9983
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s.
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
def at (   self,
  i 
)

Definition at line 9975 of file z3py.py.

9976  def at(self, i):
9977  if _is_int(i):
9978  i = IntVal(i, self.ctx)
9979  return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is...
def at
Definition: z3py.py:9975
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
def IntVal
Definition: z3py.py:2937
def is_string (   self)

Definition at line 9980 of file z3py.py.

9981  def is_string(self):
9982  return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast()))
def is_string
Definition: z3py.py:9980
bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s)
Check if s is a string sort.
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
def is_string_value (   self)

Definition at line 9983 of file z3py.py.

Referenced by SeqRef.as_string().

9984  def is_string_value(self):
9985  return Z3_is_string(self.ctx_ref(), self.as_ast())
def is_string_value
Definition: z3py.py:9983
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
def sort (   self)

Definition at line 9961 of file z3py.py.

9962  def sort(self):
9963  return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
def sort
Definition: z3py.py:9961
Strings, Sequences and Regular expressions.
Definition: z3py.py:9922
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.