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