SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Incomplete.h
Go to the documentation of this file.
1
#pragma once
2
3
#include <
smtrat-modules/NewCoveringModule/NewCoveringModule.tpp
>
4
#include <
smtrat-modules/SATModule/SATModule.h
>
5
#include <
smtrat-solver/Manager.h
>
6
7
namespace
smtrat
{
8
9
namespace
internal {
10
struct
NewCoveringSettings : NewCoveringSettings2 {
11
using
op
=
cadcells::operators::Mccallum<cadcells::operators::MccallumSettings>
;
12
};
13
}
// namespace internal
14
15
class
NewCovering_Incomplete
:
public
Manager
{
16
public
:
17
NewCovering_Incomplete
()
18
:
Manager
() {
19
setStrategy
(
20
addBackend
<
SATModule<SATSettings1>
>(
21
addBackend
<
NewCoveringModule<internal::NewCoveringSettings>
>()));
22
}
23
};
24
}
// namespace smtrat
Manager.h
NewCoveringModule.tpp
SATModule.h
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_Incomplete
Definition:
Incomplete.h:15
smtrat::NewCovering_Incomplete::NewCovering_Incomplete
NewCovering_Incomplete()
Definition:
Incomplete.h:17
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
Incomplete.h
Generated by
1.9.1