SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PPSTropDefault.h
Go to the documentation of this file.
1
#pragma once
2
3
#include <
smtrat-modules/CoveringNGModule/CoveringNGModule.h
>
4
#include <
smtrat-modules/FPPModule/FPPModule.h
>
5
#include <
smtrat-modules/STropModule/STropModule.h
>
6
#include <
smtrat-solver/Manager.h
>
7
8
namespace
smtrat
{
9
10
/**
11
* The most efficient CoveringNG strategy with preprocessing and subtropical. Is slightly slower than PPDefault.
12
*
13
*/
14
class
CoveringNG_PPSTropDefault
:
public
Manager
{
15
public
:
16
CoveringNG_PPSTropDefault
() :
Manager
() {
17
setStrategy
(
18
addBackend
<
FPPModule<FPPSettings1>
>({
19
addBackend<STropModule<STropSettings3>>({
20
addBackend<CoveringNGModule<CoveringNGSettingsDefault>>()
21
})
22
})
23
);
24
}
25
};
26
}
// namespace smtrat
CoveringNGModule.h
FPPModule.h
Manager.h
STropModule.h
smtrat::CoveringNG_PPSTropDefault
The most efficient CoveringNG strategy with preprocessing and subtropical.
Definition:
PPSTropDefault.h:14
smtrat::CoveringNG_PPSTropDefault::CoveringNG_PPSTropDefault
CoveringNG_PPSTropDefault()
Definition:
PPSTropDefault.h:16
smtrat::FPPModule
Definition:
FPPModule.h:18
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::Manager::addBackend
BackendLink addBackend(const std::initializer_list< BackendLink > &backends={})
Definition:
Manager.h:396
smtrat
Class to create the formulas for axioms.
Definition:
handle_options.h:10
smtrat-strategies
strategies
CoveringNG
PPSTropDefault.h
Generated by
1.9.1