SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PBPPStrategyLIA_ICP.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 
14 namespace smtrat
15 {
17  public Manager
18  {
19  public:
21  setStrategy({
22  //addBackend<FPPModule<FPPSettingsPB>>(
23  //addBackend<PBPPModule<PBPPSettings1>>(
24  addBackend<PBPPModule<PBPPSettingsLIAOnly>>(
25  addBackend<FPPModule<FPPSettingsPB>>(
26  addBackend<SATModule<SATSettings1>>(
27  //addBackend<VSModule<VSSettings234>>(
28  addBackend<ICPModule<ICPSettings4>>(
29  //addBackend<CubeLIAModule<CubeLIASettings1>>(
30  addBackend<LRAModule<LRASettings1>>()
31  //)
32  )
33  )
34  )
35  //)
36  });
37  }
38  };
39 } // 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.