A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.
Definition at line 559 of file z3py.py.
◆ __eq__() 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
Reimplemented from AstRef.
Definition at line 618 of file z3py.py.
618 def__eq__(self, other):
619 """Return `True` if `self` and `other` are the same Z3 sort. 622 >>> p.sort() == BoolSort() 624 >>> p.sort() == IntSort()bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
Referenced by CheckSatResult.__ne__(), and Probe.__ne__().
◆ __hash__()Hash code.
Reimplemented from AstRef.
Definition at line 642 of file z3py.py.
644 returnAstRef.__hash__(self)
◆ __ne__() 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 631 of file z3py.py.
631 def__ne__(self, other):
632 """Return `True` if `self` and `other` are not the same Z3 sort. 635 >>> p.sort() != BoolSort() 637 >>> p.sort() != IntSort() 640 return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
◆ as_ast()Return a pointer to the corresponding C Z3_ast object.
Reimplemented from AstRef.
Definition at line 562 of file z3py.py.
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.
Referenced by AstRef.__del__(), SeqRef.__ge__(), SeqRef.__getitem__(), SeqRef.__gt__(), BitVecRef.__invert__(), SeqRef.__le__(), CharRef.__le__(), SeqRef.__lt__(), ArithRef.__neg__(), BitVecRef.__neg__(), AlgebraicNumRef.approx(), ExprRef.arg(), IntNumRef.as_binary_string(), BitVecNumRef.as_binary_string(), RatNumRef.as_decimal(), AlgebraicNumRef.as_decimal(), IntNumRef.as_string(), RatNumRef.as_string(), BitVecNumRef.as_string(), FiniteDomainRef.as_string(), FiniteDomainNumRef.as_string(), FPRef.as_string(), FPRMRef.as_string(), FPNumRef.as_string(), SeqRef.as_string(), SeqRef.at(), ExprRef.decl(), ArrayRef.default(), RatNumRef.denominator(), AstRef.eq(), FPNumRef.exponent(), FPNumRef.exponent_as_bv(), FPNumRef.exponent_as_long(), AstRef.get_id(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), PatternRef.get_id(), QuantifierRef.get_id(), AstRef.hash(), AlgebraicNumRef.index(), CharRef.is_digit(), SeqRef.is_string(), SeqRef.is_string_value(), FPNumRef.isInf(), FPNumRef.isNaN(), FPNumRef.isNegative(), FPNumRef.isNormal(), FPNumRef.isPositive(), FPNumRef.isSubnormal(), FPNumRef.isZero(), ExprRef.num_args(), RatNumRef.numerator(), AlgebraicNumRef.poly(), AstRef.sexpr(), FPNumRef.sign(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPNumRef.significand_as_long(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), FiniteDomainRef.sort(), FPRef.sort(), SeqRef.sort(), CharRef.to_bv(), CharRef.to_int(), and AstRef.translate().
◆ cast()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 FPSortRef, BitVecSortRef, ArithSortRef, BoolSortRef, and TypeVarRef.
Definition at line 593 of file z3py.py.
594 """Try to cast `val` as an element of sort `self`. 596 This method is used in Z3Py to convert Python objects such as integers, 597 floats, longs and strings into Z3 expressions. 600 >>> RealSort().cast(x) 604_z3_assert(
is_expr(val),
"Z3 expression expected")
605_z3_assert(self.eq(val.sort()),
"Sort mismatch")
◆ get_id()Return unique identifier for object. It can be used for hash-tables and maps.
Reimplemented from AstRef.
Definition at line 565 of file z3py.py.
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....
◆ kind()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 568 of file z3py.py.
569 """Return the Z3 internal kind of a sort. 570 This method can be used to test if `self` is one of the Z3 builtin sorts. 573 >>> b.kind() == Z3_BOOL_SORT 575 >>> b.kind() == Z3_INT_SORT 577 >>> A = ArraySort(IntSort(), IntSort()) 578 >>> A.kind() == Z3_ARRAY_SORT 580 >>> A.kind() == Z3_INT_SORT 583 return_sort_kind(self.ctx, self.ast)
Referenced by ArithSortRef.is_int(), and ArithSortRef.is_real().
◆ name()Return the name (string) of sort `self`. >>> BoolSort().name() 'Bool' >>> ArraySort(IntSort(), IntSort()).name() 'Array'
Definition at line 608 of file z3py.py.
609 """Return the name (string) of sort `self`. 611 >>> BoolSort().name() 613 >>> ArraySort(IntSort(), IntSort()).name()Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
Referenced by Datatype.__deepcopy__(), and Datatype.__repr__().
◆ subsort() def subsort ( self, other )Return `True` if `self` is a subsort of `other`. >>> IntSort().subsort(RealSort()) True
Reimplemented in BitVecSortRef, ArithSortRef, BoolSortRef, and TypeVarRef.
Definition at line 585 of file z3py.py.
585 defsubsort(self, other):
586 """Return `True` if `self` is a subsort of `other`. 588 >>> IntSort().subsort(RealSort())RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4