cprover
string_builtin_function.h
Go to the documentation of this file.
1
3
4#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
5#define CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
6
8
10#include <util/optional.h>
11#include <util/string_expr.h>
12
13#include <vector>
14
15#define CHARACTER_FOR_UNKNOWN '?'
16
73{
74public:
77 virtual ~string_builtin_functiont() = default;
78
80 {
81 return {};
82 }
83
84 virtual std::vector<array_string_exprt> string_arguments() const
85 {
86 return {};
87 }
88
93 virtual optionalt<exprt>
94 eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
95
96 virtual std::string name() const = 0;
97
104 virtual string_constraintst
105 constraints(string_constraint_generatort &constraint_generator) const = 0;
106
109 virtual exprt length_constraint() const = 0;
110
112
116 virtual bool maybe_testing_function() const
117 {
118 return true;
119 }
120
121protected:
123
126 {
127 }
128};
129
132{
133public:
136
143 result(std::move(result)),
144 input(std::move(input))
145 {
146 }
147
154 const exprt &return_code,
155 const std::vector<exprt> &fun_args,
157
159 {
160 return result;
161 }
162 std::vector<array_string_exprt> string_arguments() const override
163 {
164 return {input};
165 }
166 bool maybe_testing_function() const override
167 {
168 return false;
169 }
170};
171
175{
176public:
178
184 const exprt &return_code,
185 const std::vector<exprt> &fun_args,
188 {
189 PRECONDITION(fun_args.size() == 4);
190 character = fun_args[3];
191 }
192
194 eval(const std::function<exprt(const exprt &)> &get_value) const override;
195
196 std::string name() const override
197 {
198 return "concat_char";
199 }
200
202 constraints(string_constraint_generatort &generator) const override;
203
204 exprt length_constraint() const override;
205};
206
210{
211public:
214
220 const exprt &return_code,
221 const std::vector<exprt> &fun_args,
224 {
225 PRECONDITION(fun_args.size() == 5);
226 position = fun_args[3];
227 character = fun_args[4];
228 }
229
231 eval(const std::function<exprt(const exprt &)> &get_value) const override;
232
233 std::string name() const override
234 {
235 return "set_char";
236 }
237
239 constraints(string_constraint_generatort &generator) const override;
240
241 // \todo: length_constraint is not the best possible name because we also
242 // \todo: add constraint about the return code
243 exprt length_constraint() const override;
244};
245
250{
251public:
253 const exprt &return_code,
254 const std::vector<exprt> &fun_args,
257 {
258 }
259
261 eval(const std::function<exprt(const exprt &)> &get_value) const override;
262
263 std::string name() const override
264 {
265 return "to_lower_case";
266 }
267
269 constraints(string_constraint_generatort &generator) const override;
270
271 exprt length_constraint() const override
272 {
273 return and_exprt(
278 };
279};
280
285{
286public:
288 const exprt &return_code,
289 const std::vector<exprt> &fun_args,
292 {
293 }
294
301 std::move(return_code),
302 std::move(result),
303 std::move(input),
305 {
306 }
307
309 eval(const std::function<exprt(const exprt &)> &get_value) const override;
310
311 std::string name() const override
312 {
313 return "to_upper_case";
314 }
315
316 string_constraintst constraints(class symbol_generatort &fresh_symbol) const;
317
319 constraints(string_constraint_generatort &generator) const override
320 {
321 return constraints(generator.fresh_symbol);
322 };
323
324 exprt length_constraint() const override
325 {
326 return and_exprt(
331 };
332};
333
336{
337public:
340
342 const exprt &return_code,
343 const std::vector<exprt> &fun_args,
345
347 {
348 return result;
349 }
350
351 bool maybe_testing_function() const override
352 {
353 return false;
354 }
355};
356
359{
360public:
362 const exprt &return_code,
363 const std::vector<exprt> &fun_args,
366 {
367 PRECONDITION(fun_args.size() <= 4);
368 if(fun_args.size() == 4)
369 radix = fun_args[3];
370 else
371 radix = from_integer(10, arg.type());
372 };
373
375 eval(const std::function<exprt(const exprt &)> &get_value) const override;
376
377 std::string name() const override
378 {
379 return "string_of_int";
380 }
381
383 constraints(string_constraint_generatort &generator) const override;
384
385 exprt length_constraint() const override;
386
387private:
389};
390
393{
394public:
396 std::vector<array_string_exprt> under_test;
397 std::vector<exprt> args;
398 std::vector<array_string_exprt> string_arguments() const override
399 {
400 return under_test;
401 }
402};
403
409{
410public:
413 std::vector<array_string_exprt> string_args;
414 std::vector<exprt> args;
415
417 const exprt &return_code,
420
421 std::string name() const override
422 {
424 return id2string(
426 }
427 std::vector<array_string_exprt> string_arguments() const override
428 {
429 return std::vector<array_string_exprt>(string_args);
430 }
432 {
433 return string_res;
434 }
435
437 eval(const std::function<exprt(const exprt &)> &) const override
438 {
439 return {};
440 }
441
443 constraints(string_constraint_generatort &generator) const override;
444
445 exprt length_constraint() const override
446 {
447 // For now, there is no need for implementing that as `constraints`
448 // should always be called on these functions
450 }
451};
452
457 const array_string_exprt &a,
458 const std::function<exprt(const exprt &)> &get_value);
459
462 const std::vector<mp_integer> &array,
463 const array_typet &array_type);
464
465#endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Boolean AND.
Definition: std_expr.h:1974
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
Definition: array_pool.cpp:26
Arrays with given size.
Definition: std_types.h:763
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
Application of (mathematical) function.
const irep_idt & id() const
Definition: irep.h:396
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
std::vector< array_string_exprt > string_args
optionalt< array_string_exprt > string_res
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
optionalt< array_string_exprt > string_result() const override
std::vector< array_string_exprt > string_arguments() const override
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
function_application_exprt 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...
Base class for string functions that are built in the solver.
virtual optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const =0
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
string_builtin_functiont(const string_builtin_functiont &)=delete
virtual optionalt< array_string_exprt > string_result() const
string_builtin_functiont(exprt return_code, array_poolt &array_pool)
virtual bool maybe_testing_function() const
Tells whether the builtin function can be a testing function, that is a function that does not return...
virtual ~string_builtin_functiont()=default
virtual exprt length_constraint() const =0
Constraint ensuring that the length of the strings are coherent with the function call.
virtual string_constraintst constraints(string_constraint_generatort &constraint_generator) const =0
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
virtual std::string name() const =0
virtual std::vector< array_string_exprt > string_arguments() const
Adding a character at the end of a string.
string_concat_char_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
String creation from other types.
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...
string_creation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
String creation from integer types.
string_of_int_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
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...
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
std::string name() const override
Setting a character at a particular position of a string.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring that result is similar to input where the character at index position is ...
string_set_char_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
std::vector< array_string_exprt > string_arguments() const override
std::vector< array_string_exprt > under_test
Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowerc...
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
string_to_lower_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
string_to_upper_case_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)
string_to_upper_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
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...
String builtin_function transforming one string into another.
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
optionalt< array_string_exprt > string_result() const override
string_transformation_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)
std::vector< array_string_exprt > string_arguments() const override
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Generation of fresh symbols of a given type.
Definition: array_pool.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
API to expression classes for 'mathematical' expressions.
STL namespace.
nonstd::optional< T > optionalt
Definition: optional.h:35
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define UNIMPLEMENTED
Definition: invariant.h:525
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
optionalt< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Given a function get_value which gives a valuation to expressions, attempt to find the current value ...
Generates string constraints to link results from string functions with their arguments.
String expressions for the string solver.
Collection of constraints of different types: existential formulas, universal formulas,...