cprover
|
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>
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, const exprt &offset) |
Add axioms ensuring the length of res corresponds that of s1 where we inserted s2 at position offset . More... | |
Generates string constraints for the family of insert Java functions.
Definition in file string_constraint_generator_insert.cpp.
exprt length_constraint_for_insert | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2, | ||
const exprt & | offset | ||
) |
Add axioms ensuring the length of res
corresponds that of s1
where we inserted s2
at position offset
.
Definition at line 74 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().