cprover
string_constraint_generator_indexof.cpp File Reference

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

+ 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.

Function Documentation

◆ add_axioms_for_index_of() [1/2]

std::pair<exprt, string_constraintst> 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_symbolgenerator of fresh symbols
    stran array of characters expression
    ca character expression
    from_indexan 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<exprt, string_constraintst> 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_symbolgenerator of fresh symbols
ffunction application with arguments refined_string haystack, refined_string or character needle, and optional integer from_index with default value 0
array_poolpool of arrays representing strings
Returns
integer expression

Definition at line 291 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_index_of_string()

std::pair<exprt, string_constraintst> 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_symbolgenerator of fresh symbols
    haystackan array of character expression
    needlean array of character expression
    from_indexan 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<exprt, string_constraintst> 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_symbolgenerator of fresh symbols
    stran array of characters expression
    ca character expression
    from_indexan 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<exprt, string_constraintst> 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_symbolgenerator of fresh symbols
ffunction application with arguments refined_string haystack, refined_string or character needle, and optional integer from_index with default value |haystack|-1
array_poolpool of arrays representing strings
Returns
an integer expression

Definition at line 415 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_last_index_of_string()

std::pair<exprt, string_constraintst> 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_symbolgenerator of fresh symbols
    haystackan array of characters expression
    needlean array of characters expression
    from_indexinteger 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.