12#ifndef CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H
13#define CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H
34 std::unique_ptr<string_builtin_functiont>
data;
37 std::unique_ptr<string_builtin_functiont> d,
51 data = std::move(other.data);
79 std::unique_ptr<const string_nodet>
82 builtin_function_nodet &
96 const string_nodet &node,
97 const std::function<
void(
const builtin_function_nodet &)> &f)
const;
99 const builtin_function_nodet &node,
100 const std::function<
void(
const string_nodet &)> &f)
const;
108 const std::function<
exprt(
const exprt &)> &get_value)
const;
133 std::unordered_map<array_string_exprt, std::size_t, irep_hash>
169 return 2 * node.index +
182 const std::function<
void(
const nodet &)> &f)
const;
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Correspondance between arrays and pointers string representations.
Base class for all expressions.
Base class for string functions that are built in the solver.
A builtin function node contains a builtin function call.
builtin_function_nodet & operator=(builtin_function_nodet &&other)
std::unique_ptr< string_builtin_functiont > data
builtin_function_nodet(builtin_function_nodet &&other)
builtin_function_nodet(std::unique_ptr< string_builtin_functiont > d, std::size_t i)
nodet(const string_nodet &string_node)
nodet(const builtin_function_nodet &builtin)
bool operator==(const nodet &n) const
enum string_dependenciest::nodet::@6 kind
A string node points to builtin_function on which it depends.
string_nodet(array_string_exprt e, const std::size_t index)
optionalt< std::size_t > result_from
std::vector< std::size_t > dependencies
Keep track of dependencies between strings.
std::unique_ptr< const string_nodet > node_at(const array_string_exprt &e) const
void for_each_node(const std::function< void(const nodet &)> &f) const
Applies f on all nodes.
builtin_function_nodet & make_node(std::unique_ptr< string_builtin_functiont > builtin_function)
void output_dot(std::ostream &stream) const
void clean_cache()
Clean the cache used by eval
std::vector< builtin_function_nodet > builtin_function_nodes
Set of nodes representing builtin_functions.
void clear()
Clear the content of the dependency graph.
NODISCARD string_constraintst add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
const string_builtin_functiont & get_builtin_function(const builtin_function_nodet &node) const
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...
std::vector< string_nodet > string_nodes
Set of nodes representing strings.
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.
std::vector< optionalt< exprt > > eval_string_cache
void for_each_successor(const nodet &i, const std::function< void(const nodet &)> &f) const
Applies f on all successors of the node n.
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.
string_nodet & get_node(const array_string_exprt &e)
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...
Generation of fresh symbols of a given type.
optionalt< exprt > add_node(string_dependenciest &dependencies, const exprt &expr, array_poolt &array_pool, symbol_generatort &fresh_symbol)
When a sub-expression of expr is a builtin_function, add a "string_builtin_function" node to the grap...
Collection of constraints of different types: existential formulas, universal formulas,...
size_t operator()(const string_dependenciest::nodet &node) const