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)
 
def from_string (self, s)
 
def serialize (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

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

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

1019  def __eq__(self, other):
1020  """Return a Z3 expression that represents the constraint `self == other`.
1021 
1022  If `other` is `None`, then this method simply returns `False`.
1023 
1024  >>> a = Int('a')
1025  >>> b = Int('b')
1026  >>> a == b
1027  a == b
1028  >>> a is None
1029  False
1030  """
1031  if other is None:
1032  return False
1033  a, b = _coerce_exprs(self, other)
1034  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
1035 
def __eq__(self, other)
Definition: z3py.py:1019
def ctx_ref(self)
Definition: z3py.py:400
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
def __hash__ (   self)
Hash code. 

Definition at line 1036 of file z3py.py.

1036  def __hash__(self):
1037  """ Hash code. """
1038  return AstRef.__hash__(self)
1039 
def __hash__(self)
Definition: z3py.py:1036
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 1040 of file z3py.py.

1040  def __ne__(self, other):
1041  """Return a Z3 expression that represents the constraint `self != other`.
1042 
1043  If `other` is `None`, then this method simply returns `True`.
1044 
1045  >>> a = Int('a')
1046  >>> b = Int('b')
1047  >>> a != b
1048  a != b
1049  >>> a is not None
1050  True
1051  """
1052  if other is None:
1053  return True
1054  a, b = _coerce_exprs(self, other)
1055  _args, sz = _to_ast_array((a, b))
1056  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
1057 
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 __ne__(self, other)
Definition: z3py.py:1040
def ctx_ref(self)
Definition: z3py.py:400
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 1092 of file z3py.py.

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

1092  def arg(self, idx):
1093  """Return argument `idx` of the application `self`.
1094 
1095  This method assumes that `self` is a function application with at least `idx+1` arguments.
1096 
1097  >>> a = Int('a')
1098  >>> b = Int('b')
1099  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1100  >>> t = f(a, b, 0)
1101  >>> t.arg(0)
1102  a
1103  >>> t.arg(1)
1104  b
1105  >>> t.arg(2)
1106  0
1107  """
1108  if z3_debug():
1109  _z3_assert(is_app(self), "Z3 application expected")
1110  _z3_assert(idx < self.num_args(), "Invalid argument index")
1111  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
1112 
def as_ast(self)
Definition: z3py.py:392
def is_app(a)
Definition: z3py.py:1283
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(self)
Definition: z3py.py:1076
def z3_debug()
Definition: z3py.py:62
def arg(self, idx)
Definition: z3py.py:1092
def ctx_ref(self)
Definition: z3py.py:400
def as_ast (   self)

Definition at line 990 of file z3py.py.

990  def as_ast(self):
991  return self.ast
992 
def as_ast(self)
Definition: z3py.py:990
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 1113 of file z3py.py.

1113  def children(self):
1114  """Return a list containing the children of the given expression
1115 
1116  >>> a = Int('a')
1117  >>> b = Int('b')
1118  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1119  >>> t = f(a, b, 0)
1120  >>> t.children()
1121  [a, b, 0]
1122  """
1123  if is_app(self):
1124  return [self.arg(i) for i in range(self.num_args())]
1125  else:
1126  return []
1127 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def is_app(a)
Definition: z3py.py:1283
def num_args(self)
Definition: z3py.py:1076
def arg(self, idx)
Definition: z3py.py:1092
def children(self)
Definition: z3py.py:1113
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 1061 of file z3py.py.

Referenced by ExprRef.params().

1061  def decl(self):
1062  """Return the Z3 function declaration associated with a Z3 application.
1063 
1064  >>> f = Function('f', IntSort(), IntSort())
1065  >>> a = Int('a')
1066  >>> t = f(a)
1067  >>> eq(t.decl(), f)
1068  True
1069  >>> (a + 1).decl()
1070  +
1071  """
1072  if z3_debug():
1073  _z3_assert(is_app(self), "Z3 application expected")
1074  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
1075 
Function Declarations.
Definition: z3py.py:740
def as_ast(self)
Definition: z3py.py:392
def is_app(a)
Definition: z3py.py:1283
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 decl(self)
Definition: z3py.py:1061
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
def from_string (   self,
  s 
)

Definition at line 1128 of file z3py.py.

1128  def from_string(self, s):
1129  pass
1130 
def from_string(self, s)
Definition: z3py.py:1128
def get_id (   self)

Definition at line 993 of file z3py.py.

993  def get_id(self):
994  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
995 
def as_ast(self)
Definition: z3py.py:392
def get_id(self)
Definition: z3py.py:993
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 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 1076 of file z3py.py.

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

1076  def num_args(self):
1077  """Return the number of arguments of a Z3 application.
1078 
1079  >>> a = Int('a')
1080  >>> b = Int('b')
1081  >>> (a + b).num_args()
1082  2
1083  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1084  >>> t = f(a, b, 0)
1085  >>> t.num_args()
1086  3
1087  """
1088  if z3_debug():
1089  _z3_assert(is_app(self), "Z3 application expected")
1090  return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
1091 
def as_ast(self)
Definition: z3py.py:392
def is_app(a)
Definition: z3py.py:1283
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 num_args(self)
Definition: z3py.py:1076
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
def params (   self)

Definition at line 1058 of file z3py.py.

1058  def params(self):
1059  return self.decl().params()
1060 
def decl(self)
Definition: z3py.py:1061
def params(self)
Definition: z3py.py:1058
def serialize (   self)

Definition at line 1131 of file z3py.py.

1131  def serialize(self):
1132  s = Solver()
1133  f = Function('F', self.sort(), BoolSort(self.ctx))
1134  s.add(f(self))
1135  return s.sexpr()
1136 
def BoolSort
Definition: z3py.py:1731
def Function(name, sig)
Definition: z3py.py:881
def serialize(self)
Definition: z3py.py:1131
def sort(self)
Definition: z3py.py:996
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 996 of file z3py.py.

Referenced by ArrayRef.domain(), ArrayRef.domain_n(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), ExprRef.serialize(), BitVecRef.size(), and ExprRef.sort_kind().

996  def sort(self):
997  """Return the sort of expression `self`.
998 
999  >>> x = Int('x')
1000  >>> (x + 1).sort()
1001  Int
1002  >>> y = Real('y')
1003  >>> (x + y).sort()
1004  Real
1005  """
1006  return _sort(self.ctx, self.as_ast())
1007 
def as_ast(self)
Definition: z3py.py:392
def sort(self)
Definition: z3py.py:996
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 1008 of file z3py.py.

1008  def sort_kind(self):
1009  """Shorthand for `self.sort().kind()`.
1010 
1011  >>> a = Array('a', IntSort(), IntSort())
1012  >>> a.sort_kind() == Z3_ARRAY_SORT
1013  True
1014  >>> a.sort_kind() == Z3_INT_SORT
1015  False
1016  """
1017  return self.sort().kind()
1018 
def sort_kind(self)
Definition: z3py.py:1008
def sort(self)
Definition: z3py.py:996