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