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 957 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 997 of file z3py.py.

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

997  def __eq__(self, other):
998  """Return a Z3 expression that represents the constraint `self == other`.
999 
1000  If `other` is `None`, then this method simply returns `False`.
1001 
1002  >>> a = Int('a')
1003  >>> b = Int('b')
1004  >>> a == b
1005  a == b
1006  >>> a is None
1007  False
1008  """
1009  if other is None:
1010  return False
1011  a, b = _coerce_exprs(self, other)
1012  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
1013 
def __eq__(self, other)
Definition: z3py.py:997
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 1014 of file z3py.py.

1014  def __hash__(self):
1015  """ Hash code. """
1016  return AstRef.__hash__(self)
1017 
def __hash__(self)
Definition: z3py.py:1014
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 1018 of file z3py.py.

1018  def __ne__(self, other):
1019  """Return a Z3 expression that represents the constraint `self != other`.
1020 
1021  If `other` is `None`, then this method simply returns `True`.
1022 
1023  >>> a = Int('a')
1024  >>> b = Int('b')
1025  >>> a != b
1026  a != b
1027  >>> a is not None
1028  True
1029  """
1030  if other is None:
1031  return True
1032  a, b = _coerce_exprs(self, other)
1033  _args, sz = _to_ast_array((a, b))
1034  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
1035 
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:1018
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 1070 of file z3py.py.

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

1070  def arg(self, idx):
1071  """Return argument `idx` of the application `self`.
1072 
1073  This method assumes that `self` is a function application with at least `idx+1` arguments.
1074 
1075  >>> a = Int('a')
1076  >>> b = Int('b')
1077  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1078  >>> t = f(a, b, 0)
1079  >>> t.arg(0)
1080  a
1081  >>> t.arg(1)
1082  b
1083  >>> t.arg(2)
1084  0
1085  """
1086  if z3_debug():
1087  _z3_assert(is_app(self), "Z3 application expected")
1088  _z3_assert(idx < self.num_args(), "Invalid argument index")
1089  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
1090 
def as_ast(self)
Definition: z3py.py:392
def is_app(a)
Definition: z3py.py:1261
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:1054
def z3_debug()
Definition: z3py.py:62
def arg(self, idx)
Definition: z3py.py:1070
def ctx_ref(self)
Definition: z3py.py:400
def as_ast (   self)

Definition at line 968 of file z3py.py.

968  def as_ast(self):
969  return self.ast
970 
def as_ast(self)
Definition: z3py.py:968
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 1091 of file z3py.py.

1091  def children(self):
1092  """Return a list containing the children of the given expression
1093 
1094  >>> a = Int('a')
1095  >>> b = Int('b')
1096  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1097  >>> t = f(a, b, 0)
1098  >>> t.children()
1099  [a, b, 0]
1100  """
1101  if is_app(self):
1102  return [self.arg(i) for i in range(self.num_args())]
1103  else:
1104  return []
1105 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def is_app(a)
Definition: z3py.py:1261
def num_args(self)
Definition: z3py.py:1054
def arg(self, idx)
Definition: z3py.py:1070
def children(self)
Definition: z3py.py:1091
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 1039 of file z3py.py.

Referenced by ExprRef.params().

1039  def decl(self):
1040  """Return the Z3 function declaration associated with a Z3 application.
1041 
1042  >>> f = Function('f', IntSort(), IntSort())
1043  >>> a = Int('a')
1044  >>> t = f(a)
1045  >>> eq(t.decl(), f)
1046  True
1047  >>> (a + 1).decl()
1048  +
1049  """
1050  if z3_debug():
1051  _z3_assert(is_app(self), "Z3 application expected")
1052  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
1053 
Function Declarations.
Definition: z3py.py:718
def as_ast(self)
Definition: z3py.py:392
def is_app(a)
Definition: z3py.py:1261
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:1039
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
def from_string (   self,
  s 
)

Definition at line 1106 of file z3py.py.

1106  def from_string(self, s):
1107  pass
1108 
def from_string(self, s)
Definition: z3py.py:1106
def get_id (   self)

Definition at line 971 of file z3py.py.

971  def get_id(self):
972  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
973 
def as_ast(self)
Definition: z3py.py:392
def get_id(self)
Definition: z3py.py:971
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 1054 of file z3py.py.

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

1054  def num_args(self):
1055  """Return the number of arguments of a Z3 application.
1056 
1057  >>> a = Int('a')
1058  >>> b = Int('b')
1059  >>> (a + b).num_args()
1060  2
1061  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1062  >>> t = f(a, b, 0)
1063  >>> t.num_args()
1064  3
1065  """
1066  if z3_debug():
1067  _z3_assert(is_app(self), "Z3 application expected")
1068  return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
1069 
def as_ast(self)
Definition: z3py.py:392
def is_app(a)
Definition: z3py.py:1261
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:1054
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
def params (   self)

Definition at line 1036 of file z3py.py.

1036  def params(self):
1037  return self.decl().params()
1038 
def decl(self)
Definition: z3py.py:1039
def params(self)
Definition: z3py.py:1036
def serialize (   self)

Definition at line 1109 of file z3py.py.

1109  def serialize(self):
1110  s = Solver()
1111  f = Function('F', self.sort(), BoolSort(self.ctx))
1112  s.add(f(self))
1113  return s.sexpr()
1114 
def BoolSort
Definition: z3py.py:1687
def Function(name, sig)
Definition: z3py.py:859
def serialize(self)
Definition: z3py.py:1109
def sort(self)
Definition: z3py.py:974
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 974 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().

974  def sort(self):
975  """Return the sort of expression `self`.
976 
977  >>> x = Int('x')
978  >>> (x + 1).sort()
979  Int
980  >>> y = Real('y')
981  >>> (x + y).sort()
982  Real
983  """
984  return _sort(self.ctx, self.as_ast())
985 
def as_ast(self)
Definition: z3py.py:392
def sort(self)
Definition: z3py.py:974
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 986 of file z3py.py.

986  def sort_kind(self):
987  """Shorthand for `self.sort().kind()`.
988 
989  >>> a = Array('a', IntSort(), IntSort())
990  >>> a.sort_kind() == Z3_ARRAY_SORT
991  True
992  >>> a.sort_kind() == Z3_INT_SORT
993  False
994  """
995  return self.sort().kind()
996 
def sort_kind(self)
Definition: z3py.py:986
def sort(self)
Definition: z3py.py:974