string_constraint_generator_transformation.cpp File Reference

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

#include "string_constraint_generator.h"
#include <util/arith_tools.h>
#include <util/mathematical_expr.h>

Include dependency graph for string_constraint_generator_transformation.cpp:

Go to the source code of this file.

Functions
static std::optional< std::pair< exprt, exprt > >	to_char_pair (exprt expr1, exprt expr2, std::function< array_string_exprt(const exprt &)> get_string_expr, array_poolt &array_pool)
	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 std::optional<std::pair<exprt, exprt> > to_char_pair ( exprt  expr1, exprt  expr2, std::function< array_string_exprt(const exprt &)>  get_string_expr, array_poolt &  array_pool  )

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

expr1	First expression
expr2	Second expression
get_string_expr	Function that yields an array_string_exprt corresponding to either expr1 or expr2, for the case where they are not primitive chars.
array_pool	pool of arrays representing strings

Returns

Optional pair of two expressions

Definition at line 272 of file string_constraint_generator_transformation.cpp.