string_constraint_instantiation.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Defines related function for string constraints.
 
Author: Jesse Sigal, jesse.sigal@diffblue.com
 
\*******************************************************************/

 
#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
#define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
 
#include <util/mp_arith.h>
#include <util/std_expr.h> // IWYU pragma: keep
 
#include <set>
 
class string_constraintt;
struct string_not_contains_constraintt;

exprt instantiate(
  const string_constraintt &axiom,
  const exprt &str,
  const exprt &val);
 
std::vector<exprt> instantiate_not_contains(
  const string_not_contains_constraintt &axiom,
  const std::set<std::pair<exprt, exprt>> &index_pairs,
  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
    &witnesses);

class linear_functiont
{
public:
  explicit linear_functiont(const exprt &f);

  void add(const linear_functiont &other);

  exprt to_expr(bool negated = false) const;

  static exprt solve(linear_functiont f, const exprt &var, const exprt &val);

  std::string format();
 
private:
  mp_integer constant_coefficient;
  std::unordered_map<exprt, mp_integer, irep_hash> coefficients;
  typet type;
};
 
#endif // CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H