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

Public Member Functions

def as_ast
 
def get_id
 
def kind
 
def subsort
 
def cast
 
def name
 
def __eq__
 
def __ne__
 
def __hash__
 
- 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

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

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 CheckSatResult.__ne__(), and Probe.__ne__().

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

Definition at line 582 of file z3py.py.

583  def __hash__(self):
584  """ Hash code. """
585  return AstRef.__hash__(self)
def __hash__
Definition: z3py.py:582
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.

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

Definition at line 503 of file z3py.py.

504  def as_ast(self):
505  return Z3_sort_to_ast(self.ctx_ref(), self.ast)
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 as_ast
Definition: z3py.py:503
def ctx_ref
Definition: z3py.py:352
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.

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

Definition at line 506 of file z3py.py.

507  def get_id(self):
508  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
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 as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
def get_id
Definition: z3py.py:506
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.

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

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

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

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