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 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 791 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 830 of file z3py.py.

Referenced by Probe.__ne__().

830  def __eq__(self, other):
831  """Return a Z3 expression that represents the constraint `self == other`.
832 
833  If `other` is `None`, then this method simply returns `False`.
834 
835  >>> a = Int('a')
836  >>> b = Int('b')
837  >>> a == b
838  a == b
839  >>> a is None
840  False
841  """
842  if other is None:
843  return False
844  a, b = _coerce_exprs(self, other)
845  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
846 
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 847 of file z3py.py.

847  def __hash__(self):
848  """ Hash code. """
849  return AstRef.__hash__(self)
850 

§ __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 851 of file z3py.py.

851  def __ne__(self, other):
852  """Return a Z3 expression that represents the constraint `self != other`.
853 
854  If `other` is `None`, then this method simply returns `True`.
855 
856  >>> a = Int('a')
857  >>> b = Int('b')
858  >>> a != b
859  a != b
860  >>> a is not None
861  True
862  """
863  if other is None:
864  return True
865  a, b = _coerce_exprs(self, other)
866  _args, sz = _to_ast_array((a, b))
867  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
868 
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 903 of file z3py.py.

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

903  def arg(self, idx):
904  """Return argument `idx` of the application `self`.
905 
906  This method assumes that `self` is a function application with at least `idx+1` arguments.
907 
908  >>> a = Int('a')
909  >>> b = Int('b')
910  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
911  >>> t = f(a, b, 0)
912  >>> t.arg(0)
913  a
914  >>> t.arg(1)
915  b
916  >>> t.arg(2)
917  0
918  """
919  if __debug__:
920  _z3_assert(is_app(self), "Z3 application expected")
921  _z3_assert(idx < self.num_args(), "Invalid argument index")
922  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
923 
def is_app(a)
Definition: z3py.py:1055
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 801 of file z3py.py.

801  def as_ast(self):
802  return self.ast
803 

§ 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 924 of file z3py.py.

924  def children(self):
925  """Return a list containing the children of the given expression
926 
927  >>> a = Int('a')
928  >>> b = Int('b')
929  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
930  >>> t = f(a, b, 0)
931  >>> t.children()
932  [a, b, 0]
933  """
934  if is_app(self):
935  return [self.arg(i) for i in range(self.num_args())]
936  else:
937  return []
938 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
def is_app(a)
Definition: z3py.py:1055

§ 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 872 of file z3py.py.

Referenced by ExprRef.params().

872  def decl(self):
873  """Return the Z3 function declaration associated with a Z3 application.
874 
875  >>> f = Function('f', IntSort(), IntSort())
876  >>> a = Int('a')
877  >>> t = f(a)
878  >>> eq(t.decl(), f)
879  True
880  >>> (a + 1).decl()
881  +
882  """
883  if __debug__:
884  _z3_assert(is_app(self), "Z3 application expected")
885  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
886 
def is_app(a)
Definition: z3py.py:1055
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 804 of file z3py.py.

804  def get_id(self):
805  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
806 
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 887 of file z3py.py.

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

887  def num_args(self):
888  """Return the number of arguments of a Z3 application.
889 
890  >>> a = Int('a')
891  >>> b = Int('b')
892  >>> (a + b).num_args()
893  2
894  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
895  >>> t = f(a, b, 0)
896  >>> t.num_args()
897  3
898  """
899  if __debug__:
900  _z3_assert(is_app(self), "Z3 application expected")
901  return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
902 
def is_app(a)
Definition: z3py.py:1055
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 869 of file z3py.py.

869  def params(self):
870  return self.decl().params()
871 

§ 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 807 of file z3py.py.

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

807  def sort(self):
808  """Return the sort of expression `self`.
809 
810  >>> x = Int('x')
811  >>> (x + 1).sort()
812  Int
813  >>> y = Real('y')
814  >>> (x + y).sort()
815  Real
816  """
817  return _sort(self.ctx, self.as_ast())
818 

§ 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 819 of file z3py.py.

819  def sort_kind(self):
820  """Shorthand for `self.sort().kind()`.
821 
822  >>> a = Array('a', IntSort(), IntSort())
823  >>> a.sort_kind() == Z3_ARRAY_SORT
824  True
825  >>> a.sort_kind() == Z3_INT_SORT
826  False
827  """
828  return self.sort().kind()
829