string_dependencies.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: String solver
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
 
#ifndef CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H
#define CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H
 
#include <memory>
 
#include "string_builtin_function.h"
 
class string_dependenciest
{
public:
  class builtin_function_nodet
  {
  public:
    // index in the `builtin_function_nodes` vector
    std::size_t index;
    // pointer to the builtin function
    std::unique_ptr<string_builtin_functiont> data;
 
    explicit builtin_function_nodet(
      std::unique_ptr<string_builtin_functiont> d,
      std::size_t i)
      : index(i), data(std::move(d))
    {
    }
 
    builtin_function_nodet(builtin_function_nodet &&other)
      : index(other.index), data(std::move(other.data))
    {
    }
 
    builtin_function_nodet &operator=(builtin_function_nodet &&other)
    {
      index = other.index;
      data = std::move(other.data);
      return *this;
    }
  };
 
  class string_nodet
  {
  public:
    // expression the node corresponds to
    array_string_exprt expr;
    // index in the string_nodes vector
    std::size_t index;
    // builtin functions on which it depends, refered by there index in
    // builtin_function node vector.
    // \todo should these we shared pointers?
    std::vector<std::size_t> dependencies;
    // builtin function of which it is the result
    std::optional<std::size_t> result_from;
 
    explicit string_nodet(array_string_exprt e, const std::size_t index)
      : expr(std::move(e)), index(index)
    {
    }
  };
 
  string_nodet &get_node(const array_string_exprt &e);
 
  std::unique_ptr<const string_nodet>
  node_at(const array_string_exprt &e) const;
 
  builtin_function_nodet &
  make_node(std::unique_ptr<string_builtin_functiont> builtin_function);
  const string_builtin_functiont &
  get_builtin_function(const builtin_function_nodet &node) const;
 
  void add_dependency(
    const array_string_exprt &e,
    const builtin_function_nodet &builtin_function);
 
  void for_each_dependency(
    const string_nodet &node,
    const std::function<void(const builtin_function_nodet &)> &f) const;
  void for_each_dependency(
    const builtin_function_nodet &node,
    const std::function<void(const string_nodet &)> &f) const;
 
  std::optional<exprt> eval(
    const array_string_exprt &s,
    const std::function<exprt(const exprt &)> &get_value) const;
 
  void clean_cache();
 
  void output_dot(std::ostream &stream) const;
 
  [[nodiscard]] string_constraintst add_constraints(
    string_constraint_generatort &generatort,
    message_handlert &message_handler);
 
  void clear();
 
private:
  std::vector<builtin_function_nodet> builtin_function_nodes;
 
  std::vector<string_nodet> string_nodes;
 
  std::unordered_map<array_string_exprt, std::size_t, irep_hash>
    node_index_pool;
 
  class nodet
  {
  public:
    enum
    {
      BUILTIN,
      STRING
    } kind;
    std::size_t index;
 
    explicit nodet(const builtin_function_nodet &builtin)
      : kind(BUILTIN), index(builtin.index)
    {
    }
 
    explicit nodet(const string_nodet &string_node)
      : kind(STRING), index(string_node.index)
    {
    }
 
    bool operator==(const nodet &n) const
    {
      return n.kind == kind && n.index == index;
    }
  };
 
  // NOLINTNEXTLINE(readability/identifiers)
  struct node_hash
  {
    size_t operator()(const string_dependenciest::nodet &node) const
    {
      return 2 * node.index +
             (node.kind == string_dependenciest::nodet::STRING ? 0 : 1);
    }
  };
 
  mutable std::vector<std::optional<exprt>> eval_string_cache;
 
  void for_each_node(const std::function<void(const nodet &)> &f) const;
 
  void for_each_successor(
    const nodet &i,
    const std::function<void(const nodet &)> &f) const;
};
 
std::optional<exprt> add_node(
  string_dependenciest &dependencies,
  const exprt &expr,
  array_poolt &array_pool,
  symbol_generatort &fresh_symbol);
 
#endif // CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H