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 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 __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 769 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 808 of file z3py.py.

Referenced by Probe.__ne__().

808  def __eq__(self, other):
809  """Return a Z3 expression that represents the constraint `self == other`.
810 
811  If `other` is `None`, then this method simply returns `False`.
812 
813  >>> a = Int('a')
814  >>> b = Int('b')
815  >>> a == b
816  a == b
817  >>> a is None
818  False
819  """
820  if other is None:
821  return False
822  a, b = _coerce_exprs(self, other)
823  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
824 
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 825 of file z3py.py.

825  def __hash__(self):
826  """ Hash code. """
827  return AstRef.__hash__(self)
828 

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

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

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

878  def arg(self, idx):
879  """Return argument `idx` of the application `self`.
880 
881  This method assumes that `self` is a function application with at least `idx+1` arguments.
882 
883  >>> a = Int('a')
884  >>> b = Int('b')
885  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
886  >>> t = f(a, b, 0)
887  >>> t.arg(0)
888  a
889  >>> t.arg(1)
890  b
891  >>> t.arg(2)
892  0
893  """
894  if __debug__:
895  _z3_assert(is_app(self), "Z3 application expected")
896  _z3_assert(idx < self.num_args(), "Invalid argument index")
897  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
898 
def is_app(a)
Definition: z3py.py:1029

§ as_ast()

def as_ast (   self)

Definition at line 779 of file z3py.py.

779  def as_ast(self):
780  return self.ast
781 

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

899  def children(self):
900  """Return a list containing the children of the given expression
901 
902  >>> a = Int('a')
903  >>> b = Int('b')
904  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
905  >>> t = f(a, b, 0)
906  >>> t.children()
907  [a, b, 0]
908  """
909  if is_app(self):
910  return [self.arg(i) for i in range(self.num_args())]
911  else:
912  return []
913 
def is_app(a)
Definition: z3py.py:1029

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

847  def decl(self):
848  """Return the Z3 function declaration associated with a Z3 application.
849 
850  >>> f = Function('f', IntSort(), IntSort())
851  >>> a = Int('a')
852  >>> t = f(a)
853  >>> eq(t.decl(), f)
854  True
855  >>> (a + 1).decl()
856  +
857  """
858  if __debug__:
859  _z3_assert(is_app(self), "Z3 application expected")
860  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
861 
def is_app(a)
Definition: z3py.py:1029

§ get_id()

def get_id (   self)

Definition at line 782 of file z3py.py.

782  def get_id(self):
783  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
784 

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

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

862  def num_args(self):
863  """Return the number of arguments of a Z3 application.
864 
865  >>> a = Int('a')
866  >>> b = Int('b')
867  >>> (a + b).num_args()
868  2
869  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
870  >>> t = f(a, b, 0)
871  >>> t.num_args()
872  3
873  """
874  if __debug__:
875  _z3_assert(is_app(self), "Z3 application expected")
876  return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
877 
def is_app(a)
Definition: z3py.py:1029

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

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

785  def sort(self):
786  """Return the sort of expression `self`.
787 
788  >>> x = Int('x')
789  >>> (x + 1).sort()
790  Int
791  >>> y = Real('y')
792  >>> (x + y).sort()
793  Real
794  """
795  return _sort(self.ctx, self.as_ast())
796 

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

797  def sort_kind(self):
798  """Shorthand for `self.sort().kind()`.
799 
800  >>> a = Array('a', IntSort(), IntSort())
801  >>> a.sort_kind() == Z3_ARRAY_SORT
802  True
803  >>> a.sort_kind() == Z3_INT_SORT
804  False
805  """
806  return self.sort().kind()
807