Public Member Functions | |
def | as_ast |
def | get_id |
def | kind |
def | subsort |
def | cast |
def | name |
def | __eq__ |
def | __ne__ |
A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.
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 | ) |
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.