@@ -57,44 +57,4 @@ inline void cnf_gate_and(cnft &cnf, literalt a, literalt b, literalt o) {
57
57
cnf.lcnf (lits);
58
58
}
59
59
60
- inline std::optional<std::pair<std::string, std::size_t >>
61
- b2h_conversion_specs (const exprt &expr)
62
- {
63
- if (expr.id () == ID_constant) {
64
- auto &constant_expr = to_constant_expr (expr);
65
- const typet &type = constant_expr.type ();
66
- if (type.id () == ID_unsignedbv || type.id () == ID_signedbv) {
67
- const std::size_t &width = to_bitvector_type (type).get_width ();
68
- const std::string value = id2string (constant_expr.get_value ());
69
- if (value.size () == width &&
70
- std::all_of (value.begin (), value.end (),
71
- [](char c) { return (c == ' 0' || c == ' 1' ); })) {
72
- return std::make_pair (value, width);
73
- }
74
- }
75
- }
76
-
77
- return {};
78
- }
79
-
80
- inline void binary_to_hex_reinterpret (exprt &expr) {
81
- auto conversion_specs = b2h_conversion_specs (expr);
82
- if (conversion_specs.has_value ()) {
83
- expr.set (ID_value, integer2bvrep (string2integer (conversion_specs->first , 2 ),
84
- conversion_specs->second ));
85
- }
86
- }
87
-
88
- inline exprt binary_to_hex (const exprt &expr) {
89
- auto conversion_specs = b2h_conversion_specs (expr);
90
- if (conversion_specs.has_value ()) {
91
- return constant_exprt{
92
- integer2bvrep (string2integer (conversion_specs->first , 2 ),
93
- conversion_specs->second ),
94
- expr.type ()};
95
- }
96
-
97
- return expr;
98
- }
99
-
100
60
#endif // HW_CBMC_UTIL_EBMC_UTIL_H
0 commit comments