ExprRef Class Reference

Expressions. More...

Inheritance diagram for ExprRef:

Public Member Functions
	as_ast (self)
	get_id (self)
	sort (self)
	sort_kind (self)
	__eq__ (self, other)
	__hash__ (self)
	__ne__ (self, other)
	params (self)
	decl (self)
	kind (self)
	num_args (self)
	arg (self, idx)
	children (self)
	update (self, *args)
	from_string (self, s)
	serialize (self)
Public Member Functions inherited from AstRef
	__init__ (self, ast, ctx=None)
	__del__ (self)
	__deepcopy__ (self, memo={})
	__str__ (self)
	__repr__ (self)
	__nonzero__ (self)
	__bool__ (self)
	sexpr (self)
	ctx_ref (self)
	eq (self, other)
	translate (self, target)
	__copy__ (self)
	hash (self)
	py_value (self)
Public Member Functions inherited from Z3PPObject
	use_pp (self)

Data Fields
	ctx
	ast
Data Fields inherited from AstRef
	ast
	ctx

Additional Inherited Members
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

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

Member Function Documentation

__eq__()

__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

Reimplemented from AstRef.

Definition at line 1061 of file z3py.py.

    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
        """
        if other is None:
            return False
        a, b = _coerce_exprs(self, other)
        return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
 

Referenced by CheckSatResult.__ne__().

__hash__()

__hash__

(

self

)

 Hash code. 

Reimplemented from AstRef.

Definition at line 1078 of file z3py.py.

    def __hash__(self):
        """ Hash code. """
        return AstRef.__hash__(self)
 

__ne__()

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

    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
        """
        if other is None:
            return True
        a, b = _coerce_exprs(self, other)
        _args, sz = _to_ast_array((a, b))
        return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
 

arg()

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

    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
        """
        if z3_debug():
            _z3_assert(is_app(self), "Z3 application expected")
            _z3_assert(idx < self.num_args(), "Invalid argument index")
        return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
 

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

as_ast()

as_ast

(

self

)

Return a pointer to the corresponding C Z3_ast object.

Reimplemented from AstRef.

Reimplemented in PatternRef, and QuantifierRef.

Definition at line 1032 of file z3py.py.

    def as_ast(self):
        return self.ast
 

Referenced by AstRef.__del__(), BitVecRef.__invert__(), ArithRef.__neg__(), BitVecRef.__neg__(), ExprRef.arg(), IntNumRef.as_binary_string(), BitVecNumRef.as_binary_string(), RatNumRef.as_decimal(), AlgebraicNumRef.as_decimal(), IntNumRef.as_string(), RatNumRef.as_string(), BitVecNumRef.as_string(), ExprRef.decl(), ArrayRef.default(), RatNumRef.denominator(), AstRef.eq(), AstRef.get_id(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), PatternRef.get_id(), QuantifierRef.get_id(), AstRef.hash(), AlgebraicNumRef.index(), ExprRef.num_args(), AlgebraicNumRef.poly(), RatNumRef.py_value(), AstRef.sexpr(), AstRef.translate(), and ExprRef.update().

children()

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]

Reimplemented in QuantifierRef.

Definition at line 1162 of file z3py.py.

    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]
        """
        if is_app(self):
            return [self.arg(i) for i in range(self.num_args())]
        else:
            return []
 

decl()

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

    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()
        +
        """
        if z3_debug():
            _z3_assert(is_app(self), "Z3 application expected")
        return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
 

Referenced by ExprRef.params().

from_string()

from_string	(		self,
			s
	)

Definition at line 1201 of file z3py.py.

    def from_string(self, s):
        pass
 

get_id()

get_id

(

self

)

Return unique identifier for object. It can be used for hash-tables and maps.

Reimplemented from AstRef.

Reimplemented in PatternRef, and QuantifierRef.

Definition at line 1035 of file z3py.py.

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

kind()

kind

(

self

)

Return the Z3 internal kind of a function application.

Definition at line 1118 of file z3py.py.

    def kind(self):
        """Return the Z3 internal kind of a function application."""
        if z3_debug():
            _z3_assert(is_app(self), "Z3 application expected")
        return Z3_get_decl_kind(self.ctx_ref(), Z3_get_app_decl(self.ctx_ref(), self.ast))
        
 

Referenced by ArithSortRef.is_int(), ArithSortRef.is_real(), and ExprRef.sort_kind().

num_args()

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

    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
        """
        if z3_debug():
            _z3_assert(is_app(self), "Z3 application expected")
        return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
 

Referenced by AstRef.__bool__(), ExprRef.arg(), FuncEntry.arg_value(), FuncEntry.as_list(), ExprRef.children(), and ExprRef.update().

params()

params

(

self

)

Definition at line 1100 of file z3py.py.

    def params(self):
        return self.decl().params()
 

Referenced by ParamsRef.__deepcopy__(), ParamsRef.__del__(), ParamsRef.__repr__(), ExprRef.params(), ParamsRef.set(), and ParamsRef.validate().

serialize()

serialize

(

self

)

Definition at line 1204 of file z3py.py.

    def serialize(self):
        s = Solver()
        f = Function('F', self.sort(), BoolSort(self.ctx))
        s.add(f(self))
        return s.sexpr()
 

sort()

sort

(

self

)

Return the sort of expression `self`.

>>> x = Int('x')
>>> (x + 1).sort()
Int
>>> y = Real('y')
>>> (x + y).sort()
Real

Reimplemented in BoolRef, QuantifierRef, ArithRef, BitVecRef, ArrayRef, DatatypeRef, FiniteDomainRef, FPRef, and SeqRef.

Definition at line 1038 of file z3py.py.

    def sort(self):
        """Return the sort of expression `self`.
 
        >>> x = Int('x')
        >>> (x + 1).sort()
        Int
        >>> y = Real('y')
        >>> (x + y).sort()
        Real
        """
        return _sort(self.ctx, self.as_ast())
 

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

sort_kind()

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

    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
        """
        return self.sort().kind()
 

update()

update	(		self,
		*	args
	)

Update the arguments of the expression.

Return a new expression with the same function declaration and updated arguments.
The number of new arguments must match the current number of arguments.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> a = Int('a')
>>> b = Int('b')
>>> c = Int('c')
>>> t = f(a, b)
>>> t.update(c, c)
f(c, c)

Definition at line 1177 of file z3py.py.

    def update(self, *args):
        """Update the arguments of the expression.
        
        Return a new expression with the same function declaration and updated arguments.
        The number of new arguments must match the current number of arguments.
        
        >>> f = Function('f', IntSort(), IntSort(), IntSort())
        >>> a = Int('a')
        >>> b = Int('b')
        >>> c = Int('c')
        >>> t = f(a, b)
        >>> t.update(c, c)
        f(c, c)
        """
        if z3_debug():
            _z3_assert(is_app(self), "Z3 application expected")
            _z3_assert(len(args) == self.num_args(), "Number of arguments does not match")
            _z3_assert(all([is_expr(arg) for arg in args]), "Z3 expressions expected")
        num = len(args)
        _args = (Ast * num)()
        for i in range(num):
            _args[i] = args[i].as_ast()
        return _to_expr_ref(Z3_update_term(self.ctx_ref(), self.as_ast(), num, _args), self.ctx)
 

Field Documentation

ast

ast

Definition at line 1122 of file z3py.py.

Referenced by FuncDeclRef.__call__(), AstRef.__deepcopy__(), AstRef.__del__(), SortRef.__eq__(), SortRef.__ne__(), DatatypeSortRef.accessor(), FuncDeclRef.arity(), AstRef.as_ast(), ExprRef.as_ast(), QuantifierRef.as_ast(), FuncDeclRef.as_func_decl(), QuantifierRef.body(), FuncDeclRef.domain(), ArraySortRef.domain_n(), QuantifierRef.is_exists(), QuantifierRef.is_lambda(), FuncDeclRef.kind(), SortRef.name(), QuantifierRef.no_pattern(), QuantifierRef.num_no_patterns(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), FuncDeclRef.params(), QuantifierRef.pattern(), QuantifierRef.qid(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), QuantifierRef.skolem_id(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

ctx

ctx

Definition at line 1048 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), ModelRef.project(), ModelRef.project_with_witness(), Solver.push(), AstVector.push(), QuantifierRef.qid(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), ParamsRef.set(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), ParamDescrsRef.size(), Goal.size(), QuantifierRef.skolem_id(), AstVector.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), ExprRef.update(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().