SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
AllModulesStrategy.h
Go to the documentation of this file.
1 #pragma once
2 
4 
22 
23 namespace smtrat
24 {
26  public Manager
27  {
28  public:
30  setStrategy({
31  addBackend<BEModule<BESettings1>>(),
33  addBackend<NewCADModule<NewCADSettingsNaive>>(),
34  addBackend<CNFerModule>(),
35  addBackend<EMModule<EMSettings1>>(),
37  addBackend<FPPModule<FPPSettings1>>(),
39  addBackend<ICPModule<ICPSettings1>>(),
41  addBackend<IntBlastModule<IntBlastSettings1>>(),
43  addBackend<LRAModule<LRASettings1>>(),
45  addBackend<SATModule<SATSettings1>>(),
47  addBackend<VSModule<VSSettings1>>(),
48  });
49  }
50  };
51 } // namespace smtrat
A module, which searches for bounds of arithmetic variables and polynomials.
A module, which iteratively finds boolean and arithmetic substitutions and applies them to all formul...
Removes factors of polynomials from the formula.
Splits the sum-of-squares (sos) decomposition of all constraints with a sos as left-hand side.
A solver module based on Groebner basis.
Definition: GBModule.h:46
A module which checks whether the equations contained in the received (linear integer) formula have a...
Definition: IntEqModule.h:22
Base class for solvers.
Definition: Manager.h:34
void setStrategy(const std::initializer_list< BackendLink > &backends)
Definition: Manager.h:385
BackendLink addBackend(const std::initializer_list< BackendLink > &backends={})
Definition: Manager.h:396
Class to create the formulas for axioms.