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 
8 
10 #include <util/optional.h>
11 #include <util/string_expr.h>
12 
13 #include <vector>
14 
15 #define CHARACTER_FOR_UNKNOWN '?'
16 
73 {
74 public:
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 
121 protected:
123 
126  {
127  }
128 };
129 
132 {
133 public:
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 {
176 public:
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 {
211 public:
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 {
251 public:
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(
274  equal_exprt(
278  };
279 };
280 
285 {
286 public:
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),
304  array_pool)
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(
327  equal_exprt(
331  };
332 };
333 
336 {
337 public:
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 {
360 public:
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 
387 private:
389 };
390 
393 {
394 public:
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 {
410 public:
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  {
423  PRECONDITION(function_application.function().id() == ID_symbol);
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:1920
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:407
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 ...
virtual std::vector< array_string_exprt > string_arguments() const
string_builtin_functiont(const string_builtin_functiont &)=delete
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 optionalt< array_string_exprt > string_result() const
virtual std::string name() const =0
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.
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_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:49
API to expression classes for 'mathematical' expressions.
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,...