SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PBPPStrategyLIA_VS.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include "../solver/Manager.h"
4 
5 #include "../modules/LRAModule/LRAModule.h"
6 #include "../modules/FPPModule/FPPModule.h"
7 #include "../modules/PBPPModule/PBPPModule.h"
8 #include "../modules/SATModule/SATModule.h"
9 #include "../modules/ICPModule/ICPModule.h"
10 #include "../modules/VSModule/VSModule.h"
11 #include "../modules/CubeLIAModule/CubeLIAModule.h"
12 
13 namespace smtrat
14 {
16  public Manager
17  {
18  public:
20  setStrategy({
21  //addBackend<FPPModule<FPPSettingsPB>>(
22  //addBackend<PBPPModule<PBPPSettings1>>(
23  addBackend<PBPPModule<PBPPSettingsLIAOnly>>(
24  addBackend<FPPModule<FPPSettingsPB>>(
25  addBackend<SATModule<SATSettings1>>(
26  addBackend<VSModule<VSSettings234>>(
27  //addBackend<ICPModule<ICPSettings4>>(
28  //addBackend<CubeLIAModule<CubeLIASettings1>>(
29  addBackend<LRAModule<LRASettings1>>()
30  //)
31  )
32  )
33  )
34  //)
35  });
36  }
37  };
38 } // namespace smtrat
Base class for solvers.
Definition: Manager.h:34
void setStrategy(const std::initializer_list< BackendLink > &backends)
Definition: Manager.h:385
Class to create the formulas for axioms.