cprover
Loading...
Searching...
No Matches
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
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
128};
129
132{
133public:
136
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
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
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:
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
279};
280
285{
286public:
294
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
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)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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.
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
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...
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 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.
#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,...