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