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 
16 {
17 public:
19  virtual ~string_builtin_functiont() = default;
20 
22  {
23  return {};
24  }
25 
26  virtual std::vector<array_string_exprt> string_arguments() const
27  {
28  return {};
29  }
30 
31  virtual optionalt<exprt>
32  eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
33 
34  virtual std::string name() const = 0;
35 
38  virtual exprt
39  add_constraints(string_constraint_generatort &constraint_generator) const = 0;
40 
43  virtual exprt length_constraint() const = 0;
44 
46 
50  virtual bool maybe_testing_function() const
51  {
52  return true;
53  }
54 
55 private:
56  string_builtin_functiont() = default;
57 
58 protected:
61  {
62  }
63 };
64 
67 {
68 public:
71  std::vector<exprt> args;
72 
79  const exprt &return_code,
80  const std::vector<exprt> &fun_args,
81  array_poolt &array_pool);
82 
84  {
85  return result;
86  }
87  std::vector<array_string_exprt> string_arguments() const override
88  {
89  return {input};
90  }
91 
93  virtual std::vector<mp_integer> eval(
94  const std::vector<mp_integer> &input_value,
95  const std::vector<mp_integer> &args_value) const = 0;
96 
98  eval(const std::function<exprt(const exprt &)> &get_value) const override;
99 
100  bool maybe_testing_function() const override
101  {
102  return false;
103  }
104 };
105 
109 {
110 public:
116  const exprt &return_code,
117  const std::vector<exprt> &fun_args,
118  array_poolt &array_pool)
120  {
121  }
122 
123  std::vector<mp_integer> eval(
124  const std::vector<mp_integer> &input_value,
125  const std::vector<mp_integer> &args_value) const override;
126 
127  std::string name() const override
128  {
129  return "concat_char";
130  }
131 
133  {
134  return generator.add_axioms_for_concat_char(result, input, args[0]);
135  }
136 
137  exprt length_constraint() const override
138  {
140  }
141 };
142 
145 {
146 public:
150  std::vector<exprt> args;
151 
159  const exprt &return_code,
160  const std::vector<exprt> &fun_args,
161  array_poolt &array_pool);
162 
164  {
165  return result;
166  }
167  std::vector<array_string_exprt> string_arguments() const override
168  {
169  return {input1, input2};
170  }
171 
173  virtual std::vector<mp_integer> eval(
174  const std::vector<mp_integer> &input1_value,
175  const std::vector<mp_integer> &input2_value,
176  const std::vector<mp_integer> &args_value) const;
177 
179  eval(const std::function<exprt(const exprt &)> &get_value) const override;
180 
181  std::string name() const override
182  {
183  return "insert";
184  }
185 
187  {
188  if(args.size() == 1)
189  return generator.add_axioms_for_insert(result, input1, input2, args[0]);
190  if(args.size() == 3)
192  UNREACHABLE;
193  };
194 
195  exprt length_constraint() const override
196  {
197  if(args.size() == 1)
199  if(args.size() == 3)
201  UNREACHABLE;
202  };
203 
204  bool maybe_testing_function() const override
205  {
206  return false;
207  }
208 
209 protected:
212  {
213  }
214 };
215 
218 {
219 public:
227  const exprt &return_code,
228  const std::vector<exprt> &fun_args,
229  array_poolt &array_pool);
230 
231  std::vector<mp_integer> eval(
232  const std::vector<mp_integer> &input1_value,
233  const std::vector<mp_integer> &input2_value,
234  const std::vector<mp_integer> &args_value) const override;
235 
236  std::string name() const override
237  {
238  return "concat";
239  }
240 
242  {
243  if(args.size() == 0)
244  return generator.add_axioms_for_concat(result, input1, input2);
245  if(args.size() == 2)
246  return generator.add_axioms_for_concat_substr(
247  result, input1, input2, args[0], args[1]);
248  UNREACHABLE;
249  };
250 
251  exprt length_constraint() const override
252  {
253  if(args.size() == 0)
255  if(args.size() == 2)
257  result, input1, input2, args[0], args[1]);
258  UNREACHABLE;
259  }
260 };
261 
264 {
265 public:
267  std::vector<exprt> args;
269 
271  {
272  return result;
273  }
274 
275  bool maybe_testing_function() const override
276  {
277  return false;
278  }
279 };
280 
283 {
284 public:
286  std::vector<array_string_exprt> under_test;
287  std::vector<exprt> args;
288  std::vector<array_string_exprt> string_arguments() const override
289  {
290  return under_test;
291  }
292 };
293 
299 {
300 public:
303  std::vector<array_string_exprt> string_args;
304  std::vector<exprt> args;
305 
307  const exprt &return_code,
309  array_poolt &array_pool);
310 
311  std::string name() const override
312  {
314  }
315  std::vector<array_string_exprt> string_arguments() const override
316  {
317  return std::vector<array_string_exprt>(string_args);
318  }
320  {
321  return string_res;
322  }
323 
325  eval(const std::function<exprt(const exprt &)> &get_value) const override
326  {
327  return {};
328  }
329 
331  {
333  };
334 
335  exprt length_constraint() const override
336  {
337  // For now, there is no need for implementing that as `add_constraints`
338  // should always be called on these functions
340  }
341 };
342 
343 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
std::vector< array_string_exprt > string_arguments() const override
string_builtin_functiont()=default
exprt add_axioms_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset...
Adding a character at the end of a string.
Generates string constraints to link results from string functions with their arguments.
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.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
application of (mathematical) function
Definition: std_expr.h:4531
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
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.
function_application_exprt function_application
std::vector< array_string_exprt > under_test
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.
std::vector< array_string_exprt > string_arguments() const override
virtual ~string_builtin_functiont()=default
std::vector< array_string_exprt > string_arguments() const override
const irep_idt & get_identifier() const
Definition: std_expr.h:128
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
virtual optionalt< array_string_exprt > string_result() const
String inserting a string into another one.
std::vector< array_string_exprt > string_args
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.
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
string_builtin_functiont(const exprt &return_code)
String creation from other types.
exprt add_axioms_for_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms...
virtual exprt length_constraint() const =0
Constraint ensuring that the length of the strings are coherent with the function call...
virtual std::vector< array_string_exprt > string_arguments() const
String builtin_function transforming one string into another.
optionalt< array_string_exprt > string_result() const override
virtual std::vector< mp_integer > eval(const std::vector< mp_integer > &input_value, const std::vector< mp_integer > &args_value) const =0
Evaluate the result from a concrete valuation of the arguments.
exprt add_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
optionalt< array_string_exprt > string_result() const override
string_insertion_builtin_functiont(const exprt &return_code)
nonstd::optional< T > optionalt
Definition: optional.h:35
std::vector< mp_integer > eval(const std::vector< mp_integer > &input_value, const std::vector< mp_integer > &args_value) const override
Evaluate the result from a concrete valuation of the arguments.
virtual exprt add_constraints(string_constraint_generatort &constraint_generator) const =0
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
exprt length_constraint_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 ...
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
virtual optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const =0
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...
optionalt< array_string_exprt > string_result() const override
exprt length_constraint_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the length of res corresponds that of s1 where we inserted s2 at position offset...
exprt add_axioms_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index â...
exprt length_constraint_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
symbol_exprt & function()
Definition: std_expr.h:4552
string_transformation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
String expressions for the string solver.
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
#define UNIMPLEMENTED
Definition: invariant.h:266
Base class for all expressions.
Definition: expr.h:42
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
optionalt< array_string_exprt > string_res
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
#define UNREACHABLE
Definition: invariant.h:250
optionalt< array_string_exprt > string_result() const override
Functions that are not yet supported in this class but are supported by string_constraint_generatort...
exprt add_axioms_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, const exprt &c)
Add axioms enforcing that res is the concatenation of s1 with character c.
virtual bool maybe_testing_function() const
Tells whether the builtin function can be a testing function, that is a function that does not return...
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.
virtual std::string name() const =0
exprt add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.