cprover
string_dependenciest Class Reference

Keep track of dependencies between strings. More...

#include <string_refinement_util.h>

Collaboration diagram for string_dependenciest:
[legend]

Classes

class  builtin_function_nodet
 A builtin function node contains a builtin function call. More...
 
struct  node_hash
 Hash function for nodes. More...
 
class  nodet
 
class  string_nodet
 A string node points to builtin_function on which it depends. More...
 

Public Member Functions

string_nodetget_node (const array_string_exprt &e)
 
std::unique_ptr< const string_nodetnode_at (const array_string_exprt &e) const
 
builtin_function_nodetmake_node (std::unique_ptr< string_builtin_functiont > &builtin_function)
 builtin_function is reset to an empty pointer after the node is created More...
 
const string_builtin_functiontget_builtin_function (const builtin_function_nodet &node) const
 
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. More...
 
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. More...
 
void for_each_dependency (const builtin_function_nodet &node, const std::function< void(const string_nodet &)> &f) const
 
optionalt< exprteval (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 depends Warning: eval uses a cache which must be cleaned everytime the valuations given by get_value can change. More...
 
void clean_cache ()
 Clean the cache used by eval More...
 
void output_dot (std::ostream &stream) 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 constraints. More...
 
void clear ()
 Clear the content of the dependency graph. More...
 

Private Member Functions

void for_each_node (const std::function< void(const nodet &)> &f) const
 Applies f on all nodes. More...
 
void for_each_successor (const nodet &i, const std::function< void(const nodet &)> &f) const
 Applies f on all successors of the node n. More...
 

Private Attributes

std::vector< builtin_function_nodetbuiltin_function_nodes
 Set of nodes representing builtin_functions. More...
 
std::vector< string_nodetstring_nodes
 Set of nodes representing strings. More...
 
std::unordered_map< array_string_exprt, std::size_t, irep_hashnode_index_pool
 Nodes describing dependencies of a string: values of the map correspond to indexes in the vector string_nodes. More...
 
std::vector< optionalt< exprt > > eval_string_cache
 

Detailed Description

Keep track of dependencies between strings.

Each string points to the builtin_function calls on which it depends. Each builtin_function points to the strings on which the result depends.

Definition at line 164 of file string_refinement_util.h.

Member Function Documentation

◆ add_constraints()

void string_dependenciest::add_constraints ( string_constraint_generatort generatort)

For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding constraints.

For the other builtin only add constraints on the length.

Definition at line 504 of file string_refinement_util.cpp.

References string_constraint_generatort::add_lemma(), builtin_function_nodes, irept::data, for_each_successor(), get_reachable(), and string_dependenciest::nodet::index.

Referenced by string_refinementt::dec_solve().

◆ add_dependency()

void string_dependenciest::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.

If it is an if_exprt we add the sub-expressions that are not if_exprts instead.

Definition at line 293 of file string_refinement_util.cpp.

References string_dependenciest::string_nodet::dependencies, for_each_atomic_string(), get_node(), and string_dependenciest::builtin_function_nodet::index.

Referenced by add_dependency_to_string_subexprs(), and add_node().

◆ clean_cache()

void string_dependenciest::clean_cache ( )

Clean the cache used by eval

Definition at line 366 of file string_refinement_util.cpp.

References eval_string_cache, and string_nodes.

Referenced by clear(), and string_refinementt::dec_solve().

◆ clear()

void string_dependenciest::clear ( void  )

Clear the content of the dependency graph.

Definition at line 303 of file string_refinement_util.cpp.

References builtin_function_nodes, clean_cache(), node_index_pool, and string_nodes.

◆ eval()

optionalt< exprt > string_dependenciest::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 depends Warning: eval uses a cache which must be cleaned everytime the valuations given by get_value can change.

Definition at line 344 of file string_refinement_util.cpp.

References builtin_function_nodes, eval_string_cache, node_index_pool, and string_nodes.

Referenced by string_refinementt::get().

◆ for_each_dependency() [1/2]

void string_dependenciest::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.

Definition at line 443 of file string_refinement_util.cpp.

References builtin_function_nodes, and string_dependenciest::string_nodet::dependencies.

Referenced by for_each_successor().

◆ for_each_dependency() [2/2]

void string_dependenciest::for_each_dependency ( const builtin_function_nodet node,
const std::function< void(const string_nodet &)> &  f 
) const

◆ for_each_node()

void string_dependenciest::for_each_node ( const std::function< void(const nodet &)> &  f) const
private

Applies f on all nodes.

Definition at line 471 of file string_refinement_util.cpp.

References builtin_function_nodes, and string_nodes.

Referenced by output_dot().

◆ for_each_successor()

void string_dependenciest::for_each_successor ( const nodet i,
const std::function< void(const nodet &)> &  f 
) const
private

◆ get_builtin_function()

const string_builtin_functiont & string_dependenciest::get_builtin_function ( const builtin_function_nodet node) const

Definition at line 275 of file string_refinement_util.cpp.

References string_dependenciest::builtin_function_nodet::data.

Referenced by add_node().

◆ get_node()

string_dependenciest::string_nodet & string_dependenciest::get_node ( const array_string_exprt e)

Definition at line 248 of file string_refinement_util.cpp.

References node_index_pool, and string_nodes.

Referenced by add_dependency(), and add_node().

◆ make_node()

string_dependenciest::builtin_function_nodet & string_dependenciest::make_node ( std::unique_ptr< string_builtin_functiont > &  builtin_function)

builtin_function is reset to an empty pointer after the node is created

Definition at line 267 of file string_refinement_util.cpp.

References builtin_function_nodes.

Referenced by add_node().

◆ node_at()

std::unique_ptr< const string_dependenciest::string_nodet > string_dependenciest::node_at ( const array_string_exprt e) const

Definition at line 259 of file string_refinement_util.cpp.

References node_index_pool, and string_nodes.

Referenced by for_each_dependency().

◆ output_dot()

Member Data Documentation

◆ builtin_function_nodes

std::vector<builtin_function_nodet> string_dependenciest::builtin_function_nodes
private

Set of nodes representing builtin_functions.

Definition at line 266 of file string_refinement_util.h.

Referenced by add_constraints(), clear(), eval(), for_each_dependency(), for_each_node(), for_each_successor(), make_node(), and output_dot().

◆ eval_string_cache

std::vector<optionalt<exprt> > string_dependenciest::eval_string_cache
mutableprivate

Definition at line 314 of file string_refinement_util.h.

Referenced by clean_cache(), and eval().

◆ node_index_pool

std::unordered_map<array_string_exprt, std::size_t, irep_hash> string_dependenciest::node_index_pool
private

Nodes describing dependencies of a string: values of the map correspond to indexes in the vector string_nodes.

Definition at line 274 of file string_refinement_util.h.

Referenced by clear(), eval(), get_node(), and node_at().

◆ string_nodes

std::vector<string_nodet> string_dependenciest::string_nodes
private

Set of nodes representing strings.

Definition at line 269 of file string_refinement_util.h.

Referenced by clean_cache(), clear(), eval(), for_each_node(), for_each_successor(), get_node(), node_at(), and output_dot().


The documentation for this class was generated from the following files: