SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
OptimizationPreprocessing.h
Go to the documentation of this file.
1 #pragma once
2 
6 // #include <smtrat-modules/SplitSOSModule/SplitSOSModule.h>
11 // #include <smtrat-modules/LVEModule/LVEModule.h>
12 
13 
14 namespace smtrat
15 {
17  public Manager
18  {
19  public:
21  setStrategy({
22  addBackend<GBPPModule<GBPPSettings1>>(
23  addBackend<MCBModule<MCBSettings1>>(
24  addBackend<ICEModule<ICESettings1>>(
25  addBackend<EMModule<EMSettings1>>(
26  addBackend<PFEModule<PFESettings1>>(
27  // addBackend<SplitSOSModule<SplitSOSSettings1>>({
28  addBackend<ESModule<ESSettingsDefault>>(
29  // addBackend<LVEModule<LVESettings1>>()
30  )
31  // })
32  )
33  )
34  )
35  )
36  )
37  });
38  }
39 
40  };
41 
42 } // namespace smtrat
A module, which iteratively finds boolean and arithmetic substitutions and applies them to all formul...
Supports optimization.
Removes factors of polynomials from the formula.
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.