string_constraint.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Defines string constraints. These are formulas talking about strings.
        We implemented two forms of constraints: `string_constraintt`
        are formulas of the form $\forall univ_var \in [lb,ub[. prem => body$,
        and not_contains_constraintt of the form:
        $\forall x in [lb,ub[. p(x) => \exists y in [lb,ub[. s1[x+y] != s2[y]$.
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/

 
#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
#define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
 
#include <util/format_expr.h>
#include <util/string_expr.h>
#include <util/union_find_replace.h>
 
class message_handlert;

class string_constraintt final
{
public:
  // String constraints are of the form
  // forall univ_var in [lower_bound,upper_bound[. body
  symbol_exprt univ_var;
  exprt lower_bound;
  exprt upper_bound;
  exprt body;
 
  string_constraintt(
    const symbol_exprt &_univ_var,
    const exprt &lower_bound,
    const exprt &upper_bound,
    const exprt &body,
    message_handlert &message_handler);
 
  // Default bound inferior is 0
  string_constraintt(
    symbol_exprt univ_var,
    exprt upper_bound,
    exprt body,
    message_handlert &message_handler)
    : string_constraintt(
        univ_var,
        from_integer(0, univ_var.type()),
        upper_bound,
        body,
        message_handler)
  {
  }
 
  exprt univ_within_bounds() const
  {
    return and_exprt(
      binary_relation_exprt(lower_bound, ID_le, univ_var),
      binary_relation_exprt(upper_bound, ID_gt, univ_var));
  }
 
  void replace_expr(union_find_replacet &replace_map)
  {
    replace_map.replace_expr(lower_bound);
    replace_map.replace_expr(upper_bound);
    replace_map.replace_expr(body);
  }
 
  exprt negation() const
  {
    return and_exprt(univ_within_bounds(), not_exprt(body));
  }
};

inline std::string to_string(const string_constraintt &expr)
{
  std::ostringstream out;
  out << "forall " << format(expr.univ_var) << " in ["
      << format(expr.lower_bound) << ", " << format(expr.upper_bound) << "). "
      << format(expr.body);
  return out.str();
}

struct string_not_contains_constraintt
{
  exprt univ_lower_bound;
  exprt univ_upper_bound;
  exprt premise;
  exprt exists_lower_bound;
  exprt exists_upper_bound;
  array_string_exprt s0;
  array_string_exprt s1;
};
 
std::string to_string(const string_not_contains_constraintt &expr);
 
void replace(
  const union_find_replacet &replace_map,
  string_not_contains_constraintt &constraint);
 
bool operator==(
  const string_not_contains_constraintt &left,
  const string_not_contains_constraintt &right);
 
// NOLINTNEXTLINE [allow specialization within 'std']
namespace std
{
template <>
// NOLINTNEXTLINE [struct identifier 'hash' does not end in t]
struct hash<string_not_contains_constraintt>
{
  size_t operator()(const string_not_contains_constraintt &constraint) const
  {
    return irep_hash()(constraint.univ_lower_bound) ^
           irep_hash()(constraint.univ_upper_bound) ^
           irep_hash()(constraint.exists_lower_bound) ^
           irep_hash()(constraint.exists_upper_bound) ^
           irep_hash()(constraint.premise) ^ irep_hash()(constraint.s0) ^
           irep_hash()(constraint.s1);
  }
};
} // namespace std
 
#endif