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 
26 exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
27 {
28  const extractbits_exprt exp_bits(
29  src, spec.f + spec.e - 1, spec.f, unsignedbv_typet(spec.e));
30 
31  // Exponent is in biased form (numbers from -128 to 127 are encoded with
32  // integer from 0 to 255) we have to remove the bias.
33  return minus_exprt(
34  typecast_exprt(exp_bits, signedbv_typet(32)),
35  from_integer(spec.bias(), signedbv_typet(32)));
36 }
37 
42 exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
43 {
44  return extractbits_exprt(src, spec.f - 1, 0, unsignedbv_typet(spec.f));
45 }
46 
58  const exprt &src,
59  const ieee_float_spect &spec,
60  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 {
93  exprt rounding =
95  return floatbv_typecast_exprt(f, rounding, signedbv_typet(32));
96 }
97 
103 exprt floatbv_mult(const exprt &f, const exprt &g)
104 {
105  PRECONDITION(f.type() == g.type());
107  exprt mult(ID_floatbv_mult, f.type());
108  mult.copy_to_operands(f);
109  mult.copy_to_operands(g);
110  mult.copy_to_operands(from_integer(rounding, unsignedbv_typet(32)));
111  return mult;
112 }
113 
121 {
122  exprt rounding =
124  return floatbv_typecast_exprt(i, rounding, spec.to_type());
125 }
126 
140 {
141  exprt log_10_of_2 =
142  constant_float(0.30102999566398119521373889472449302, spec);
143  exprt bin_exp = get_exponent(f, spec);
144  exprt float_bin_exp = floatbv_of_int_expr(bin_exp, spec);
145  exprt dec_exp = floatbv_mult(float_bin_exp, log_10_of_2);
146  binary_relation_exprt negative_exp(dec_exp, ID_lt, constant_float(0.0, spec));
147  // Rounding to zero is not correct for negative numbers, so we substract 1.
148  minus_exprt dec_minus_one(dec_exp, constant_float(1.0, spec));
149  if_exprt adjust_for_neg(negative_exp, dec_minus_one, dec_exp);
150  return round_expr_to_zero(adjust_for_neg);
151 }
152 
158 std::pair<exprt, string_constraintst>
161 {
162  PRECONDITION(f.arguments().size() == 3);
163  array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]);
164  return add_axioms_for_string_of_float(res, f.arguments()[2]);
165 }
166 
170 std::pair<exprt, string_constraintst>
173 {
175 }
176 
189 std::pair<exprt, string_constraintst>
191  const array_string_exprt &res,
192  const exprt &f)
193 {
194  const floatbv_typet &type = to_floatbv_type(f.type());
195  const ieee_float_spect float_spec(type);
196  const typet &char_type = res.content().type().subtype();
197  const typet &index_type = res.length_type();
198 
199  // We will look at the first 5 digits of the fractional part.
200  // shifted is floor(f * 1e5)
201  const exprt shifting = constant_float(1e5, float_spec);
202  const exprt shifted = round_expr_to_zero(floatbv_mult(f, shifting));
203  // Numbers with greater or equal value to the following, should use
204  // the exponent notation.
205  const exprt max_non_exponent_notation = from_integer(100000, shifted.type());
206  // fractional_part is floor(f * 100000) % 100000
207  const mod_exprt fractional_part(shifted, max_non_exponent_notation);
208  const array_string_exprt fractional_part_str =
210  auto result1 =
211  add_axioms_for_fractional_part(fractional_part_str, fractional_part, 6);
212 
213  // The axiom added to convert to integer should always be satisfiable even
214  // when the preconditions are not satisfied.
215  const mod_exprt integer_part(
216  round_expr_to_zero(f), max_non_exponent_notation);
217  // We should not need more than 8 characters to represent the integer
218  // part of the float.
219  const array_string_exprt integer_part_str =
221  auto result2 =
222  add_axioms_for_string_of_int(integer_part_str, integer_part, 8);
223 
224  auto result3 =
225  add_axioms_for_concat(res, integer_part_str, fractional_part_str);
226  merge(result3.second, std::move(result1.second));
227  merge(result3.second, std::move(result2.second));
228 
229  const auto return_code =
230  maximum(result1.first, maximum(result2.first, result3.first));
231  return {return_code, std::move(result3.second)};
232 }
233 
241 std::pair<exprt, string_constraintst>
243  const array_string_exprt &res,
244  const exprt &int_expr,
245  size_t max_size)
246 {
247  PRECONDITION(int_expr.type().id() == ID_signedbv);
248  PRECONDITION(max_size >= 2);
249  string_constraintst constraints;
250  const typet &type = int_expr.type();
251  const typet &char_type = res.content().type().subtype();
252  const typet &index_type = res.length_type();
253  const exprt ten = from_integer(10, type);
254  const exprt zero_char = from_integer('0', char_type);
255  const exprt nine_char = from_integer('9', char_type);
256  const exprt max = from_integer(max_size, index_type);
257 
258  // We add axioms:
259  // a1 : 2 <= |res| <= max_size
260  // a2 : starts_with_dot && no_trailing_zero && is_number
261  // starts_with_dot: res[0] = '.'
262  // is_number: forall i:[1, max_size[. '0' < res[i] < '9'
263  // no_trailing_zero: forall j:[2, max_size[. !(|res| = j+1 && res[j] = '0')
264  // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0)
265 
266  const and_exprt a1(
269  constraints.existential.push_back(a1);
270 
271  equal_exprt starts_with_dot(res[0], from_integer('.', char_type));
272 
273  exprt::operandst digit_constraints;
274  digit_constraints.push_back(starts_with_dot);
275  exprt sum = from_integer(0, type);
276 
277  for(size_t j = 1; j < max_size; j++)
278  {
279  // after_end is |res| <= j
280  binary_relation_exprt after_end(
282  ID_le,
283  from_integer(j, res.length_type()));
284  mult_exprt ten_sum(sum, ten);
285 
286  // sum = 10 * sum + after_end ? 0 : (res[j]-'0')
287  if_exprt to_add(
288  after_end,
289  from_integer(0, type),
290  typecast_exprt(minus_exprt(res[j], zero_char), type));
291  sum = plus_exprt(ten_sum, to_add);
292 
294  binary_relation_exprt(res[j], ID_ge, zero_char),
295  binary_relation_exprt(res[j], ID_le, nine_char));
296  digit_constraints.push_back(is_number);
297 
298  // There are no trailing zeros except for ".0" (i.e j=2)
299  if(j > 1)
300  {
301  not_exprt no_trailing_zero(and_exprt(
302  equal_exprt(
304  from_integer(j + 1, res.length_type())),
305  equal_exprt(res[j], zero_char)));
306  digit_constraints.push_back(no_trailing_zero);
307  }
308  }
309 
310  exprt a2 = conjunction(digit_constraints);
311  constraints.existential.push_back(a2);
312 
313  equal_exprt a3(int_expr, sum);
314  constraints.existential.push_back(a3);
315 
316  return {from_integer(0, signedbv_typet(32)), std::move(constraints)};
317 }
318 
334 std::pair<exprt, string_constraintst>
336  const array_string_exprt &res,
337  const exprt &float_expr)
338 {
339  string_constraintst constraints;
341  const typet float_type = float_spec.to_type();
342  const signedbv_typet int_type(32);
343  const typet &index_type = res.length_type();
344  const typet &char_type = res.content().type().subtype();
345 
346  // This is used for rounding float to integers.
347  exprt round_to_zero_expr = from_integer(ieee_floatt::ROUND_TO_ZERO, int_type);
348 
349  // `bin_exponent` is $e$ in the formulas
350  exprt bin_exponent = get_exponent(float_expr, float_spec);
351 
352  // $m$ from the formula is a value between 0.0 and 2.0 represented
353  // with values in the range 0x000000 0xFFFFFF so 1 corresponds to 0x800000.
354  // `bin_significand_int` represents $m * 0x800000$
355  exprt bin_significand_int =
356  get_significand(float_expr, float_spec, unsignedbv_typet(32));
357  // `bin_significand` represents $m$ and is obtained
358  // by multiplying `binary_significand_as_int` by
359  // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7
360  exprt bin_significand = floatbv_mult(
361  floatbv_typecast_exprt(bin_significand_int, round_to_zero_expr, float_type),
362  constant_float(1.1920928955078125e-7, float_spec));
363 
364  // This is a first approximation of the exponent that will adjust
365  // if the fraction we get is greater than 10
366  exprt dec_exponent_estimate =
367  estimate_decimal_exponent(float_expr, float_spec);
368 
369  // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128]
370  std::vector<double> two_power_e_over_ten_power_d_table(
371  {1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28,
372  2.56, 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768,
373  6.5536, 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861,
374  1.67772, 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748,
375  4.29497, 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756,
376  1.09951, 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737,
377  2.81475, 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288,
378  7.20576, 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337,
379  1.84467, 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118,
380  4.72237, 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463,
381  1.20893, 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743,
382  3.09485, 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141,
383  7.92282, 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412,
384  2.02824, 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615,
385  5.1923, 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614,
386  1.32923, 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141});
387 
388  // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[-128,-1]
389  std::vector<double> two_power_e_over_ten_power_d_table_negatives(
390  {2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158,
391  7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965,
392  1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519,
393  4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089,
394  1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559,
395  3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590,
396  8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879,
397  2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051,
398  5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889,
399  1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636,
400  3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747,
401  9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415,
402  2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023,
403  5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939,
404  1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313,
405  3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5});
406 
407  // bias_table used to find the bias factor
408  exprt conversion_factor_table_size = from_integer(
409  two_power_e_over_ten_power_d_table_negatives.size() +
410  two_power_e_over_ten_power_d_table.size(),
411  int_type);
412  array_exprt conversion_factor_table(
413  {}, array_typet(float_type, conversion_factor_table_size));
414  for(const auto &negative : two_power_e_over_ten_power_d_table_negatives)
415  conversion_factor_table.copy_to_operands(
416  constant_float(negative, float_spec));
417  for(const auto &positive : two_power_e_over_ten_power_d_table)
418  conversion_factor_table.copy_to_operands(
419  constant_float(positive, float_spec));
420 
421  // The index in the table, corresponding to exponent e is e+128
422  plus_exprt shifted_index(bin_exponent, from_integer(128, int_type));
423 
424  // bias_factor is $2^e / 10^(floor(log_10(2)*e))$ that is $2^e/10^d$
425  index_exprt conversion_factor(
426  conversion_factor_table, shifted_index, float_type);
427 
428  // `dec_significand` is $n = m * bias_factor$
429  exprt dec_significand = floatbv_mult(conversion_factor, bin_significand);
430  exprt dec_significand_int = round_expr_to_zero(dec_significand);
431 
432  // `dec_exponent` is $d$ in the formulas
433  // it is obtained from the approximation, checking whether it is not too small
434  binary_relation_exprt estimate_too_small(
435  dec_significand_int, ID_ge, from_integer(10, int_type));
436  if_exprt decimal_exponent(
437  estimate_too_small,
438  plus_exprt(dec_exponent_estimate, from_integer(1, int_type)),
439  dec_exponent_estimate);
440 
441  // `dec_significand` is divided by 10 if it exceeds 10
442  dec_significand = if_exprt(
443  estimate_too_small,
444  floatbv_mult(dec_significand, constant_float(0.1, float_spec)),
445  dec_significand);
446  dec_significand_int = round_expr_to_zero(dec_significand);
447  array_string_exprt string_expr_integer_part =
449  auto result1 = add_axioms_for_string_of_int(
450  string_expr_integer_part, dec_significand_int, 3);
451  minus_exprt fractional_part(
452  dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec));
453 
454  // shifted_float is floor(float_expr * 1e5)
455  exprt shifting = constant_float(1e5, float_spec);
456  exprt shifted_float =
457  round_expr_to_zero(floatbv_mult(fractional_part, shifting));
458 
459  // Numbers with greater or equal value to the following, should use
460  // the exponent notation.
461  exprt max_non_exponent_notation = from_integer(100000, shifted_float.type());
462 
463  // fractional_part_shifted is floor(float_expr * 100000) % 100000
464  const mod_exprt fractional_part_shifted(
465  shifted_float, max_non_exponent_notation);
466 
467  array_string_exprt string_fractional_part =
469  auto result2 = add_axioms_for_fractional_part(
470  string_fractional_part, fractional_part_shifted, 6);
471 
472  // string_expr_with_fractional_part =
473  // concat(string_with_do, string_fractional_part)
474  const array_string_exprt string_expr_with_fractional_part =
476  auto result3 = add_axioms_for_concat(
477  string_expr_with_fractional_part,
478  string_expr_integer_part,
479  string_fractional_part);
480 
481  // string_expr_with_E = concat(string_fraction, string_lit_E)
482  const array_string_exprt stringE =
484  auto result4 = add_axioms_for_constant(stringE, "E");
485  const array_string_exprt string_expr_with_E =
487  auto result5 = add_axioms_for_concat(
488  string_expr_with_E, string_expr_with_fractional_part, stringE);
489 
490  // exponent_string = string_of_int(decimal_exponent)
491  const array_string_exprt exponent_string =
493  auto result6 =
494  add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3);
495 
496  // string_expr = concat(string_expr_with_E, exponent_string)
497  auto result7 =
498  add_axioms_for_concat(res, string_expr_with_E, exponent_string);
499 
500  const exprt return_code = maximum(
501  result1.first,
502  maximum(
503  result2.first,
504  maximum(
505  result3.first,
506  maximum(
507  result4.first,
508  maximum(result5.first, maximum(result6.first, result7.first))))));
509  merge(result7.second, std::move(result1.second));
510  merge(result7.second, std::move(result2.second));
511  merge(result7.second, std::move(result3.second));
512  merge(result7.second, std::move(result4.second));
513  merge(result7.second, std::move(result5.second));
514  merge(result7.second, std::move(result6.second));
515  return {return_code, std::move(result7.second)};
516 }
517 
524 std::pair<exprt, string_constraintst>
527 {
528  PRECONDITION(f.arguments().size() == 3);
529  const array_string_exprt res =
530  array_pool.find(f.arguments()[1], f.arguments()[0]);
531  const exprt &arg = f.arguments()[2];
533 }
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:150
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:221
ieee_floatt
Definition: ieee_float.h:120
array_string_exprt::length_type
const typet & length_type() const
Definition: string_expr.h:69
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:139
typet::subtype
const typet & subtype() const
Definition: type.h:47
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:51
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
array_poolt::find
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition: array_pool.cpp:182
typet
The type of an expression, extends irept.
Definition: type.h:29
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1379
and_exprt
Boolean AND.
Definition: std_expr.h:2137
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
array_poolt::get_or_create_length
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:24
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
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:120
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:36
array_string_exprt::content
exprt & content()
Definition: string_expr.h:74
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:42
string_constraint_generatort::add_axioms_for_string_of_float
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
Definition: string_constraint_generator_float.cpp:159
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1190
ieee_floatt::from_float
void from_float(const float f)
Definition: ieee_float.cpp:1114
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:58
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
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:100
ieee_float_spect
Definition: ieee_float.h:26
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:81
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:400
bitor_exprt
Bit-wise OR.
Definition: std_expr.h:2388
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:1248
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2067
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:25
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
less_than_or_equal_to
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:36
string_constraint_generatort::add_axioms_from_double
std::pair< exprt, string_constraintst > add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
Definition: string_constraint_generator_float.cpp:171
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
ieee_floatt::rounding_modet
rounding_modet
Definition: ieee_float.h:126
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:26
minus_exprt
Binary minus.
Definition: std_expr.h:940
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
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:57
string_constraint_generatort::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:242
string_constraint_generatort::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
floatbv_mult
exprt floatbv_mult(const exprt &f, const exprt &g)
Multiplication of expressions representing floating points.
Definition: string_constraint_generator_float.cpp:103
array_typet
Arrays with given size.
Definition: std_types.h:965
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:99
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
string_constraint_generatort::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)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
Definition: string_constraint_generator_valueof.cpp:118
ieee_float_spect::bias
mp_integer bias() const
Definition: ieee_float.cpp:20
string_constraint_generatort::add_axioms_from_float_scientific_notation
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
Definition: string_constraint_generator_float.cpp:335
string_constraint_generatort::add_axioms_for_concat
std::pair< exprt, string_constraintst > 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.
Definition: string_concatenation_builtin_function.cpp:158
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:2697
float_bv.h
index_exprt
Array index operator.
Definition: std_expr.h:1293
greater_than
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition: string_expr.h:25
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
string_constraint_generator.h
Generates string constraints to link results from string functions with their arguments.
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:1432
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: array_pool.cpp:55
mod_exprt
Modulo.
Definition: std_expr.h:1100
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:37
not_exprt
Boolean negation.
Definition: std_expr.h:2843
ieee_floatt::from_double
void from_double(const double d)
Definition: ieee_float.cpp:1090