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)
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__ (self)
 
def __str__ (self)
 
def __repr__ (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 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 450 of file z3py.py.

Member Function Documentation

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 508 of file z3py.py.

Referenced by CheckSatResult.__ne__(), and Probe.__ne__().

508  def __eq__(self, other):
509  """Return `True` if `self` and `other` are the same Z3 sort.
510 
511  >>> p = Bool('p')
512  >>> p.sort() == BoolSort()
513  True
514  >>> p.sort() == IntSort()
515  False
516  """
517  if other == None:
518  return False
519  return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
520 
def ctx_ref(self)
Definition: z3py.py:305
Z3_bool Z3_API Z3_is_eq_sort(__in Z3_context c, __in Z3_sort s1, __in Z3_sort s2)
compare sorts.
def __eq__(self, other)
Definition: z3py.py:508
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 521 of file z3py.py.

521  def __ne__(self, other):
522  """Return `True` if `self` and `other` are not the same Z3 sort.
523 
524  >>> p = Bool('p')
525  >>> p.sort() != BoolSort()
526  False
527  >>> p.sort() != IntSort()
528  True
529  """
530  return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
531 
def __ne__(self, other)
Definition: z3py.py:521
def ctx_ref(self)
Definition: z3py.py:305
Z3_bool Z3_API Z3_is_eq_sort(__in Z3_context c, __in Z3_sort s1, __in Z3_sort s2)
compare sorts.
def as_ast (   self)

Definition at line 452 of file z3py.py.

452  def as_ast(self):
453  return Z3_sort_to_ast(self.ctx_ref(), self.ast)
454 
def as_ast(self)
Definition: z3py.py:452
Z3_ast Z3_API Z3_sort_to_ast(__in Z3_context c, __in Z3_sort s)
Convert a Z3_sort into Z3_ast. This is just type casting.
def ctx_ref(self)
Definition: z3py.py:305
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 483 of file z3py.py.

483  def cast(self, val):
484  """Try to cast `val` as an element of sort `self`.
485 
486  This method is used in Z3Py to convert Python objects such as integers,
487  floats, longs and strings into Z3 expressions.
488 
489  >>> x = Int('x')
490  >>> RealSort().cast(x)
491  ToReal(x)
492  """
493  if __debug__:
494  _z3_assert(is_expr(val), "Z3 expression expected")
495  _z3_assert(self.eq(val.sort()), "Sort mismatch")
496  return val
497 
def cast(self, val)
Definition: z3py.py:483
def eq(self, other)
Definition: z3py.py:309
def is_expr(a)
Definition: z3py.py:961
def get_id (   self)

Definition at line 455 of file z3py.py.

455  def get_id(self):
456  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
457 
458 
def as_ast(self)
Definition: z3py.py:296
unsigned Z3_API Z3_get_ast_id(__in 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.
def get_id(self)
Definition: z3py.py:455
def ctx_ref(self)
Definition: z3py.py:305
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 459 of file z3py.py.

Referenced by ArithSortRef.is_int(), and ArithSortRef.is_real().

459  def kind(self):
460  """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
461 
462  >>> b = BoolSort()
463  >>> b.kind() == Z3_BOOL_SORT
464  True
465  >>> b.kind() == Z3_INT_SORT
466  False
467  >>> A = ArraySort(IntSort(), IntSort())
468  >>> A.kind() == Z3_ARRAY_SORT
469  True
470  >>> A.kind() == Z3_INT_SORT
471  False
472  """
473  return _sort_kind(self.ctx, self.ast)
474 
def kind(self)
Definition: z3py.py:459
def name (   self)
Return the name (string) of sort `self`.

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

Definition at line 498 of file z3py.py.

498  def name(self):
499  """Return the name (string) of sort `self`.
500 
501  >>> BoolSort().name()
502  'Bool'
503  >>> ArraySort(IntSort(), IntSort()).name()
504  'Array'
505  """
506  return _symbol2py(self.ctx, Z3_get_sort_name(self.ctx_ref(), self.ast))
507 
Z3_symbol Z3_API Z3_get_sort_name(__in Z3_context c, __in Z3_sort d)
Return the sort name as a symbol.
def ctx_ref(self)
Definition: z3py.py:305
def name(self)
Definition: z3py.py:498
def subsort (   self,
  other 
)
Return `True` if `self` is a subsort of `other`. 

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

Definition at line 475 of file z3py.py.

475  def subsort(self, other):
476  """Return `True` if `self` is a subsort of `other`.
477 
478  >>> IntSort().subsort(RealSort())
479  True
480  """
481  return False
482 
def subsort(self, other)
Definition: z3py.py:475