#include "string_constraint_generator.h"
#include <util/mathematical_expr.h>
#include <util/string_expr.h>
#include <vector>

Include dependency graph for string_builtin_function.h:

This graph shows which files directly or indirectly include this file:

Classes
class	string_builtin_functiont
	Base class for string functions that are built in the solver. More...

class	string_transformation_builtin_functiont
	String builtin_function transforming one string into another. More...

class	string_concat_char_builtin_functiont
	Adding a character at the end of a string. More...

class	string_set_char_builtin_functiont
	Setting a character at a particular position of a string. More...

class	string_to_lower_case_builtin_functiont
	Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowercase character. More...

class	string_to_upper_case_builtin_functiont
	Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding uppercase character. More...

class	string_creation_builtin_functiont
	String creation from other types. More...

class	string_of_int_builtin_functiont
	String creation from integer types. More...

class	string_test_builtin_functiont
	String test. More...

class	string_builtin_function_with_no_evalt
	Functions that are not yet supported in this class but are supported by string_constraint_generatort. More...

Macros
#define	CHARACTER_FOR_UNKNOWN '?'
	Module: String solver Author: Diffblue Ltd. More...

Functions
std::optional< std::vector< mp_integer > >	eval_string (const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
	Given a function `get_value` which gives a valuation to expressions, attempt to find the current value of the array `a`. More...

array_string_exprt	make_string (const std::vector< mp_integer > &array, const array_typet &array_type)
	Make a string from a constant array. More...

Macro Definition Documentation

◆ CHARACTER_FOR_UNKNOWN

#define CHARACTER_FOR_UNKNOWN '?'

Module: String solver Author: Diffblue Ltd.

Definition at line 14 of file string_builtin_function.h.

std::optional<std::vector<mp_integer> > eval_string	(	const array_string_exprt &	a,
		const std::function< exprt(const exprt &)> &	get_value
	)

Given a function get_value which gives a valuation to expressions, attempt to find the current value of the array a.

If the valuation of some characters are missing, then return an empty optional.

array_string_exprt make_string	(	const std::vector< mp_integer > &	array,
		const array_typet &	array_type
	)

Make a string from a constant array.