Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * Class for initializing the modules of quantifiers engine.
14 : : */
15 : :
16 : : #include "theory/quantifiers/quantifiers_modules.h"
17 : :
18 : : #include "options/quantifiers_options.h"
19 : : #include "options/strings_options.h"
20 : : #include "theory/quantifiers/relevant_domain.h"
21 : : #include "theory/quantifiers/term_registry.h"
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace quantifiers {
26 : :
27 : 43830 : QuantifiersModules::QuantifiersModules()
28 : : : d_rel_dom(nullptr),
29 : : d_alpha_equiv(nullptr),
30 : : d_inst_engine(nullptr),
31 : : d_model_engine(nullptr),
32 : : d_bint(nullptr),
33 : : d_qcf(nullptr),
34 : : d_sg_gen(nullptr),
35 : : d_synth_e(nullptr),
36 : : d_fs(nullptr),
37 : : d_ipool(nullptr),
38 : : d_i_cbqi(nullptr),
39 : : d_qsplit(nullptr),
40 : 43830 : d_sygus_inst(nullptr)
41 : : {
42 : 43830 : }
43 : 43584 : QuantifiersModules::~QuantifiersModules() {}
44 : 43830 : void QuantifiersModules::initialize(Env& env,
45 : : QuantifiersState& qs,
46 : : QuantifiersInferenceManager& qim,
47 : : QuantifiersRegistry& qr,
48 : : TermRegistry& tr,
49 : : QModelBuilder* builder,
50 : : std::vector<QuantifiersModule*>& modules)
51 : : {
52 : : // add quantifiers modules
53 : 43830 : const Options& options = env.getOptions();
54 [ + + ]: 43830 : if (options.quantifiers.conflictBasedInst)
55 : : {
56 : 28625 : d_qcf.reset(new QuantConflictFind(env, qs, qim, qr, tr));
57 : 28625 : modules.push_back(d_qcf.get());
58 : : }
59 [ + + ]: 43830 : if (options.quantifiers.quantSubCbqi)
60 : : {
61 : 16 : d_issc.reset(new InstStrategySubConflict(env, qs, qim, qr, tr));
62 : 16 : modules.push_back(d_issc.get());
63 : : }
64 [ + + ]: 43830 : if (options.quantifiers.conjectureGen)
65 : : {
66 : 79 : d_sg_gen.reset(new ConjectureGenerator(env, qs, qim, qr, tr));
67 : 79 : modules.push_back(d_sg_gen.get());
68 : : }
69 [ + + ]: 43830 : if (options.quantifiers.eMatching)
70 : : {
71 : 43147 : d_inst_engine.reset(new InstantiationEngine(env, qs, qim, qr, tr));
72 : 43147 : modules.push_back(d_inst_engine.get());
73 : : }
74 [ + + ]: 43830 : if (options.quantifiers.cegqi)
75 : : {
76 : 43498 : d_i_cbqi.reset(new InstStrategyCegqi(env, qs, qim, qr, tr));
77 : 43498 : modules.push_back(d_i_cbqi.get());
78 : 43498 : qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
79 : : }
80 [ + + ]: 43830 : if (options.quantifiers.sygus)
81 : : {
82 : 7270 : d_synth_e.reset(new SynthEngine(env, qs, qim, qr, tr));
83 : 7270 : modules.push_back(d_synth_e.get());
84 : : }
85 : : // bounded integer instantiation is used when the user requests it via
86 : : // fmfBound, or if strings are enabled.
87 [ + + ][ + + ]: 43830 : if (options.quantifiers.fmfBound || options.strings.stringExp)
88 : : {
89 : 32173 : d_bint.reset(new BoundedIntegers(env, qs, qim, qr, tr));
90 : 32173 : modules.push_back(d_bint.get());
91 : : }
92 : :
93 [ + + ][ + + ]: 43830 : if (options.quantifiers.finiteModelFind || options.quantifiers.fmfBound
94 [ + + ]: 42847 : || options.strings.stringExp)
95 : : {
96 : 32316 : d_model_engine.reset(new ModelEngine(env, qs, qim, qr, tr, builder));
97 : 32316 : modules.push_back(d_model_engine.get());
98 : : }
99 [ + + ]: 43830 : if (options.quantifiers.quantDynamicSplit != options::QuantDSplitMode::NONE)
100 : : {
101 : 40665 : d_qsplit.reset(new QuantDSplit(env, qs, qim, qr, tr));
102 : 40665 : modules.push_back(d_qsplit.get());
103 : : }
104 [ + - ]: 43830 : if (options.quantifiers.quantAlphaEquiv)
105 : : {
106 : 43830 : d_alpha_equiv.reset(new AlphaEquivalence(env));
107 : : }
108 : : // full saturation : instantiate from relevant domain, then arbitrary terms
109 [ + + ][ + + ]: 43830 : if (options.quantifiers.enumInst || options.quantifiers.enumInstInterleave)
110 : : {
111 : 334 : d_rel_dom.reset(new RelevantDomain(env, qs, qr, tr));
112 : 334 : d_fs.reset(new InstStrategyEnum(env, qs, qim, qr, tr, d_rel_dom.get()));
113 : 334 : modules.push_back(d_fs.get());
114 : : }
115 [ + - ]: 43830 : if (options.quantifiers.poolInst)
116 : : {
117 : 43830 : d_ipool.reset(new InstStrategyPool(env, qs, qim, qr, tr));
118 : 43830 : modules.push_back(d_ipool.get());
119 : : }
120 [ + + ]: 43830 : if (options.quantifiers.sygusInst)
121 : : {
122 : 154 : d_sygus_inst.reset(new SygusInst(env, qs, qim, qr, tr));
123 : 154 : modules.push_back(d_sygus_inst.get());
124 : : }
125 [ + + ]: 43830 : if (options.quantifiers.mbqi)
126 : : {
127 : 517 : d_mbqi.reset(new InstStrategyMbqi(env, qs, qim, qr, tr));
128 : 517 : modules.push_back(d_mbqi.get());
129 : : }
130 [ + + ]: 43830 : if (options.quantifiers.oracles)
131 : : {
132 : 466 : d_oracleEngine.reset(new OracleEngine(env, qs, qim, qr, tr));
133 : 466 : modules.push_back(d_oracleEngine.get());
134 : : }
135 : 43830 : }
136 : :
137 : : } // namespace quantifiers
138 : : } // namespace theory
139 : : } // namespace cvc5::internal
|
