Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties 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 __ne__
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __str__
 
def __repr__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
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 732 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 == None
False

Definition at line 771 of file z3py.py.

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

772  def __eq__(self, other):
773  """Return a Z3 expression that represents the constraint `self == other`.
774 
775  If `other` is `None`, then this method simply returns `False`.
776 
777  >>> a = Int('a')
778  >>> b = Int('b')
779  >>> a == b
780  a == b
781  >>> a == None
782  False
783  """
784  if other == None:
785  return False
786  a, b = _coerce_exprs(self, other)
787  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __eq__
Definition: z3py.py:771
Z3_ast Z3_API Z3_mk_eq(__in Z3_context c, __in Z3_ast l, __in Z3_ast r)
Create an AST node representing l = r.
def ctx_ref
Definition: z3py.py:305
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 != None
True

Definition at line 788 of file z3py.py.

789  def __ne__(self, other):
790  """Return a Z3 expression that represents the constraint `self != other`.
791 
792  If `other` is `None`, then this method simply returns `True`.
793 
794  >>> a = Int('a')
795  >>> b = Int('b')
796  >>> a != b
797  a != b
798  >>> a != None
799  True
800  """
801  if other == None:
802  return True
803  a, b = _coerce_exprs(self, other)
804  _args, sz = _to_ast_array((a, b))
805  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
Z3_ast Z3_API Z3_mk_distinct(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).The distinct construct is us...
def ctx_ref
Definition: z3py.py:305
def __ne__
Definition: z3py.py:788
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 837 of file z3py.py.

Referenced by ExprRef.children().

838  def arg(self, idx):
839  """Return argument `idx` of the application `self`.
840 
841  This method assumes that `self` is a function application with at least `idx+1` arguments.
842 
843  >>> a = Int('a')
844  >>> b = Int('b')
845  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
846  >>> t = f(a, b, 0)
847  >>> t.arg(0)
848  a
849  >>> t.arg(1)
850  b
851  >>> t.arg(2)
852  0
853  """
854  if __debug__:
855  _z3_assert(is_app(self), "Z3 application expected")
856  _z3_assert(idx < self.num_args(), "Invalid argument index")
857  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
def num_args
Definition: z3py.py:821
def as_ast
Definition: z3py.py:296
def ctx_ref
Definition: z3py.py:305
def arg
Definition: z3py.py:837
Z3_ast Z3_API Z3_get_app_arg(__in Z3_context c, __in Z3_app a, __in unsigned i)
Return the i-th argument of the given application.
def is_app
Definition: z3py.py:970
def as_ast (   self)

Definition at line 742 of file z3py.py.

743  def as_ast(self):
744  return self.ast
def as_ast
Definition: z3py.py:742
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 858 of file z3py.py.

859  def children(self):
860  """Return a list containing the children of the given expression
861 
862  >>> a = Int('a')
863  >>> b = Int('b')
864  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
865  >>> t = f(a, b, 0)
866  >>> t.children()
867  [a, b, 0]
868  """
869  if is_app(self):
870  return [self.arg(i) for i in range(self.num_args())]
871  else:
872  return []
def num_args
Definition: z3py.py:821
def arg
Definition: z3py.py:837
def children
Definition: z3py.py:858
def is_app
Definition: z3py.py:970
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 806 of file z3py.py.

807  def decl(self):
808  """Return the Z3 function declaration associated with a Z3 application.
809 
810  >>> f = Function('f', IntSort(), IntSort())
811  >>> a = Int('a')
812  >>> t = f(a)
813  >>> eq(t.decl(), f)
814  True
815  >>> (a + 1).decl()
816  +
817  """
818  if __debug__:
819  _z3_assert(is_app(self), "Z3 application expected")
820  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
Function Declarations.
Definition: z3py.py:587
Z3_func_decl Z3_API Z3_get_app_decl(__in Z3_context c, __in Z3_app a)
Return the declaration of a constant or function application.
def as_ast
Definition: z3py.py:296
def ctx_ref
Definition: z3py.py:305
def decl
Definition: z3py.py:806
def is_app
Definition: z3py.py:970
def get_id (   self)

Definition at line 745 of file z3py.py.

746  def get_id(self):
747  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
unsigned Z3_API Z3_get_ast_id(__in Z3_context c, Z3_ast t)
Return a unique identifier for t.
def get_id
Definition: z3py.py:745
def as_ast
Definition: z3py.py:296
def ctx_ref
Definition: z3py.py:305
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 821 of file z3py.py.

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

822  def num_args(self):
823  """Return the number of arguments of a Z3 application.
824 
825  >>> a = Int('a')
826  >>> b = Int('b')
827  >>> (a + b).num_args()
828  2
829  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
830  >>> t = f(a, b, 0)
831  >>> t.num_args()
832  3
833  """
834  if __debug__:
835  _z3_assert(is_app(self), "Z3 application expected")
836  return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
unsigned Z3_API Z3_get_app_num_args(__in Z3_context c, __in 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
Definition: z3py.py:821
def as_ast
Definition: z3py.py:296
def ctx_ref
Definition: z3py.py:305
def is_app
Definition: z3py.py:970
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 748 of file z3py.py.

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

749  def sort(self):
750  """Return the sort of expression `self`.
751 
752  >>> x = Int('x')
753  >>> (x + 1).sort()
754  Int
755  >>> y = Real('y')
756  >>> (x + y).sort()
757  Real
758  """
759  return _sort(self.ctx, self.as_ast())
def sort
Definition: z3py.py:748
def as_ast
Definition: z3py.py:296
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 760 of file z3py.py.

761  def sort_kind(self):
762  """Shorthand for `self.sort().kind()`.
763 
764  >>> a = Array('a', IntSort(), IntSort())
765  >>> a.sort_kind() == Z3_ARRAY_SORT
766  True
767  >>> a.sort_kind() == Z3_INT_SORT
768  False
769  """
770  return self.sort().kind()
def sort
Definition: z3py.py:748
def sort_kind
Definition: z3py.py:760