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__ (self, ast, ctx=None)
 
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 449 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 506 of file z3py.py.

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

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

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

Definition at line 451 of file z3py.py.

451  def as_ast(self):
452  return Z3_sort_to_ast(self.ctx_ref(), self.ast)
453 
def as_ast(self)
Definition: z3py.py:451
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.
def ctx_ref(self)
Definition: z3py.py:304
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 481 of file z3py.py.

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

Definition at line 454 of file z3py.py.

454  def get_id(self):
455  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
456 
def as_ast(self)
Definition: z3py.py:296
def get_id(self)
Definition: z3py.py:454
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.
def ctx_ref(self)
Definition: z3py.py:304
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 457 of file z3py.py.

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

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

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

Definition at line 496 of file z3py.py.

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

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

Definition at line 473 of file z3py.py.

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