Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Class for initializing the modules of quantifiers engine.
11 : : */
12 : :
13 : : #include "theory/quantifiers/quantifiers_modules.h"
14 : :
15 : : #include "options/quantifiers_options.h"
16 : : #include "options/strings_options.h"
17 : : #include "theory/quantifiers/relevant_domain.h"
18 : : #include "theory/quantifiers/term_registry.h"
19 : :
20 : : namespace cvc5::internal {
21 : : namespace theory {
22 : : namespace quantifiers {
23 : :
24 : 43524 : QuantifiersModules::QuantifiersModules()
25 : 43524 : : d_rel_dom(nullptr),
26 : 43524 : d_alpha_equiv(nullptr),
27 : 43524 : d_inst_engine(nullptr),
28 : 43524 : d_model_engine(nullptr),
29 : 43524 : d_bint(nullptr),
30 : 43524 : d_qcf(nullptr),
31 : 43524 : d_sg_gen(nullptr),
32 : 43524 : d_synth_e(nullptr),
33 : 43524 : d_fs(nullptr),
34 : 43524 : d_ipool(nullptr),
35 : 43524 : d_i_cbqi(nullptr),
36 : 43524 : d_qsplit(nullptr),
37 : 87048 : d_sygus_inst(nullptr)
38 : : {
39 : 43524 : }
40 : 43190 : QuantifiersModules::~QuantifiersModules() {}
41 : 43524 : void QuantifiersModules::initialize(Env& env,
42 : : QuantifiersState& qs,
43 : : QuantifiersInferenceManager& qim,
44 : : QuantifiersRegistry& qr,
45 : : TermRegistry& tr,
46 : : QModelBuilder* builder,
47 : : std::vector<QuantifiersModule*>& modules)
48 : : {
49 : : // add quantifiers modules
50 : 43524 : const Options& options = env.getOptions();
51 [ + + ]: 43524 : if (options.quantifiers.conflictBasedInst)
52 : : {
53 : 30122 : d_qcf.reset(new QuantConflictFind(env, qs, qim, qr, tr));
54 : 30122 : modules.push_back(d_qcf.get());
55 : : }
56 [ + + ]: 43524 : if (options.quantifiers.quantSubCbqi)
57 : : {
58 : 14 : d_issc.reset(new InstStrategySubConflict(env, qs, qim, qr, tr));
59 : 14 : modules.push_back(d_issc.get());
60 : : }
61 [ + + ]: 43524 : if (options.quantifiers.conjectureGen)
62 : : {
63 : 68 : d_sg_gen.reset(new ConjectureGenerator(env, qs, qim, qr, tr));
64 : 68 : modules.push_back(d_sg_gen.get());
65 : : }
66 [ + + ]: 43524 : if (options.quantifiers.eMatching)
67 : : {
68 : 42834 : d_inst_engine.reset(new InstantiationEngine(env, qs, qim, qr, tr));
69 : 42834 : modules.push_back(d_inst_engine.get());
70 : : }
71 [ + + ]: 43524 : if (options.quantifiers.cegqi)
72 : : {
73 : 43219 : d_i_cbqi.reset(new InstStrategyCegqi(env, qs, qim, qr, tr));
74 : 43219 : modules.push_back(d_i_cbqi.get());
75 : 43219 : qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
76 : : }
77 [ + + ]: 43524 : if (options.quantifiers.sygus)
78 : : {
79 : 6232 : d_synth_e.reset(new SynthEngine(env, qs, qim, qr, tr));
80 : 6232 : modules.push_back(d_synth_e.get());
81 : : }
82 : : // bounded integer instantiation is used when the user requests it via
83 : : // fmfBound, or if strings are enabled.
84 [ + + ][ + + ]: 43524 : if (options.quantifiers.fmfBound || options.strings.stringExp)
85 : : {
86 : 31947 : d_bint.reset(new BoundedIntegers(env, qs, qim, qr, tr));
87 : 31947 : modules.push_back(d_bint.get());
88 : : }
89 : :
90 [ + + ][ + + ]: 43524 : if (options.quantifiers.finiteModelFind || options.quantifiers.fmfBound
91 [ + + ]: 42556 : || options.strings.stringExp)
92 : : {
93 : 32093 : d_model_engine.reset(new ModelEngine(env, qs, qim, qr, tr, builder));
94 : 32093 : modules.push_back(d_model_engine.get());
95 : : }
96 [ + + ]: 43524 : if (options.quantifiers.quantDynamicSplit != options::QuantDSplitMode::NONE)
97 : : {
98 : 40353 : d_qsplit.reset(new QuantDSplit(env, qs, qim, qr, tr));
99 : 40353 : modules.push_back(d_qsplit.get());
100 : : }
101 [ + - ]: 43524 : if (options.quantifiers.quantAlphaEquiv)
102 : : {
103 : 43524 : d_alpha_equiv.reset(new AlphaEquivalence(env));
104 : : }
105 : : // full saturation : instantiate from relevant domain, then arbitrary terms
106 [ + + ][ + + ]: 43524 : if (options.quantifiers.enumInst || options.quantifiers.enumInstInterleave)
107 : : {
108 : 337 : d_rel_dom.reset(new RelevantDomain(env, qs, qr, tr));
109 : 337 : d_fs.reset(new InstStrategyEnum(env, qs, qim, qr, tr, d_rel_dom.get()));
110 : 337 : modules.push_back(d_fs.get());
111 : : }
112 [ + - ]: 43524 : if (options.quantifiers.poolInst)
113 : : {
114 : 43524 : d_ipool.reset(new InstStrategyPool(env, qs, qim, qr, tr));
115 : 43524 : modules.push_back(d_ipool.get());
116 : : }
117 [ + + ]: 43524 : if (options.quantifiers.sygusInst)
118 : : {
119 : 153 : d_sygus_inst.reset(new SygusInst(env, qs, qim, qr, tr));
120 : 153 : modules.push_back(d_sygus_inst.get());
121 : : }
122 [ + + ]: 43524 : if (options.quantifiers.mbqi)
123 : : {
124 : 781 : d_mbqi.reset(new InstStrategyMbqi(env, qs, qim, qr, tr));
125 : 781 : modules.push_back(d_mbqi.get());
126 : : }
127 [ + + ]: 43524 : if (options.quantifiers.oracles)
128 : : {
129 : 535 : d_oracleEngine.reset(new OracleEngine(env, qs, qim, qr, tr));
130 : 535 : modules.push_back(d_oracleEngine.get());
131 : : }
132 : 43524 : }
133 : :
134 : : } // namespace quantifiers
135 : : } // namespace theory
136 : : } // namespace cvc5::internal
|
