string_refinement_util.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: String solver
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
#define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
 
#include "string_constraint.h"
 
#include <map>
#include <set>
 
bool is_char_type(const typet &type);
 
bool is_char_array_type(const typet &type, const namespacet &ns);
 
bool is_char_pointer_type(const typet &type);
 
bool has_char_pointer_subtype(const typet &type, const namespacet &ns);
 
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns);
 
std::string
utf16_constant_array_to_java(const array_exprt &arr, std::size_t length);
 
struct index_set_pairt
{
  std::map<exprt, std::set<exprt>> cumulative;
  std::map<exprt, std::set<exprt>> current;
};
 
struct string_axiomst
{
  std::vector<string_constraintt> universal;
  std::vector<string_not_contains_constraintt> not_contains;
};
 
class sparse_arrayt
{
public:
  explicit sparse_arrayt(const with_exprt &expr);
 
  static exprt to_if_expression(const with_exprt &expr, const exprt &index);
 
protected:
  exprt default_value;
  std::map<std::size_t, exprt> entries;
  explicit sparse_arrayt(exprt default_value) : default_value(default_value)
  {
  }
};
 
class interval_sparse_arrayt final : public sparse_arrayt
{
public:
  explicit interval_sparse_arrayt(const with_exprt &expr) : sparse_arrayt(expr)
  {
  }
 
  interval_sparse_arrayt(const array_exprt &expr, const exprt &extra_value);
 
  interval_sparse_arrayt(
    const array_list_exprt &expr,
    const exprt &extra_value);
 
  exprt to_if_expression(const exprt &index) const;
 
  static std::optional<interval_sparse_arrayt>
  of_expr(const exprt &expr, const exprt &extra_value);
 
  array_exprt concretize(std::size_t size, const typet &index_type) const;
 
  exprt at(std::size_t index) const;
 
  explicit interval_sparse_arrayt(exprt default_value)
    : sparse_arrayt(default_value)
  {
  }
};
 
#endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H