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

#include <IntBlastModule.h>

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

Public Member Functions

 BlastedPoly ()
 
 BlastedPoly (Integer _constant)
 
 BlastedPoly (Integer _constant, FormulasT _constraints)
 
 BlastedPoly (AnnotatedBVTerm _term)
 
 BlastedPoly (AnnotatedBVTerm _term, FormulasT _constraints)
 
bool is_constant () const
 
const Integer & constant () const
 
const AnnotatedBVTerm & term () const
 
const FormulasT & constraints () const
 
const Integer & lower_bound () const
 
const Integer & upper_bound () const
 

Private Attributes

bool mIsConstant
 
Integer mConstant
 
AnnotatedBVTerm mTerm
 
FormulasT mConstraints
 

Friends

std::ostream & operator<< (std::ostream &_out, const BlastedPoly &_poly)
 

Detailed Description

Definition at line 153 of file IntBlastModule.h.

Constructor & Destructor Documentation

◆ BlastedPoly() [1/5]

smtrat::BlastedPoly::BlastedPoly ( )
inline

Definition at line 162 of file IntBlastModule.h.

◆ BlastedPoly() [2/5]

smtrat::BlastedPoly::BlastedPoly ( Integer  _constant)
inline

Definition at line 166 of file IntBlastModule.h.

◆ BlastedPoly() [3/5]

smtrat::BlastedPoly::BlastedPoly ( Integer  _constant,
FormulasT  _constraints 
)
inline

Definition at line 170 of file IntBlastModule.h.

◆ BlastedPoly() [4/5]

smtrat::BlastedPoly::BlastedPoly ( AnnotatedBVTerm  _term)
inline

Definition at line 174 of file IntBlastModule.h.

◆ BlastedPoly() [5/5]

smtrat::BlastedPoly::BlastedPoly ( AnnotatedBVTerm  _term,
FormulasT  _constraints 
)
inline

Definition at line 178 of file IntBlastModule.h.

Member Function Documentation

◆ constant()

const Integer& smtrat::BlastedPoly::constant ( ) const
inline

Definition at line 186 of file IntBlastModule.h.

◆ constraints()

const FormulasT& smtrat::BlastedPoly::constraints ( ) const
inline

Definition at line 196 of file IntBlastModule.h.

◆ is_constant()

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

Definition at line 182 of file IntBlastModule.h.

◆ lower_bound()

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

Definition at line 200 of file IntBlastModule.h.

Here is the call graph for this function:

◆ term()

const AnnotatedBVTerm& smtrat::BlastedPoly::term ( ) const
inline

Definition at line 191 of file IntBlastModule.h.

◆ upper_bound()

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

Definition at line 208 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 BlastedPoly &  _poly 
)
friend

Definition at line 216 of file IntBlastModule.h.

Field Documentation

◆ mConstant

Integer smtrat::BlastedPoly::mConstant
private

Definition at line 157 of file IntBlastModule.h.

◆ mConstraints

FormulasT smtrat::BlastedPoly::mConstraints
private

Definition at line 159 of file IntBlastModule.h.

◆ mIsConstant

bool smtrat::BlastedPoly::mIsConstant
private

Definition at line 156 of file IntBlastModule.h.

◆ mTerm

AnnotatedBVTerm smtrat::BlastedPoly::mTerm
private

Definition at line 158 of file IntBlastModule.h.

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