Go to the documentation of this file.
9 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
10 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
113 const exprt &extra_value);
127 exprt at(std::size_t index)
const;
144 void add(
const std::size_t i,
const exprt &expr);
176 std::unique_ptr<string_builtin_functiont>
data;
179 std::unique_ptr<string_builtin_functiont> d,
193 data = std::move(other.data);
221 std::unique_ptr<const string_nodet>
225 builtin_function_nodet &
226 make_node(std::unique_ptr<string_builtin_functiont> &builtin_function);
235 const builtin_function_nodet &builtin_function);
239 const string_nodet &node,
240 const std::function<
void(
const builtin_function_nodet &)> &f)
const;
242 const builtin_function_nodet &node,
243 const std::function<
void(
const string_nodet &)> &f)
const;
251 const std::function<
exprt(
const exprt &)> &get_value)
const;
275 std::unordered_map<array_string_exprt, std::size_t, irep_hash>
311 return 2 * node.index +
324 const std::function<
void(
const nodet &)> &f)
const;
345 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
Operator to update elements in structs and arrays.
std::vector< string_constraintt > universal
The type of an expression, extends irept.
Correspondance between arrays and pointers string representations.
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
const string_builtin_functiont & get_builtin_function(const builtin_function_nodet &node) const
Represents arrays by the indexes up to which the value remains the same.
A string node points to builtin_function on which it depends.
exprt to_if_expression(const exprt &index) const
sparse_arrayt(exprt default_value)
builtin_function_nodet & make_node(std::unique_ptr< string_builtin_functiont > &builtin_function)
builtin_function is reset to an empty pointer after the node is created
Base class for all expressions.
nodet(const string_nodet &string_node)
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor,...
void for_each_successor(const nodet &i, const std::function< void(const nodet &)> &f) const
Applies f on all successors of the node n.
nodet(const builtin_function_nodet &builtin)
string_nodet & get_node(const array_string_exprt &e)
A builtin function node contains a builtin function call.
size_t operator()(const string_dependenciest::nodet &node) const optional_noexcept
bitvector_typet index_type()
sparse_arrayt(const with_exprt &expr)
Initialize a sparse array from an expression of the form array_of(x) with {i:=a} with {j:=b} ....
interval_sparse_arrayt(exprt default_value)
Array containing the same value at each index.
static exprt to_if_expression(const with_exprt &expr, const exprt &index)
Creates an if_expr corresponding to the result of accessing the array at the given index.
optionalt< std::size_t > result_from
void add_dependency(const array_string_exprt &e, const builtin_function_nodet &builtin_function)
Add edge from node for e to node for builtin_function if e is a simple array expression.
interval_sparse_arrayt(const with_exprt &expr)
An expression of the form array_of(x) with {i:=a} with {j:=b} is converted to an array arr where for ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::vector< builtin_function_nodet > builtin_function_nodes
Set of nodes representing builtin_functions.
exprt at(std::size_t index) const
Get the value at the specified index.
std::vector< string_nodet > string_nodes
Set of nodes representing strings.
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
void for_each_node(const std::function< void(const nodet &)> &f) const
Applies f on all nodes.
void clean_cache()
Clean the cache used by eval
string_nodet(array_string_exprt e, const std::size_t index)
bool add_node(string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool)
When right hand side of equation is a builtin_function add a "string_builtin_function" node to the gr...
optionalt< exprt > eval(const array_string_exprt &s, const std::function< exprt(const exprt &)> &get_value) const
Attempt to evaluate the given string from the dependencies and valuation of strings on which it depen...
void output_dot(std::ostream &stream) const
enum string_dependenciest::nodet::@5 kind
std::unique_ptr< const string_nodet > node_at(const array_string_exprt &e) const
void add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
std::unordered_map< array_string_exprt, std::size_t, irep_hash > node_index_pool
Nodes describing dependencies of a string: values of the map correspond to indexes in the vector stri...
nonstd::optional< T > optionalt
Base class for string functions that are built in the solver.
builtin_function_nodet(std::unique_ptr< string_builtin_functiont > d, std::size_t i)
std::vector< optionalt< exprt > > eval_string_cache
std::map< exprt, std::vector< std::size_t > > equations_containing
Record index of the equations that contain a given expression.
std::unique_ptr< string_builtin_functiont > data
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
std::vector< std::size_t > dependencies
std::unordered_map< std::size_t, std::vector< exprt > > strings_in_equation
Record expressions that are contained in the equation with the given index.
Keep track of dependencies between strings.
std::map< std::size_t, exprt > entries
std::map< exprt, std::set< exprt > > current
builtin_function_nodet & operator=(builtin_function_nodet &&other)
std::vector< exprt > find_expressions(const std::size_t i)
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
builtin_function_nodet(builtin_function_nodet &&other)
std::map< exprt, std::set< exprt > > cumulative
void for_each_dependency(const string_nodet &node, const std::function< void(const builtin_function_nodet &)> &f) const
Applies f to each node on which node depends.
Array constructor from a list of index-element pairs Operands are index/value pairs,...
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
bool operator==(const nodet &n) const
std::vector< std::size_t > find_equations(const exprt &expr)
Array constructor from list of elements.
std::vector< string_not_contains_constraintt > not_contains
void clear()
Clear the content of the dependency graph.