cprover
|
Generates string constraints for string transformations, that is, functions taking one string and returning another. More...
#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_constraint_generator.h>
#include <util/arith_tools.h>
Go to the source code of this file.
Functions | |
static exprt | is_upper_case (const exprt &character) |
Expression which is true for uppercase characters of the Basic Latin and Latin-1 supplement of unicode. More... | |
static exprt | is_lower_case (const exprt &character) |
Expression which is true for lower_case characters of the Basic Latin and Latin-1 supplement of unicode. More... | |
static optionalt< std::pair< exprt, exprt > > | to_char_pair (exprt expr1, exprt expr2, std::function< array_string_exprt(const exprt &)> get_string_expr) |
Convert two expressions to pair of chars If both expressions are characters, return pair of them If both expressions are 1-length strings, return first character of each Otherwise return empty optional. More... | |
Generates string constraints for string transformations, that is, functions taking one string and returning another.
Definition in file string_constraint_generator_transformation.cpp.
Expression which is true for lower_case characters of the Basic Latin and Latin-1 supplement of unicode.
Definition at line 284 of file string_constraint_generator_transformation.cpp.
References from_integer(), is_upper_case(), and exprt::type().
Referenced by string_constraint_generatort::add_axioms_for_to_upper_case().
Expression which is true for uppercase characters of the Basic Latin and Latin-1 supplement of unicode.
Definition at line 251 of file string_constraint_generator_transformation.cpp.
References disjunction(), from_integer(), and exprt::type().
Referenced by string_constraint_generatort::add_axioms_for_to_lower_case(), and is_lower_case().
|
static |
Convert two expressions to pair of chars If both expressions are characters, return pair of them If both expressions are 1-length strings, return first character of each Otherwise return empty optional.
expr1 | First expression |
expr2 | Second expression |
Definition at line 462 of file string_constraint_generator_transformation.cpp.
References irept::id(), numeric_cast(), and exprt::type().
Referenced by string_constraint_generatort::add_axioms_for_replace().