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

#include <Optimization.h>

Inheritance diagram for smtrat::Optimization< Solver >:
Inheritance graph
[legend]
Collaboration diagram for smtrat::Optimization< Solver >:
Collaboration graph
[legend]

Data Structures

struct  Objective
 

Public Member Functions

 Optimization (Solver &s)
 
void add_objective (const Poly &objective, bool minimize=true)
 
void remove_objective (const Poly &objective)
 
void reset ()
 
bool active () const
 
std::tuple< Answer, Model, ObjectiveValues > compute (bool full=true)
 

Private Member Functions

const std::vector< Objective > & objectives () const
 
const carl::Variable & objectiveVariable (const Objective &objective) const
 

Private Attributes

Solver & mSolver
 
std::vector< Objective > mObjectives
 
carl::Variable mOptimizationVarInt
 
carl::Variable mOptimizationVarReal
 

Detailed Description

template<typename Solver>
class smtrat::Optimization< Solver >

Definition at line 10 of file Optimization.h.

Constructor & Destructor Documentation

◆ Optimization()

template<typename Solver >
smtrat::Optimization< Solver >::Optimization ( Solver &  s)
inline

Definition at line 32 of file Optimization.h.

Member Function Documentation

◆ active()

template<typename Solver >
bool smtrat::Optimization< Solver >::active ( ) const
inline

Definition at line 54 of file Optimization.h.

Here is the caller graph for this function:

◆ add_objective()

template<typename Solver >
void smtrat::Optimization< Solver >::add_objective ( const Poly &  objective,
bool  minimize = true 
)
inline

Definition at line 38 of file Optimization.h.

Here is the caller graph for this function:

◆ compute()

template<typename Solver >
std::tuple<Answer,Model,ObjectiveValues> smtrat::Optimization< Solver >::compute ( bool  full = true)
inline

Definition at line 58 of file Optimization.h.

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

◆ objectives()

template<typename Solver >
const std::vector<Objective>& smtrat::Optimization< Solver >::objectives ( ) const
inlineprivate

Definition at line 20 of file Optimization.h.

Here is the caller graph for this function:

◆ objectiveVariable()

template<typename Solver >
const carl::Variable& smtrat::Optimization< Solver >::objectiveVariable ( const Objective &  objective) const
inlineprivate

Definition at line 27 of file Optimization.h.

Here is the caller graph for this function:

◆ remove_objective()

template<typename Solver >
void smtrat::Optimization< Solver >::remove_objective ( const Poly &  objective)
inline

Definition at line 42 of file Optimization.h.

Here is the caller graph for this function:

◆ reset()

template<typename Solver >
void smtrat::Optimization< Solver >::reset ( )
inline

Definition at line 50 of file Optimization.h.

Here is the caller graph for this function:

Field Documentation

◆ mObjectives

template<typename Solver >
std::vector<Objective> smtrat::Optimization< Solver >::mObjectives
private

Definition at line 18 of file Optimization.h.

◆ mOptimizationVarInt

template<typename Solver >
carl::Variable smtrat::Optimization< Solver >::mOptimizationVarInt
private

Definition at line 24 of file Optimization.h.

◆ mOptimizationVarReal

template<typename Solver >
carl::Variable smtrat::Optimization< Solver >::mOptimizationVarReal
private

Definition at line 25 of file Optimization.h.

◆ mSolver

template<typename Solver >
Solver& smtrat::Optimization< Solver >::mSolver
private

Definition at line 12 of file Optimization.h.

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