cprover
Loading...
Searching...
No Matches
string_constraint_generator_float.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generates string constraints for functions generating strings
4 from other types, in particular int, long, float, double, char, bool
5
6Author: Romain Brenguier, romain.brenguier@diffblue.com
7
8\*******************************************************************/
9
13
15
16#include <util/bitvector_expr.h>
17#include <util/floatbv_expr.h>
18#include <util/ieee_float.h>
20
29exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
30{
31 const extractbits_exprt exp_bits(
32 src, spec.f + spec.e - 1, spec.f, unsignedbv_typet(spec.e));
33
34 // Exponent is in biased form (numbers from -128 to 127 are encoded with
35 // integer from 0 to 255) we have to remove the bias.
36 return minus_exprt(
37 typecast_exprt(exp_bits, signedbv_typet(32)),
38 from_integer(spec.bias(), signedbv_typet(32)));
39}
40
45exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
46{
47 return extractbits_exprt(src, spec.f - 1, 0, unsignedbv_typet(spec.f));
48}
49
61 const exprt &src,
62 const ieee_float_spect &spec,
63 const typet &type)
64{
65 PRECONDITION(type.id() == ID_unsignedbv);
66 PRECONDITION(to_unsignedbv_type(type).get_width() > spec.f);
67 typecast_exprt fraction(get_fraction(src, spec), type);
68 exprt exponent = get_exponent(src, spec);
69 equal_exprt all_zeros(exponent, from_integer(0, exponent.type()));
70 exprt hidden_bit = from_integer((1 << spec.f), type);
71 bitor_exprt with_hidden_bit(fraction, hidden_bit);
72 return if_exprt(all_zeros, fraction, with_hidden_bit);
73}
74
79exprt constant_float(const double f, const ieee_float_spect &float_spec)
80{
81 ieee_floatt fl(float_spec);
82 if(float_spec == ieee_float_spect::single_precision())
83 fl.from_float(f);
84 else if(float_spec == ieee_float_spect::double_precision())
85 fl.from_double(f);
86 else
88 return fl.to_expr();
89}
90
95{
96 exprt rounding =
98 return floatbv_typecast_exprt(f, rounding, signedbv_typet(32));
99}
100
106exprt floatbv_mult(const exprt &f, const exprt &g)
107{
108 PRECONDITION(f.type() == g.type());
110 exprt mult(ID_floatbv_mult, f.type());
111 mult.copy_to_operands(f);
112 mult.copy_to_operands(g);
114 return mult;
115}
116
124{
125 exprt rounding =
127 return floatbv_typecast_exprt(i, rounding, spec.to_type());
128}
129
143{
144 exprt log_10_of_2 =
145 constant_float(0.30102999566398119521373889472449302, spec);
146 exprt bin_exp = get_exponent(f, spec);
147 exprt float_bin_exp = floatbv_of_int_expr(bin_exp, spec);
148 exprt dec_exp = floatbv_mult(float_bin_exp, log_10_of_2);
149 binary_relation_exprt negative_exp(dec_exp, ID_lt, constant_float(0.0, spec));
150 // Rounding to zero is not correct for negative numbers, so we substract 1.
151 minus_exprt dec_minus_one(dec_exp, constant_float(1.0, spec));
152 if_exprt adjust_for_neg(negative_exp, dec_minus_one, dec_exp);
153 return round_expr_to_zero(adjust_for_neg);
154}
155
161std::pair<exprt, string_constraintst>
164{
165 PRECONDITION(f.arguments().size() == 3);
167 return add_axioms_for_string_of_float(res, f.arguments()[2]);
168}
169
173std::pair<exprt, string_constraintst>
176{
178}
179
192std::pair<exprt, string_constraintst>
194 const array_string_exprt &res,
195 const exprt &f)
196{
197 const floatbv_typet &type = to_floatbv_type(f.type());
198 const ieee_float_spect float_spec(type);
200 const typet &index_type = res.length_type();
201
202 // We will look at the first 5 digits of the fractional part.
203 // shifted is floor(f * 1e5)
204 const exprt shifting = constant_float(1e5, float_spec);
205 const exprt shifted = round_expr_to_zero(floatbv_mult(f, shifting));
206 // Numbers with greater or equal value to the following, should use
207 // the exponent notation.
208 const exprt max_non_exponent_notation = from_integer(100000, shifted.type());
209 // fractional_part is floor(f * 100000) % 100000
210 const mod_exprt fractional_part(shifted, max_non_exponent_notation);
211 const array_string_exprt fractional_part_str =
213 auto result1 =
214 add_axioms_for_fractional_part(fractional_part_str, fractional_part, 6);
215
216 // The axiom added to convert to integer should always be satisfiable even
217 // when the preconditions are not satisfied.
218 const mod_exprt integer_part(
219 round_expr_to_zero(f), max_non_exponent_notation);
220 // We should not need more than 8 characters to represent the integer
221 // part of the float.
222 const array_string_exprt integer_part_str =
224 auto result2 =
225 add_axioms_for_string_of_int(integer_part_str, integer_part, 8);
226
227 auto result3 =
228 add_axioms_for_concat(res, integer_part_str, fractional_part_str);
229 merge(result3.second, std::move(result1.second));
230 merge(result3.second, std::move(result2.second));
231
232 const auto return_code =
233 maximum(result1.first, maximum(result2.first, result3.first));
234 return {return_code, std::move(result3.second)};
235}
236
244std::pair<exprt, string_constraintst>
246 const array_string_exprt &res,
247 const exprt &int_expr,
248 size_t max_size)
249{
250 PRECONDITION(int_expr.type().id() == ID_signedbv);
251 PRECONDITION(max_size >= 2);
252 string_constraintst constraints;
253 const typet &type = int_expr.type();
255 const typet &index_type = res.length_type();
256 const exprt ten = from_integer(10, type);
257 const exprt zero_char = from_integer('0', char_type);
258 const exprt nine_char = from_integer('9', char_type);
259 const exprt max = from_integer(max_size, index_type);
260
261 // We add axioms:
262 // a1 : 2 <= |res| <= max_size
263 // a2 : starts_with_dot && no_trailing_zero && is_number
264 // starts_with_dot: res[0] = '.'
265 // is_number: forall i:[1, max_size[. '0' < res[i] < '9'
266 // no_trailing_zero: forall j:[2, max_size[. !(|res| = j+1 && res[j] = '0')
267 // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0)
268
269 const and_exprt a1(
272 constraints.existential.push_back(a1);
273
274 equal_exprt starts_with_dot(res[0], from_integer('.', char_type));
275
276 exprt::operandst digit_constraints;
277 digit_constraints.push_back(starts_with_dot);
278 exprt sum = from_integer(0, type);
279
280 for(size_t j = 1; j < max_size; j++)
281 {
282 // after_end is |res| <= j
283 binary_relation_exprt after_end(
285 ID_le,
286 from_integer(j, res.length_type()));
287 mult_exprt ten_sum(sum, ten);
288
289 // sum = 10 * sum + after_end ? 0 : (res[j]-'0')
290 if_exprt to_add(
291 after_end,
292 from_integer(0, type),
293 typecast_exprt(minus_exprt(res[j], zero_char), type));
294 sum = plus_exprt(ten_sum, to_add);
295
297 binary_relation_exprt(res[j], ID_ge, zero_char),
298 binary_relation_exprt(res[j], ID_le, nine_char));
299 digit_constraints.push_back(is_number);
300
301 // There are no trailing zeros except for ".0" (i.e j=2)
302 if(j > 1)
303 {
304 not_exprt no_trailing_zero(and_exprt(
307 from_integer(j + 1, res.length_type())),
308 equal_exprt(res[j], zero_char)));
309 digit_constraints.push_back(no_trailing_zero);
310 }
311 }
312
313 exprt a2 = conjunction(digit_constraints);
314 constraints.existential.push_back(a2);
315
316 equal_exprt a3(int_expr, sum);
317 constraints.existential.push_back(a3);
318
319 return {from_integer(0, signedbv_typet(32)), std::move(constraints)};
320}
321
337std::pair<exprt, string_constraintst>
339 const array_string_exprt &res,
340 const exprt &float_expr)
341{
342 string_constraintst constraints;
344 const typet float_type = float_spec.to_type();
345 const signedbv_typet int_type(32);
346 const typet &index_type = res.length_type();
348
349 // This is used for rounding float to integers.
350 exprt round_to_zero_expr = from_integer(ieee_floatt::ROUND_TO_ZERO, int_type);
351
352 // `bin_exponent` is $e$ in the formulas
353 exprt bin_exponent = get_exponent(float_expr, float_spec);
354
355 // $m$ from the formula is a value between 0.0 and 2.0 represented
356 // with values in the range 0x000000 0xFFFFFF so 1 corresponds to 0x800000.
357 // `bin_significand_int` represents $m * 0x800000$
358 exprt bin_significand_int =
359 get_significand(float_expr, float_spec, unsignedbv_typet(32));
360 // `bin_significand` represents $m$ and is obtained
361 // by multiplying `binary_significand_as_int` by
362 // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7
363 exprt bin_significand = floatbv_mult(
364 floatbv_typecast_exprt(bin_significand_int, round_to_zero_expr, float_type),
365 constant_float(1.1920928955078125e-7, float_spec));
366
367 // This is a first approximation of the exponent that will adjust
368 // if the fraction we get is greater than 10
369 exprt dec_exponent_estimate =
370 estimate_decimal_exponent(float_expr, float_spec);
371
372 // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128]
373 std::vector<double> two_power_e_over_ten_power_d_table(
374 {1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28,
375 2.56, 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768,
376 6.5536, 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861,
377 1.67772, 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748,
378 4.29497, 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756,
379 1.09951, 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737,
380 2.81475, 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288,
381 7.20576, 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337,
382 1.84467, 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118,
383 4.72237, 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463,
384 1.20893, 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743,
385 3.09485, 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141,
386 7.92282, 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412,
387 2.02824, 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615,
388 5.1923, 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614,
389 1.32923, 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141});
390
391 // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[-128,-1]
392 std::vector<double> two_power_e_over_ten_power_d_table_negatives(
393 {2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158,
394 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965,
395 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519,
396 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089,
397 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559,
398 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590,
399 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879,
400 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051,
401 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889,
402 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636,
403 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747,
404 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415,
405 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023,
406 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939,
407 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313,
408 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5});
409
410 // bias_table used to find the bias factor
411 exprt conversion_factor_table_size = from_integer(
412 two_power_e_over_ten_power_d_table_negatives.size() +
413 two_power_e_over_ten_power_d_table.size(),
414 int_type);
415 array_exprt conversion_factor_table(
416 {}, array_typet(float_type, conversion_factor_table_size));
417 for(const auto &negative : two_power_e_over_ten_power_d_table_negatives)
418 conversion_factor_table.copy_to_operands(
419 constant_float(negative, float_spec));
420 for(const auto &positive : two_power_e_over_ten_power_d_table)
421 conversion_factor_table.copy_to_operands(
422 constant_float(positive, float_spec));
423
424 // The index in the table, corresponding to exponent e is e+128
425 plus_exprt shifted_index(bin_exponent, from_integer(128, int_type));
426
427 // bias_factor is $2^e / 10^(floor(log_10(2)*e))$ that is $2^e/10^d$
428 index_exprt conversion_factor(
429 conversion_factor_table, shifted_index, float_type);
430
431 // `dec_significand` is $n = m * bias_factor$
432 exprt dec_significand = floatbv_mult(conversion_factor, bin_significand);
433 exprt dec_significand_int = round_expr_to_zero(dec_significand);
434
435 // `dec_exponent` is $d$ in the formulas
436 // it is obtained from the approximation, checking whether it is not too small
437 binary_relation_exprt estimate_too_small(
438 dec_significand_int, ID_ge, from_integer(10, int_type));
439 if_exprt decimal_exponent(
440 estimate_too_small,
441 plus_exprt(dec_exponent_estimate, from_integer(1, int_type)),
442 dec_exponent_estimate);
443
444 // `dec_significand` is divided by 10 if it exceeds 10
445 dec_significand = if_exprt(
446 estimate_too_small,
447 floatbv_mult(dec_significand, constant_float(0.1, float_spec)),
448 dec_significand);
449 dec_significand_int = round_expr_to_zero(dec_significand);
450 array_string_exprt string_expr_integer_part =
452 auto result1 = add_axioms_for_string_of_int(
453 string_expr_integer_part, dec_significand_int, 3);
454 minus_exprt fractional_part(
455 dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec));
456
457 // shifted_float is floor(float_expr * 1e5)
458 exprt shifting = constant_float(1e5, float_spec);
459 exprt shifted_float =
460 round_expr_to_zero(floatbv_mult(fractional_part, shifting));
461
462 // Numbers with greater or equal value to the following, should use
463 // the exponent notation.
464 exprt max_non_exponent_notation = from_integer(100000, shifted_float.type());
465
466 // fractional_part_shifted is floor(float_expr * 100000) % 100000
467 const mod_exprt fractional_part_shifted(
468 shifted_float, max_non_exponent_notation);
469
470 array_string_exprt string_fractional_part =
472 auto result2 = add_axioms_for_fractional_part(
473 string_fractional_part, fractional_part_shifted, 6);
474
475 // string_expr_with_fractional_part =
476 // concat(string_with_do, string_fractional_part)
477 const array_string_exprt string_expr_with_fractional_part =
479 auto result3 = add_axioms_for_concat(
480 string_expr_with_fractional_part,
481 string_expr_integer_part,
482 string_fractional_part);
483
484 // string_expr_with_E = concat(string_fraction, string_lit_E)
485 const array_string_exprt stringE =
487 auto result4 = add_axioms_for_constant(stringE, "E");
488 const array_string_exprt string_expr_with_E =
490 auto result5 = add_axioms_for_concat(
491 string_expr_with_E, string_expr_with_fractional_part, stringE);
492
493 // exponent_string = string_of_int(decimal_exponent)
494 const array_string_exprt exponent_string =
496 auto result6 =
497 add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3);
498
499 // string_expr = concat(string_expr_with_E, exponent_string)
500 auto result7 =
501 add_axioms_for_concat(res, string_expr_with_E, exponent_string);
502
503 const exprt return_code = maximum(
504 result1.first,
505 maximum(
506 result2.first,
507 maximum(
508 result3.first,
509 maximum(
510 result4.first,
511 maximum(result5.first, maximum(result6.first, result7.first))))));
512 merge(result7.second, std::move(result1.second));
513 merge(result7.second, std::move(result2.second));
514 merge(result7.second, std::move(result3.second));
515 merge(result7.second, std::move(result4.second));
516 merge(result7.second, std::move(result5.second));
517 merge(result7.second, std::move(result6.second));
518 return {return_code, std::move(result7.second)};
519}
520
527std::pair<exprt, string_constraintst>
530{
531 PRECONDITION(f.arguments().size() == 3);
532 const array_string_exprt res =
533 array_pool.find(f.arguments()[1], f.arguments()[0]);
534 const exprt &arg = f.arguments()[2];
536}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
API to expression classes for bitvectors.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
floatbv_typet float_type()
Definition: c_types.cpp:195
bitvector_typet index_type()
Definition: c_types.cpp:22
bitvector_typet char_type()
Definition: c_types.cpp:124
Boolean AND.
Definition: std_expr.h:1974
Array constructor from list of elements.
Definition: std_expr.h:1476
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
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:57
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:184
const typet & length_type() const
Definition: string_expr.h:69
exprt & content()
Definition: string_expr.h:74
Arrays with given size.
Definition: std_types.h:763
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Bit-wise OR.
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
typet & type()
Return the type of the expression.
Definition: expr.h:82
Extracts a sub-range of a bit-vector operand.
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
static ieee_float_spect single_precision()
Definition: ieee_float.h:71
class floatbv_typet to_type() const
Definition: ieee_float.cpp:25
mp_integer bias() const
Definition: ieee_float.cpp:20
static ieee_float_spect double_precision()
Definition: ieee_float.h:77
std::size_t f
Definition: ieee_float.h:27
std::size_t e
Definition: ieee_float.h:27
constant_exprt to_expr() const
Definition: ieee_float.cpp:703
void from_float(const float f)
void from_double(const double d)
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
const irep_idt & id() const
Definition: irep.h:396
Binary minus.
Definition: std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
Boolean negation.
Definition: std_expr.h:2181
The plus expression Associativity is not specified.
Definition: std_expr.h:914
Fixed-width bit-vector with two's complement interpretation.
std::pair< exprt, string_constraintst > add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
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.
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.
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....
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.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
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.
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
API to expression classes for floating-point arithmetic.
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:34
Generates string constraints to link results from string functions with their arguments.
exprt maximum(const exprt &a, const exprt &b)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
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...
exprt floatbv_mult(const exprt &f, const exprt &g)
Multiplication of expressions representing floating points.
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.
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...
exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
Gets the unbiased exponent in a floating-point bit-vector.
exprt constant_float(const double f, const ieee_float_spect &float_spec)
Create an expression to represent a float or double value.
exprt round_expr_to_zero(const exprt &f)
Round a float expression to an integer closer to 0.
exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
Gets the fraction without hidden bit.
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:36
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition: string_expr.h:25
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177