SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PBPPStrategyGroe_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<PBPPSettings1>>(
27  addBackend<FPPModule<FPPSettingsPB>>(
28  addBackend<SATModule<SATSettings1>>(
29  //addBackend<VSModule<VSSettings234>>(
30  //addBackend<ICPModule<ICPSettings4>>(
31  //addBackend<CubeLIAModule<CubeLIASettings1>>(
32  addBackend<LRAModule<LRASettings1>>()
33  //)
34  )
35  )
36  )
37  )
38  });
39  }
40  };
41 } // 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.