SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
RatIntBlast.h
Go to the documentation of this file.
1 /**
2  * @file RatIntBlast.h
3  */
4 #pragma once
5 
6 #include "../solver/Manager.h"
7 #include "../modules/FPPModule/FPPModule.h"
8 #include "../modules/IncWidthModule/IncWidthModule.h"
9 #include "../modules/IntBlastModule/IntBlastModule.h"
10 #include "../modules/SATModule/SATModule.h"
11 
12 namespace smtrat
13 {
14  /**
15  * Strategy description.
16  *
17  * @author
18  * @since
19  * @version
20  *
21  */
22  class RatIntBlast:
23  public Manager
24  {
25 
26  public:
27 
29  {
31  {
32  addBackend<FPPModule<FPPSettings1>>(
33  {
34  addBackend<IncWidthModule<IncWidthSettings2>>(
35  {
36 // addBackend<SATModule<SATSettings1>>(
37 // {
38  addBackend<IntBlastModule<IntBlastSettings2>>()
39 // })
40  })
41  })
42  });
43  }
44  };
45 } // namespace smtrat
Base class for solvers.
Definition: Manager.h:34
void setStrategy(const std::initializer_list< BackendLink > &backends)
Definition: Manager.h:385
Strategy description.
Definition: RatIntBlast.h:24
Class to create the formulas for axioms.