Z3
 
Loading...
Searching...
No Matches
CharRef Class Reference
+ 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)
 
 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 11070 of file z3py.py.

Member Function Documentation

◆ __le__()

__le__ ( self,
other )

Definition at line 11073 of file z3py.py.

11073 def __le__(self, other):
11074 other = _coerce_char(other, self.ctx)
11075 return _to_expr_ref(Z3_mk_char_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
11076
Z3_ast Z3_API Z3_mk_char_le(Z3_context c, Z3_ast ch1, Z3_ast ch2)
Create less than or equal to between two characters.

◆ is_digit()

is_digit ( self)

Definition at line 11083 of file z3py.py.

11083 def is_digit(self):
11084 return _to_expr_ref(Z3_mk_char_is_digit(self.ctx_ref(), self.as_ast()), self.ctx)
11085
11086
Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)
Create a check if the character is a digit.

◆ to_bv()

to_bv ( self)

Definition at line 11080 of file z3py.py.

11080 def to_bv(self):
11081 return _to_expr_ref(Z3_mk_char_to_bv(self.ctx_ref(), self.as_ast()), self.ctx)
11082
Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch)
Create a bit-vector (code point) from character.

◆ to_int()

to_int ( self)

Definition at line 11077 of file z3py.py.

11077 def to_int(self):
11078 return _to_expr_ref(Z3_mk_char_to_int(self.ctx_ref(), self.as_ast()), self.ctx)
11079
Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)
Create an integer (code point) from character.