SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PPFilterNoop.h
Go to the documentation of this file.
1
#pragma once
2
3
#include <
smtrat-modules/CoveringNGModule/CoveringNGModule.h
>
4
#include <
smtrat-modules/CoveringNGModule/CoveringNGModule.tpp
>
5
#include <
smtrat-modules/FPPModule/FPPModule.h
>
6
#include <
smtrat-solver/Manager.h
>
7
8
namespace
smtrat
{
9
10
11
namespace
internal {
12
13
struct
CoveringNGSettings : CoveringNGSettingsDefault {
14
using
op
=
cadcells::operators::MccallumFiltered<cadcells::operators::MccallumFilteredSettings>
;
15
constexpr
static
auto
cell_heuristic
=
cadcells::representation::BIGGEST_CELL_FILTER
;
16
constexpr
static
auto
covering_heuristic
=
cadcells::representation::BIGGEST_CELL_COVERING_FILTER
;
17
};
18
19
}
20
21
class
CoveringNG_PPFilterNoop
:
public
Manager
{
22
public
:
23
CoveringNG_PPFilterNoop
() :
Manager
() {
24
setStrategy
(
25
addBackend
<
FPPModule<FPPSettings1>
>({
26
addBackend<CoveringNGModule<internal::CoveringNGSettings>>()
27
})
28
);
29
}
30
};
31
}
// namespace smtrat
CoveringNGModule.h
CoveringNGModule.tpp
FPPModule.h
Manager.h
smtrat::CoveringNG_PPFilterNoop
Definition:
PPFilterNoop.h:21
smtrat::CoveringNG_PPFilterNoop::CoveringNG_PPFilterNoop
CoveringNG_PPFilterNoop()
Definition:
PPFilterNoop.h:23
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::cadcells::representation::BIGGEST_CELL_FILTER
@ BIGGEST_CELL_FILTER
Definition:
heuristics.h:11
smtrat::cadcells::representation::BIGGEST_CELL_COVERING_FILTER
@ BIGGEST_CELL_COVERING_FILTER
Definition:
heuristics.h:16
smtrat
Class to create the formulas for axioms.
Definition:
handle_options.h:10
smtrat::cadcells::operators::MccallumFiltered
Definition:
operator_mccallum_filtered.h:32
smtrat::cadcells::operators::Mccallum
Definition:
operator_mccallum.h:22
smtrat::internal::CoveringNGSettings::cell_heuristic
constexpr static auto cell_heuristic
Definition:
PPFilterBoundsOnly.h:20
smtrat::internal::CoveringNGSettings::covering_heuristic
constexpr static auto covering_heuristic
Definition:
PPFilterBoundsOnly.h:21
smtrat-strategies
strategies
CoveringNG
PPFilterNoop.h
Generated by
1.9.1