1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
/********************* */
/*! \file preprocessing_pass_registry.h
** \verbatim
** Top contributors (to current version):
** Justin Xu, Yoni Zohar
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief The preprocessing pass registry
**
** This file defines the classes PreprocessingPassRegistry, which keeps track
** of the available preprocessing passes, and RegisterPass, which registers a
** preprocessing pass with the registry.
**/
#include "cvc4_private.h"
#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
#include <memory>
#include <string>
#include <unordered_map>
#include "preprocessing/preprocessing_pass.h"
namespace CVC4 {
namespace preprocessing {
class PreprocessingPassContext;
/**
* The PreprocessingPassRegistry keeps track of the available preprocessing
* passes and how to create instances of those passes. This class is intended
* to be used as a singleton and can be shared between threads (assuming that
* the memory allocator is thread-safe) as well as different solver instances.
*/
class PreprocessingPassRegistry {
public:
/**
* Gets the single instance of this class.
*/
static PreprocessingPassRegistry& getInstance();
/**
* Registers a pass. Do not call this directly, use the `RegisterPass` class
* instead.
*
* @param name The name of the preprocessing pass to register
* @param ctor A function that creates an instance of the pass given a
* preprocessing pass context
*/
void registerPassInfo(
const std::string& name,
std::function<PreprocessingPass*(PreprocessingPassContext*)> ctor);
/**
* Creates an instance of a pass.
*
* @param ppCtx The preprocessing pass context to pass to the preprocessing
* pass constructor
* @param name The name of the pass to create an instance of
*/
PreprocessingPass* createPass(PreprocessingPassContext* ppCtx,
const std::string& name);
/**
* Returns a sorted list of available preprocessing passes.
*/
std::vector<std::string> getAvailablePasses();
/**
* Checks whether a pass with a given name is available.
*
* @param name The name of the pass to check for
*/
bool hasPass(const std::string& name);
private:
/**
* Map of available preprocessing passes, mapping from preprocessing pass
* name to a function that constructs a corresponding instance.
*/
std::unordered_map<
std::string,
std::function<PreprocessingPass*(PreprocessingPassContext*)> >
d_ppInfo;
}; // class PreprocessingPassRegistry
/**
* Class used to register a preprocessing pass. In the source file of a given
* pass, create a static instance of this class, e.g.:
*
* static RegisterPass<MyPass> X("my-pass");
*
* where `MyPass` is the class of your pass and "my-pass" is its name. This
* registers the pass with the `PreprocessingPassRegistry`.
*/
template <class T>
class RegisterPass
{
public:
/**
* Creates a new preprocessing pass registration.
*
* @param name The name that should be associated with the preprocessing pass
*/
RegisterPass(const std::string& name)
{
PreprocessingPassRegistry::getInstance().registerPassInfo(name, callCtor);
}
/**
* This method is used by the `PreprocessingPassRegistry` to create a new
* instance of the preprocessing pass T.
*
* @param ppCtx The preprocessing pass context passed to the constructor of
* the preprocessing pass
*/
static PreprocessingPass* callCtor(PreprocessingPassContext* ppCtx)
{
return new T(ppCtx);
}
}; // class RegisterPass
} // namespace preprocessing
} // namespace CVC4
#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */
|
