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

622 def __eq__(self, other):
623 """Return `True` if `self` and `other` are the same Z3 sort.
624
625 >>> p = Bool('p')
626 >>> p.sort() == BoolSort()
627 True
628 >>> p.sort() == IntSort()
629 False
630 """
631 if other is None:
632 return False
633 return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
634
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 646 of file z3py.py.

646 def __hash__(self):
647 """ Hash code. """
648 return AstRef.__hash__(self)
649
650

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

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

◆ as_ast()

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

Reimplemented from AstRef.

Definition at line 566 of file z3py.py.

566 def as_ast(self):
567 return Z3_sort_to_ast(self.ctx_ref(), self.ast)
568
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 597 of file z3py.py.

597 def cast(self, val):
598 """Try to cast `val` as an element of sort `self`.
599
600 This method is used in Z3Py to convert Python objects such as integers,
601 floats, longs and strings into Z3 expressions.
602
603 >>> x = Int('x')
604 >>> RealSort().cast(x)
605 ToReal(x)
606 """
607 if z3_debug():
608 _z3_assert(is_expr(val), "Z3 expression expected")
609 _z3_assert(self.eq(val.sort()), "Sort mismatch")
610 return val
611

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

569 def get_id(self):
570 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
571
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 572 of file z3py.py.

572 def kind(self):
573 """Return the Z3 internal kind of a sort.
574 This method can be used to test if `self` is one of the Z3 builtin sorts.
575
576 >>> b = BoolSort()
577 >>> b.kind() == Z3_BOOL_SORT
578 True
579 >>> b.kind() == Z3_INT_SORT
580 False
581 >>> A = ArraySort(IntSort(), IntSort())
582 >>> A.kind() == Z3_ARRAY_SORT
583 True
584 >>> A.kind() == Z3_INT_SORT
585 False
586 """
587 return _sort_kind(self.ctx, self.ast)
588

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

612 def name(self):
613 """Return the name (string) of sort `self`.
614
615 >>> BoolSort().name()
616 'Bool'
617 >>> ArraySort(IntSort(), IntSort()).name()
618 'Array'
619 """
620 return _symbol2py(self.ctx, Z3_get_sort_name(self.ctx_ref(), self.ast))
621
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 589 of file z3py.py.

589 def subsort(self, other):
590 """Return `True` if `self` is a subsort of `other`.
591
592 >>> IntSort().subsort(RealSort())
593 True
594 """
595 return False
596