Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions
ExprRef Class Reference

Expressions. More...

+ Inheritance diagram for ExprRef:

Public Member Functions

def as_ast
 
def get_id
 
def sort
 
def sort_kind
 
def __eq__
 
def __hash__
 
def __ne__
 
def params
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
def hash
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

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

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 CheckSatResult.__ne__(), and Probe.__ne__().

903  def __eq__(self, other):
904  """Return a Z3 expression that represents the constraint `self == other`.
905 
906  If `other` is `None`, then this method simply returns `False`.
907 
908  >>> a = Int('a')
909  >>> b = Int('b')
910  >>> a == b
911  a == b
912  >>> a is None
913  False
914  """
915  if other is None:
916  return False
917  a, b = _coerce_exprs(self, other)
918  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __eq__
Definition: z3py.py:902
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
def ctx_ref
Definition: z3py.py:352
def __hash__ (   self)
Hash code. 

Definition at line 919 of file z3py.py.

920  def __hash__(self):
921  """ Hash code. """
922  return AstRef.__hash__(self)
def __hash__
Definition: z3py.py:919
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.

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

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

Definition at line 873 of file z3py.py.

874  def as_ast(self):
875  return self.ast
def as_ast
Definition: z3py.py:873
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.

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

945  def decl(self):
946  """Return the Z3 function declaration associated with a Z3 application.
947 
948  >>> f = Function('f', IntSort(), IntSort())
949  >>> a = Int('a')
950  >>> t = f(a)
951  >>> eq(t.decl(), f)
952  True
953  >>> (a + 1).decl()
954  +
955  """
956  if z3_debug():
957  _z3_assert(is_app(self), "Z3 application expected")
958  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
Function Declarations.
Definition: z3py.py:651
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 as_ast
Definition: z3py.py:344
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
def decl
Definition: z3py.py:944
def is_app
Definition: z3py.py:1127
def get_id (   self)

Definition at line 876 of file z3py.py.

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

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

Definition at line 941 of file z3py.py.

942  def params(self):
943  return self.decl().params()
def params
Definition: z3py.py:941
def decl
Definition: z3py.py:944
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(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), BitVecRef.size(), and ExprRef.sort_kind().

880  def sort(self):
881  """Return the sort of expression `self`.
882 
883  >>> x = Int('x')
884  >>> (x + 1).sort()
885  Int
886  >>> y = Real('y')
887  >>> (x + y).sort()
888  Real
889  """
890  return _sort(self.ctx, self.as_ast())
def sort
Definition: z3py.py:879
def as_ast
Definition: z3py.py:344
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.

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