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 __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__
 
def __del__ (self)
 
def __str__ (self)
 
def __repr__ (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 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__().

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

788  def __ne__(self, other):
789  """Return a Z3 expression that represents the constraint `self != other`.
790 
791  If `other` is `None`, then this method simply returns `True`.
792 
793  >>> a = Int('a')
794  >>> b = Int('b')
795  >>> a != b
796  a != b
797  >>> a != None
798  True
799  """
800  if other == None:
801  return True
802  a, b = _coerce_exprs(self, other)
803  _args, sz = _to_ast_array((a, b))
804  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
805 
def __ne__(self, other)
Definition: z3py.py:788
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(self)
Definition: z3py.py:305
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().

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

Definition at line 742 of file z3py.py.

742  def as_ast(self):
743  return self.ast
744 
def as_ast(self)
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.

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

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

Definition at line 745 of file z3py.py.

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

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

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

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