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