Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds
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 : : * Equality engine manager for central equality engine architecture
14 : : */
15 : :
16 : : #include "theory/ee_manager_central.h"
17 : :
18 : : #include "options/arith_options.h"
19 : : #include "options/theory_options.h"
20 : : #include "smt/env.h"
21 : : #include "theory/quantifiers_engine.h"
22 : : #include "theory/shared_solver.h"
23 : : #include "theory/theory_engine.h"
24 : : #include "theory/theory_state.h"
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : :
29 : 59 : EqEngineManagerCentral::EqEngineManagerCentral(Env& env,
30 : : TheoryEngine& te,
31 : 59 : SharedSolver& shs)
32 : : : EqEngineManager(env, te, shs),
33 : : d_masterEENotify(nullptr),
34 : : d_masterEqualityEngine(nullptr),
35 : : d_centralEENotify(*this),
36 : : d_centralEqualityEngine(
37 : 59 : env, context(), d_centralEENotify, "central::ee", true)
38 : : {
39 : 885 : for (TheoryId theoryId = theory::THEORY_FIRST;
40 [ + + ]: 885 : theoryId != theory::THEORY_LAST;
41 : 826 : ++theoryId)
42 : : {
43 : 826 : d_theoryNotify[theoryId] = nullptr;
44 : : }
45 [ + + ]: 59 : if (env.isTheoryProofProducing())
46 : : {
47 : : d_centralPfee =
48 : 31 : std::make_unique<eq::ProofEqEngine>(env, d_centralEqualityEngine);
49 : 31 : d_centralEqualityEngine.setProofEqualityEngine(d_centralPfee.get());
50 : : }
51 : 59 : }
52 : :
53 : 118 : EqEngineManagerCentral::~EqEngineManagerCentral() {}
54 : :
55 : 59 : void EqEngineManagerCentral::initializeTheories()
56 : : {
57 : 59 : context::Context* c = context();
58 : : // initialize the shared solver
59 : 118 : EeSetupInfo esis;
60 [ + - ]: 59 : if (d_sharedSolver.needsEqualityEngine(esis))
61 : : {
62 : : // the shared solver uses central equality engine
63 : 59 : d_sharedSolver.setEqualityEngine(&d_centralEqualityEngine);
64 : : }
65 : : else
66 : : {
67 : 0 : Unreachable() << "Expected shared solver to use equality engine";
68 : : }
69 : : // whether to use master equality engine as central
70 : 59 : bool masterEqToCentral = true;
71 : : // setup info for each theory
72 : 118 : std::map<TheoryId, EeSetupInfo> esiMap;
73 : : // set of theories that need equality engines
74 : 118 : std::unordered_set<TheoryId> eeTheories;
75 : 59 : const LogicInfo& linfo = logicInfo();
76 : 885 : for (TheoryId theoryId = theory::THEORY_FIRST;
77 [ + + ]: 885 : theoryId != theory::THEORY_LAST;
78 : 826 : ++theoryId)
79 : : {
80 : 826 : Theory* t = d_te.theoryOf(theoryId);
81 [ - + ]: 826 : if (t == nullptr)
82 : : {
83 : : // theory not active, skip
84 : 0 : continue;
85 : : }
86 [ + + ]: 826 : if (!t->needsEqualityEngine(esiMap[theoryId]))
87 : : {
88 : : // theory said it doesn't need an equality engine, skip
89 : 118 : continue;
90 : : }
91 : : // otherwise add it to the set of equality engine theories
92 : 708 : eeTheories.insert(theoryId);
93 : : // if the logic has a theory that does not use central equality engine,
94 : : // we can't use the central equality engine for the master equality
95 : : // engine
96 [ + - ]: 649 : if (theoryId != THEORY_QUANTIFIERS && linfo.isTheoryEnabled(theoryId)
97 [ + + ][ + + ]: 1357 : && !usesCentralEqualityEngine(options(), theoryId))
[ + + ]
98 : : {
99 [ + - ]: 118 : Trace("ee-central") << "Must use separate master equality engine due to "
100 : 59 : << theoryId << std::endl;
101 : 59 : masterEqToCentral = false;
102 : : }
103 : : }
104 : :
105 : : // initialize the master equality engine, which may be the central equality
106 : : // engine
107 [ + - ]: 59 : if (linfo.isQuantified())
108 : : {
109 : : // construct the master equality engine
110 [ - + ][ - + ]: 59 : Assert(d_masterEqualityEngine == nullptr);
[ - - ]
111 : 59 : QuantifiersEngine* qe = d_te.getQuantifiersEngine();
112 [ - + ][ - + ]: 59 : Assert(qe != nullptr);
[ - - ]
113 : 59 : d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe));
114 [ + - ]: 59 : if (!masterEqToCentral)
115 : : {
116 : 118 : d_masterEqualityEngineAlloc = std::make_unique<eq::EqualityEngine>(
117 : 118 : d_env, c, *d_masterEENotify.get(), "master::ee", false);
118 : 59 : d_masterEqualityEngine = d_masterEqualityEngineAlloc.get();
119 : : }
120 : : else
121 : : {
122 [ - - ]: 0 : Trace("ee-central")
123 : 0 : << "Master equality engine is the central equality engine"
124 : 0 : << std::endl;
125 : 0 : d_masterEqualityEngine = &d_centralEqualityEngine;
126 : 0 : d_centralEENotify.d_newClassNotify.push_back(d_masterEENotify.get());
127 : : }
128 : : }
129 : :
130 : : // allocate equality engines per theory
131 : 885 : for (TheoryId theoryId = theory::THEORY_FIRST;
132 [ + + ]: 885 : theoryId != theory::THEORY_LAST;
133 : 826 : ++theoryId)
134 : : {
135 [ + - ]: 1652 : Trace("ee-central") << "Setup equality engine for " << theoryId
136 : 826 : << std::endl;
137 : : // always allocate an object in d_einfo here
138 : 826 : EeTheoryInfo& eet = d_einfo[theoryId];
139 [ + + ]: 826 : if (eeTheories.find(theoryId) == eeTheories.end())
140 : : {
141 [ + - ]: 236 : Trace("ee-central") << "..." << theoryId << " does not need ee"
142 : 118 : << std::endl;
143 : 767 : continue;
144 : : }
145 : 708 : Theory* t = d_te.theoryOf(theoryId);
146 [ - + ][ - + ]: 708 : Assert(t != nullptr);
[ - - ]
147 [ - + ][ - + ]: 708 : Assert(esiMap.find(theoryId) != esiMap.end());
[ - - ]
148 : 708 : EeSetupInfo& esi = esiMap[theoryId];
149 [ + + ]: 708 : if (esi.d_useMaster)
150 : : {
151 [ + - ]: 59 : Trace("ee-central") << "...uses master" << std::endl;
152 : : // the theory said it wants to use the master equality engine
153 : 59 : eet.d_usedEe = d_masterEqualityEngine;
154 : 59 : continue;
155 : : }
156 : : // set the notify
157 : 649 : eq::EqualityEngineNotify* notify = esi.d_notify;
158 : 649 : d_theoryNotify[theoryId] = notify;
159 : : // split on whether integrated, or whether asked for master
160 [ + + ]: 649 : if (usesCentralEqualityEngine(options(), t->getId()))
161 : : {
162 [ + - ]: 590 : Trace("ee-central") << "...uses central" << std::endl;
163 : : // the theory uses the central equality engine
164 : 590 : eet.d_usedEe = &d_centralEqualityEngine;
165 [ + - ]: 590 : if (linfo.isTheoryEnabled(theoryId))
166 : : {
167 : : // add to vectors for the kinds of notifications
168 [ + + ]: 590 : if (esi.needsNotifyNewClass())
169 : : {
170 : 236 : d_centralEENotify.d_newClassNotify.push_back(notify);
171 : : }
172 [ + + ]: 590 : if (esi.needsNotifyMerge())
173 : : {
174 : 295 : d_centralEENotify.d_mergeNotify.push_back(notify);
175 : : }
176 [ + + ]: 590 : if (esi.needsNotifyDisequal())
177 : : {
178 : 118 : d_centralEENotify.d_disequalNotify.push_back(notify);
179 : : }
180 : : }
181 : 590 : continue;
182 : : }
183 [ + - ]: 59 : Trace("ee-central") << "...uses new" << std::endl;
184 : 59 : eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
185 : : // the theory uses the equality engine
186 : 59 : eet.d_usedEe = eet.d_allocEe.get();
187 [ + - ]: 59 : if (!masterEqToCentral)
188 : : {
189 : : // set the master equality engine of the theory's equality engine
190 : 59 : eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine);
191 : : }
192 : : }
193 : :
194 : : // set the master equality engine of the theory's equality engine
195 [ + - ]: 59 : if (!masterEqToCentral)
196 : : {
197 : 59 : d_centralEqualityEngine.setMasterEqualityEngine(d_masterEqualityEngine);
198 : : }
199 : 59 : }
200 : :
201 : 15264 : bool EqEngineManagerCentral::usesCentralEqualityEngine(const Options& opts,
202 : : TheoryId id)
203 : : {
204 [ - + ][ - + ]: 15264 : Assert(opts.theory.eeMode == options::EqEngineMode::CENTRAL);
[ - - ]
205 [ + + ]: 15264 : if (id == THEORY_BUILTIN)
206 : : {
207 : 2162 : return true;
208 : : }
209 [ + + ]: 13102 : if (id == THEORY_ARITH)
210 : : {
211 : : // conditional on whether we are using the equality solver
212 : 3012 : return opts.arith.arithEqSolver;
213 : : }
214 [ + + ][ + + ]: 9373 : return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS
215 [ + + ][ + + ]: 6737 : || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS
[ + + ]
216 [ + + ][ + + ]: 19463 : || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV;
[ + + ][ + + ]
217 : : }
218 : :
219 : 0 : void EqEngineManagerCentral::notifyBuildingModel() {}
220 : :
221 : 59 : EqEngineManagerCentral::CentralNotifyClass::CentralNotifyClass(
222 : 59 : EqEngineManagerCentral& eemc)
223 : 59 : : d_eemc(eemc), d_mNotify(nullptr), d_quantEngine(nullptr)
224 : : {
225 : 59 : }
226 : :
227 : 3402 : bool EqEngineManagerCentral::CentralNotifyClass::eqNotifyTriggerPredicate(
228 : : TNode predicate, bool value)
229 : : {
230 [ + - ]: 6804 : Trace("eem-central") << "eqNotifyTriggerPredicate: " << predicate
231 : 3402 : << std::endl;
232 : 3402 : return d_eemc.eqNotifyTriggerPredicate(predicate, value);
233 : : }
234 : :
235 : 3628 : bool EqEngineManagerCentral::CentralNotifyClass::eqNotifyTriggerTermEquality(
236 : : TheoryId tag, TNode t1, TNode t2, bool value)
237 : : {
238 [ + - ]: 7256 : Trace("eem-central") << "eqNotifyTriggerTermEquality: " << t1 << " " << t2
239 : 3628 : << value << ", tag = " << tag << std::endl;
240 : 3628 : return d_eemc.eqNotifyTriggerTermEquality(tag, t1, t2, value);
241 : : }
242 : :
243 : 21 : void EqEngineManagerCentral::CentralNotifyClass::eqNotifyConstantTermMerge(
244 : : TNode t1, TNode t2)
245 : : {
246 [ + - ]: 42 : Trace("eem-central") << "eqNotifyConstantTermMerge: " << t1 << " " << t2
247 : 21 : << std::endl;
248 : 21 : d_eemc.eqNotifyConstantTermMerge(t1, t2);
249 : 21 : }
250 : :
251 : 4201 : void EqEngineManagerCentral::CentralNotifyClass::eqNotifyNewClass(TNode t)
252 : : {
253 [ + - ]: 4201 : Trace("eem-central") << "...eqNotifyNewClass " << t << std::endl;
254 : : // notify all theories that have new equivalence class notifications
255 [ + + ]: 21005 : for (eq::EqualityEngineNotify* notify : d_newClassNotify)
256 : : {
257 : 16804 : notify->eqNotifyNewClass(t);
258 : : }
259 : 4201 : }
260 : :
261 : 5905 : void EqEngineManagerCentral::CentralNotifyClass::eqNotifyMerge(TNode t1,
262 : : TNode t2)
263 : : {
264 [ + - ]: 5905 : Trace("eem-central") << "...eqNotifyMerge " << t1 << ", " << t2 << std::endl;
265 : : // notify all theories that have merge notifications
266 [ + + ]: 35430 : for (eq::EqualityEngineNotify* notify : d_mergeNotify)
267 : : {
268 : 29525 : notify->eqNotifyMerge(t1, t2);
269 : : }
270 : 5905 : }
271 : :
272 : 514 : void EqEngineManagerCentral::CentralNotifyClass::eqNotifyDisequal(TNode t1,
273 : : TNode t2,
274 : : TNode reason)
275 : : {
276 [ + - ]: 1028 : Trace("eem-central") << "...eqNotifyDisequal " << t1 << ", " << t2
277 : 514 : << std::endl;
278 : : // notify all theories that have disequal notifications
279 [ + + ]: 1542 : for (eq::EqualityEngineNotify* notify : d_disequalNotify)
280 : : {
281 : 1028 : notify->eqNotifyDisequal(t1, t2, reason);
282 : : }
283 : 514 : }
284 : :
285 : 3402 : bool EqEngineManagerCentral::eqNotifyTriggerPredicate(TNode predicate,
286 : : bool value)
287 : : {
288 : : // always propagate with the shared solver
289 [ + - ]: 6804 : Trace("eem-central") << "...propagate " << predicate << ", " << value
290 : 3402 : << " with shared solver" << std::endl;
291 : 3402 : return d_sharedSolver.propagateLit(predicate, value);
292 : : }
293 : :
294 : 3628 : bool EqEngineManagerCentral::eqNotifyTriggerTermEquality(TheoryId tag,
295 : : TNode a,
296 : : TNode b,
297 : : bool value)
298 : : {
299 : : // propagate to theory engine
300 : 3628 : bool ok = d_sharedSolver.propagateLit(a.eqNode(b), value);
301 [ + + ]: 3628 : if (!ok)
302 : : {
303 : 18 : return false;
304 : : }
305 : : // no need to propagate shared term equalities to the UF theory
306 [ + + ]: 3610 : if (tag == THEORY_UF)
307 : : {
308 : 1312 : return true;
309 : : }
310 : : // propagate shared equality
311 : 2298 : return d_sharedSolver.propagateSharedEquality(tag, a, b, value);
312 : : }
313 : :
314 : 21 : void EqEngineManagerCentral::eqNotifyConstantTermMerge(TNode t1, TNode t2)
315 : : {
316 : 42 : Node lit = t1.eqNode(t2);
317 : 42 : TrustNode conflict;
318 [ + + ]: 21 : if (d_centralPfee != nullptr)
319 : : {
320 : 12 : conflict = d_centralPfee->assertConflict(lit);
321 : : }
322 : : else
323 : : {
324 : 9 : Node conf = d_centralEqualityEngine.mkExplainLit(lit);
325 : 9 : conflict = TrustNode::mkTrustConflict(conf);
326 : : }
327 [ + - ]: 42 : Trace("eem-central") << "...explained conflict of " << lit << " ... "
328 : 21 : << conflict << std::endl;
329 : 21 : d_sharedSolver.sendConflict(conflict, InferenceId::EQ_CONSTANT_MERGE);
330 : 42 : return;
331 : : }
332 : :
333 : : } // namespace theory
334 : : } // namespace cvc5::internal
|
