SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Member Functions | Private Attributes
smtrat::MaxSMT< Solver, Strategy > Class Template Reference

#include <MaxSMT.h>

Inheritance diagram for smtrat::MaxSMT< Solver, Strategy >:
Inheritance graph
[legend]
Collaboration diagram for smtrat::MaxSMT< Solver, Strategy >:
Collaboration graph
[legend]

Public Member Functions

 MaxSMT (Solver &s)
 
void add_soft_formula (const FormulaT &formula, Rational weight, const std::string &id)
 
void remove_soft_formula (const FormulaT &formula)
 
void reset ()
 
bool active () const
 
std::tuple< Answer, Model, ObjectiveValues > compute ()
 

Private Member Functions

bool satisfied (const FormulaT &formula, const Model &model)
 

Private Attributes

Solver & mSolver
 
std::vector< FormulaT > mSoftFormulas
 
std::map< FormulaT, std::string > mSoftFormulaIds
 

Detailed Description

template<typename Solver, MaxSMTStrategy Strategy>
class smtrat::MaxSMT< Solver, Strategy >

Definition at line 28 of file MaxSMT.h.

Constructor & Destructor Documentation

◆ MaxSMT()

template<typename Solver , MaxSMTStrategy Strategy>
smtrat::MaxSMT< Solver, Strategy >::MaxSMT ( Solver &  s)
inline

Definition at line 39 of file MaxSMT.h.

Member Function Documentation

◆ active()

template<typename Solver , MaxSMTStrategy Strategy>
bool smtrat::MaxSMT< Solver, Strategy >::active ( ) const
inline

Definition at line 59 of file MaxSMT.h.

Here is the caller graph for this function:

◆ add_soft_formula()

template<typename Solver , MaxSMTStrategy Strategy>
void smtrat::MaxSMT< Solver, Strategy >::add_soft_formula ( const FormulaT &  formula,
Rational  weight,
const std::string &  id 
)
inline

Definition at line 41 of file MaxSMT.h.

Here is the caller graph for this function:

◆ compute()

template<typename Solver , MaxSMTStrategy Strategy>
std::tuple<Answer,Model,ObjectiveValues> smtrat::MaxSMT< Solver, Strategy >::compute ( )
inline

Definition at line 63 of file MaxSMT.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ remove_soft_formula()

template<typename Solver , MaxSMTStrategy Strategy>
void smtrat::MaxSMT< Solver, Strategy >::remove_soft_formula ( const FormulaT &  formula)
inline

Definition at line 50 of file MaxSMT.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ reset()

template<typename Solver , MaxSMTStrategy Strategy>
void smtrat::MaxSMT< Solver, Strategy >::reset ( )
inline

Definition at line 55 of file MaxSMT.h.

Here is the caller graph for this function:

◆ satisfied()

template<typename Solver , MaxSMTStrategy Strategy>
bool smtrat::MaxSMT< Solver, Strategy >::satisfied ( const FormulaT &  formula,
const Model &  model 
)
inlineprivate

Definition at line 34 of file MaxSMT.h.

Here is the call graph for this function:
Here is the caller graph for this function:

Field Documentation

◆ mSoftFormulaIds

template<typename Solver , MaxSMTStrategy Strategy>
std::map<FormulaT, std::string> smtrat::MaxSMT< Solver, Strategy >::mSoftFormulaIds
private

Definition at line 32 of file MaxSMT.h.

◆ mSoftFormulas

template<typename Solver , MaxSMTStrategy Strategy>
std::vector<FormulaT> smtrat::MaxSMT< Solver, Strategy >::mSoftFormulas
private

Definition at line 31 of file MaxSMT.h.

◆ mSolver

template<typename Solver , MaxSMTStrategy Strategy>
Solver& smtrat::MaxSMT< Solver, Strategy >::mSolver
private

Definition at line 30 of file MaxSMT.h.

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