Z3
Public Member Functions
CharRef Class Reference
+ Inheritance diagram for CharRef:

Public Member Functions

def __le__ (self, other)
 
def to_int (self)
 
def to_bv (self)
 
def is_digit (self)
 
- Public Member Functions inherited from ExprRef
def as_ast (self)
 
def get_id (self)
 
def sort (self)
 
def sort_kind (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __ne__ (self, other)
 
def params (self)
 
def decl (self)
 
def num_args (self)
 
def arg (self, idx)
 
def children (self)
 
def from_string (self, s)
 
def serialize (self)
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__ (self)
 
def __deepcopy__
 
def __str__ (self)
 
def __repr__ (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __nonzero__ (self)
 
def __bool__ (self)
 
def sexpr (self)
 
def as_ast (self)
 
def get_id (self)
 
def ctx_ref (self)
 
def eq (self, other)
 
def translate (self, target)
 
def __copy__ (self)
 
def hash (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Character expression.

Definition at line 10879 of file z3py.py.

Member Function Documentation

def __le__ (   self,
  other 
)

Definition at line 10882 of file z3py.py.

10882  def __le__(self, other):
10883  other = _coerce_char(other, self.ctx)
10884  return _to_expr_ref(Z3_mk_char_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
10885 
def as_ast(self)
Definition: z3py.py:392
def ctx_ref(self)
Definition: z3py.py:400
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.
def __le__(self, other)
Definition: z3py.py:10882
def is_digit (   self)

Definition at line 10892 of file z3py.py.

10892  def is_digit(self):
10893  return _to_expr_ref(Z3_mk_char_is_digit(self.ctx_ref(), self.as_ast()), self.ctx)
10894 
10895 
Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)
Create a check if the character is a digit.
def as_ast(self)
Definition: z3py.py:392
def is_digit(self)
Definition: z3py.py:10892
def ctx_ref(self)
Definition: z3py.py:400
def to_bv (   self)

Definition at line 10889 of file z3py.py.

10889  def to_bv(self):
10890  return _to_expr_ref(Z3_mk_char_to_bv(self.ctx_ref(), self.as_ast()), self.ctx)
10891 
def to_bv(self)
Definition: z3py.py:10889
def as_ast(self)
Definition: z3py.py:392
Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch)
Create a bit-vector (code point) from character.
def ctx_ref(self)
Definition: z3py.py:400
def to_int (   self)

Definition at line 10886 of file z3py.py.

10886  def to_int(self):
10887  return _to_expr_ref(Z3_mk_char_to_int(self.ctx_ref(), self.as_ast()), self.ctx)
10888 
def to_int(self)
Definition: z3py.py:10886
def as_ast(self)
Definition: z3py.py:392
Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)
Create an integer (code point) from character.
def ctx_ref(self)
Definition: z3py.py:400