Inheritance diagram for CharRef:

Public Member Functions
	__le__ (self, other)
	to_int (self)
	to_bv (self)
	is_digit (self)
Public Member Functions inherited from ExprRef
	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)
	__eq__ (self, other)
	__hash__ (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)

Additional Inherited Members
Data Fields inherited from AstRef
	ast = ast
	ctx = _get_ctx(ctx)
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

Detailed Description

Character expression.

Definition at line 11247 of file z3py.py.

Member Function Documentation

◆ le()

__le__	(		self,
			other )

Definition at line 11250 of file z3py.py.

    def __le__(self, other):
        other = _coerce_char(other, self.ctx)
        return _to_expr_ref(Z3_mk_char_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
 

◆ is_digit()

is_digit ( self )

Definition at line 11260 of file z3py.py.

    def is_digit(self):
        return _to_expr_ref(Z3_mk_char_is_digit(self.ctx_ref(), self.as_ast()), self.ctx)

◆ to_bv()

to_bv ( self )

Definition at line 11257 of file z3py.py.

    def to_bv(self):
        return _to_expr_ref(Z3_mk_char_to_bv(self.ctx_ref(), self.as_ast()), self.ctx)
 

◆ to_int()

to_int ( self )

Definition at line 11254 of file z3py.py.

    def to_int(self):
        return _to_expr_ref(Z3_mk_char_to_int(self.ctx_ref(), self.as_ast()), self.ctx)
 

Public Member Functions