SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
FMVSNL.h
Go to the documentation of this file.
1
#pragma once
2
3
#include <
smtrat-modules/FPPModule/FPPModule.h
>
4
#include <
smtrat-modules/SATModule/SATModule.h
>
5
6
namespace
smtrat
7
{
8
class
MCSAT_FMVSNL
:
public
Manager
9
{
10
public
:
11
MCSAT_FMVSNL
():
Manager
() {
12
setStrategy
(
13
addBackend
<
FPPModule<FPPSettings1>
>(
14
addBackend
<
SATModule<SATSettingsMCSATFMVSNL>
>()
15
)
16
);
17
}
18
};
19
}
// namespace smtrat
FPPModule.h
SATModule.h
smtrat::FPPModule
Definition:
FPPModule.h:18
smtrat::MCSAT_FMVSNL
Definition:
FMVSNL.h:9
smtrat::MCSAT_FMVSNL::MCSAT_FMVSNL
MCSAT_FMVSNL()
Definition:
FMVSNL.h:11
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::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-strategies
strategies
MCSAT
FMVSNL.h
Generated by
1.9.1