string_constraint_generator_insert.cpp File Reference

Generates string constraints for the family of insert Java functions. More...

#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_constraint_generator.h>
#include <util/deprecate.h>

Include dependency graph for string_constraint_generator_insert.cpp:

Go to the source code of this file.

Functions
exprt	length_constraint_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
	Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2. More...

Detailed Description

Generates string constraints for the family of insert Java functions.

Definition in file string_constraint_generator_insert.cpp.

Function Documentation

length_constraint_for_insert()

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

Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2.

Definition at line 76 of file string_constraint_generator_insert.cpp.

References array_string_exprt::length().

Referenced by string_constraint_generatort::add_axioms_for_insert(), and string_insertion_builtin_functiont::length_constraint().