22 const exprt &code_point)
134 const exprt pair =
pair_value(char1_as_int, char2_as_int, return_type);
165 const exprt pair =
pair_value(char1_as_int, char2_as_int, return_type);
The type of an expression.
Generates string constraints to link results from string functions with their arguments.
exprt add_axioms_for_code_point_at(const function_application_exprt &f)
add axioms corresponding to the String.codePointAt java function
A generic base class for relations, i.e., binary predicates.
application of (mathematical) function
const signedbv_typet get_return_code_type()
equal_exprt axiom_for_has_length(const exprt &rhs) const
exprt add_axioms_for_code_point_count(const function_application_exprt &f)
Add axioms corresponding the String.codePointCount java function.
exprt add_axioms_for_offset_by_code_point(const function_application_exprt &f)
Add axioms corresponding the String.offsetByCodePointCount java function.
exprt minimum(const exprt &a, const exprt &b)
const irep_idt & id() const
exprt pair_value(exprt char1, exprt char2, typet return_type)
the output corresponds to the unicode character given by the pair of characters of inputs assuming it...
division (integer and real)
exprt::operandst argumentst
#define PRECONDITION(CONDITION)
static exprt is_low_surrogate(const exprt &chr)
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en...
exprt maximum(const exprt &a, const exprt &b)
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
Base class for all expressions.
exprt add_axioms_for_code_point(const array_string_exprt &res, const exprt &code_point)
add axioms for the conversion of an integer representing a java code point to a utf-16 string ...
exprt add_axioms_for_code_point_before(const function_application_exprt &f)
add axioms corresponding to the String.codePointBefore java function
std::vector< exprt > lemmas
Expression to hold a symbol (variable)
const typet & subtype() const
static exprt is_high_surrogate(const exprt &chr)
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en...
bitvector_typet char_type()
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
symbol_generatort fresh_symbol