cprover
string_builtin_function.h
Go to the documentation of this file.
1 
4 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
5 #define CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
6 
7 #include <vector>
8 #include <util/optional.h>
9 #include <util/string_expr.h>
11 
12 class array_poolt;
13 struct string_constraintst;
15 
16 #define CHARACTER_FOR_UNKNOWN '?'
17 
20 {
21 public:
23  virtual ~string_builtin_functiont() = default;
24 
26  {
27  return {};
28  }
29 
30  virtual std::vector<array_string_exprt> string_arguments() const
31  {
32  return {};
33  }
34 
39  virtual optionalt<exprt>
40  eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
41 
42  virtual std::string name() const = 0;
43 
46  virtual string_constraintst
47  constraints(string_constraint_generatort &constraint_generator) const = 0;
48 
51  virtual exprt length_constraint() const = 0;
52 
54 
58  virtual bool maybe_testing_function() const
59  {
60  return true;
61  }
62 
63 private:
64  string_builtin_functiont() = default;
65 
66 protected:
68  : return_code(std::move(return_code))
69  {
70  }
71 };
72 
75 {
76 public:
79 
85  result(std::move(result)),
86  input(std::move(input))
87  {
88  }
89 
96  const exprt &return_code,
97  const std::vector<exprt> &fun_args,
98  array_poolt &array_pool);
99 
101  {
102  return result;
103  }
104  std::vector<array_string_exprt> string_arguments() const override
105  {
106  return {input};
107  }
108  bool maybe_testing_function() const override
109  {
110  return false;
111  }
112 };
113 
117 {
118 public:
120 
126  const exprt &return_code,
127  const std::vector<exprt> &fun_args,
128  array_poolt &array_pool)
130  {
131  PRECONDITION(fun_args.size() == 4);
132  character = fun_args[3];
133  }
134 
136  eval(const std::function<exprt(const exprt &)> &get_value) const override;
137 
138  std::string name() const override
139  {
140  return "concat_char";
141  }
142 
144  constraints(string_constraint_generatort &generator) const override;
145 
146  exprt length_constraint() const override;
147 };
148 
152 {
153 public:
156 
162  const exprt &return_code,
163  const std::vector<exprt> &fun_args,
164  array_poolt &array_pool)
166  {
167  PRECONDITION(fun_args.size() == 5);
168  position = fun_args[3];
169  character = fun_args[4];
170  }
171 
173  eval(const std::function<exprt(const exprt &)> &get_value) const override;
174 
175  std::string name() const override
176  {
177  return "set_char";
178  }
179 
181  constraints(string_constraint_generatort &generator) const override;
182 
183  // \todo: length_constraint is not the best possible name because we also
184  // \todo: add constraint about the return code
185  exprt length_constraint() const override;
186 };
187 
192 {
193 public:
195  const exprt &return_code,
196  const std::vector<exprt> &fun_args,
197  array_poolt &array_pool)
199  {
200  }
201 
203  eval(const std::function<exprt(const exprt &)> &get_value) const override;
204 
205  std::string name() const override
206  {
207  return "to_lower_case";
208  }
209 
211  constraints(string_constraint_generatort &generator) const override;
212 
213  exprt length_constraint() const override
214  {
215  return and_exprt(
218  };
219 };
220 
225 {
226 public:
228  const exprt &return_code,
229  const std::vector<exprt> &fun_args,
230  array_poolt &array_pool)
232  {
233  }
234 
240  std::move(return_code),
241  std::move(result),
242  std::move(input))
243  {
244  }
245 
247  eval(const std::function<exprt(const exprt &)> &get_value) const override;
248 
249  std::string name() const override
250  {
251  return "to_upper_case";
252  }
253 
254  string_constraintst constraints(class symbol_generatort &fresh_symbol) const;
255 
257  constraints(string_constraint_generatort &generator) const override
258  {
259  return constraints(generator.fresh_symbol);
260  };
261 
262  exprt length_constraint() const override
263  {
264  return and_exprt(
267  };
268 };
269 
272 {
273 public:
277  std::vector<exprt> args;
278 
286  const exprt &return_code,
287  const std::vector<exprt> &fun_args,
288  array_poolt &array_pool);
289 
291  {
292  return result;
293  }
294  std::vector<array_string_exprt> string_arguments() const override
295  {
296  return {input1, input2};
297  }
298 
300  virtual std::vector<mp_integer> eval(
301  const std::vector<mp_integer> &input1_value,
302  const std::vector<mp_integer> &input2_value,
303  const std::vector<mp_integer> &args_value) const;
304 
306  eval(const std::function<exprt(const exprt &)> &get_value) const override;
307 
308  std::string name() const override
309  {
310  return "insert";
311  }
312 
314  constraints(string_constraint_generatort &generator) const override;
315 
316  exprt length_constraint() const override;
317 
318  bool maybe_testing_function() const override
319  {
320  return false;
321  }
322 
323 protected:
326  {
327  }
328 };
329 
332 {
333 public:
341  const exprt &return_code,
342  const std::vector<exprt> &fun_args,
343  array_poolt &array_pool);
344 
345  std::vector<mp_integer> eval(
346  const std::vector<mp_integer> &input1_value,
347  const std::vector<mp_integer> &input2_value,
348  const std::vector<mp_integer> &args_value) const override;
349 
350  std::string name() const override
351  {
352  return "concat";
353  }
354 
356  constraints(string_constraint_generatort &generator) const override;
357 
358  exprt length_constraint() const override;
359 };
360 
363 {
364 public:
367 
369  const exprt &return_code,
370  const std::vector<exprt> &fun_args,
371  array_poolt &array_pool);
372 
374  {
375  return result;
376  }
377 
378  bool maybe_testing_function() const override
379  {
380  return false;
381  }
382 };
383 
386 {
387 public:
389  const exprt &return_code,
390  const std::vector<exprt> &fun_args,
391  array_poolt &array_pool)
392  : string_creation_builtin_functiont(return_code, fun_args, array_pool)
393  {
394  PRECONDITION(fun_args.size() <= 4);
395  if(fun_args.size() == 4)
396  radix = fun_args[3];
397  else
398  radix = from_integer(10, arg.type());
399  };
400 
402  eval(const std::function<exprt(const exprt &)> &get_value) const override;
403 
404  std::string name() const override
405  {
406  return "string_of_int";
407  }
408 
410  constraints(string_constraint_generatort &generator) const override;
411 
412  exprt length_constraint() const override;
413 
414 private:
416 };
417 
420 {
421 public:
423  std::vector<array_string_exprt> under_test;
424  std::vector<exprt> args;
425  std::vector<array_string_exprt> string_arguments() const override
426  {
427  return under_test;
428  }
429 };
430 
436 {
437 public:
440  std::vector<array_string_exprt> string_args;
441  std::vector<exprt> args;
442 
444  const exprt &return_code,
446  array_poolt &array_pool);
447 
448  std::string name() const override
449  {
451  }
452  std::vector<array_string_exprt> string_arguments() const override
453  {
454  return std::vector<array_string_exprt>(string_args);
455  }
457  {
458  return string_res;
459  }
460 
462  eval(const std::function<exprt(const exprt &)> &) const override
463  {
464  return {};
465  }
466 
468  constraints(string_constraint_generatort &generator) const override;
469 
470  exprt length_constraint() const override
471  {
472  // For now, there is no need for implementing that as `constraints`
473  // should always be called on these functions
475  }
476 };
477 
478 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
string_builtin_functiont::string_builtin_functiont
string_builtin_functiont(exprt return_code)
Definition: string_builtin_function.h:67
string_builtin_functiont::maybe_testing_function
virtual bool maybe_testing_function() const
Tells whether the builtin function can be a testing function, that is a function that does not return...
Definition: string_builtin_function.h:58
string_concat_char_builtin_functiont::constraints
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
Definition: string_builtin_function.cpp:196
string_creation_builtin_functiont::maybe_testing_function
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
Definition: string_builtin_function.h:378
string_of_int_builtin_functiont::radix
exprt radix
Definition: string_builtin_function.h:415
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
string_concatenation_builtin_functiont::string_concatenation_builtin_functiont
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.
Definition: string_builtin_function.cpp:52
string_test_builtin_functiont::result
exprt result
Definition: string_builtin_function.h:422
string_insertion_builtin_functiont
String inserting a string into another one.
Definition: string_builtin_function.h:271
string_builtin_functiont::~string_builtin_functiont
virtual ~string_builtin_functiont()=default
string_builtin_functiont::string_builtin_functiont
string_builtin_functiont()=default
string_to_lower_case_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:205
string_to_lower_case_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.h:213
string_builtin_function_with_no_evalt::name
std::string name() const override
Definition: string_builtin_function.h:448
string_insertion_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.cpp:508
string_to_upper_case_builtin_functiont::constraints
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
Definition: string_builtin_function.cpp:422
array_poolt
Correspondance between arrays and pointers string representations.
Definition: string_constraint_generator.h:49
optional.h
string_builtin_functiont::return_code
exprt return_code
Definition: string_builtin_function.h:53
string_insertion_builtin_functiont::maybe_testing_function
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
Definition: string_builtin_function.h:318
string_transformation_builtin_functiont
String builtin_function transforming one string into another.
Definition: string_builtin_function.h:74
string_of_int_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.cpp:575
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:133
and_exprt
Boolean AND.
Definition: std_expr.h:2409
string_set_char_builtin_functiont::position
exprt position
Definition: string_builtin_function.h:154
string_to_lower_case_builtin_functiont::string_to_lower_case_builtin_functiont
string_to_lower_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Definition: string_builtin_function.h:194
string_builtin_function_with_no_evalt::function_application
function_application_exprt function_application
Definition: string_builtin_function.h:438
string_creation_builtin_functiont
String creation from other types.
Definition: string_builtin_function.h:362
exprt
Base class for all expressions.
Definition: expr.h:54
string_builtin_function_with_no_evalt::string_args
std::vector< array_string_exprt > string_args
Definition: string_builtin_function.h:440
string_to_upper_case_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:396
string_concat_char_builtin_functiont::string_concat_char_builtin_functiont
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.
Definition: string_builtin_function.h:125
string_of_int_builtin_functiont::string_of_int_builtin_functiont
string_of_int_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Definition: string_builtin_function.h:388
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:108
string_builtin_function_with_no_evalt::args
std::vector< exprt > args
Definition: string_builtin_function.h:441
string_to_lower_case_builtin_functiont
Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowerc...
Definition: string_builtin_function.h:190
string_builtin_functiont::string_result
virtual optionalt< array_string_exprt > string_result() const
Definition: string_builtin_function.h:25
string_transformation_builtin_functiont::string_transformation_builtin_functiont
string_transformation_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input)
Definition: string_builtin_function.h:80
string_to_lower_case_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:301
string_insertion_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:308
equal_exprt
Equality.
Definition: std_expr.h:1484
string_builtin_functiont::constraints
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...
string_builtin_functiont::string_arguments
virtual std::vector< array_string_exprt > string_arguments() const
Definition: string_builtin_function.h:30
string_constraint_generatort
Definition: string_constraint_generator.h:120
string_set_char_builtin_functiont::string_set_char_builtin_functiont
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.
Definition: string_builtin_function.h:161
string_insertion_builtin_functiont::input1
array_string_exprt input1
Definition: string_builtin_function.h:275
string_concat_char_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:138
string_insertion_builtin_functiont::eval
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.
Definition: string_builtin_function.cpp:443
string_concatenation_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.cpp:159
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
string_concat_char_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.cpp:215
string_transformation_builtin_functiont::input
array_string_exprt input
Definition: string_builtin_function.h:78
string_insertion_builtin_functiont::result
array_string_exprt result
Definition: string_builtin_function.h:274
symbol_generatort
Generation of fresh symbols of a given type.
Definition: string_constraint_generator.h:32
string_builtin_function_with_no_evalt
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
Definition: string_builtin_function.h:435
string_to_upper_case_builtin_functiont
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
Definition: string_builtin_function.h:223
string_set_char_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:175
string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
Definition: string_builtin_function.cpp:604
string_insertion_builtin_functiont::constraints
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...
Definition: string_builtin_function.cpp:493
string_insertion_builtin_functiont::string_result
optionalt< array_string_exprt > string_result() const override
Definition: string_builtin_function.h:290
string_set_char_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.cpp:275
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
string_test_builtin_functiont::args
std::vector< exprt > args
Definition: string_builtin_function.h:424
string_concatenation_builtin_functiont
Definition: string_builtin_function.h:330
string_insertion_builtin_functiont::string_insertion_builtin_functiont
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.
Definition: string_builtin_function.cpp:36
string_builtin_function_with_no_evalt::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.h:470
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
string_test_builtin_functiont::string_arguments
std::vector< array_string_exprt > string_arguments() const override
Definition: string_builtin_function.h:425
string_insertion_builtin_functiont::string_insertion_builtin_functiont
string_insertion_builtin_functiont(const exprt &return_code)
Definition: string_builtin_function.h:324
string_test_builtin_functiont::under_test
std::vector< array_string_exprt > under_test
Definition: string_builtin_function.h:423
function_application_exprt
Application of (mathematical) function.
Definition: std_expr.h:4481
string_concat_char_builtin_functiont::character
exprt character
Definition: string_builtin_function.h:119
string_of_int_builtin_functiont
String creation from integer types.
Definition: string_builtin_function.h:385
string_builtin_function_with_no_evalt::constraints
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...
Definition: string_builtin_function.cpp:634
string_to_upper_case_builtin_functiont::constraints
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...
Definition: string_builtin_function.h:257
string_concat_char_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:169
string_builtin_function_with_no_evalt::string_result
optionalt< array_string_exprt > string_result() const override
Definition: string_builtin_function.h:456
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
string_builtin_functiont
Base class for string functions that are built in the solver.
Definition: string_builtin_function.h:19
string_transformation_builtin_functiont::string_arguments
std::vector< array_string_exprt > string_arguments() const override
Definition: string_builtin_function.h:104
string_transformation_builtin_functiont::string_result
optionalt< array_string_exprt > string_result() const override
Definition: string_builtin_function.h:100
string_builtin_functiont::eval
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_concatenation_builtin_functiont::constraints
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...
Definition: string_builtin_function.cpp:140
string_of_int_builtin_functiont::constraints
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...
Definition: string_builtin_function.cpp:566
string_to_upper_case_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:249
string_of_int_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:404
string_set_char_builtin_functiont
Setting a character at a particular position of a string.
Definition: string_builtin_function.h:150
string_builtin_function_with_no_evalt::string_res
optionalt< array_string_exprt > string_res
Definition: string_builtin_function.h:439
string_concatenation_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:350
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:497
string_creation_builtin_functiont::result
array_string_exprt result
Definition: string_builtin_function.h:365
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
string_concat_char_builtin_functiont
Adding a character at the end of a string.
Definition: string_builtin_function.h:115
string_creation_builtin_functiont::arg
exprt arg
Definition: string_builtin_function.h:366
array_string_exprt::length
exprt & length()
Definition: string_expr.h:70
string_builtin_functiont::length_constraint
virtual exprt length_constraint() const =0
Constraint ensuring that the length of the strings are coherent with the function call.
string_transformation_builtin_functiont::maybe_testing_function
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
Definition: string_builtin_function.h:108
string_set_char_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:220
function_application_exprt::function
symbol_exprt & function()
Definition: std_expr.h:4496
string_builtin_functiont::name
virtual std::string name() const =0
string_insertion_builtin_functiont::input2
array_string_exprt input2
Definition: string_builtin_function.h:276
string_test_builtin_functiont
String test.
Definition: string_builtin_function.h:419
string_set_char_builtin_functiont::character
exprt character
Definition: string_builtin_function.h:155
string_insertion_builtin_functiont::args
std::vector< exprt > args
Definition: string_builtin_function.h:277
string_to_upper_case_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.h:262
string_to_upper_case_builtin_functiont::string_to_upper_case_builtin_functiont
string_to_upper_case_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input)
Definition: string_builtin_function.h:235
string_concatenation_builtin_functiont::eval
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.
Definition: string_builtin_function.cpp:119
string_to_upper_case_builtin_functiont::string_to_upper_case_builtin_functiont
string_to_upper_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Definition: string_builtin_function.h:227
string_constraint_generator.h
string_expr.h
string_insertion_builtin_functiont::string_arguments
std::vector< array_string_exprt > string_arguments() const override
Definition: string_builtin_function.h:294
string_creation_builtin_functiont::string_result
optionalt< array_string_exprt > string_result() const override
Definition: string_builtin_function.h:373
string_transformation_builtin_functiont::result
array_string_exprt result
Definition: string_builtin_function.h:77
array_string_exprt
Definition: string_expr.h:67
string_builtin_function_with_no_evalt::eval
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 ...
Definition: string_builtin_function.h:462
string_to_lower_case_builtin_functiont::constraints
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
Definition: string_builtin_function.cpp:369
string_builtin_function_with_no_evalt::string_arguments
std::vector< array_string_exprt > string_arguments() const override
Definition: string_builtin_function.h:452
string_creation_builtin_functiont::string_creation_builtin_functiont
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.
Definition: string_builtin_function.cpp:522
string_set_char_builtin_functiont::constraints
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 ...
Definition: string_builtin_function.cpp:245
string_of_int_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:533