SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
MAXSATBackendStrategy.h
Go to the documentation of this file.
1
#pragma once
2
3
#include <
smtrat-solver/Manager.h
>
4
5
#include <
smtrat-modules/SATModule/SATModule.h
>
6
#include <
smtrat-modules/LRAModule/LRAModule.h
>
7
#include <
smtrat-modules/PBPPModule/PBPPModule.h
>
8
9
namespace
smtrat
{
10
11
// TODO avoid using a special backend module for MaxSMT
12
13
/**
14
* This strategy is used as a artificial backend in the MaxSMT Module
15
*
16
* See MaxSMTSettings.h to adjust the used backend.
17
*/
18
class
MAXSATBackendStrategy
:
19
public
Manager
20
{
21
public
:
22
MAXSATBackendStrategy
():
Manager
()
23
{
24
setStrategy
(
25
{
26
addBackend<PBPPModule<PBPPSettingsMaxSMT>>(
27
addBackend<SATModule<SATSettings1>>(
28
addBackend<LRAModule<LRASettings1>>()
29
)
30
),
31
});
32
}
33
};
34
35
}
// namespace smtrat
LRAModule.h
Manager.h
PBPPModule.h
Supports optimization.
SATModule.h
smtrat::MAXSATBackendStrategy
This strategy is used as a artificial backend in the MaxSMT Module.
Definition:
MAXSATBackendStrategy.h:20
smtrat::MAXSATBackendStrategy::MAXSATBackendStrategy
MAXSATBackendStrategy()
Definition:
MAXSATBackendStrategy.h:22
smtrat::Manager
Base class for solvers.
Definition:
Manager.h:34
smtrat::Manager::setStrategy
void setStrategy(const std::initializer_list< BackendLink > &backends)
Definition:
Manager.h:385
smtrat
Class to create the formulas for axioms.
Definition:
handle_options.h:10
smtrat-strategies
strategies
MAXSATBackendStrategy.h
Generated by
1.9.1