string_insertion_builtin_function.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: String solver
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/
 
#ifndef CPROVER_SOLVERS_STRINGS_STRING_INSERTION_BUILTIN_FUNCTION_H
#define CPROVER_SOLVERS_STRINGS_STRING_INSERTION_BUILTIN_FUNCTION_H
 
#include "string_builtin_function.h"

class string_insertion_builtin_functiont : public string_builtin_functiont
{
public:
  array_string_exprt result;
  array_string_exprt input1;
  array_string_exprt input2;
  std::vector<exprt> args;

  string_insertion_builtin_functiont(
    const exprt &return_code,
    const std::vector<exprt> &fun_args,
    array_poolt &array_pool);
 
  std::optional<array_string_exprt> string_result() const override
  {
    return result;
  }
  std::vector<array_string_exprt> string_arguments() const override
  {
    return {input1, input2};
  }

  virtual std::vector<mp_integer> eval(
    const std::vector<mp_integer> &input1_value,
    const std::vector<mp_integer> &input2_value,
    const std::vector<mp_integer> &args_value) const;
 
  std::optional<exprt>
  eval(const std::function<exprt(const exprt &)> &get_value) const override;
 
  std::string name() const override
  {
    return "insert";
  }

  string_constraintst constraints(
    string_constraint_generatort &generator,
    message_handlert &message_handler) const override;

  exprt length_constraint() const override;
 
  bool maybe_testing_function() const override
  {
    return false;
  }
 
protected:
  string_insertion_builtin_functiont(
    const exprt &return_code,
    array_poolt &array_pool)
    : string_builtin_functiont(return_code, array_pool)
  {
  }
};
 
#endif // CPROVER_SOLVERS_STRINGS_STRING_INSERTION_BUILTIN_FUNCTION_H