cprover
string_constraint_generator_testing.cpp File Reference

Generates string constraints for string functions that return Boolean values. More...

+ Include dependency graph for string_constraint_generator_testing.cpp:

Go to the source code of this file.

Functions

std::pair< exprt, string_constraintstadd_axioms_for_is_prefix (symbol_generatort &fresh_symbol, const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
 Add axioms stating that the returned expression is true exactly when the offset is greater or equal to 0 and the first string is a prefix of the second one, starting at position offset. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_is_prefix (symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool)
 Test if the target is a prefix of the string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_is_empty (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Add axioms stating that the returned value is true exactly when the argument string is empty. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_is_suffix (symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool)
 Test if the target is a suffix of the string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_contains (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Test whether a string contains another. More...
 

Detailed Description

Generates string constraints for string functions that return Boolean values.

Definition in file string_constraint_generator_testing.cpp.

Function Documentation

◆ add_axioms_for_contains()

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

Test whether a string contains another.

Add axioms ensuring the returned value is true when the first string contains the second. These axioms are:

  1. \( contains \Rightarrow |s_0| \ge |s_1| \)
  2. \( contains \Rightarrow 0 \le startpos \le |s_0|-|s_1| \)
  3. \( !contains \Rightarrow startpos = -1 \)
  4. \( \forall qvar < |s_1|.\ contains \Rightarrow s_1[qvar] = s_0[startpos + qvar] \)
  5. \( \forall startpos \le |s_0|-|s_1|. \ (!contains \land |s_0| \ge |s_1|) \Rightarrow \exists witness < |s_1|. \ s_1[witness] \ne s_0[startpos+witness] \)
    Warning
    slow for target longer than one character
    Parameters
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments refined_string s0 refined_string s1
    array_poolpool of arrays representing strings
    Returns
    Boolean expression contains

Definition at line 233 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_empty()

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

Add axioms stating that the returned value is true exactly when the argument string is empty.

Deprecated:
should use string_length(s)==0 instead
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with a string argument
array_poolpool of arrays representing strings
Returns
a Boolean expression

Definition at line 126 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_prefix() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_is_prefix ( symbol_generatort fresh_symbol,
const array_string_exprt prefix,
const array_string_exprt str,
const exprt offset 
)

Add axioms stating that the returned expression is true exactly when the offset is greater or equal to 0 and the first string is a prefix of the second one, starting at position offset.

These axioms are:

  1. isprefix => offset_within_bounds
  2. forall qvar in [0, |prefix|). isprefix => str[qvar + offset] = prefix[qvar]
  3. !isprefix => !offset_within_bounds || 0 <= witness < |prefix| && str[witness+offset] != prefix[witness]

where offset_within_bounds is: offset >= 0 && offset <= |str| && |str| - offset >= |prefix|

Parameters
fresh_symbolgenerator of fresh symbols
prefixan array of characters
stran array of characters
offsetan integer
Returns
Boolean expression isprefix

Definition at line 37 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_prefix() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_is_prefix ( symbol_generatort fresh_symbol,
const function_application_exprt f,
bool  swap_arguments,
array_poolt array_pool 
)

Test if the target is a prefix of the string.

Add axioms ensuring the return value is true when the string starts with the given target. These axioms are detailed here: string_constraint_generatort::add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)

Parameters
fresh_symbolgenerator of fresh symbols
fa function application with arguments refined_string s0, refined string s1 and optional integer argument offset whose default value is 0
swap_argumentsa Boolean telling whether the prefix is the second argument or the first argument
array_poolpool of arrays representing strings
Returns
boolean expression isprefix

Definition at line 99 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_suffix()

std::pair<exprt, string_constraintst> add_axioms_for_is_suffix ( symbol_generatort fresh_symbol,
const function_application_exprt f,
bool  swap_arguments,
array_poolt array_pool 
)

Test if the target is a suffix of the string.

Add axioms ensuring the return value is true when the first string ends with the given target. These axioms are:

  1. \( \texttt{issuffix} \Rightarrow |s_0| \ge |s_1| \)
  2. \( \forall i <|s_1|.\ {\tt issuffix} \Rightarrow s_1[i] = s_0[i + |s_0| - |s_1|] \)
  3. \( \lnot {\tt issuffix} \Rightarrow (|s_1| > |s_0| \land {\tt witness}=-1) \lor (|s_1| > {witness} \ge 0 \land s_1[{witness}] \ne s_0[{witness} + |s_0| - |s_1|] \)
Parameters
fresh_symbolgenerator of fresh symbols
fa function application with arguments refined_string s0 and refined_string s1
swap_argumentsboolean flag telling whether the suffix is the second argument or the first argument
array_poolpool of arrays representing strings
Returns
Boolean expression issuffix

Definition at line 168 of file string_constraint_generator_testing.cpp.