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

#include <IntBlastModule.h>

Collaboration diagram for smtrat::AnnotatedBVTerm:
Collaboration graph
[legend]

Public Member Functions

 AnnotatedBVTerm ()
 
 AnnotatedBVTerm (const BVAnnotation &_type, const carl::BVTerm &_term)
 
 AnnotatedBVTerm (std::size_t _width, bool _signed, Integer _offset=0)
 
 AnnotatedBVTerm (const BVAnnotation &_type)
 
const BVAnnotation & type () const
 
const carl::BVTerm & term () const
 
const carl::BVTerm & operator() () const
 

Private Attributes

BVAnnotation mType
 
carl::BVTerm mTerm
 

Friends

std::ostream & operator<< (std::ostream &_out, const AnnotatedBVTerm &_term)
 

Detailed Description

Definition at line 105 of file IntBlastModule.h.

Constructor & Destructor Documentation

◆ AnnotatedBVTerm() [1/4]

smtrat::AnnotatedBVTerm::AnnotatedBVTerm ( )
inline

Definition at line 112 of file IntBlastModule.h.

◆ AnnotatedBVTerm() [2/4]

smtrat::AnnotatedBVTerm::AnnotatedBVTerm ( const BVAnnotation &  _type,
const carl::BVTerm &  _term 
)
inline

Definition at line 116 of file IntBlastModule.h.

Here is the call graph for this function:

◆ AnnotatedBVTerm() [3/4]

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

Definition at line 122 of file IntBlastModule.h.

◆ AnnotatedBVTerm() [4/4]

smtrat::AnnotatedBVTerm::AnnotatedBVTerm ( const BVAnnotation &  _type)
inline

Definition at line 126 of file IntBlastModule.h.

Here is the call graph for this function:

Member Function Documentation

◆ operator()()

const carl::BVTerm& smtrat::AnnotatedBVTerm::operator() ( ) const
inline

Definition at line 144 of file IntBlastModule.h.

◆ term()

const carl::BVTerm& smtrat::AnnotatedBVTerm::term ( ) const
inline

Definition at line 140 of file IntBlastModule.h.

◆ type()

const BVAnnotation& smtrat::AnnotatedBVTerm::type ( ) const
inline

Definition at line 135 of file IntBlastModule.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<< ( std::ostream &  _out,
const AnnotatedBVTerm &  _term 
)
friend

Definition at line 148 of file IntBlastModule.h.

Field Documentation

◆ mTerm

carl::BVTerm smtrat::AnnotatedBVTerm::mTerm
private

Definition at line 109 of file IntBlastModule.h.

◆ mType

BVAnnotation smtrat::AnnotatedBVTerm::mType
private

Definition at line 108 of file IntBlastModule.h.

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