ComplexRef Class Reference

Inheritance diagram for ComplexRef:

Public Member Functions
	sort (self)
	real_part (self)
	imag_part (self)
Public Member Functions inherited from ArithRef
	is_int (self)
	is_real (self)
	__add__ (self, other)
	__radd__ (self, other)
	__mul__ (self, other)
	__rmul__ (self, other)
	__sub__ (self, other)
	__rsub__ (self, other)
	__pow__ (self, other)
	__rpow__ (self, other)
	__div__ (self, other)
	__truediv__ (self, other)
	__rdiv__ (self, other)
	__rtruediv__ (self, other)
	__mod__ (self, other)
	__rmod__ (self, other)
	__neg__ (self)
	__pos__ (self)
	__le__ (self, other)
	__lt__ (self, other)
	__gt__ (self, other)
	__ge__ (self, other)
	__abs__ (self)
Public Member Functions inherited from ExprRef
	as_ast (self)
	get_id (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
Data Fields inherited from ArithRef
	ctx
Data Fields inherited from ExprRef
	ctx
	ast
Data Fields inherited from AstRef
	ast
	ctx

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

Detailed Description

A Complex expression supporting arithmetic, equality, and projections.

Complex numbers do not support ordering or exponentiation.

Definition at line 3318 of file z3py.py.

Member Function Documentation

imag_part()

imag_part

(

self

)

Definition at line 3330 of file z3py.py.

    def imag_part(self):
        return ImagPart(self)
 
 

real_part()

real_part

(

self

)

Definition at line 3327 of file z3py.py.

    def real_part(self):
        return RealPart(self)
 

sort()

sort

(

self

)

Return the sort (type) of the arithmetical expression `self`.

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

Reimplemented from ArithRef.

Definition at line 3324 of file z3py.py.

    def sort(self):
        return ComplexSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
 

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

Field Documentation

ctx

ctx

Definition at line 3325 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(), FiniteSetSortRef.cast(), 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(), DatatypeRef.update_field(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().