cprover
string_constraint_generator_indexof.cpp File Reference

Generates string constraints for the family of indexOf and lastIndexOf java functions. More...

#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_constraint_generator.h>
Include dependency graph for string_constraint_generator_indexof.cpp:

Go to the source code of this file.

## Functions

std::pair< exprt, string_constraintstadd_axioms_for_index_of (symbol_generatort &fresh_symbol, const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the first occurrence of needle (c) starting the search at from_index, or is -1 if no such character occurs at or after position from_index. More...

std::pair< exprt, string_constraintstadd_axioms_for_index_of_string (symbol_generatort &fresh_symbol, const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
Add axioms stating that the returned value index is the index within haystack of the first occurrence of needle starting the search at from_index, or -1 if needle does not occur at or after position from_index. More...

std::pair< exprt, string_constraintstadd_axioms_for_last_index_of_string (symbol_generatort &fresh_symbol, const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index. More...

std::pair< exprt, string_constraintstadd_axioms_for_index_of (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Index of the first occurence of a target inside the string. More...

std::pair< exprt, string_constraintstadd_axioms_for_last_index_of (symbol_generatort &fresh_symbol, const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the last occurrence of needle (c) starting the search backward at from_index, or -1 if no such character occurs at or before position from_index. More...

std::pair< exprt, string_constraintstadd_axioms_for_last_index_of (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Index of the last occurence of a target inside the string. More...

## Detailed Description

Generates string constraints for the family of indexOf and lastIndexOf java functions.

Definition in file string_constraint_generator_indexof.cpp.

## ◆ add_axioms_for_index_of() [1/2]

 std::pair add_axioms_for_index_of ( symbol_generatort & fresh_symbol, const array_string_exprt & str, const exprt & c, const exprt & from_index )

Add axioms stating that the returned value is the index within haystack (str) of the first occurrence of needle (c) starting the search at from_index, or is -1 if no such character occurs at or after position from_index.

These axioms are:

1. $$-1 \le {\tt index} < |{\tt haystack}|$$
2. $$\lnot contains \Leftrightarrow {\tt index} = -1$$
3. $$contains \Rightarrow {\tt from\_index} \le {\tt index} \land {\tt haystack}[{\tt index}] = {\tt needle}$$
4. $$\forall i \in [{\tt from\_index}, {\tt index}).\ contains \Rightarrow {\tt haystack}[i] \ne {\tt needle}$$
5. $$\forall m, n \in [{\tt from\_index}, |{\tt haystack}|) .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle}$$
Parameters
 fresh_symbol generator of fresh symbols str an array of characters expression c a character expression from_index an integer expression
Returns
integer expression index

Definition at line 38 of file string_constraint_generator_indexof.cpp.

## ◆ add_axioms_for_index_of() [2/2]

 std::pair add_axioms_for_index_of ( symbol_generatort & fresh_symbol, const function_application_exprt & f, array_poolt & array_pool )

Index of the first occurence of a target inside the string.

If the target is a character: Add axioms stating that the returned value is the index within haystack (str) of the first occurrence of needle (c) starting the search at from_index, or is -1 if no such character occurs at or after position from_index. (More...)

If the target is a refined_string: Add axioms stating that the returned value index is the index within haystack of the first occurrence of needle starting the search at from_index, or -1 if needle does not occur at or after position from_index. (More...)

Warning
slow for string targets
Parameters
 fresh_symbol generator of fresh symbols f function application with arguments refined_string haystack, refined_string or character needle, and optional integer from_index with default value 0 array_pool pool of arrays representing strings
Returns
integer expression

Definition at line 291 of file string_constraint_generator_indexof.cpp.

 std::pair add_axioms_for_index_of_string ( symbol_generatort & fresh_symbol, const array_string_exprt & haystack, const array_string_exprt & needle, const exprt & from_index )

Add axioms stating that the returned value index is the index within haystack of the first occurrence of needle starting the search at from_index, or -1 if needle does not occur at or after position from_index.

If needle is an empty string then the result is from_index.

These axioms are:

1. $$contains \Rightarrow {\tt from\_index} \le \tt{index} \le |{\tt haystack}|-|{\tt needle} |$$
2. $$\lnot contains \Leftrightarrow {\tt index} = -1$$
3. $$\forall n \in [0,|{\tt needle}|).\ contains \Rightarrow {\tt haystack}[n + {\tt index}] = {\tt needle}[n]$$
4. $$\forall n \in [{\tt from\_index}, {\tt index}).\ contains \Rightarrow (\exists m \in [0,|{\tt needle}|).\ {\tt haystack}[m+n] \ne {\tt needle}[m]])$$
5. $$\forall n \in [{\tt from\_index},|{\tt haystack}|-|{\tt needle}|] .\ \lnot contains \Rightarrow (\exists m \in [0,|{\tt needle}|) .\ {\tt haystack}[m+n] \ne {\tt needle}[m])$$
6. $$|{\tt needle}| = 0 \Rightarrow \tt{index} = from_index$$
Parameters
 fresh_symbol generator of fresh symbols haystack an array of character expression needle an array of character expression from_index an integer expression
Returns
integer expression index representing the first index of needle in haystack

Definition at line 111 of file string_constraint_generator_indexof.cpp.

## ◆ add_axioms_for_last_index_of() [1/2]

 std::pair add_axioms_for_last_index_of ( symbol_generatort & fresh_symbol, const array_string_exprt & str, const exprt & c, const exprt & from_index )

Add axioms stating that the returned value is the index within haystack (str) of the last occurrence of needle (c) starting the search backward at from_index, or -1 if no such character occurs at or before position from_index.

These axioms are :

1. $$-1 \le {\tt index} \le {\tt from\_index} \land {\tt index} < |{\tt haystack}|$$
2. $${\tt index} = -1 \Leftrightarrow \lnot contains$$
3. $$contains \Rightarrow {\tt haystack}[{\tt index}] = {\tt needle} )$$
4. $$\forall n \in [{\tt index} +1, min({\tt from\_index}+1, |{\tt haystack}|)) .\ contains \Rightarrow {\tt haystack}[n] \ne {\tt needle}$$
5. $$\forall m \in [0, min({\tt from\_index}+1, |{\tt haystack}|)) .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle}$$
Parameters
 fresh_symbol generator of fresh symbols str an array of characters expression c a character expression from_index an integer expression
Returns
integer expression index representing the last index of needle in haystack before or at from_index, or -1 if there is none

Definition at line 346 of file string_constraint_generator_indexof.cpp.

## ◆ add_axioms_for_last_index_of() [2/2]

 std::pair add_axioms_for_last_index_of ( symbol_generatort & fresh_symbol, const function_application_exprt & f, array_poolt & array_pool )

Index of the last occurence of a target inside the string.

If the target is a character: Add axioms stating that the returned value is the index within haystack (str) of the last occurrence of needle (c) starting the search backward at from_index, or -1 if no such character occurs at or before position from_index. (More...)

If the target is a refined_string: Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index. (More...)

Warning
slow for string targets
Parameters
 fresh_symbol generator of fresh symbols f function application with arguments refined_string haystack, refined_string or character needle, and optional integer from_index with default value |haystack|-1 array_pool pool of arrays representing strings
Returns
an integer expression

Definition at line 415 of file string_constraint_generator_indexof.cpp.

 std::pair add_axioms_for_last_index_of_string ( symbol_generatort & fresh_symbol, const array_string_exprt & haystack, const array_string_exprt & needle, const exprt & from_index )

Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index.

If needle is the empty string, the result is from_index.

These axioms are:

1. $$contains \Rightarrow -1 \le {\tt index} \land {\tt index} \le {\tt from\_index} \land {\tt index} \le |{\tt haystack}| - |{\tt needle}|$$
2. $$\lnot contains \Leftrightarrow {\tt index}= -1$$
3. $$\forall n \in [0, |{\tt needle}|).\ contains \Rightarrow {\tt haystack}[n+{\tt index}] = {\tt needle}[n]$$
4. $$\forall n \in [{\tt index}+1, min({\tt from\_index}, |{\tt haystack}| - |{\tt needle}|)] .\ contains \Rightarrow (\exists m \in [0,|{\tt needle}|) .\ {\tt haystack}[m+n] \ne {\tt needle}[m]])$$
5. $$\forall n \in [0, min({\tt from\_index}, |{\tt haystack}| - |{\tt needle}|)] .\ \lnot contains \Rightarrow (\exists m \in [0,|{\tt needle}|) .\ {\tt haystack}[m+n] \ne {\tt needle}[m])$$
6. $$|{\tt needle}| = 0 \Rightarrow index = from_index$$
Parameters
 fresh_symbol generator of fresh symbols haystack an array of characters expression needle an array of characters expression from_index integer expression
Returns
integer expression index representing the last index of needle in haystack before or at from_index, or -1 if there is none

Definition at line 205 of file string_constraint_generator_indexof.cpp.