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

Referenced by Probe.__ne__().

902  def __eq__(self, other):
903  """Return a Z3 expression that represents the constraint `self == other`.
904 
905  If `other` is `None`, then this method simply returns `False`.
906 
907  >>> a = Int('a')
908  >>> b = Int('b')
909  >>> a == b
910  a == b
911  >>> a is None
912  False
913  """
914  if other is None:
915  return False
916  a, b = _coerce_exprs(self, other)
917  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
918 
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 919 of file z3py.py.

919  def __hash__(self):
920  """ Hash code. """
921  return AstRef.__hash__(self)
922 

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

923  def __ne__(self, other):
924  """Return a Z3 expression that represents the constraint `self != other`.
925 
926  If `other` is `None`, then this method simply returns `True`.
927 
928  >>> a = Int('a')
929  >>> b = Int('b')
930  >>> a != b
931  a != b
932  >>> a is not None
933  True
934  """
935  if other is None:
936  return True
937  a, b = _coerce_exprs(self, other)
938  _args, sz = _to_ast_array((a, b))
939  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
940 
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 975 of file z3py.py.

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

975  def arg(self, idx):
976  """Return argument `idx` of the application `self`.
977 
978  This method assumes that `self` is a function application with at least `idx+1` arguments.
979 
980  >>> a = Int('a')
981  >>> b = Int('b')
982  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
983  >>> t = f(a, b, 0)
984  >>> t.arg(0)
985  a
986  >>> t.arg(1)
987  b
988  >>> t.arg(2)
989  0
990  """
991  if z3_debug():
992  _z3_assert(is_app(self), "Z3 application expected")
993  _z3_assert(idx < self.num_args(), "Invalid argument index")
994  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
995 
def is_app(a)
Definition: z3py.py:1127
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.
def z3_debug()
Definition: z3py.py:58

◆ as_ast()

def as_ast (   self)

Definition at line 873 of file z3py.py.

873  def as_ast(self):
874  return self.ast
875 

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

996  def children(self):
997  """Return a list containing the children of the given expression
998 
999  >>> a = Int('a')
1000  >>> b = Int('b')
1001  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1002  >>> t = f(a, b, 0)
1003  >>> t.children()
1004  [a, b, 0]
1005  """
1006  if is_app(self):
1007  return [self.arg(i) for i in range(self.num_args())]
1008  else:
1009  return []
1010 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
def is_app(a)
Definition: z3py.py:1127

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

Referenced by ExprRef.params().

944  def decl(self):
945  """Return the Z3 function declaration associated with a Z3 application.
946 
947  >>> f = Function('f', IntSort(), IntSort())
948  >>> a = Int('a')
949  >>> t = f(a)
950  >>> eq(t.decl(), f)
951  True
952  >>> (a + 1).decl()
953  +
954  """
955  if z3_debug():
956  _z3_assert(is_app(self), "Z3 application expected")
957  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
958 
def is_app(a)
Definition: z3py.py:1127
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
def z3_debug()
Definition: z3py.py:58

◆ get_id()

def get_id (   self)

Definition at line 876 of file z3py.py.

876  def get_id(self):
877  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
878 
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 959 of file z3py.py.

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

959  def num_args(self):
960  """Return the number of arguments of a Z3 application.
961 
962  >>> a = Int('a')
963  >>> b = Int('b')
964  >>> (a + b).num_args()
965  2
966  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
967  >>> t = f(a, b, 0)
968  >>> t.num_args()
969  3
970  """
971  if z3_debug():
972  _z3_assert(is_app(self), "Z3 application expected")
973  return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
974 
def is_app(a)
Definition: z3py.py:1127
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...
def z3_debug()
Definition: z3py.py:58

◆ params()

def params (   self)

Definition at line 941 of file z3py.py.

941  def params(self):
942  return self.decl().params()
943 

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

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

879  def sort(self):
880  """Return the sort of expression `self`.
881 
882  >>> x = Int('x')
883  >>> (x + 1).sort()
884  Int
885  >>> y = Real('y')
886  >>> (x + y).sort()
887  Real
888  """
889  return _sort(self.ctx, self.as_ast())
890 

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

891  def sort_kind(self):
892  """Shorthand for `self.sort().kind()`.
893 
894  >>> a = Array('a', IntSort(), IntSort())
895  >>> a.sort_kind() == Z3_ARRAY_SORT
896  True
897  >>> a.sort_kind() == Z3_INT_SORT
898  False
899  """
900  return self.sort().kind()
901