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__ (self, ast, ctx=None)
 
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 736 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 775 of file z3py.py.

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

775  def __eq__(self, other):
776  """Return a Z3 expression that represents the constraint `self == other`.
777 
778  If `other` is `None`, then this method simply returns `False`.
779 
780  >>> a = Int('a')
781  >>> b = Int('b')
782  >>> a == b
783  a == b
784  >>> a == None
785  False
786  """
787  if other == None:
788  return False
789  a, b = _coerce_exprs(self, other)
790  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
791 
def __eq__(self, other)
Definition: z3py.py:775
def ctx_ref(self)
Definition: z3py.py:304
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, 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 792 of file z3py.py.

792  def __ne__(self, other):
793  """Return a Z3 expression that represents the constraint `self != other`.
794 
795  If `other` is `None`, then this method simply returns `True`.
796 
797  >>> a = Int('a')
798  >>> b = Int('b')
799  >>> a != b
800  a != b
801  >>> a != None
802  True
803  """
804  if other == None:
805  return True
806  a, b = _coerce_exprs(self, other)
807  _args, sz = _to_ast_array((a, b))
808  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
809 
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]).The distinct construct is us...
def __ne__(self, other)
Definition: z3py.py:792
def ctx_ref(self)
Definition: z3py.py:304
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 841 of file z3py.py.

Referenced by ExprRef.children().

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

Definition at line 746 of file z3py.py.

746  def as_ast(self):
747  return self.ast
748 
def as_ast(self)
Definition: z3py.py:746
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 862 of file z3py.py.

862  def children(self):
863  """Return a list containing the children of the given expression
864 
865  >>> a = Int('a')
866  >>> b = Int('b')
867  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
868  >>> t = f(a, b, 0)
869  >>> t.children()
870  [a, b, 0]
871  """
872  if is_app(self):
873  return [self.arg(i) for i in range(self.num_args())]
874  else:
875  return []
876 
def is_app(a)
Definition: z3py.py:981
def num_args(self)
Definition: z3py.py:825
def arg(self, idx)
Definition: z3py.py:841
def children(self)
Definition: z3py.py:862
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 810 of file z3py.py.

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

Definition at line 749 of file z3py.py.

749  def get_id(self):
750  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
751 
def as_ast(self)
Definition: z3py.py:296
def get_id(self)
Definition: z3py.py:749
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.
def ctx_ref(self)
Definition: z3py.py:304
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 825 of file z3py.py.

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

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

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

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

764  def sort_kind(self):
765  """Shorthand for `self.sort().kind()`.
766 
767  >>> a = Array('a', IntSort(), IntSort())
768  >>> a.sort_kind() == Z3_ARRAY_SORT
769  True
770  >>> a.sort_kind() == Z3_INT_SORT
771  False
772  """
773  return self.sort().kind()
774 
def sort_kind(self)
Definition: z3py.py:764
def sort(self)
Definition: z3py.py:752