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__
 
def __del__ (self)
 
def __deepcopy__
 
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 559 of file z3py.py.

Member Function Documentation

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

Referenced by CheckSatResult.__ne__(), and Probe.__ne__().

618  def __eq__(self, other):
619  """Return `True` if `self` and `other` are the same Z3 sort.
620 
621  >>> p = Bool('p')
622  >>> p.sort() == BoolSort()
623  True
624  >>> p.sort() == IntSort()
625  False
626  """
627  if other is None:
628  return False
629  return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
630 
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
def ctx_ref(self)
Definition: z3py.py:400
def __eq__(self, other)
Definition: z3py.py:618
def __hash__ (   self)
Hash code. 

Definition at line 642 of file z3py.py.

642  def __hash__(self):
643  """ Hash code. """
644  return AstRef.__hash__(self)
645 
646 
def __hash__(self)
Definition: z3py.py:642
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.
633 
634  >>> p = Bool('p')
635  >>> p.sort() != BoolSort()
636  False
637  >>> p.sort() != IntSort()
638  True
639  """
640  return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
641 
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
def __ne__(self, other)
Definition: z3py.py:631
def ctx_ref(self)
Definition: z3py.py:400
def as_ast (   self)

Definition at line 562 of file z3py.py.

562  def as_ast(self):
563  return Z3_sort_to_ast(self.ctx_ref(), self.ast)
564 
def as_ast(self)
Definition: z3py.py:562
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.
def ctx_ref(self)
Definition: z3py.py:400
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)

Definition at line 593 of file z3py.py.

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

Definition at line 565 of file z3py.py.

565  def get_id(self):
566  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
567 
def as_ast(self)
Definition: z3py.py:392
def get_id(self)
Definition: z3py.py:565
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. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.
def ctx_ref(self)
Definition: z3py.py:400
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 568 of file z3py.py.

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

568  def kind(self):
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.
571 
572  >>> b = BoolSort()
573  >>> b.kind() == Z3_BOOL_SORT
574  True
575  >>> b.kind() == Z3_INT_SORT
576  False
577  >>> A = ArraySort(IntSort(), IntSort())
578  >>> A.kind() == Z3_ARRAY_SORT
579  True
580  >>> A.kind() == Z3_INT_SORT
581  False
582  """
583  return _sort_kind(self.ctx, self.ast)
584 
def kind(self)
Definition: z3py.py:568
def name (   self)
Return the name (string) of sort `self`.

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

Definition at line 608 of file z3py.py.

608  def name(self):
609  """Return the name (string) of sort `self`.
610 
611  >>> BoolSort().name()
612  'Bool'
613  >>> ArraySort(IntSort(), IntSort()).name()
614  'Array'
615  """
616  return _symbol2py(self.ctx, Z3_get_sort_name(self.ctx_ref(), self.ast))
617 
def ctx_ref(self)
Definition: z3py.py:400
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
def name(self)
Definition: z3py.py:608
def subsort (   self,
  other 
)
Return `True` if `self` is a subsort of `other`.

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

Definition at line 585 of file z3py.py.

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