SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
BVSolver.h
Go to the documentation of this file.
1 /**
2  * @file BVSolver.h
3  */
4 #pragma once
5 
7 
11 
12 namespace smtrat
13 {
14  /**
15  * Strategy description.
16  *
17  * @author
18  * @since
19  * @version
20  *
21  */
22  class BVSolver:
23  public Manager
24  {
25  public:
27  {
28  setStrategy({
29  addBackend<FPPModule<FPPSettings3>>({
30  addBackend<BVModule<BVSettings1>>({
31  addBackend<SATModule<SATSettings1>>()
32  })
33  })
34  });
35  }
36 
37  void removeFormula( const FormulaT& _subformula )
38  {
39  remove( _subformula );
40  }
41 
42  };
43 
44 } // namespace smtrat
Strategy description.
Definition: BVSolver.h:24
void removeFormula(const FormulaT &_subformula)
Definition: BVSolver.h:37
Base class for solvers.
Definition: Manager.h:34
ModuleInput::iterator remove(ModuleInput::iterator _subformula)
Removes the formula at the given position in the conjunction of formulas, which will be considered fo...
Definition: Manager.cpp:159
void setStrategy(const std::initializer_list< BackendLink > &backends)
Definition: Manager.h:385
Class to create the formulas for axioms.
carl::Formula< Poly > FormulaT
Definition: types.h:37