cprover
string_constraint_generator_float.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for functions generating strings
4  from other types, in particular int, long, float, double, char, bool
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
13 
15 
17 
18 
28  const exprt &src, const ieee_float_spect &spec)
29 {
30  const extractbits_exprt exp_bits(
31  src, spec.f + spec.e - 1, spec.f, unsignedbv_typet(spec.e));
32 
33  // Exponent is in biased form (numbers from -128 to 127 are encoded with
34  // integer from 0 to 255) we have to remove the bias.
35  return minus_exprt(
36  typecast_exprt(exp_bits, signedbv_typet(32)),
37  from_integer(spec.bias(), signedbv_typet(32)));
38 }
39 
44 exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
45 {
46  return extractbits_exprt(src, spec.f-1, 0, unsignedbv_typet(spec.f));
47 }
48 
60  const exprt &src, const ieee_float_spect &spec, const typet &type)
61 {
62  PRECONDITION(type.id()==ID_unsignedbv);
63  PRECONDITION(to_unsignedbv_type(type).get_width()>spec.f);
64  typecast_exprt fraction(get_fraction(src, spec), type);
65  exprt exponent=get_exponent(src, spec);
66  equal_exprt all_zeros(exponent, from_integer(0, exponent.type()));
67  exprt hidden_bit=from_integer((1 << spec.f), type);
68  bitor_exprt with_hidden_bit(fraction, hidden_bit);
69  return if_exprt(all_zeros, fraction, with_hidden_bit);
70 }
71 
76 exprt constant_float(const double f, const ieee_float_spect &float_spec)
77 {
78  ieee_floatt fl(float_spec);
79  if(float_spec==ieee_float_spect::single_precision())
80  fl.from_float(f);
81  else if(float_spec==ieee_float_spect::double_precision())
82  fl.from_double(f);
83  else
85  return fl.to_expr();
86 }
87 
92 {
94  return floatbv_typecast_exprt(f, rounding, signedbv_typet(32));
95 }
96 
102 exprt floatbv_mult(const exprt &f, const exprt &g)
103 {
104  PRECONDITION(f.type()==g.type());
106  exprt mult(ID_floatbv_mult, f.type());
107  mult.copy_to_operands(f);
108  mult.copy_to_operands(g);
109  mult.copy_to_operands(from_integer(rounding, unsignedbv_typet(32)));
110  return mult;
111 }
112 
120 {
122  return floatbv_typecast_exprt(i, rounding, spec.to_type());
123 }
124 
138 {
139  exprt log_10_of_2=constant_float(0.30102999566398119521373889472449302, spec);
140  exprt bin_exp=get_exponent(f, spec);
141  exprt float_bin_exp=floatbv_of_int_expr(bin_exp, spec);
142  exprt dec_exp=floatbv_mult(float_bin_exp, log_10_of_2);
143  binary_relation_exprt negative_exp(dec_exp, ID_lt, constant_float(0.0, spec));
144  // Rounding to zero is not correct for negative numbers, so we substract 1.
145  minus_exprt dec_minus_one(dec_exp, constant_float(1.0, spec));
146  if_exprt adjust_for_neg(negative_exp, dec_minus_one, dec_exp);
147  return round_expr_to_zero(adjust_for_neg);
148 }
149 
158 std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
159  symbol_generatort &fresh_symbol,
161  array_poolt &array_pool,
162  const namespacet &ns)
163 {
164  PRECONDITION(f.arguments().size() == 3);
165  array_string_exprt res =
166  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
168  fresh_symbol, res, f.arguments()[2], array_pool, ns);
169 }
170 
177 std::pair<exprt, string_constraintst> add_axioms_from_double(
178  symbol_generatort &fresh_symbol,
180  array_poolt &array_pool,
181  const namespacet &ns)
182 {
183  return add_axioms_for_string_of_float(fresh_symbol, f, array_pool, ns);
184 }
185 
201 std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
202  symbol_generatort &fresh_symbol,
203  const array_string_exprt &res,
204  const exprt &f,
205  array_poolt &array_pool,
206  const namespacet &ns)
207 {
208  const floatbv_typet &type=to_floatbv_type(f.type());
209  const ieee_float_spect float_spec(type);
210  const typet &char_type = res.content().type().subtype();
211  const typet &index_type = res.length().type();
212 
213  // We will look at the first 5 digits of the fractional part.
214  // shifted is floor(f * 1e5)
215  const exprt shifting = constant_float(1e5, float_spec);
216  const exprt shifted = round_expr_to_zero(floatbv_mult(f, shifting));
217  // Numbers with greater or equal value to the following, should use
218  // the exponent notation.
219  const exprt max_non_exponent_notation = from_integer(100000, shifted.type());
220  // fractional_part is floor(f * 100000) % 100000
221  const mod_exprt fractional_part(shifted, max_non_exponent_notation);
222  const array_string_exprt fractional_part_str =
223  array_pool.fresh_string(index_type, char_type);
224  auto result1 =
225  add_axioms_for_fractional_part(fractional_part_str, fractional_part, 6);
226 
227  // The axiom added to convert to integer should always be satisfiable even
228  // when the preconditions are not satisfied.
229  const mod_exprt integer_part(
230  round_expr_to_zero(f), max_non_exponent_notation);
231  // We should not need more than 8 characters to represent the integer
232  // part of the float.
233  const array_string_exprt integer_part_str =
234  array_pool.fresh_string(index_type, char_type);
235  auto result2 =
236  add_axioms_for_string_of_int(integer_part_str, integer_part, 8, ns);
237 
238  auto result3 = add_axioms_for_concat(
239  fresh_symbol, res, integer_part_str, fractional_part_str);
240  merge(result3.second, std::move(result1.second));
241  merge(result3.second, std::move(result2.second));
242 
243  const auto return_code =
244  maximum(result1.first, maximum(result2.first, result3.first));
245  return {return_code, std::move(result3.second)};
246 }
247 
255 std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
256  const array_string_exprt &res,
257  const exprt &int_expr,
258  size_t max_size)
259 {
260  PRECONDITION(int_expr.type().id()==ID_signedbv);
261  PRECONDITION(max_size>=2);
262  string_constraintst constraints;
263  const typet &type=int_expr.type();
264  const typet &char_type = res.content().type().subtype();
265  const typet &index_type = res.length().type();
266  const exprt ten = from_integer(10, type);
267  const exprt zero_char = from_integer('0', char_type);
268  const exprt nine_char = from_integer('9', char_type);
269  const exprt max = from_integer(max_size, index_type);
270 
271  // We add axioms:
272  // a1 : 2 <= |res| <= max_size
273  // a2 : starts_with_dot && no_trailing_zero && is_number
274  // starts_with_dot: res[0] = '.'
275  // is_number: forall i:[1, max_size[. '0' < res[i] < '9'
276  // no_trailing_zero: forall j:[2, max_size[. !(|res| = j+1 && res[j] = '0')
277  // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0)
278 
279  const and_exprt a1(length_gt(res, 1), length_le(res, max));
280  constraints.existential.push_back(a1);
281 
282  equal_exprt starts_with_dot(res[0], from_integer('.', char_type));
283 
284  exprt::operandst digit_constraints;
285  digit_constraints.push_back(starts_with_dot);
286  exprt sum=from_integer(0, type);
287 
288  for(size_t j=1; j<max_size; j++)
289  {
290  // after_end is |res| <= j
291  binary_relation_exprt after_end(
292  res.length(), ID_le, from_integer(j, res.length().type()));
293  mult_exprt ten_sum(sum, ten);
294 
295  // sum = 10 * sum + after_end ? 0 : (res[j]-'0')
296  if_exprt to_add(
297  after_end,
298  from_integer(0, type),
299  typecast_exprt(minus_exprt(res[j], zero_char), type));
300  sum=plus_exprt(ten_sum, to_add);
301 
303  binary_relation_exprt(res[j], ID_ge, zero_char),
304  binary_relation_exprt(res[j], ID_le, nine_char));
305  digit_constraints.push_back(is_number);
306 
307  // There are no trailing zeros except for ".0" (i.e j=2)
308  if(j>1)
309  {
310  not_exprt no_trailing_zero(and_exprt(
311  equal_exprt(res.length(), from_integer(j+1, res.length().type())),
312  equal_exprt(res[j], zero_char)));
313  digit_constraints.push_back(no_trailing_zero);
314  }
315  }
316 
317  exprt a2=conjunction(digit_constraints);
318  constraints.existential.push_back(a2);
319 
320  equal_exprt a3(int_expr, sum);
321  constraints.existential.push_back(a3);
322 
323  return {from_integer(0, signedbv_typet(32)), std::move(constraints)};
324 }
325 
344 std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
345  symbol_generatort &fresh_symbol,
346  const array_string_exprt &res,
347  const exprt &f,
348  array_poolt &array_pool,
349  const namespacet &ns)
350 {
351  string_constraintst constraints;
353  const typet float_type = float_spec.to_type();
354  const signedbv_typet int_type(32);
355  const typet &index_type = res.length().type();
356  const typet &char_type = res.content().type().subtype();
357 
358  // This is used for rounding float to integers.
359  exprt round_to_zero_expr=from_integer(ieee_floatt::ROUND_TO_ZERO, int_type);
360 
361  // `bin_exponent` is $e$ in the formulas
362  exprt bin_exponent=get_exponent(f, float_spec);
363 
364  // $m$ from the formula is a value between 0.0 and 2.0 represented
365  // with values in the range 0x000000 0xFFFFFF so 1 corresponds to 0x800000.
366  // `bin_significand_int` represents $m * 0x800000$
367  exprt bin_significand_int=
368  get_significand(f, float_spec, unsignedbv_typet(32));
369  // `bin_significand` represents $m$ and is obtained
370  // by multiplying `binary_significand_as_int` by
371  // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7
372  exprt bin_significand=floatbv_mult(
373  floatbv_typecast_exprt(bin_significand_int, round_to_zero_expr, float_type),
374  constant_float(1.1920928955078125e-7, float_spec));
375 
376  // This is a first approximation of the exponent that will adjust
377  // if the fraction we get is greater than 10
378  exprt dec_exponent_estimate=estimate_decimal_exponent(f, float_spec);
379 
380  // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128]
381  std::vector<double> two_power_e_over_ten_power_d_table(
382  { 1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28, 2.56,
383  5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768, 6.5536,
384  1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861, 1.67772,
385  3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748, 4.29497,
386  8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756, 1.09951,
387  2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737, 2.81475,
388  5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288, 7.20576,
389  1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337, 1.84467,
390  3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118, 4.72237,
391  9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463, 1.20893,
392  2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743, 3.09485,
393  6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141, 7.92282,
394  1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412, 2.02824,
395  4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615, 5.1923,
396  1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614, 1.32923,
397  2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141});
398 
399  // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[-128,-1]
400  std::vector<double> two_power_e_over_ten_power_d_table_negatives(
401  { 2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158,
402  7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965,
403  1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519,
404  4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089,
405  1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559,
406  3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590,
407  8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879,
408  2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051,
409  5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889,
410  1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636,
411  3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747,
412  9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415,
413  2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023,
414  5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939,
415  1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313,
416  3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5});
417 
418  // bias_table used to find the bias factor
419  exprt conversion_factor_table_size=from_integer(
420  two_power_e_over_ten_power_d_table_negatives.size()+
421  two_power_e_over_ten_power_d_table.size(),
422  int_type);
423  array_exprt conversion_factor_table(
424  array_typet(float_type, conversion_factor_table_size));
425  for(const auto &f : two_power_e_over_ten_power_d_table_negatives)
426  conversion_factor_table.copy_to_operands(constant_float(f, float_spec));
427  for(const auto &f : two_power_e_over_ten_power_d_table)
428  conversion_factor_table.copy_to_operands(constant_float(f, float_spec));
429 
430  // The index in the table, corresponding to exponent e is e+128
431  plus_exprt shifted_index(bin_exponent, from_integer(128, int_type));
432 
433  // bias_factor is $2^e / 10^(floor(log_10(2)*e))$ that is $2^e/10^d$
434  index_exprt conversion_factor(
435  conversion_factor_table, shifted_index, float_type);
436 
437  // `dec_significand` is $n = m * bias_factor$
438  exprt dec_significand=floatbv_mult(conversion_factor, bin_significand);
439  exprt dec_significand_int=round_expr_to_zero(dec_significand);
440 
441  // `dec_exponent` is $d$ in the formulas
442  // it is obtained from the approximation, checking whether it is not too small
443  binary_relation_exprt estimate_too_small(
444  dec_significand_int, ID_ge, from_integer(10, int_type));
445  if_exprt decimal_exponent(
446  estimate_too_small,
447  plus_exprt(dec_exponent_estimate, from_integer(1, int_type)),
448  dec_exponent_estimate);
449 
450  // `dec_significand` is divided by 10 if it exceeds 10
451  dec_significand=if_exprt(
452  estimate_too_small,
453  floatbv_mult(dec_significand, constant_float(0.1, float_spec)),
454  dec_significand);
455  dec_significand_int=round_expr_to_zero(dec_significand);
456  array_string_exprt string_expr_integer_part =
457  array_pool.fresh_string(index_type, char_type);
458  auto result1 = add_axioms_for_string_of_int(
459  string_expr_integer_part, dec_significand_int, 3, ns);
460  minus_exprt fractional_part(
461  dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec));
462 
463  // shifted_float is floor(f * 1e5)
464  exprt shifting=constant_float(1e5, float_spec);
465  exprt shifted_float=
466  round_expr_to_zero(floatbv_mult(fractional_part, shifting));
467 
468  // Numbers with greater or equal value to the following, should use
469  // the exponent notation.
470  exprt max_non_exponent_notation=from_integer(100000, shifted_float.type());
471 
472  // fractional_part_shifted is floor(f * 100000) % 100000
473  const mod_exprt fractional_part_shifted(
474  shifted_float, max_non_exponent_notation);
475 
476  array_string_exprt string_fractional_part =
477  array_pool.fresh_string(index_type, char_type);
478  auto result2 = add_axioms_for_fractional_part(
479  string_fractional_part, fractional_part_shifted, 6);
480 
481  // string_expr_with_fractional_part =
482  // concat(string_with_do, string_fractional_part)
483  const array_string_exprt string_expr_with_fractional_part =
484  array_pool.fresh_string(index_type, char_type);
485  auto result3 = add_axioms_for_concat(
486  fresh_symbol,
487  string_expr_with_fractional_part,
488  string_expr_integer_part,
489  string_fractional_part);
490 
491  // string_expr_with_E = concat(string_fraction, string_lit_E)
492  const array_string_exprt stringE =
493  array_pool.fresh_string(index_type, char_type);
494  auto result4 = add_axioms_for_constant(stringE, "E");
495  const array_string_exprt string_expr_with_E =
496  array_pool.fresh_string(index_type, char_type);
497  auto result5 = add_axioms_for_concat(
498  fresh_symbol,
499  string_expr_with_E,
500  string_expr_with_fractional_part,
501  stringE);
502 
503  // exponent_string = string_of_int(decimal_exponent)
504  const array_string_exprt exponent_string =
505  array_pool.fresh_string(index_type, char_type);
506  auto result6 =
507  add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3, ns);
508 
509  // string_expr = concat(string_expr_with_E, exponent_string)
510  auto result7 = add_axioms_for_concat(
511  fresh_symbol, res, string_expr_with_E, exponent_string);
512 
513  const exprt return_code = maximum(
514  result1.first,
515  maximum(
516  result2.first,
517  maximum(
518  result3.first,
519  maximum(
520  result4.first,
521  maximum(result5.first, maximum(result6.first, result7.first))))));
522  merge(result7.second, std::move(result1.second));
523  merge(result7.second, std::move(result2.second));
524  merge(result7.second, std::move(result3.second));
525  merge(result7.second, std::move(result4.second));
526  merge(result7.second, std::move(result5.second));
527  merge(result7.second, std::move(result6.second));
528  return {return_code, std::move(result7.second)};
529 }
530 
540 std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
541  symbol_generatort &fresh_symbol,
543  array_poolt &array_pool,
544  const namespacet &ns)
545 {
546  PRECONDITION(f.arguments().size() == 3);
547  const array_string_exprt res =
548  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
549  const exprt &arg = f.arguments()[2];
551  fresh_symbol, res, arg, array_pool, ns);
552 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
function_application_exprt::arguments
argumentst & arguments()
Definition: std_expr.h:4506
ieee_floatt
Definition: ieee_float.h:119
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
add_axioms_for_fractional_part
std::pair< exprt, string_constraintst > add_axioms_for_fractional_part(const array_string_exprt &res, const exprt &int_expr, size_t max_size)
Add axioms for representing the fractional part of a floating point starting with a dot.
Definition: string_constraint_generator_float.cpp:255
estimate_decimal_exponent
exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec)
Estimate the decimal exponent that should be used to represent a given floating point value in decima...
Definition: string_constraint_generator_float.cpp:137
typet::subtype
const typet & subtype() const
Definition: type.h:38
conjunction
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:50
add_axioms_from_float_scientific_notation
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms to write the float in scientific notation.
Definition: string_constraint_generator_float.cpp:344
is_number
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Definition: mathematical_types.cpp:17
constant_float
exprt constant_float(const double f, const ieee_float_spect &float_spec)
Create an expression to represent a float or double value.
Definition: string_constraint_generator_float.cpp:76
add_axioms_for_string_of_float
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
String representation of a float value.
Definition: string_constraint_generator_float.cpp:158
typet
The type of an expression, extends irept.
Definition: type.h:27
array_poolt
Correspondance between arrays and pointers string representations.
Definition: string_constraint_generator.h:49
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1398
length_gt
binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
Definition: string_expr.h:28
and_exprt
Boolean AND.
Definition: std_expr.h:2409
round_expr_to_zero
exprt round_expr_to_zero(const exprt &f)
Round a float expression to an integer closer to 0.
Definition: string_constraint_generator_float.cpp:91
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt
Base class for all expressions.
Definition: expr.h:54
floatbv_of_int_expr
exprt floatbv_of_int_expr(const exprt &i, const ieee_float_spect &spec)
Convert integers to floating point to be used in operations with other values that are in floating po...
Definition: string_constraint_generator_float.cpp:119
char_array_of_pointer
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Definition: string_constraint_generator_main.cpp:325
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:108
array_string_exprt::content
exprt & content()
Definition: string_expr.h:80
add_axioms_for_constant
std::pair< exprt, string_constraintst > add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
Definition: string_constraint_generator_constants.cpp:24
get_fraction
exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
Gets the fraction without hidden bit.
Definition: string_constraint_generator_float.cpp:44
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
ieee_floatt::from_float
void from_float(const float f)
Definition: ieee_float.cpp:1114
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
merge
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Definition: string_constraint_generator_main.cpp:225
ieee_float_spect
Definition: ieee_float.h:25
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
ieee_float_spect::e
std::size_t e
Definition: ieee_float.h:30
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
add_axioms_from_double
std::pair< exprt, string_constraintst > add_axioms_from_double(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms corresponding to the String.valueOf(D) java function.
Definition: string_constraint_generator_float.cpp:177
symbol_generatort
Generation of fresh symbols of a given type.
Definition: string_constraint_generator.h:32
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:583
bitor_exprt
Bit-wise OR.
Definition: std_expr.h:2702
ieee_float_spect::double_precision
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1262
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2336
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1278
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
function_application_exprt
Application of (mathematical) function.
Definition: std_expr.h:4481
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
ieee_floatt::rounding_modet
rounding_modet
Definition: ieee_float.h:125
get_exponent
exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
Gets the unbiased exponent in a floating-point bit-vector.
Definition: string_constraint_generator_float.cpp:27
minus_exprt
Binary minus.
Definition: std_expr.h:1106
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
length_le
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
Definition: string_expr.h:41
get_significand
exprt get_significand(const exprt &src, const ieee_float_spect &spec, const typet &type)
Gets the significand as a java integer, looking for the hidden bit.
Definition: string_constraint_generator_float.cpp:59
floatbv_mult
exprt floatbv_mult(const exprt &f, const exprt &g)
Multiplication of expressions representing floating points.
Definition: string_constraint_generator_float.cpp:102
array_typet
Arrays with given size.
Definition: std_types.h:1000
ieee_floatt::ROUND_TO_EVEN
@ ROUND_TO_EVEN
Definition: ieee_float.h:127
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
array_string_exprt::length
exprt & length()
Definition: string_expr.h:70
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
add_axioms_for_string_of_int
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
Definition: string_constraint_generator_valueof.cpp:132
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
add_axioms_for_concat
std::pair< exprt, string_constraintst > add_axioms_for_concat(symbol_generatort &fresh_symbol, 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.
Definition: string_constraint_generator_concat.cpp:126
ieee_float_spect::bias
mp_integer bias() const
Definition: ieee_float.cpp:21
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3157
float_bv.h
index_exprt
Array index operator.
Definition: std_expr.h:1595
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
string_constraint_generator.h
ieee_float_spect::single_precision
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1739
array_string_exprt
Definition: string_expr.h:67
ieee_floatt::ROUND_TO_ZERO
@ ROUND_TO_ZERO
Definition: ieee_float.h:128
array_poolt::fresh_string
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
Definition: string_constraint_generator_main.cpp:87
mod_exprt
Modulo.
Definition: std_expr.h:1287
ieee_float_spect::f
std::size_t f
Definition: ieee_float.h:30
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:110
not_exprt
Boolean negation.
Definition: std_expr.h:3308
ieee_floatt::from_double
void from_double(const double d)
Definition: ieee_float.cpp:1090