SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PreprocessingOne.h
Go to the documentation of this file.
1 /**
2  * @file PreprocessingOne.h
3  */
4 #pragma once
5 
9 // #include <smtrat-modules/SplitSOSModule/SplitSOSModule.h>
15 
16 namespace smtrat
17 {
18  /**
19  * Strategy description.
20  *
21  * @author
22  * @since
23  * @version
24  *
25  */
27  public Manager
28  {
29  public:
31  setStrategy({
32  addBackend<SymmetryModule<SymmetrySettings1>>(
33  addBackend<GBPPModule<GBPPSettings1>>(
34  addBackend<MCBModule<MCBSettings1>>(
35  addBackend<ICEModule<ICESettings1>>(
36  addBackend<EMModule<EMSettings1>>(
37  addBackend<PFEModule<PFESettings1>>(
38  // addBackend<SplitSOSModule<SplitSOSSettings1>>({
39  addBackend<ESModule<ESSettingsDefault>>()
40  // })
41  )
42  )
43  )
44  )
45  )
46  )
47  });
48  }
49 
50  };
51 
52 } // 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
Strategy description.
Class to create the formulas for axioms.