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:950
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.
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