SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Static Public Member Functions | Private Attributes | Friends
smtrat::BVAnnotation Class Reference

#include <IntBlastModule.h>

Public Member Functions

 BVAnnotation ()
 
 BVAnnotation (std::size_t _width, bool _signed, Integer _offset=0)
 
std::size_t width () const
 
bool isSigned () const
 
bool is_constant () const
 
bool hasOffset () const
 
BVAnnotation withOffset (Integer _newOffset) const
 
BVAnnotation withWidth (std::size_t _width) const
 
const Integer & offset () const
 
const carl::Interval< Integer > & bounds () const
 
const Integer & lower_bound () const
 
const Integer & upper_bound () const
 

Static Public Member Functions

static BVAnnotation forSum (BVAnnotation _summand1, BVAnnotation _summand2)
 
static BVAnnotation forProduct (BVAnnotation _factor1, BVAnnotation _factor2)
 

Private Attributes

std::size_t mWidth
 
bool mSigned
 
Integer mOffset
 
carl::Interval< Integer > mBounds
 

Friends

std::ostream & operator<< (std::ostream &_out, const BVAnnotation &_type)
 

Detailed Description

Definition at line 18 of file IntBlastModule.h.

Constructor & Destructor Documentation

◆ BVAnnotation() [1/2]

smtrat::BVAnnotation::BVAnnotation ( )
inline

Definition at line 27 of file IntBlastModule.h.

Here is the caller graph for this function:

◆ BVAnnotation() [2/2]

smtrat::BVAnnotation::BVAnnotation ( std::size_t  _width,
bool  _signed,
Integer  _offset = 0 
)
inline

Definition at line 31 of file IntBlastModule.h.

Member Function Documentation

◆ bounds()

const carl::Interval<Integer>& smtrat::BVAnnotation::bounds ( ) const
inline

Definition at line 64 of file IntBlastModule.h.

◆ forProduct()

static BVAnnotation smtrat::BVAnnotation::forProduct ( BVAnnotation  _factor1,
BVAnnotation  _factor2 
)
inlinestatic

Definition at line 93 of file IntBlastModule.h.

Here is the call graph for this function:

◆ forSum()

static BVAnnotation smtrat::BVAnnotation::forSum ( BVAnnotation  _summand1,
BVAnnotation  _summand2 
)
inlinestatic

Definition at line 76 of file IntBlastModule.h.

Here is the call graph for this function:

◆ hasOffset()

bool smtrat::BVAnnotation::hasOffset ( ) const
inline

Definition at line 48 of file IntBlastModule.h.

Here is the caller graph for this function:

◆ is_constant()

bool smtrat::BVAnnotation::is_constant ( ) const
inline

Definition at line 44 of file IntBlastModule.h.

◆ isSigned()

bool smtrat::BVAnnotation::isSigned ( ) const
inline

Definition at line 40 of file IntBlastModule.h.

Here is the caller graph for this function:

◆ lower_bound()

const Integer& smtrat::BVAnnotation::lower_bound ( ) const
inline

Definition at line 68 of file IntBlastModule.h.

Here is the caller graph for this function:

◆ offset()

const Integer& smtrat::BVAnnotation::offset ( ) const
inline

Definition at line 60 of file IntBlastModule.h.

Here is the caller graph for this function:

◆ upper_bound()

const Integer& smtrat::BVAnnotation::upper_bound ( ) const
inline

Definition at line 72 of file IntBlastModule.h.

Here is the caller graph for this function:

◆ width()

std::size_t smtrat::BVAnnotation::width ( ) const
inline

Definition at line 36 of file IntBlastModule.h.

Here is the caller graph for this function:

◆ withOffset()

BVAnnotation smtrat::BVAnnotation::withOffset ( Integer  _newOffset) const
inline

Definition at line 52 of file IntBlastModule.h.

Here is the call graph for this function:

◆ withWidth()

BVAnnotation smtrat::BVAnnotation::withWidth ( std::size_t  _width) const
inline

Definition at line 56 of file IntBlastModule.h.

Here is the call graph for this function:

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<< ( std::ostream &  _out,
const BVAnnotation &  _type 
)
friend

Definition at line 100 of file IntBlastModule.h.

Field Documentation

◆ mBounds

carl::Interval<Integer> smtrat::BVAnnotation::mBounds
private

Definition at line 24 of file IntBlastModule.h.

◆ mOffset

Integer smtrat::BVAnnotation::mOffset
private

Definition at line 23 of file IntBlastModule.h.

◆ mSigned

bool smtrat::BVAnnotation::mSigned
private

Definition at line 22 of file IntBlastModule.h.

◆ mWidth

std::size_t smtrat::BVAnnotation::mWidth
private

Definition at line 21 of file IntBlastModule.h.

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