cprover
string_insertion_builtin_function.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String solver
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_SOLVERS_STRINGS_STRING_INSERTION_BUILTIN_FUNCTION_H
10 #define CPROVER_SOLVERS_STRINGS_STRING_INSERTION_BUILTIN_FUNCTION_H
11 
13 
16 {
17 public:
21  std::vector<exprt> args;
22 
30  const exprt &return_code,
31  const std::vector<exprt> &fun_args,
33 
35  {
36  return result;
37  }
38  std::vector<array_string_exprt> string_arguments() const override
39  {
40  return {input1, input2};
41  }
42 
44  virtual std::vector<mp_integer> eval(
45  const std::vector<mp_integer> &input1_value,
46  const std::vector<mp_integer> &input2_value,
47  const std::vector<mp_integer> &args_value) const;
48 
50  eval(const std::function<exprt(const exprt &)> &get_value) const override;
51 
52  std::string name() const override
53  {
54  return "insert";
55  }
56 
70  constraints(string_constraint_generatort &generator) const override;
71 
75  exprt length_constraint() const override;
76 
77  bool maybe_testing_function() const override
78  {
79  return false;
80  }
81 
82 protected:
84  const exprt &return_code,
87  {
88  }
89 };
90 
91 #endif // CPROVER_SOLVERS_STRINGS_STRING_INSERTION_BUILTIN_FUNCTION_H
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
Base class for all expressions.
Definition: expr.h:54
Base class for string functions that are built in the solver.
String inserting a string into another one.
optionalt< array_string_exprt > string_result() const override
string_insertion_builtin_functiont(const exprt &return_code, array_poolt &array_pool)
string_insertion_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
string_constraintst constraints(string_constraint_generatort &generator) const override
Constraints ensuring the result corresponds to input1 where we inserted input2 at position offset giv...
std::vector< array_string_exprt > string_arguments() const override
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
Evaluate the result from a concrete valuation of the arguments.
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
nonstd::optional< T > optionalt
Definition: optional.h:35
Collection of constraints of different types: existential formulas, universal formulas,...