cprover
string_insertion_builtin_function.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: String solver
4
5Author: 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{
17public:
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
82protected:
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.
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.
optionalt< array_string_exprt > string_result() const override
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,...