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 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 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 Probe.__ne__().

775 
776  def __eq__(self, other):
777  """Return a Z3 expression that represents the constraint `self == other`.
778 
779  If `other` is `None`, then this method simply returns `False`.
780 
781  >>> a = Int('a')
782  >>> b = Int('b')
783  >>> a == b
784  a == b
785  >>> a == None
786  False
787  """
788  if other == None:
789  return False
790  a, b = _coerce_exprs(self, other)
791  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
z3py.ExprRef.__eq__
def __eq__
Definition: z3py.py:775
Z3_mk_eq
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 
793  def __ne__(self, other):
794  """Return a Z3 expression that represents the constraint `self != other`.
795 
796  If `other` is `None`, then this method simply returns `True`.
797 
798  >>> a = Int('a')
799  >>> b = Int('b')
800  >>> a != b
801  a != b
802  >>> a != None
803  True
804  """
805  if other == None:
806  return True
807  a, b = _coerce_exprs(self, other)
808  _args, sz = _to_ast_array((a, b))
809  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
Z3_mk_distinct
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...
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
z3py.ExprRef.__ne__
def __ne__
Definition: z3py.py:792
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 
842  def arg(self, idx):
843  """Return argument `idx` of the application `self`.
844 
845  This method assumes that `self` is a function application with at least `idx+1` arguments.
846 
847  >>> a = Int('a')
848  >>> b = Int('b')
849  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
850  >>> t = f(a, b, 0)
851  >>> t.arg(0)
852  a
853  >>> t.arg(1)
854  b
855  >>> t.arg(2)
856  0
857  """
858  if __debug__:
859  _z3_assert(is_app(self), "Z3 application expected")
860  _z3_assert(idx < self.num_args(), "Invalid argument index")
861  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
Z3_get_app_arg
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.
z3py.ExprRef.num_args
def num_args
Definition: z3py.py:825
z3py.AstRef.as_ast
def as_ast
Definition: z3py.py:296
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
z3py.ExprRef.arg
def arg
Definition: z3py.py:841
z3py.is_app
def is_app
Definition: z3py.py:981
def as_ast (   self)

Definition at line 746 of file z3py.py.

746 
747  def as_ast(self):
748  return self.ast
z3py.ExprRef.as_ast
def as_ast
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 
863  def children(self):
864  """Return a list containing the children of the given expression
865 
866  >>> a = Int('a')
867  >>> b = Int('b')
868  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
869  >>> t = f(a, b, 0)
870  >>> t.children()
871  [a, b, 0]
872  """
873  if is_app(self):
874  return [self.arg(i) for i in range(self.num_args())]
875  else:
876  return []
z3py.ExprRef.num_args
def num_args
Definition: z3py.py:825
z3py.ExprRef.arg
def arg
Definition: z3py.py:841
z3py.ExprRef.children
def children
Definition: z3py.py:862
z3py.is_app
def is_app
Definition: z3py.py:981
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 
811  def decl(self):
812  """Return the Z3 function declaration associated with a Z3 application.
813 
814  >>> f = Function('f', IntSort(), IntSort())
815  >>> a = Int('a')
816  >>> t = f(a)
817  >>> eq(t.decl(), f)
818  True
819  >>> (a + 1).decl()
820  +
821  """
822  if __debug__:
823  _z3_assert(is_app(self), "Z3 application expected")
824  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
z3py.FuncDeclRef
Function Declarations.
Definition: z3py.py:591
Z3_get_app_decl
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
z3py.AstRef.as_ast
def as_ast
Definition: z3py.py:296
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
z3py.ExprRef.decl
def decl
Definition: z3py.py:810
z3py.is_app
def is_app
Definition: z3py.py:981
def get_id (   self)

Definition at line 749 of file z3py.py.

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

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

764 
765  def sort_kind(self):
766  """Shorthand for `self.sort().kind()`.
767 
768  >>> a = Array('a', IntSort(), IntSort())
769  >>> a.sort_kind() == Z3_ARRAY_SORT
770  True
771  >>> a.sort_kind() == Z3_INT_SORT
772  False
773  """
774  return self.sort().kind()
z3py.ExprRef.sort
def sort
Definition: z3py.py:752
z3py.ExprRef.sort_kind
def sort_kind
Definition: z3py.py:764
Generated on Fri Apr 12 2019 11:38:53 for Z3 by   doxygen 1.8.5