GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/preprocessing_pass_registry.cpp Lines: 56 56 100.0 %
Date: 2021-03-23 Branches: 152 314 48.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file preprocessing_pass_registry.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andres Noetzli, Yoni Zohar, Justin Xu
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief The preprocessing pass registry
13
 **
14
 ** This file defines the classes PreprocessingPassRegistry, which keeps track
15
 ** of the available preprocessing passes.
16
 **/
17
18
#include "preprocessing/preprocessing_pass_registry.h"
19
20
#include <algorithm>
21
#include <utility>
22
23
#include "base/check.h"
24
#include "base/map_util.h"
25
#include "base/output.h"
26
#include "preprocessing/passes/ackermann.h"
27
#include "preprocessing/passes/apply_substs.h"
28
#include "preprocessing/passes/bool_to_bv.h"
29
#include "preprocessing/passes/bv_abstraction.h"
30
#include "preprocessing/passes/bv_eager_atoms.h"
31
#include "preprocessing/passes/bv_gauss.h"
32
#include "preprocessing/passes/bv_intro_pow2.h"
33
#include "preprocessing/passes/bv_to_bool.h"
34
#include "preprocessing/passes/bv_to_int.h"
35
#include "preprocessing/passes/extended_rewriter_pass.h"
36
#include "preprocessing/passes/foreign_theory_rewrite.h"
37
#include "preprocessing/passes/fun_def_fmf.h"
38
#include "preprocessing/passes/global_negate.h"
39
#include "preprocessing/passes/ho_elim.h"
40
#include "preprocessing/passes/int_to_bv.h"
41
#include "preprocessing/passes/ite_removal.h"
42
#include "preprocessing/passes/ite_simp.h"
43
#include "preprocessing/passes/miplib_trick.h"
44
#include "preprocessing/passes/nl_ext_purify.h"
45
#include "preprocessing/passes/non_clausal_simp.h"
46
#include "preprocessing/passes/pseudo_boolean_processor.h"
47
#include "preprocessing/passes/quantifier_macros.h"
48
#include "preprocessing/passes/quantifiers_preprocess.h"
49
#include "preprocessing/passes/real_to_int.h"
50
#include "preprocessing/passes/rewrite.h"
51
#include "preprocessing/passes/sep_skolem_emp.h"
52
#include "preprocessing/passes/sort_infer.h"
53
#include "preprocessing/passes/static_learning.h"
54
#include "preprocessing/passes/strings_eager_pp.h"
55
#include "preprocessing/passes/sygus_inference.h"
56
#include "preprocessing/passes/synth_rew_rules.h"
57
#include "preprocessing/passes/theory_preprocess.h"
58
#include "preprocessing/passes/theory_rewrite_eq.h"
59
#include "preprocessing/passes/unconstrained_simplifier.h"
60
#include "preprocessing/preprocessing_pass.h"
61
62
namespace CVC4 {
63
namespace preprocessing {
64
65
using namespace CVC4::preprocessing::passes;
66
67
8998
PreprocessingPassRegistry& PreprocessingPassRegistry::getInstance()
68
{
69
8998
  static PreprocessingPassRegistry* ppReg = new PreprocessingPassRegistry();
70
8998
  return *ppReg;
71
}
72
73
201994
void PreprocessingPassRegistry::registerPassInfo(
74
    const std::string& name,
75
    std::function<PreprocessingPass*(PreprocessingPassContext*)> ctor)
76
{
77
201994
  AlwaysAssert(!ContainsKey(d_ppInfo, name));
78
201994
  d_ppInfo[name] = ctor;
79
201994
}
80
81
305898
PreprocessingPass* PreprocessingPassRegistry::createPass(
82
    PreprocessingPassContext* ppCtx, const std::string& name)
83
{
84
305898
  return d_ppInfo[name](ppCtx);
85
}
86
87
8997
std::vector<std::string> PreprocessingPassRegistry::getAvailablePasses()
88
{
89
8997
  std::vector<std::string> passes;
90
314895
  for (const auto& info : d_ppInfo)
91
  {
92
305898
    passes.push_back(info.first);
93
  }
94
8997
  std::sort(passes.begin(), passes.end());
95
8997
  return passes;
96
}
97
98
1
bool PreprocessingPassRegistry::hasPass(const std::string& name)
99
{
100
1
  return d_ppInfo.find(name) != d_ppInfo.end();
101
}
102
103
namespace {
104
105
/**
106
 * This method is stored by the `PreprocessingPassRegistry` and used to create
107
 * a new instance of the preprocessing pass T.
108
 *
109
 * @param ppCtx The preprocessing pass context passed to the constructor of
110
 *              the preprocessing pass
111
 */
112
template <class T>
113
305898
PreprocessingPass* callCtor(PreprocessingPassContext* ppCtx)
114
{
115
305898
  return new T(ppCtx);
116
}
117
118
}  // namespace
119
120
5941
PreprocessingPassRegistry::PreprocessingPassRegistry()
121
{
122
5941
  registerPassInfo("apply-substs", callCtor<ApplySubsts>);
123
5941
  registerPassInfo("bv-gauss", callCtor<BVGauss>);
124
5941
  registerPassInfo("static-learning", callCtor<StaticLearning>);
125
5941
  registerPassInfo("ite-simp", callCtor<ITESimp>);
126
5941
  registerPassInfo("global-negate", callCtor<GlobalNegate>);
127
5941
  registerPassInfo("int-to-bv", callCtor<IntToBV>);
128
5941
  registerPassInfo("bv-to-int", callCtor<BVToInt>);
129
5941
  registerPassInfo("foreign-theory-rewrite", callCtor<ForeignTheoryRewrite>);
130
5941
  registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>);
131
5941
  registerPassInfo("real-to-int", callCtor<RealToInt>);
132
5941
  registerPassInfo("sygus-infer", callCtor<SygusInference>);
133
5941
  registerPassInfo("bv-to-bool", callCtor<BVToBool>);
134
5941
  registerPassInfo("bv-intro-pow2", callCtor<BvIntroPow2>);
135
5941
  registerPassInfo("sort-inference", callCtor<SortInferencePass>);
136
5941
  registerPassInfo("sep-skolem-emp", callCtor<SepSkolemEmp>);
137
5941
  registerPassInfo("rewrite", callCtor<Rewrite>);
138
5941
  registerPassInfo("bv-abstraction", callCtor<BvAbstraction>);
139
5941
  registerPassInfo("bv-eager-atoms", callCtor<BvEagerAtoms>);
140
5941
  registerPassInfo("pseudo-boolean-processor",
141
                   callCtor<PseudoBooleanProcessor>);
142
5941
  registerPassInfo("unconstrained-simplifier",
143
                   callCtor<UnconstrainedSimplifier>);
144
5941
  registerPassInfo("quantifiers-preprocess", callCtor<QuantifiersPreprocess>);
145
5941
  registerPassInfo("ite-removal", callCtor<IteRemoval>);
146
5941
  registerPassInfo("miplib-trick", callCtor<MipLibTrick>);
147
5941
  registerPassInfo("non-clausal-simp", callCtor<NonClausalSimp>);
148
5941
  registerPassInfo("ackermann", callCtor<Ackermann>);
149
5941
  registerPassInfo("ext-rew-pre", callCtor<ExtRewPre>);
150
5941
  registerPassInfo("theory-preprocess", callCtor<TheoryPreprocess>);
151
5941
  registerPassInfo("quantifier-macros", callCtor<QuantifierMacros>);
152
5941
  registerPassInfo("nl-ext-purify", callCtor<NlExtPurify>);
153
5941
  registerPassInfo("bool-to-bv", callCtor<BoolToBV>);
154
5941
  registerPassInfo("ho-elim", callCtor<HoElim>);
155
5941
  registerPassInfo("fun-def-fmf", callCtor<FunDefFmf>);
156
5941
  registerPassInfo("theory-rewrite-eq", callCtor<TheoryRewriteEq>);
157
5941
  registerPassInfo("strings-eager-pp", callCtor<StringsEagerPp>);
158
5941
}
159
160
}  // namespace preprocessing
161
26685
}  // namespace CVC4