SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PPComplete.h
Go to the documentation of this file.
1
#pragma once
2
3
#include <
smtrat-modules/FPPModule/FPPModule.h
>
4
#include <
smtrat-modules/NewCoveringModule/NewCoveringModule.tpp
>
5
#include <
smtrat-modules/SATModule/SATModule.h
>
6
#include <
smtrat-solver/Manager.h
>
7
8
namespace
smtrat
{
9
10
namespace
internal {
11
struct
NewCoveringSettings : NewCoveringSettings2 {
12
using
op
=
cadcells::operators::Mccallum<cadcells::operators::MccallumSettingsComplete>
;
13
};
14
}
// namespace internal
15
16
class
NewCovering_PPComplete
:
public
Manager
{
17
public
:
18
NewCovering_PPComplete
()
19
:
Manager
() {
20
setStrategy
(
21
addBackend
<
FPPModule<FPPSettings1>
>(
22
addBackend
<
SATModule<SATSettings1>
>(
23
addBackend
<
NewCoveringModule<internal::NewCoveringSettings>
>())));
24
}
25
};
26
}
// namespace smtrat
FPPModule.h
Manager.h
NewCoveringModule.tpp
SATModule.h
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::NewCoveringModule
Definition:
NewCoveringModule.h:36
smtrat::NewCovering_PPComplete
Definition:
PPComplete.h:16
smtrat::NewCovering_PPComplete::NewCovering_PPComplete
NewCovering_PPComplete()
Definition:
PPComplete.h:18
smtrat::SATModule
Implements a module performing DPLL style SAT checking.
Definition:
SATModule.h:62
smtrat
Class to create the formulas for axioms.
Definition:
handle_options.h:10
smtrat::cadcells::operators::Mccallum
Definition:
operator_mccallum.h:22
smtrat-strategies
strategies
NewCovering
PPComplete.h
Generated by
1.9.1