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

Referenced by Probe.__ne__().

891  def __eq__(self, other):
892  """Return a Z3 expression that represents the constraint `self == other`.
893 
894  If `other` is `None`, then this method simply returns `False`.
895 
896  >>> a = Int('a')
897  >>> b = Int('b')
898  >>> a == b
899  a == b
900  >>> a is None
901  False
902  """
903  if other is None:
904  return False
905  a, b = _coerce_exprs(self, other)
906  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
907 
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 908 of file z3py.py.

908  def __hash__(self):
909  """ Hash code. """
910  return AstRef.__hash__(self)
911 

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

912  def __ne__(self, other):
913  """Return a Z3 expression that represents the constraint `self != other`.
914 
915  If `other` is `None`, then this method simply returns `True`.
916 
917  >>> a = Int('a')
918  >>> b = Int('b')
919  >>> a != b
920  a != b
921  >>> a is not None
922  True
923  """
924  if other is None:
925  return True
926  a, b = _coerce_exprs(self, other)
927  _args, sz = _to_ast_array((a, b))
928  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
929 
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 964 of file z3py.py.

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

964  def arg(self, idx):
965  """Return argument `idx` of the application `self`.
966 
967  This method assumes that `self` is a function application with at least `idx+1` arguments.
968 
969  >>> a = Int('a')
970  >>> b = Int('b')
971  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
972  >>> t = f(a, b, 0)
973  >>> t.arg(0)
974  a
975  >>> t.arg(1)
976  b
977  >>> t.arg(2)
978  0
979  """
980  if __debug__:
981  _z3_assert(is_app(self), "Z3 application expected")
982  _z3_assert(idx < self.num_args(), "Invalid argument index")
983  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
984 
def is_app(a)
Definition: z3py.py:1116
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 862 of file z3py.py.

862  def as_ast(self):
863  return self.ast
864 

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

985  def children(self):
986  """Return a list containing the children of the given expression
987 
988  >>> a = Int('a')
989  >>> b = Int('b')
990  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
991  >>> t = f(a, b, 0)
992  >>> t.children()
993  [a, b, 0]
994  """
995  if is_app(self):
996  return [self.arg(i) for i in range(self.num_args())]
997  else:
998  return []
999 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
def is_app(a)
Definition: z3py.py:1116

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

Referenced by ExprRef.params().

933  def decl(self):
934  """Return the Z3 function declaration associated with a Z3 application.
935 
936  >>> f = Function('f', IntSort(), IntSort())
937  >>> a = Int('a')
938  >>> t = f(a)
939  >>> eq(t.decl(), f)
940  True
941  >>> (a + 1).decl()
942  +
943  """
944  if __debug__:
945  _z3_assert(is_app(self), "Z3 application expected")
946  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
947 
def is_app(a)
Definition: z3py.py:1116
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 865 of file z3py.py.

865  def get_id(self):
866  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
867 
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 948 of file z3py.py.

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

948  def num_args(self):
949  """Return the number of arguments of a Z3 application.
950 
951  >>> a = Int('a')
952  >>> b = Int('b')
953  >>> (a + b).num_args()
954  2
955  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
956  >>> t = f(a, b, 0)
957  >>> t.num_args()
958  3
959  """
960  if __debug__:
961  _z3_assert(is_app(self), "Z3 application expected")
962  return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
963 
def is_app(a)
Definition: z3py.py:1116
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 930 of file z3py.py.

930  def params(self):
931  return self.decl().params()
932 

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

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

868  def sort(self):
869  """Return the sort of expression `self`.
870 
871  >>> x = Int('x')
872  >>> (x + 1).sort()
873  Int
874  >>> y = Real('y')
875  >>> (x + y).sort()
876  Real
877  """
878  return _sort(self.ctx, self.as_ast())
879 

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

880  def sort_kind(self):
881  """Shorthand for `self.sort().kind()`.
882 
883  >>> a = Array('a', IntSort(), IntSort())
884  >>> a.sort_kind() == Z3_ARRAY_SORT
885  True
886  >>> a.sort_kind() == Z3_INT_SORT
887  False
888  """
889  return self.sort().kind()
890