10 #ifndef CPROVER_UTIL_FIXEDBV_H 11 #define CPROVER_UTIL_FIXEDBV_H 29 integer_bits(_integer_bits), width(_width)
67 std::string format(
const format_spect &format_spec)
const;
103 #endif // CPROVER_UTIL_FIXEDBV_H std::size_t get_fraction_bits() const
std::string to_ansi_c_string() const
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &src)
void set_value(const mp_integer &_v)
guardt & operator-=(guardt &g1, const guardt &g2)
static fixedbvt zero(const fixedbv_typet &type)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool operator==(const fixedbvt &other) const
A constant literal expression.
const mp_integer & get_value() const
bool operator<(const fixedbvt &other) const
bool operator!=(const fixedbvt &other) const
bool operator>=(const fixedbvt &other) const
bool operator<=(const fixedbvt &other) const
Fixed-width bit-vector with signed fixed-point interpretation.
bool operator==(const interval_templatet< T > &a, const interval_templatet< T > &b)
fixedbv_spect(std::size_t _width, std::size_t _integer_bits)
fixedbvt(const fixedbv_spect &_spec)
bool operator>(const fixedbvt &other) const