string_constraint_generator_concat.cpp File Reference

Generates string constraints for functions adding content add the end of strings. More...

#include <solvers/refinement/string_constraint_generator.h>

Include dependency graph for string_constraint_generator_concat.cpp:

Go to the source code of this file.

Functions
std::pair< exprt, string_constraintst >	add_axioms_for_concat_substr (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
	Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index ‘start_index’and ending at indexend_index'‘. More...
exprt	length_constraint_for_concat_substr (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start, const exprt &end)
	Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at indexend'‘. More...
exprt	length_constraint_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
	Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 More...
exprt	length_constraint_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1)
	Add axioms enforcing that the length of res is that of the concatenation of s1 with. More...
std::pair< exprt, string_constraintst >	add_axioms_for_concat (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
	Add axioms enforcing that res is equal to the concatenation of s1 and s2. More...
std::pair< exprt, string_constraintst >	add_axioms_for_concat_code_point (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
	Add axioms corresponding to the StringBuilder.appendCodePoint(I) function. More...

Detailed Description

Generates string constraints for functions adding content add the end of strings.

Definition in file string_constraint_generator_concat.cpp.

Function Documentation

add_axioms_for_concat()

std::pair<exprt, string_constraintst> add_axioms_for_concat	(	symbol_generatort &	fresh_symbol,
		const array_string_exprt &	res,
		const array_string_exprt &	s1,
		const array_string_exprt &	s2
	)

Add axioms enforcing that res is equal to the concatenation of s1 and s2.

Deprecated:

should use concat_substr instead

Parameters

fresh_symbol	generator of fresh symbols
res	string_expression corresponding to the result
s1	the string expression to append to
s2	the string expression to append to the first one

Returns

an integer expression

Definition at line 126 of file string_constraint_generator_concat.cpp.

add_axioms_for_concat_code_point()

std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point	(	symbol_generatort &	fresh_symbol,
		const function_application_exprt &	f,
		array_poolt &	array_pool
	)

Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.

Deprecated:

java specific

Parameters

fresh_symbol	generator of fresh symbols
f	function application with two arguments: a string and a code point
array_pool	pool of arrays representing strings

Returns

an expression

Definition at line 143 of file string_constraint_generator_concat.cpp.

add_axioms_for_concat_substr()

std::pair<exprt, string_constraintst> add_axioms_for_concat_substr	(	symbol_generatort &	fresh_symbol,
		const array_string_exprt &	res,
		const array_string_exprt &	s1,
		const array_string_exprt &	s2,
		const exprt &	start_index,
		const exprt &	end_index
	)

Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index ‘start_index’and ending at indexend_index'‘.

Where start_index’ is max(0, start_index) and end_index' is max(min(end_index, s2.length), start_index') If s1.length + end_index' - start_index' is greater than the maximal integer of the type of res.length, then the result gets truncated to the size of this maximal integer.

These axioms are:

1. \(|res| = overflow ? |s_1| + end\_index' - start\_index' : max_int \)
2. \(\forall i<|s_1|. res[i]=s_1[i] \)
3. \(\forall i< |res| - |s_1|.\ res[i+|s_1|] = s_2[start\_index'+i]\)

Parameters

fresh_symbol	generator of fresh symbols
res	an array of characters expression
s1	an array of characters expression
s2	an array of characters expression
start_index	integer expression
end_index	integer expression

Returns

integer expression 0

Definition at line 38 of file string_constraint_generator_concat.cpp.

length_constraint_for_concat()

exprt length_constraint_for_concat	(	const array_string_exprt &	res,
		const array_string_exprt &	s1,
		const array_string_exprt &	s2
	)

Add axioms enforcing that the length of res is that of the concatenation of s1 with s2

Definition at line 99 of file string_constraint_generator_concat.cpp.

length_constraint_for_concat_char()

exprt length_constraint_for_concat_char	(	const array_string_exprt &	res,
		const array_string_exprt &	s1
	)

Add axioms enforcing that the length of res is that of the concatenation of s1 with.

Definition at line 109 of file string_constraint_generator_concat.cpp.

length_constraint_for_concat_substr()

exprt length_constraint_for_concat_substr	(	const array_string_exprt &	res,
		const array_string_exprt &	s1,
		const array_string_exprt &	s2,
		const exprt &	start,
		const exprt &	end
	)

Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at indexend'‘.

Where start_index’ is max(0, start) and end' is max(min(end, s2.length), start')

Definition at line 81 of file string_constraint_generator_concat.cpp.