cprover
string_concatenation_builtin_function.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Builtin functions for string concatenations
4 
5 Author: Romain Brenguier, Joel Allred
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_STRINGS_STRING_CONCATENATION_BUILTIN_FUNCTION_H
13 #define CPROVER_SOLVERS_STRINGS_STRING_CONCATENATION_BUILTIN_FUNCTION_H
14 
17 
20 {
21 public:
29  const exprt &return_code,
30  const std::vector<exprt> &fun_args,
32 
33  std::vector<mp_integer> eval(
34  const std::vector<mp_integer> &input1_value,
35  const std::vector<mp_integer> &input2_value,
36  const std::vector<mp_integer> &args_value) const override;
37 
38  std::string name() const override
39  {
40  return "concat";
41  }
42 
44  constraints(string_constraint_generatort &generator) const override;
45 
46  exprt length_constraint() const override;
47 };
48 
49 #endif // CPROVER_SOLVERS_STRINGS_STRING_CONCATENATION_BUILTIN_FUNCTION_H
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:43
Base class for all expressions.
Definition: expr.h:54
string_concatenation_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
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
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 override
Evaluate the result from a concrete valuation of the arguments.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
String inserting a string into another one.
Collection of constraints of different types: existential formulas, universal formulas,...