Z3
Public Member Functions
SortRef Class Reference
+ Inheritance diagram for SortRef:

Public Member Functions

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

A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.

Definition at line 501 of file z3py.py.

Member Function Documentation

◆ __eq__()

def __eq__ (   self,
  other 
)
Return `True` if `self` and `other` are the same Z3 sort.

>>> p = Bool('p')
>>> p.sort() == BoolSort()
True
>>> p.sort() == IntSort()
False

Definition at line 558 of file z3py.py.

Referenced by Probe.__ne__().

558  def __eq__(self, other):
559  """Return `True` if `self` and `other` are the same Z3 sort.
560 
561  >>> p = Bool('p')
562  >>> p.sort() == BoolSort()
563  True
564  >>> p.sort() == IntSort()
565  False
566  """
567  if other is None:
568  return False
569  return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
570 
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.

◆ __hash__()

def __hash__ (   self)
Hash code. 

Definition at line 582 of file z3py.py.

582  def __hash__(self):
583  """ Hash code. """
584  return AstRef.__hash__(self)
585 

◆ __ne__()

def __ne__ (   self,
  other 
)
Return `True` if `self` and `other` are not the same Z3 sort.

>>> p = Bool('p')
>>> p.sort() != BoolSort()
False
>>> p.sort() != IntSort()
True

Definition at line 571 of file z3py.py.

571  def __ne__(self, other):
572  """Return `True` if `self` and `other` are not the same Z3 sort.
573 
574  >>> p = Bool('p')
575  >>> p.sort() != BoolSort()
576  False
577  >>> p.sort() != IntSort()
578  True
579  """
580  return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
581 
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.

◆ as_ast()

def as_ast (   self)

Definition at line 503 of file z3py.py.

503  def as_ast(self):
504  return Z3_sort_to_ast(self.ctx_ref(), self.ast)
505 
Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s)
Convert a Z3_sort into Z3_ast. This is just type casting.

◆ cast()

def cast (   self,
  val 
)
Try to cast `val` as an element of sort `self`.

This method is used in Z3Py to convert Python objects such as integers,
floats, longs and strings into Z3 expressions.

>>> x = Int('x')
>>> RealSort().cast(x)
ToReal(x)

Definition at line 533 of file z3py.py.

533  def cast(self, val):
534  """Try to cast `val` as an element of sort `self`.
535 
536  This method is used in Z3Py to convert Python objects such as integers,
537  floats, longs and strings into Z3 expressions.
538 
539  >>> x = Int('x')
540  >>> RealSort().cast(x)
541  ToReal(x)
542  """
543  if z3_debug():
544  _z3_assert(is_expr(val), "Z3 expression expected")
545  _z3_assert(self.eq(val.sort()), "Sort mismatch")
546  return val
547 
def z3_debug()
Definition: z3py.py:58
def is_expr(a)
Definition: z3py.py:1105

◆ get_id()

def get_id (   self)

Definition at line 506 of file z3py.py.

506  def get_id(self):
507  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
508 
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.

◆ kind()

def kind (   self)
Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.

>>> b = BoolSort()
>>> b.kind() == Z3_BOOL_SORT
True
>>> b.kind() == Z3_INT_SORT
False
>>> A = ArraySort(IntSort(), IntSort())
>>> A.kind() == Z3_ARRAY_SORT
True
>>> A.kind() == Z3_INT_SORT
False

Definition at line 509 of file z3py.py.

509  def kind(self):
510  """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
511 
512  >>> b = BoolSort()
513  >>> b.kind() == Z3_BOOL_SORT
514  True
515  >>> b.kind() == Z3_INT_SORT
516  False
517  >>> A = ArraySort(IntSort(), IntSort())
518  >>> A.kind() == Z3_ARRAY_SORT
519  True
520  >>> A.kind() == Z3_INT_SORT
521  False
522  """
523  return _sort_kind(self.ctx, self.ast)
524 

◆ name()

def name (   self)
Return the name (string) of sort `self`.

>>> BoolSort().name()
'Bool'
>>> ArraySort(IntSort(), IntSort()).name()
'Array'

Definition at line 548 of file z3py.py.

548  def name(self):
549  """Return the name (string) of sort `self`.
550 
551  >>> BoolSort().name()
552  'Bool'
553  >>> ArraySort(IntSort(), IntSort()).name()
554  'Array'
555  """
556  return _symbol2py(self.ctx, Z3_get_sort_name(self.ctx_ref(), self.ast))
557 
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.

◆ subsort()

def subsort (   self,
  other 
)
Return `True` if `self` is a subsort of `other`.

>>> IntSort().subsort(RealSort())
True

Definition at line 525 of file z3py.py.

525  def subsort(self, other):
526  """Return `True` if `self` is a subsort of `other`.
527 
528  >>> IntSort().subsort(RealSort())
529  True
530  """
531  return False
532