Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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__

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

00508 
00509     def __eq__(self, other):
00510         """Return `True` if `self` and `other` are the same Z3 sort.
00511         
00512         >>> p = Bool('p')
00513         >>> p.sort() == BoolSort()
00514         True
00515         >>> p.sort() == IntSort()
00516         False
00517         """
00518         if other == None:
00519             return False
00520         return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)

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.

00521 
00522     def __ne__(self, other):
00523         """Return `True` if `self` and `other` are not the same Z3 sort.
00524         
00525         >>> p = Bool('p')
00526         >>> p.sort() != BoolSort()
00527         False
00528         >>> p.sort() != IntSort()
00529         True
00530         """
00531         return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)

def as_ast (   self)
Return a pointer to the corresponding C Z3_ast object.

Reimplemented from AstRef.

Definition at line 452 of file z3py.py.

Referenced by ExprRef.arg(), ExprRef.decl(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), ExprRef.num_args(), ExprRef.sort(), and BoolRef.sort().

00452 
00453     def as_ast(self):
00454         return Z3_sort_to_ast(self.ctx_ref(), self.ast)

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)

Reimplemented in BitVecSortRef, ArithSortRef, and BoolSortRef.

Definition at line 483 of file z3py.py.

00483 
00484     def cast(self, val):
00485         """Try to cast `val` as an element of sort `self`. 
00486 
00487         This method is used in Z3Py to convert Python objects such as integers,
00488         floats, longs and strings into Z3 expressions.
00489 
00490         >>> x = Int('x')
00491         >>> RealSort().cast(x)
00492         ToReal(x)
00493         """ 
00494         if __debug__:
00495             _z3_assert(is_expr(val), "Z3 expression expected")
00496             _z3_assert(self.eq(val.sort()), "Sort mismatch")
00497         return val

def get_id (   self)
Return unique identifier for object. It can be used for hash-tables and maps.

Reimplemented from AstRef.

Definition at line 455 of file z3py.py.

00455 
00456     def get_id(self):
00457         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
00458 

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.

00459 
00460     def kind(self):
00461         """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
00462         
00463         >>> b = BoolSort()
00464         >>> b.kind() == Z3_BOOL_SORT
00465         True
00466         >>> b.kind() == Z3_INT_SORT
00467         False
00468         >>> A = ArraySort(IntSort(), IntSort())
00469         >>> A.kind() == Z3_ARRAY_SORT
00470         True
00471         >>> A.kind() == Z3_INT_SORT
00472         False
00473         """
00474         return _sort_kind(self.ctx, self.ast)

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.

00498 
00499     def name(self):
00500         """Return the name (string) of sort `self`.
00501         
00502         >>> BoolSort().name()
00503         'Bool'
00504         >>> ArraySort(IntSort(), IntSort()).name()
00505         'Array'
00506         """
00507         return _symbol2py(self.ctx, Z3_get_sort_name(self.ctx_ref(), self.ast))

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

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

Reimplemented in BitVecSortRef, and ArithSortRef.

Definition at line 475 of file z3py.py.

00475 
00476     def subsort(self, other):
00477         """Return `True` if `self` is a subsort of `other`. 
00478         
00479         >>> IntSort().subsort(RealSort())
00480         True
00481         """
00482         return False

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines