blob: 06f8a4212ef755f87064f393006d5a1fc759f61a (
plain)
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
|
/******************************************************************************
* Top contributors (to current version):
* Andres Noetzli, Justin Xu, Mathias Preiner
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 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.
* ****************************************************************************
*
* The preprocessing pass registry
*
* This file defines the classes PreprocessingPassRegistry, which keeps track
* of the available preprocessing passes.
*/
#include "cvc5_private.h"
#ifndef CVC5__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
#define CVC5__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
#include <functional>
#include <string>
#include <unordered_map>
namespace cvc5 {
namespace preprocessing {
class PreprocessingPass;
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:
/**
* Private constructor for the preprocessing pass registry. The
* registry is a singleton and no other instance should be created.
*/
PreprocessingPassRegistry();
/**
* 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
} // namespace preprocessing
} // namespace cvc5
#endif /* CVC5__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */
|