SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PBPreprocessing.h
Go to the documentation of this file.
1 /**
2  * @file PreprocessingOne.h
3  */
4 #pragma once
5 
9 // #include "../modules/PBPPModule/PBPPModule.h"
10 
11 namespace smtrat
12 {
13  /**
14  * Strategy description.
15  *
16  * @author
17  * @since
18  * @version
19  *
20  */
22  public Manager
23  {
24  public:
26  setStrategy({
27  //addBackend<GBPPModule<GBPPSettings1>>(
28  //addBackend<PBPPModule<PBPPSettings1>>(
29  addBackend<ESModule<ESSettingsDefault>>()
30  //)
31  //)
32  });
33  }
34 
35  };
36 
38  public Manager
39  {
40  public:
42  setStrategy({
43  addBackend<GBPPModule<GBPPSettings1>>(
44  //addBackend<PBPPModule<PBPPSettings1>>(
45  addBackend<ESModule<ESSettingsDefault>>()
46  //)
47  )
48  });
49  }
50 
51  };
52 
53 } // namespace smtrat
A module, which iteratively finds boolean and arithmetic substitutions and applies them to all formul...
Supports optimization.
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.