Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/preprocessing_pass_registry.cpp	Lines:	56	56	100.0 %
Date:	2021-08-20	Branches:	152	314	48.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andres Noetzli, Yoni Zohar, Justin Xu
 *
 * 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 "preprocessing/preprocessing_pass_registry.h"

#include <algorithm>
#include <utility>

#include "base/check.h"
#include "base/map_util.h"
#include "base/output.h"
#include "preprocessing/passes/ackermann.h"
#include "preprocessing/passes/apply_substs.h"
#include "preprocessing/passes/bool_to_bv.h"
#include "preprocessing/passes/bv_abstraction.h"
#include "preprocessing/passes/bv_eager_atoms.h"
#include "preprocessing/passes/bv_gauss.h"
#include "preprocessing/passes/bv_intro_pow2.h"
#include "preprocessing/passes/bv_to_bool.h"
#include "preprocessing/passes/bv_to_int.h"
#include "preprocessing/passes/extended_rewriter_pass.h"
#include "preprocessing/passes/foreign_theory_rewrite.h"
#include "preprocessing/passes/fun_def_fmf.h"
#include "preprocessing/passes/global_negate.h"
#include "preprocessing/passes/ho_elim.h"
#include "preprocessing/passes/int_to_bv.h"
#include "preprocessing/passes/ite_removal.h"
#include "preprocessing/passes/ite_simp.h"
#include "preprocessing/passes/learned_rewrite.h"
#include "preprocessing/passes/miplib_trick.h"
#include "preprocessing/passes/nl_ext_purify.h"
#include "preprocessing/passes/non_clausal_simp.h"
#include "preprocessing/passes/pseudo_boolean_processor.h"
#include "preprocessing/passes/quantifiers_preprocess.h"
#include "preprocessing/passes/real_to_int.h"
#include "preprocessing/passes/rewrite.h"
#include "preprocessing/passes/sep_skolem_emp.h"
#include "preprocessing/passes/sort_infer.h"
#include "preprocessing/passes/static_learning.h"
#include "preprocessing/passes/strings_eager_pp.h"
#include "preprocessing/passes/sygus_inference.h"
#include "preprocessing/passes/synth_rew_rules.h"
#include "preprocessing/passes/theory_preprocess.h"
#include "preprocessing/passes/theory_rewrite_eq.h"
#include "preprocessing/passes/unconstrained_simplifier.h"
#include "preprocessing/preprocessing_pass.h"

namespace cvc5 {
namespace preprocessing {

using namespace cvc5::preprocessing::passes;

PreprocessingPassRegistry& PreprocessingPassRegistry::getInstance()
{
  static PreprocessingPassRegistry* ppReg = new PreprocessingPassRegistry();
  return *ppReg;
}

void PreprocessingPassRegistry::registerPassInfo(
    const std::string& name,
    std::function<PreprocessingPass*(PreprocessingPassContext*)> ctor)
{
  AlwaysAssert(!ContainsKey(d_ppInfo, name));
  d_ppInfo[name] = ctor;
}

PreprocessingPass* PreprocessingPassRegistry::createPass(
    PreprocessingPassContext* ppCtx, const std::string& name)
{
  return d_ppInfo[name](ppCtx);
}

std::vector<std::string> PreprocessingPassRegistry::getAvailablePasses()
{
  std::vector<std::string> passes;
  for (const auto& info : d_ppInfo)
  {
    passes.push_back(info.first);
  }
  std::sort(passes.begin(), passes.end());
  return passes;
}

bool PreprocessingPassRegistry::hasPass(const std::string& name)
{
  return d_ppInfo.find(name) != d_ppInfo.end();
}

namespace {

/**
 * This method is stored by the `PreprocessingPassRegistry` and used to create
 * a new instance of the preprocessing pass T.
 *
 * @param ppCtx The preprocessing pass context passed to the constructor of
 *              the preprocessing pass
 */
template <class T>
PreprocessingPass* callCtor(PreprocessingPassContext* ppCtx)
{
  return new T(ppCtx);
}

}  // namespace

PreprocessingPassRegistry::PreprocessingPassRegistry()
{
  registerPassInfo("apply-substs", callCtor<ApplySubsts>);
  registerPassInfo("bv-gauss", callCtor<BVGauss>);
  registerPassInfo("static-learning", callCtor<StaticLearning>);
  registerPassInfo("ite-simp", callCtor<ITESimp>);
  registerPassInfo("global-negate", callCtor<GlobalNegate>);
  registerPassInfo("int-to-bv", callCtor<IntToBV>);
  registerPassInfo("bv-to-int", callCtor<BVToInt>);
  registerPassInfo("learned-rewrite", callCtor<LearnedRewrite>);
  registerPassInfo("foreign-theory-rewrite", callCtor<ForeignTheoryRewrite>);
  registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>);
  registerPassInfo("real-to-int", callCtor<RealToInt>);
  registerPassInfo("sygus-infer", callCtor<SygusInference>);
  registerPassInfo("bv-to-bool", callCtor<BVToBool>);
  registerPassInfo("bv-intro-pow2", callCtor<BvIntroPow2>);
  registerPassInfo("sort-inference", callCtor<SortInferencePass>);
  registerPassInfo("sep-skolem-emp", callCtor<SepSkolemEmp>);
  registerPassInfo("rewrite", callCtor<Rewrite>);
  registerPassInfo("bv-abstraction", callCtor<BvAbstraction>);
  registerPassInfo("bv-eager-atoms", callCtor<BvEagerAtoms>);
  registerPassInfo("pseudo-boolean-processor",
                   callCtor<PseudoBooleanProcessor>);
  registerPassInfo("unconstrained-simplifier",
                   callCtor<UnconstrainedSimplifier>);
  registerPassInfo("quantifiers-preprocess", callCtor<QuantifiersPreprocess>);
  registerPassInfo("ite-removal", callCtor<IteRemoval>);
  registerPassInfo("miplib-trick", callCtor<MipLibTrick>);
  registerPassInfo("non-clausal-simp", callCtor<NonClausalSimp>);
  registerPassInfo("ackermann", callCtor<Ackermann>);
  registerPassInfo("ext-rew-pre", callCtor<ExtRewPre>);
  registerPassInfo("theory-preprocess", callCtor<TheoryPreprocess>);
  registerPassInfo("nl-ext-purify", callCtor<NlExtPurify>);
  registerPassInfo("bool-to-bv", callCtor<BoolToBV>);
  registerPassInfo("ho-elim", callCtor<HoElim>);
  registerPassInfo("fun-def-fmf", callCtor<FunDefFmf>);
  registerPassInfo("theory-rewrite-eq", callCtor<TheoryRewriteEq>);
  registerPassInfo("strings-eager-pp", callCtor<StringsEagerPp>);
}

}  // namespace preprocessing
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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