SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
BVPreprocessing.h
Go to the documentation of this file.
1
/**
2
* @file BVPreprocessing.h
3
*/
4
5
#pragma once
6
7
#include <
smtrat-solver/Manager.h
>
8
#include <
smtrat-modules/ESModule/ESModule.h
>
9
#include <
smtrat-modules/SymmetryModule/SymmetryModule.h
>
10
11
namespace
smtrat
12
{
13
/**
14
* Strategy description.
15
*
16
* @author
17
* @since
18
* @version
19
*
20
*/
21
class
BVPreprocessing
:
22
public
Manager
23
{
24
public
:
25
BVPreprocessing
():
Manager
() {
26
setStrategy
({
27
//addBackend<SymmetryModule<SymmetrySettings1>>(
28
addBackend<ESModule<ESSettingsDefault>>()
29
//)
30
});
31
}
32
33
};
34
35
}
// namespace smtrat
ESModule.h
A module, which iteratively finds boolean and arithmetic substitutions and applies them to all formul...
Manager.h
SymmetryModule.h
smtrat::BVPreprocessing
Strategy description.
Definition:
BVPreprocessing.h:23
smtrat::BVPreprocessing::BVPreprocessing
BVPreprocessing()
Definition:
BVPreprocessing.h:25
smtrat::Manager
Base class for solvers.
Definition:
Manager.h:34
smtrat::Manager::setStrategy
void setStrategy(const std::initializer_list< BackendLink > &backends)
Definition:
Manager.h:385
smtrat
Class to create the formulas for axioms.
Definition:
handle_options.h:10
smtrat-strategies
strategies
BVPreprocessing.h
Generated by
1.9.1