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 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

◆ 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 429 of file string_constraint_generator_transformation.cpp.

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

Referenced by string_constraint_generatort::add_axioms_for_replace().