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)
def | __hash__ (self)
Public Member Functions inherited from AstRef
def | __init__ (self, ast, ctx=None)
def | __del__ (self)
def | __deepcopy__ (self, memo={})
def | __str__ (self)
def | __repr__ (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __nonzero__ (self)
def | __bool__ (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 | __copy__ (self)
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 558 of file z3py.py.

## Member Function Documentation

## ◆ __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 617 of file z3py.py.

617 def __eq__(self, other):
618 """Return `True` if `self` and `other` are the same Z3 sort.
619
620 >>> p = Bool('p')
621 >>> p.sort() == BoolSort()
622 True
623 >>> p.sort() == IntSort()
624 False
625 """
626 if other is None:
627 return False
628 return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
629
z3py.IntSort
def IntSort(ctx=None)
Definition: z3py.py:3100
z3py.BoolSort
def BoolSort(ctx=None)
Definition: z3py.py:1655
z3py.Bool
def Bool(name, ctx=None)
Definition: z3py.py:1692
Z3_is_eq_sort
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__()

def __hash__ | ( |  | self | ) |

     Hash code.

Reimplemented from AstRef.

Definition at line 641 of file z3py.py.

641 def __hash__(self):
642 """ Hash code. """
643 return AstRef.__hash__(self)
644
645

## ◆ __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 630 of file z3py.py.

630 def __ne__(self, other):
631 """Return `True` if `self` and `other` are not the same Z3 sort.
632
633 >>> p = Bool('p')
634 >>> p.sort() != BoolSort()
635 False
636 >>> p.sort() != IntSort()
637 True
638 """
639 return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
640

## ◆ as_ast()

def as_ast | ( |  | self | ) |

    Return a pointer to the corresponding C Z3_ast object.

Reimplemented from AstRef.

Definition at line 561 of file z3py.py.

561 def as_ast(self):
562 return Z3_sort_to_ast(self.ctx_ref(), self.ast)
563
Z3_sort_to_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.

Referenced by AstRef.__del__(), SeqRef.__ge__(), QuantifierRef.__getitem__(), ArrayRef.__getitem__(), SeqRef.__getitem__(), SeqRef.__gt__(), BitVecRef.__invert__(), SeqRef.__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(), 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(), and AstRef.translate().

## ◆ cast()

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 BoolSortRef, ArithSortRef, BitVecSortRef, and FPSortRef.

Definition at line 592 of file z3py.py.

592 def cast(self, val):
593 """Try to cast `val` as an element of sort `self`.
594
595 This method is used in Z3Py to convert Python objects such as integers,
596 floats, longs and strings into Z3 expressions.
597
598 >>> x = Int('x')
599 >>> RealSort().cast(x)
600 ToReal(x)
601 """
602 if z3_debug():
603 _z3_assert(is_expr(val), "Z3 expression expected")
604 _z3_assert(self.eq(val.sort()), "Sort mismatch")
605 return val
606
z3py.z3_debug
def z3_debug()
Definition: z3py.py:64
z3py.ToReal
def ToReal(a)
Definition: z3py.py:3320
z3py.RealSort
def RealSort(ctx=None)
Definition: z3py.py:3117
z3py.is_expr
def is_expr(a)
Definition: z3py.py:1210
z3py.Int
def Int(name, ctx=None)
Definition: z3py.py:3210

Referenced by SortRef.cast().

## ◆ get_id()

def get_id | ( |  | self | ) |

    Return unique identifier for object. It can be used for hash-tables and maps.

Reimplemented from AstRef.

Definition at line 564 of file z3py.py.

564 def get_id(self):
565 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
566
Z3_get_ast_id
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()

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 567 of file z3py.py.

567 def kind(self):
568 """Return the Z3 internal kind of a sort.
569 This method can be used to test if `self` is one of the Z3 builtin sorts.
570
571 >>> b = BoolSort()
572 >>> b.kind() == Z3_BOOL_SORT
573 True
574 >>> b.kind() == Z3_INT_SORT
575 False
576 >>> A = ArraySort(IntSort(), IntSort())
577 >>> A.kind() == Z3_ARRAY_SORT
578 True
579 >>> A.kind() == Z3_INT_SORT
580 False
581 """
582 return _sort_kind(self.ctx, self.ast)
583
z3py.ArraySort
def ArraySort(*sig)
Definition: z3py.py:4645

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

## ◆ name()

def name | ( |  | self | ) |

    Return the name (string) of sort `self`.

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

Definition at line 607 of file z3py.py.

607 def name(self):
608 """Return the name (string) of sort `self`.
609
610 >>> BoolSort().name()
611 'Bool'
612 >>> ArraySort(IntSort(), IntSort()).name()
613 'Array'
614 """
615 return _symbol2py(self.ctx, Z3_get_sort_name(self.ctx_ref(), self.ast))
616
Z3_get_sort_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__(), Datatype.__repr__(), and SortRef.name().

## ◆ subsort()

def subsort | ( |  | self,
|  |  | other
| ) |  |

    Return `True` if `self` is a subsort of `other`.

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

Reimplemented in BoolSortRef, ArithSortRef, and BitVecSortRef.

Definition at line 584 of file z3py.py.

584 def subsort(self, other):
585 """Return `True` if `self` is a subsort of `other`.
586
587 >>> IntSort().subsort(RealSort())
588 True
589 """
590 return False
591

Referenced by SortRef.subsort().