Z3
Loading...
Searching...
No Matches
SortRef Class Reference
Inheritance diagram for SortRef:

Public Member Functions

 as_ast (self)
 get_id (self)
 kind (self)
 subsort (self, other)
 cast (self, val)
 name (self)
 __eq__ (self, other)
 __ne__ (self, other)
 __hash__ (self)
Public Member Functions inherited from AstRef
 __init__ (self, ast, ctx=None)
 __del__ (self)
 __deepcopy__ (self, memo={})
 __str__ (self)
 __repr__ (self)
 __eq__ (self, other)
 __hash__ (self)
 __nonzero__ (self)
 __bool__ (self)
 sexpr (self)
 ctx_ref (self)
 eq (self, other)
 translate (self, target)
 __copy__ (self)
 hash (self)
 py_value (self)
Public Member Functions inherited from Z3PPObject
 use_pp (self)

Additional Inherited Members

Data Fields inherited from AstRef
 ast = ast
 ctx = _get_ctx(ctx)
Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)

Detailed Description

A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.

Definition at line 573 of file z3py.py.

Member Function Documentation

◆ __eq__()

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

632 def __eq__(self, other):
633 """Return `True` if `self` and `other` are the same Z3 sort.
634
635 >>> p = Bool('p')
636 >>> p.sort() == BoolSort()
637 True
638 >>> p.sort() == IntSort()
639 False
640 """
641 if other is None:
642 return False
643 return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
644
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.

Referenced by CheckSatResult.__ne__().

◆ __hash__()

__hash__ ( self)
Hash code. 

Definition at line 656 of file z3py.py.

656 def __hash__(self):
657 """ Hash code. """
658 return AstRef.__hash__(self)
659
660

◆ __ne__()

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

645 def __ne__(self, other):
646 """Return `True` if `self` and `other` are not the same Z3 sort.
647
648 >>> p = Bool('p')
649 >>> p.sort() != BoolSort()
650 False
651 >>> p.sort() != IntSort()
652 True
653 """
654 return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
655

◆ as_ast()

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

Reimplemented from AstRef.

Definition at line 576 of file z3py.py.

576 def as_ast(self):
577 return Z3_sort_to_ast(self.ctx_ref(), self.ast)
578
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.

◆ cast()

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

Definition at line 607 of file z3py.py.

607 def cast(self, val):
608 """Try to cast `val` as an element of sort `self`.
609
610 This method is used in Z3Py to convert Python objects such as integers,
611 floats, longs and strings into Z3 expressions.
612
613 >>> x = Int('x')
614 >>> RealSort().cast(x)
615 ToReal(x)
616 """
617 if z3_debug():
618 _z3_assert(is_expr(val), "Z3 expression expected")
619 _z3_assert(self.eq(val.sort()), "Sort mismatch")
620 return val
621

◆ get_id()

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

Reimplemented from AstRef.

Definition at line 579 of file z3py.py.

579 def get_id(self):
580 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
581
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()

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

582 def kind(self):
583 """Return the Z3 internal kind of a sort.
584 This method can be used to test if `self` is one of the Z3 builtin sorts.
585
586 >>> b = BoolSort()
587 >>> b.kind() == Z3_BOOL_SORT
588 True
589 >>> b.kind() == Z3_INT_SORT
590 False
591 >>> A = ArraySort(IntSort(), IntSort())
592 >>> A.kind() == Z3_ARRAY_SORT
593 True
594 >>> A.kind() == Z3_INT_SORT
595 False
596 """
597 return _sort_kind(self.ctx, self.ast)
598

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

◆ name()

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

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

Definition at line 622 of file z3py.py.

622 def name(self):
623 """Return the name (string) of sort `self`.
624
625 >>> BoolSort().name()
626 'Bool'
627 >>> ArraySort(IntSort(), IntSort()).name()
628 'Array'
629 """
630 return _symbol2py(self.ctx, Z3_get_sort_name(self.ctx_ref(), self.ast))
631
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.

◆ subsort()

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

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

Reimplemented in ArithSortRef, BitVecSortRef, BoolSortRef, and TypeVarRef.

Definition at line 599 of file z3py.py.

599 def subsort(self, other):
600 """Return `True` if `self` is a subsort of `other`.
601
602 >>> IntSort().subsort(RealSort())
603 True
604 """
605 return False
606