Z3
Public Member Functions
ExprRef Class Reference

Expressions. More...

+ Inheritance diagram for ExprRef:

Public Member Functions

def as_ast (self)
 
def get_id (self)
 
def sort (self)
 
def sort_kind (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __ne__ (self, other)
 
def params (self)
 
def decl (self)
 
def num_args (self)
 
def arg (self, idx)
 
def children (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

Expressions.

Constraints, formulas and terms are expressions in Z3.

Expressions are ASTs. Every expression has a sort.
There are three main kinds of expressions:
function applications, quantifiers and bounded variables.
A constant is a function application with 0 arguments.
For quantifier free problems, all expressions are
function applications.

Definition at line 805 of file z3py.py.

Member Function Documentation

◆ __eq__()

def __eq__ (   self,
  other 
)
Return a Z3 expression that represents the constraint `self == other`.

If `other` is `None`, then this method simply returns `False`.

>>> a = Int('a')
>>> b = Int('b')
>>> a == b
a == b
>>> a is None
False

Definition at line 844 of file z3py.py.

Referenced by Probe.__ne__().

844  def __eq__(self, other):
845  """Return a Z3 expression that represents the constraint `self == other`.
846 
847  If `other` is `None`, then this method simply returns `False`.
848 
849  >>> a = Int('a')
850  >>> b = Int('b')
851  >>> a == b
852  a == b
853  >>> a is None
854  False
855  """
856  if other is None:
857  return False
858  a, b = _coerce_exprs(self, other)
859  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
860 
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.

◆ __hash__()

def __hash__ (   self)
Hash code. 

Definition at line 861 of file z3py.py.

861  def __hash__(self):
862  """ Hash code. """
863  return AstRef.__hash__(self)
864 

◆ __ne__()

def __ne__ (   self,
  other 
)
Return a Z3 expression that represents the constraint `self != other`.

If `other` is `None`, then this method simply returns `True`.

>>> a = Int('a')
>>> b = Int('b')
>>> a != b
a != b
>>> a is not None
True

Definition at line 865 of file z3py.py.

865  def __ne__(self, other):
866  """Return a Z3 expression that represents the constraint `self != other`.
867 
868  If `other` is `None`, then this method simply returns `True`.
869 
870  >>> a = Int('a')
871  >>> b = Int('b')
872  >>> a != b
873  a != b
874  >>> a is not None
875  True
876  """
877  if other is None:
878  return True
879  a, b = _coerce_exprs(self, other)
880  _args, sz = _to_ast_array((a, b))
881  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
882 
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).

◆ arg()

def arg (   self,
  idx 
)
Return argument `idx` of the application `self`.

This method assumes that `self` is a function application with at least `idx+1` arguments.

>>> a = Int('a')
>>> b = Int('b')
>>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
>>> t = f(a, b, 0)
>>> t.arg(0)
a
>>> t.arg(1)
b
>>> t.arg(2)
0

Definition at line 917 of file z3py.py.

Referenced by AstRef.__bool__(), and ExprRef.children().

917  def arg(self, idx):
918  """Return argument `idx` of the application `self`.
919 
920  This method assumes that `self` is a function application with at least `idx+1` arguments.
921 
922  >>> a = Int('a')
923  >>> b = Int('b')
924  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
925  >>> t = f(a, b, 0)
926  >>> t.arg(0)
927  a
928  >>> t.arg(1)
929  b
930  >>> t.arg(2)
931  0
932  """
933  if __debug__:
934  _z3_assert(is_app(self), "Z3 application expected")
935  _z3_assert(idx < self.num_args(), "Invalid argument index")
936  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
937 
def is_app(a)
Definition: z3py.py:1069
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.

◆ as_ast()

def as_ast (   self)

Definition at line 815 of file z3py.py.

815  def as_ast(self):
816  return self.ast
817 

◆ children()

def children (   self)
Return a list containing the children of the given expression

>>> a = Int('a')
>>> b = Int('b')
>>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
>>> t = f(a, b, 0)
>>> t.children()
[a, b, 0]

Definition at line 938 of file z3py.py.

938  def children(self):
939  """Return a list containing the children of the given expression
940 
941  >>> a = Int('a')
942  >>> b = Int('b')
943  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
944  >>> t = f(a, b, 0)
945  >>> t.children()
946  [a, b, 0]
947  """
948  if is_app(self):
949  return [self.arg(i) for i in range(self.num_args())]
950  else:
951  return []
952 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
def is_app(a)
Definition: z3py.py:1069

◆ decl()

def decl (   self)
Return the Z3 function declaration associated with a Z3 application.

>>> f = Function('f', IntSort(), IntSort())
>>> a = Int('a')
>>> t = f(a)
>>> eq(t.decl(), f)
True
>>> (a + 1).decl()
+

Definition at line 886 of file z3py.py.

Referenced by ExprRef.params().

886  def decl(self):
887  """Return the Z3 function declaration associated with a Z3 application.
888 
889  >>> f = Function('f', IntSort(), IntSort())
890  >>> a = Int('a')
891  >>> t = f(a)
892  >>> eq(t.decl(), f)
893  True
894  >>> (a + 1).decl()
895  +
896  """
897  if __debug__:
898  _z3_assert(is_app(self), "Z3 application expected")
899  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
900 
def is_app(a)
Definition: z3py.py:1069
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.

◆ get_id()

def get_id (   self)

Definition at line 818 of file z3py.py.

818  def get_id(self):
819  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
820 
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.

◆ num_args()

def num_args (   self)
Return the number of arguments of a Z3 application.

>>> a = Int('a')
>>> b = Int('b')
>>> (a + b).num_args()
2
>>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
>>> t = f(a, b, 0)
>>> t.num_args()
3

Definition at line 901 of file z3py.py.

Referenced by AstRef.__bool__(), ExprRef.arg(), and ExprRef.children().

901  def num_args(self):
902  """Return the number of arguments of a Z3 application.
903 
904  >>> a = Int('a')
905  >>> b = Int('b')
906  >>> (a + b).num_args()
907  2
908  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
909  >>> t = f(a, b, 0)
910  >>> t.num_args()
911  3
912  """
913  if __debug__:
914  _z3_assert(is_app(self), "Z3 application expected")
915  return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
916 
def is_app(a)
Definition: z3py.py:1069
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...

◆ params()

def params (   self)

Definition at line 883 of file z3py.py.

883  def params(self):
884  return self.decl().params()
885 

◆ sort()

def sort (   self)
Return the sort of expression `self`.

>>> x = Int('x')
>>> (x + 1).sort()
Int
>>> y = Real('y')
>>> (x + y).sort()
Real

Definition at line 821 of file z3py.py.

Referenced by ArrayRef.domain(), ArrayRef.range(), and ExprRef.sort_kind().

821  def sort(self):
822  """Return the sort of expression `self`.
823 
824  >>> x = Int('x')
825  >>> (x + 1).sort()
826  Int
827  >>> y = Real('y')
828  >>> (x + y).sort()
829  Real
830  """
831  return _sort(self.ctx, self.as_ast())
832 

◆ sort_kind()

def sort_kind (   self)
Shorthand for `self.sort().kind()`.

>>> a = Array('a', IntSort(), IntSort())
>>> a.sort_kind() == Z3_ARRAY_SORT
True
>>> a.sort_kind() == Z3_INT_SORT
False

Definition at line 833 of file z3py.py.

833  def sort_kind(self):
834  """Shorthand for `self.sort().kind()`.
835 
836  >>> a = Array('a', IntSort(), IntSort())
837  >>> a.sort_kind() == Z3_ARRAY_SORT
838  True
839  >>> a.sort_kind() == Z3_INT_SORT
840  False
841  """
842  return self.sort().kind()
843