cprover
bv_arithmetict Class Reference

#include <bv_arithmetic.h>

Collaboration diagram for bv_arithmetict:
[legend]

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_arithmetictoperator/= (const bv_arithmetict &other)
 
bv_arithmetictoperator*= (const bv_arithmetict &other)
 
bv_arithmetictoperator+= (const bv_arithmetict &other)
 
bv_arithmetictoperator-= (const bv_arithmetict &other)
 
bv_arithmetictoperator%= (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
 

Detailed Description

Definition at line 49 of file bv_arithmetic.h.

Constructor & Destructor Documentation

◆ bv_arithmetict() [1/3]

bv_arithmetict::bv_arithmetict ( const bv_spect _spec)
inlineexplicit

Definition at line 54 of file bv_arithmetic.h.

◆ bv_arithmetict() [2/3]

bv_arithmetict::bv_arithmetict ( )
inline

Definition at line 59 of file bv_arithmetic.h.

◆ bv_arithmetict() [3/3]

bv_arithmetict::bv_arithmetict ( const exprt expr)
inlineexplicit

Definition at line 63 of file bv_arithmetic.h.

References from_expr().

Member Function Documentation

◆ adjust()

void bv_arithmetict::adjust ( )
protected

◆ change_spec()

void bv_arithmetict::change_spec ( const bv_spect dest_spec)

Definition at line 180 of file bv_arithmetic.cpp.

References adjust(), and spec.

◆ format()

std::string bv_arithmetict::format ( const format_spect format_spec) const

Definition at line 55 of file bv_arithmetic.cpp.

References integer2string(), and value.

Referenced by to_ansi_c_string().

◆ from_expr()

void bv_arithmetict::from_expr ( const exprt expr)

◆ from_integer()

void bv_arithmetict::from_integer ( const mp_integer i)

Definition at line 64 of file bv_arithmetic.cpp.

References adjust(), and value.

◆ is_zero()

bool bv_arithmetict::is_zero ( ) const
inline

Definition at line 75 of file bv_arithmetic.h.

References value.

◆ make_zero()

void bv_arithmetict::make_zero ( )
inline

Definition at line 70 of file bv_arithmetic.h.

References value.

◆ negate()

void bv_arithmetict::negate ( )

◆ operator!=()

bool bv_arithmetict::operator!= ( const bv_arithmetict other)

Definition at line 175 of file bv_arithmetic.cpp.

References value.

◆ operator%=()

bv_arithmetict & bv_arithmetict::operator%= ( const bv_arithmetict other)

Definition at line 135 of file bv_arithmetic.cpp.

References adjust(), spec, and value.

◆ operator*=()

bv_arithmetict & bv_arithmetict::operator*= ( const bv_arithmetict other)

Definition at line 105 of file bv_arithmetic.cpp.

References adjust(), spec, and value.

◆ operator+=()

bv_arithmetict & bv_arithmetict::operator+= ( const bv_arithmetict other)

Definition at line 115 of file bv_arithmetic.cpp.

References adjust(), spec, and value.

◆ operator-=()

bv_arithmetict & bv_arithmetict::operator-= ( const bv_arithmetict other)

Definition at line 125 of file bv_arithmetic.cpp.

References adjust(), spec, and value.

◆ operator/=()

bv_arithmetict & bv_arithmetict::operator/= ( const bv_arithmetict other)

Definition at line 93 of file bv_arithmetic.cpp.

References spec, and value.

◆ operator<()

bool bv_arithmetict::operator< ( const bv_arithmetict other)

Definition at line 145 of file bv_arithmetic.cpp.

References value.

◆ operator<<()

std::ostream& bv_arithmetict::operator<< ( std::ostream &  out)
inline

Definition at line 111 of file bv_arithmetic.h.

References to_ansi_c_string().

◆ operator<=()

bool bv_arithmetict::operator<= ( const bv_arithmetict other)

Definition at line 150 of file bv_arithmetic.cpp.

References value.

◆ operator==() [1/2]

bool bv_arithmetict::operator== ( const bv_arithmetict other)

Definition at line 165 of file bv_arithmetic.cpp.

References value.

◆ operator==() [2/2]

bool bv_arithmetict::operator== ( int  i)

Definition at line 170 of file bv_arithmetic.cpp.

References value.

◆ operator>()

bool bv_arithmetict::operator> ( const bv_arithmetict other)

Definition at line 155 of file bv_arithmetic.cpp.

References value.

◆ operator>=()

bool bv_arithmetict::operator>= ( const bv_arithmetict other)

Definition at line 160 of file bv_arithmetic.cpp.

References value.

◆ pack()

mp_integer bv_arithmetict::pack ( ) const

Definition at line 79 of file bv_arithmetic.cpp.

References power(), spec, value, and bv_spect::width.

◆ print()

void bv_arithmetict::print ( std::ostream &  out) const

Definition at line 50 of file bv_arithmetic.cpp.

References to_ansi_c_string().

◆ to_ansi_c_string()

std::string bv_arithmetict::to_ansi_c_string ( ) const
inline

Definition at line 86 of file bv_arithmetic.h.

References format().

Referenced by operator<<(), and print().

◆ to_expr()

exprt bv_arithmetict::to_expr ( ) const

◆ to_integer()

mp_integer bv_arithmetict::to_integer ( ) const
inline

Definition at line 82 of file bv_arithmetic.h.

References value.

◆ unpack()

void bv_arithmetict::unpack ( const mp_integer i)
inline

Definition at line 117 of file bv_arithmetic.h.

References adjust(), and value.

Referenced by bv_refinementt::check_SAT().

Member Data Documentation

◆ spec

bv_spect bv_arithmetict::spec

◆ value


The documentation for this class was generated from the following files: