cprover
|
#include <bv_arithmetic.h>
Public Member Functions | |
bv_arithmetict (const bv_spect &_spec) | |
bv_arithmetict () | |
bv_arithmetict (const exprt &expr) | |
void | negate () |
void | make_zero () |
bool | is_zero () const |
void | from_integer (const mp_integer &i) |
void | change_spec (const bv_spect &dest_spec) |
mp_integer | to_integer () const |
void | print (std::ostream &out) const |
std::string | to_ansi_c_string () const |
std::string | format (const format_spect &format_spec) const |
exprt | to_expr () const |
void | from_expr (const exprt &expr) |
bv_arithmetict & | operator/= (const bv_arithmetict &other) |
bv_arithmetict & | operator*= (const bv_arithmetict &other) |
bv_arithmetict & | operator+= (const bv_arithmetict &other) |
bv_arithmetict & | operator-= (const bv_arithmetict &other) |
bv_arithmetict & | operator%= (const bv_arithmetict &other) |
bool | operator< (const bv_arithmetict &other) |
bool | operator<= (const bv_arithmetict &other) |
bool | operator> (const bv_arithmetict &other) |
bool | operator>= (const bv_arithmetict &other) |
bool | operator== (const bv_arithmetict &other) |
bool | operator!= (const bv_arithmetict &other) |
bool | operator== (int i) |
std::ostream & | operator<< (std::ostream &out) |
void | unpack (const mp_integer &i) |
mp_integer | pack () const |
Public Attributes | |
bv_spect | spec |
Protected Member Functions | |
void | adjust () |
Protected Attributes | |
mp_integer | value |
Definition at line 49 of file bv_arithmetic.h.
|
inlineexplicit |
Definition at line 54 of file bv_arithmetic.h.
|
inline |
Definition at line 59 of file bv_arithmetic.h.
|
inlineexplicit |
Definition at line 63 of file bv_arithmetic.h.
References from_expr().
|
protected |
Definition at line 70 of file bv_arithmetic.cpp.
References power().
void bv_arithmetict::change_spec | ( | const bv_spect & | dest_spec | ) |
Definition at line 180 of file bv_arithmetic.cpp.
std::string bv_arithmetict::format | ( | const format_spect & | format_spec | ) | const |
Definition at line 55 of file bv_arithmetic.cpp.
References integer2string().
void bv_arithmetict::from_expr | ( | const exprt & | expr | ) |
Definition at line 186 of file bv_arithmetic.cpp.
References binary2integer(), bv_spect::bv_spect(), irept::get_string(), exprt::is_constant(), and exprt::type().
void bv_arithmetict::from_integer | ( | const mp_integer & | i | ) |
Definition at line 64 of file bv_arithmetic.cpp.
|
inline |
Definition at line 75 of file bv_arithmetic.h.
References from_integer().
|
inline |
Definition at line 70 of file bv_arithmetic.h.
void bv_arithmetict::negate | ( | ) |
bool bv_arithmetict::operator!= | ( | const bv_arithmetict & | other | ) |
Definition at line 175 of file bv_arithmetic.cpp.
References value.
bv_arithmetict & bv_arithmetict::operator%= | ( | const bv_arithmetict & | other | ) |
Definition at line 135 of file bv_arithmetic.cpp.
bv_arithmetict & bv_arithmetict::operator*= | ( | const bv_arithmetict & | other | ) |
Definition at line 105 of file bv_arithmetic.cpp.
bv_arithmetict & bv_arithmetict::operator+= | ( | const bv_arithmetict & | other | ) |
Definition at line 115 of file bv_arithmetic.cpp.
bv_arithmetict & bv_arithmetict::operator-= | ( | const bv_arithmetict & | other | ) |
Definition at line 125 of file bv_arithmetic.cpp.
bv_arithmetict & bv_arithmetict::operator/= | ( | const bv_arithmetict & | other | ) |
Definition at line 93 of file bv_arithmetic.cpp.
bool bv_arithmetict::operator< | ( | const bv_arithmetict & | other | ) |
Definition at line 145 of file bv_arithmetic.cpp.
References value.
|
inline |
Definition at line 111 of file bv_arithmetic.h.
bool bv_arithmetict::operator<= | ( | const bv_arithmetict & | other | ) |
Definition at line 150 of file bv_arithmetic.cpp.
References value.
bool bv_arithmetict::operator== | ( | const bv_arithmetict & | other | ) |
Definition at line 165 of file bv_arithmetic.cpp.
References value.
bool bv_arithmetict::operator== | ( | int | i | ) |
Definition at line 170 of file bv_arithmetic.cpp.
bool bv_arithmetict::operator> | ( | const bv_arithmetict & | other | ) |
Definition at line 155 of file bv_arithmetic.cpp.
References value.
bool bv_arithmetict::operator>= | ( | const bv_arithmetict & | other | ) |
Definition at line 160 of file bv_arithmetic.cpp.
References value.
mp_integer bv_arithmetict::pack | ( | ) | const |
Definition at line 79 of file bv_arithmetic.cpp.
References power().
void bv_arithmetict::print | ( | std::ostream & | out | ) | const |
Definition at line 50 of file bv_arithmetic.cpp.
|
inline |
Definition at line 86 of file bv_arithmetic.h.
References from_expr(), operator!=(), operator-=(), operator<(), operator<=(), bv_spect::operator==(), operator>(), operator>=(), and to_expr().
exprt bv_arithmetict::to_expr | ( | ) | const |
Definition at line 86 of file bv_arithmetic.cpp.
References integer2binary(), and constant_exprt::set_value().
|
inline |
Definition at line 82 of file bv_arithmetic.h.
|
inline |
Definition at line 117 of file bv_arithmetic.h.
Referenced by bv_refinementt::check_SAT().
bv_spect bv_arithmetict::spec |
Definition at line 52 of file bv_arithmetic.h.
Referenced by operator%=(), operator*=(), operator+=(), operator-=(), and operator/=().
|
protected |
Definition at line 122 of file bv_arithmetic.h.
Referenced by operator!=(), operator%=(), operator*=(), operator+=(), operator-=(), operator/=(), operator<(), operator<=(), operator==(), operator>(), and operator>=().