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 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.
|
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 429 of file string_constraint_generator_transformation.cpp.
References irept::id(), numeric_cast(), and exprt::type().
Referenced by string_constraint_generatort::add_axioms_for_replace().