SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PreprocessingTwo.h
Go to the documentation of this file.
1 #pragma once
2 
6 // #include <smtrat-modules/SplitSOSModule/SplitSOSModule.h>
10 // #include <smtrat-modules/GBPPModule/GBPPModule.h>
12 
13 namespace smtrat
14 {
15  /**
16  * Strategy description.
17  *
18  * @author
19  * @since
20  * @version
21  *
22  */
24  public Manager
25  {
26  public:
28  setStrategy({
29  addBackend<SymmetryModule<SymmetrySettings1>>(
30  // addBackend<GBPPModule<GBPPSettings1>>(
31  addBackend<MCBModule<MCBSettings1>>(
32  addBackend<ICEModule<ICESettings1>>(
33  addBackend<EMModule<EMSettings1>>(
34  addBackend<PFEModule<PFESettings1>>(
35  // addBackend<SplitSOSModule<SplitSOSSettings1>>({
36  addBackend<ESModule<ESSettingsLimitSubstitution>>()
37  // })
38  )
39  )
40  )
41  )
42  // )
43  )
44  });
45  }
46 
47  };
48 
49 } // namespace smtrat
A module, which iteratively finds boolean and arithmetic substitutions and applies them to all formul...
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.