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

Expressions. More...

+ Inheritance diagram for ExprRef:

Public Member Functions

def as_ast
 
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 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 692 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 728 of file z3py.py.

Referenced by Probe.__ne__().

729  def __eq__(self, other):
730  """Return a Z3 expression that represents the constraint `self == other`.
731 
732  If `other` is `None`, then this method simply returns `False`.
733 
734  >>> a = Int('a')
735  >>> b = Int('b')
736  >>> a == b
737  a == b
738  >>> a == None
739  False
740  """
741  if other == None:
742  return False
743  a, b = _coerce_exprs(self, other)
744  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
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 745 of file z3py.py.

746  def __ne__(self, other):
747  """Return a Z3 expression that represents the constraint `self != other`.
748 
749  If `other` is `None`, then this method simply returns `True`.
750 
751  >>> a = Int('a')
752  >>> b = Int('b')
753  >>> a != b
754  a != b
755  >>> a != None
756  True
757  """
758  if other == None:
759  return True
760  a, b = _coerce_exprs(self, other)
761  _args, sz = _to_ast_array((a, b))
762  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
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 794 of file z3py.py.

Referenced by ExprRef.children().

795  def arg(self, idx):
796  """Return argument `idx` of the application `self`.
797 
798  This method assumes that `self` is a function application with at least `idx+1` arguments.
799 
800  >>> a = Int('a')
801  >>> b = Int('b')
802  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
803  >>> t = f(a, b, 0)
804  >>> t.arg(0)
805  a
806  >>> t.arg(1)
807  b
808  >>> t.arg(2)
809  0
810  """
811  if __debug__:
812  _z3_assert(is_app(self), "Z3 application expected")
813  _z3_assert(idx < self.num_args(), "Invalid argument index")
814  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
def as_ast (   self)

Definition at line 702 of file z3py.py.

703  def as_ast(self):
704  return self.ast
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 815 of file z3py.py.

816  def children(self):
817  """Return a list containing the children of the given expression
818 
819  >>> a = Int('a')
820  >>> b = Int('b')
821  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
822  >>> t = f(a, b, 0)
823  >>> t.children()
824  [a, b, 0]
825  """
826  if is_app(self):
827  return [self.arg(i) for i in range(self.num_args())]
828  else:
829  return []
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 763 of file z3py.py.

764  def decl(self):
765  """Return the Z3 function declaration associated with a Z3 application.
766 
767  >>> f = Function('f', IntSort(), IntSort())
768  >>> a = Int('a')
769  >>> t = f(a)
770  >>> eq(t.decl(), f)
771  True
772  >>> (a + 1).decl()
773  +
774  """
775  if __debug__:
776  _z3_assert(is_app(self), "Z3 application expected")
777  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
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 778 of file z3py.py.

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

779  def num_args(self):
780  """Return the number of arguments of a Z3 application.
781 
782  >>> a = Int('a')
783  >>> b = Int('b')
784  >>> (a + b).num_args()
785  2
786  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
787  >>> t = f(a, b, 0)
788  >>> t.num_args()
789  3
790  """
791  if __debug__:
792  _z3_assert(is_app(self), "Z3 application expected")
793  return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
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 705 of file z3py.py.

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

706  def sort(self):
707  """Return the sort of expression `self`.
708 
709  >>> x = Int('x')
710  >>> (x + 1).sort()
711  Int
712  >>> y = Real('y')
713  >>> (x + y).sort()
714  Real
715  """
716  return _sort(self.ctx, self.as_ast())
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 717 of file z3py.py.

718  def sort_kind(self):
719  """Shorthand for `self.sort().kind()`.
720 
721  >>> a = Array('a', IntSort(), IntSort())
722  >>> a.sort_kind() == Z3_ARRAY_SORT
723  True
724  >>> a.sort_kind() == Z3_INT_SORT
725  False
726  """
727  return self.sort().kind()