SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
•All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
OCLWH31.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include <smtrat-solver/Manager.h>
4 
5 //#include "../modules/FPPModule/FPPModule.h"
6 #include <smtrat-modules/SATModule/SATModule.h>
7 
8 namespace smtrat
9 {
10  class MCSAT_OCLWH31: public Manager
11  {
12  public:
13  MCSAT_OCLWH31(): Manager() {
14  setStrategy(
15  addBackend<SATModule<SATSettingsMCSATOCLWH31>>()
16  );
17  }
18  };
19 } // namespace smtrat
smtrat::MCSAT_OCLWH31
Definition: OCLWH31.h:11
smtrat::MCSAT_OCLWH31::MCSAT_OCLWH31
MCSAT_OCLWH31()
Definition: OCLWH31.h:13
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