cprover
string_constraint_generator_transformation.cpp File Reference

Generates string constraints for string transformations, that is, functions taking one string and returning another. More...

Include dependency graph for string_constraint_generator_transformation.cpp:

Go to the source code of this file.

Functions

static exprt is_upper_case (const exprt &character)
 Expression which is true for uppercase characters of the Basic Latin and Latin-1 supplement of unicode. More...
 
static exprt is_lower_case (const exprt &character)
 Expression which is true for lower_case characters of the Basic Latin and Latin-1 supplement of unicode. More...
 
static optionalt< std::pair< exprt, exprt > > to_char_pair (exprt expr1, exprt expr2, std::function< array_string_exprt(const exprt &)> get_string_expr)
 Convert two expressions to pair of chars If both expressions are characters, return pair of them If both expressions are 1-length strings, return first character of each Otherwise return empty optional. More...
 

Detailed Description

Generates string constraints for string transformations, that is, functions taking one string and returning another.

Definition in file string_constraint_generator_transformation.cpp.

Function Documentation

◆ is_lower_case()

static exprt is_lower_case ( const exprt character)
static

Expression which is true for lower_case characters of the Basic Latin and Latin-1 supplement of unicode.

Definition at line 284 of file string_constraint_generator_transformation.cpp.

References from_integer(), is_upper_case(), and exprt::type().

Referenced by string_constraint_generatort::add_axioms_for_to_upper_case().

◆ is_upper_case()

static exprt is_upper_case ( const exprt character)
static

Expression which is true for uppercase characters of the Basic Latin and Latin-1 supplement of unicode.

Definition at line 251 of file string_constraint_generator_transformation.cpp.

References disjunction(), from_integer(), and exprt::type().

Referenced by string_constraint_generatort::add_axioms_for_to_lower_case(), and is_lower_case().

◆ to_char_pair()

static optionalt<std::pair<exprt, exprt> > to_char_pair ( exprt  expr1,
exprt  expr2,
std::function< array_string_exprt(const exprt &)>  get_string_expr 
)
static

Convert two expressions to pair of chars If both expressions are characters, return pair of them If both expressions are 1-length strings, return first character of each Otherwise return empty optional.

Parameters
expr1First expression
expr2Second expression
Returns
Optional pair of two expressions

Definition at line 462 of file string_constraint_generator_transformation.cpp.

References irept::id(), numeric_cast(), and exprt::type().

Referenced by string_constraint_generatort::add_axioms_for_replace().