SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
smtrat::BlastedConstr Class Reference

#include <IntBlastModule.h>

Public Member Functions

 BlastedConstr ()
 
 BlastedConstr (const FormulaT &_formula, const FormulasT &_constraints)
 
 BlastedConstr (const FormulaT &_formula)
 
 BlastedConstr (bool _satisfied)
 
const FormulaTformula () const
 
const FormulasTconstraints () const
 

Private Attributes

FormulaT mFormula
 
FormulasT mConstraints
 

Friends

std::ostream & operator<< (std::ostream &_out, const BlastedConstr &_constr)
 

Detailed Description

Definition at line 225 of file IntBlastModule.h.

Constructor & Destructor Documentation

◆ BlastedConstr() [1/4]

smtrat::BlastedConstr::BlastedConstr ( )
inline

Definition at line 232 of file IntBlastModule.h.

◆ BlastedConstr() [2/4]

smtrat::BlastedConstr::BlastedConstr ( const FormulaT _formula,
const FormulasT _constraints 
)
inline

Definition at line 235 of file IntBlastModule.h.

◆ BlastedConstr() [3/4]

smtrat::BlastedConstr::BlastedConstr ( const FormulaT _formula)
inline

Definition at line 239 of file IntBlastModule.h.

◆ BlastedConstr() [4/4]

smtrat::BlastedConstr::BlastedConstr ( bool  _satisfied)
inline

Definition at line 243 of file IntBlastModule.h.

Member Function Documentation

◆ constraints()

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

Definition at line 251 of file IntBlastModule.h.

◆ formula()

const FormulaT& smtrat::BlastedConstr::formula ( ) const
inline

Definition at line 247 of file IntBlastModule.h.

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<< ( std::ostream &  _out,
const BlastedConstr _constr 
)
friend

Definition at line 255 of file IntBlastModule.h.

Field Documentation

◆ mConstraints

FormulasT smtrat::BlastedConstr::mConstraints
private

Definition at line 229 of file IntBlastModule.h.

◆ mFormula

FormulaT smtrat::BlastedConstr::mFormula
private

Definition at line 228 of file IntBlastModule.h.


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