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 : : * [[ Add lengthier description here ]]
11 : : * \todo document this file
12 : : */
13 : :
14 : : #include "theory/shared_terms_database.h"
15 : :
16 : : #include "options/theory_options.h"
17 : : #include "theory/theory_engine.h"
18 : :
19 : : using namespace std;
20 : : using namespace cvc5::internal::theory;
21 : :
22 : : namespace cvc5::internal {
23 : :
24 : 28700 : SharedTermsDatabase::SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine)
25 : : : EnvObj(env),
26 : : ContextNotifyObj(env.getContext()),
27 : : d_statSharedTerms(
28 : 28700 : statisticsRegistry().registerInt("theory::shared_terms")),
29 : 28700 : d_addedSharedTermsSize(env.getContext(), 0),
30 : 28700 : d_termsToTheories(env.getContext()),
31 : 28700 : d_alreadyNotifiedMap(env.getContext()),
32 : 28700 : d_registeredEqualities(env.getContext()),
33 : 28700 : d_EENotify(*this),
34 : 28700 : d_theoryEngine(theoryEngine),
35 : 28700 : d_inConflict(env.getContext(), false),
36 : 28700 : d_conflictPolarity(),
37 : 28700 : d_equalityEngine(nullptr),
38 : 28700 : d_pfee(nullptr),
39 : 86100 : d_out(theoryEngine->theoryOf(THEORY_BUILTIN)->getOutputChannel())
40 : : {
41 : 28700 : }
42 : :
43 : 28700 : void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
44 : : {
45 [ - + ][ - + ]: 28700 : Assert(ee != nullptr);
[ - - ]
46 : 28700 : d_equalityEngine = ee;
47 : : // if proofs are enabled, make the proof equality engine if necessary
48 [ + + ]: 28700 : if (d_env.isTheoryProofProducing())
49 : : {
50 : 8688 : d_pfee = d_equalityEngine->getProofEqualityEngine();
51 [ + + ]: 8688 : if (d_pfee == nullptr)
52 : : {
53 : 8660 : d_pfeeAlloc = std::make_unique<eq::ProofEqEngine>(d_env, *ee);
54 : 8660 : d_pfee = d_pfeeAlloc.get();
55 : 8660 : d_equalityEngine->setProofEqualityEngine(d_pfee);
56 : : }
57 : : }
58 : 28700 : }
59 : :
60 : 28700 : bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi)
61 : : {
62 : 28700 : esi.d_notify = &d_EENotify;
63 : 28700 : esi.d_name = "shared::ee";
64 : 28700 : return true;
65 : : }
66 : :
67 : 943722 : void SharedTermsDatabase::addEqualityToPropagate(TNode equality)
68 : : {
69 [ - + ][ - + ]: 943722 : Assert(d_equalityEngine != nullptr);
[ - - ]
70 : 943722 : d_registeredEqualities.insert(equality);
71 [ + + ]: 943722 : if (d_theoryEngine->hasSatValue(equality))
72 : : {
73 : : // don't need to propagate what is already asserted
74 : 18260 : return;
75 : : }
76 : 925462 : d_equalityEngine->addTriggerPredicate(equality);
77 : 925462 : checkForConflict();
78 : : }
79 : :
80 : 2817938 : void SharedTermsDatabase::addSharedTerm(TNode atom,
81 : : TNode term,
82 : : TheoryIdSet theories)
83 : : {
84 [ + - ]: 5635876 : Trace("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", "
85 [ - + ][ - - ]: 2817938 : << term << ", " << TheoryIdSetUtil::setToString(theories)
86 : 2817938 : << ")" << std::endl;
87 : :
88 : 2817938 : std::pair<TNode, TNode> search_pair(atom, term);
89 : 2817938 : SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
90 [ + + ]: 2817938 : if (find == d_termsToTheories.end())
91 : : {
92 : : // First time for this term and this atom
93 : 2798687 : d_atomsToTerms[atom].push_back(term);
94 : 2798687 : d_addedSharedTerms.push_back(atom);
95 : 2798687 : d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
96 : 2798687 : d_termsToTheories[search_pair] = theories;
97 : : }
98 : : else
99 : : {
100 [ - + ][ - + ]: 19251 : Assert(theories != (*find).second);
[ - - ]
101 : 38502 : d_termsToTheories[search_pair] =
102 : 57753 : TheoryIdSetUtil::setUnion(theories, (*find).second);
103 : : }
104 : 2817938 : }
105 : :
106 : 11686843 : SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::begin(
107 : : TNode atom) const
108 : : {
109 [ - + ][ - + ]: 11686843 : Assert(hasSharedTerms(atom));
[ - - ]
110 : 11686843 : return d_atomsToTerms.find(atom)->second.begin();
111 : : }
112 : :
113 : 11686843 : SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::end(
114 : : TNode atom) const
115 : : {
116 [ - + ][ - + ]: 11686843 : Assert(hasSharedTerms(atom));
[ - - ]
117 : 11686843 : return d_atomsToTerms.find(atom)->second.end();
118 : : }
119 : :
120 : 40894266 : bool SharedTermsDatabase::hasSharedTerms(TNode atom) const
121 : : {
122 : 40894266 : return d_atomsToTerms.find(atom) != d_atomsToTerms.end();
123 : : }
124 : :
125 : 8964581 : void SharedTermsDatabase::backtrack()
126 : : {
127 : 11763165 : for (int i = d_addedSharedTerms.size() - 1,
128 : 8964581 : i_end = (int)d_addedSharedTermsSize;
129 [ + + ]: 11763165 : i >= i_end;
130 : : --i)
131 : : {
132 : 2798584 : TNode atom = d_addedSharedTerms[i];
133 : 2798584 : shared_terms_list& list = d_atomsToTerms[atom];
134 : 2798584 : list.pop_back();
135 [ + + ]: 2798584 : if (list.empty())
136 : : {
137 : 1018803 : d_atomsToTerms.erase(atom);
138 : : }
139 : 2798584 : }
140 : 8964581 : d_addedSharedTerms.resize(d_addedSharedTermsSize);
141 : 8964581 : }
142 : :
143 : 34139078 : TheoryIdSet SharedTermsDatabase::getTheoriesToNotify(TNode atom,
144 : : TNode term) const
145 : : {
146 : : // Get the theories that share this term from this atom
147 : 34139078 : std::pair<TNode, TNode> search_pair(atom, term);
148 : 34139078 : SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
149 [ - + ][ - + ]: 34139078 : Assert(find != d_termsToTheories.end());
[ - - ]
150 : :
151 : : // Get the theories that were already notified
152 : 34139078 : TheoryIdSet alreadyNotified = 0;
153 : 34139078 : AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
154 [ + + ]: 34139078 : if (theoriesFind != d_alreadyNotifiedMap.end())
155 : : {
156 : 32218716 : alreadyNotified = (*theoriesFind).second;
157 : : }
158 : :
159 : : // Return the ones that haven't been notified yet
160 : 68278156 : return TheoryIdSetUtil::setDifference((*find).second, alreadyNotified);
161 : 34139078 : }
162 : :
163 : 0 : TheoryIdSet SharedTermsDatabase::getNotifiedTheories(TNode term) const
164 : : {
165 : : // Get the theories that were already notified
166 : 0 : AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
167 [ - - ]: 0 : if (theoriesFind != d_alreadyNotifiedMap.end())
168 : : {
169 : 0 : return (*theoriesFind).second;
170 : : }
171 : : else
172 : : {
173 : 0 : return 0;
174 : : }
175 : : }
176 : :
177 : 7373154 : bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory,
178 : : TNode a,
179 : : TNode b,
180 : : bool value)
181 : : {
182 [ + - ]: 14746308 : Trace("shared-terms-database")
183 : 0 : << "SharedTermsDatabase::newEquality(" << theory << "," << a << "," << b
184 [ - - ]: 7373154 : << ", " << (value ? "true" : "false") << ")" << endl;
185 : :
186 [ - + ]: 7373154 : if (d_inConflict)
187 : : {
188 : 0 : return false;
189 : : }
190 : :
191 : : // Propagate away
192 : 7373154 : Node equality = a.eqNode(b);
193 [ + + ]: 7373154 : Node equalityToPropagate = value ? equality : equality.notNode();
194 : 7373154 : d_theoryEngine->assertToTheory(
195 : : equalityToPropagate, equalityToPropagate, theory, THEORY_BUILTIN);
196 : :
197 : : // As you were
198 : 7373154 : return true;
199 : 7373154 : }
200 : :
201 : 34139077 : void SharedTermsDatabase::markNotified(TNode term, TheoryIdSet theories)
202 : : {
203 : : // Find out if there are any new theories that were notified about this term
204 : 34139077 : TheoryIdSet alreadyNotified = 0;
205 : 34139077 : AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
206 [ + + ]: 34139077 : if (theoriesFind != d_alreadyNotifiedMap.end())
207 : : {
208 : 32218716 : alreadyNotified = (*theoriesFind).second;
209 : : }
210 : : TheoryIdSet newlyNotified =
211 : 34139077 : TheoryIdSetUtil::setDifference(theories, alreadyNotified);
212 : :
213 : : // If no new theories were notified, we are done
214 [ + + ]: 34139077 : if (newlyNotified == 0)
215 : : {
216 : 32181459 : return;
217 : : }
218 : :
219 [ + - ]: 3915236 : Trace("shared-terms-database")
220 : 1957618 : << "SharedTermsDatabase::markNotified(" << term << ")" << endl;
221 : :
222 : : // First update the set of notified theories for this term
223 : 3915236 : d_alreadyNotifiedMap[term] =
224 : 1957618 : TheoryIdSetUtil::setUnion(newlyNotified, alreadyNotified);
225 : :
226 [ - + ]: 1957618 : if (d_equalityEngine == nullptr)
227 : : {
228 : : // if we are not assigned an equality engine, there is nothing to do
229 : 0 : return;
230 : : }
231 : :
232 : : // Mark the shared terms in the equality engine
233 : : theory::TheoryId currentTheory;
234 : 5878269 : while ((currentTheory = TheoryIdSetUtil::setPop(newlyNotified))
235 [ + + ]: 5878269 : != THEORY_LAST)
236 : : {
237 : 3920651 : d_equalityEngine->addTriggerTerm(term, currentTheory);
238 : : }
239 : :
240 : : // Check for any conflits
241 : 1957618 : checkForConflict();
242 : : }
243 : :
244 : 2133730 : bool SharedTermsDatabase::areEqual(TNode a, TNode b) const
245 : : {
246 [ - + ][ - + ]: 2133730 : Assert(d_equalityEngine != nullptr);
[ - - ]
247 : 2133730 : if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
248 : : {
249 : 2133730 : return d_equalityEngine->areEqual(a, b);
250 : : }
251 : : else
252 : : {
253 : 0 : Assert(d_equalityEngine->hasTerm(a) || a.isConst());
254 : 0 : Assert(d_equalityEngine->hasTerm(b) || b.isConst());
255 : : // since one (or both) of them is a constant, and the other is in the
256 : : // equality engine, they are not same
257 : 0 : return false;
258 : : }
259 : : }
260 : :
261 : 2069325 : bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const
262 : : {
263 [ - + ][ - + ]: 2069325 : Assert(d_equalityEngine != nullptr);
[ - - ]
264 : 2069325 : if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
265 : : {
266 : 2069325 : return d_equalityEngine->areDisequal(a, b, false);
267 : : }
268 : : else
269 : : {
270 : 0 : Assert(d_equalityEngine->hasTerm(a) || a.isConst());
271 : 0 : Assert(d_equalityEngine->hasTerm(b) || b.isConst());
272 : : // one (or both) are in the equality engine
273 : 0 : return false;
274 : : }
275 : : }
276 : :
277 : 0 : theory::eq::EqualityEngine* SharedTermsDatabase::getEqualityEngine()
278 : : {
279 : 0 : return d_equalityEngine;
280 : : }
281 : :
282 : 13236970 : void SharedTermsDatabase::assertShared(TNode n, bool polarity, TNode reason)
283 : : {
284 [ - + ][ - + ]: 13236970 : Assert(d_equalityEngine != nullptr);
[ - - ]
285 [ + - ]: 26473940 : Trace("shared-terms-database::assert")
286 : 0 : << "SharedTermsDatabase::assertShared(" << n << ", "
287 [ - - ]: 13236970 : << (polarity ? "true" : "false") << ", " << reason << ")" << endl;
288 : : // Add it to the equality engine
289 [ + - ]: 13236970 : if (n.getKind() == Kind::EQUAL)
290 : : {
291 : 13236970 : d_equalityEngine->assertEquality(n, polarity, reason);
292 : : }
293 : : else
294 : : {
295 : 0 : d_equalityEngine->assertPredicate(n, polarity, reason);
296 : : }
297 : : // Check for conflict
298 : 13236970 : checkForConflict();
299 : 13236970 : }
300 : :
301 : 10167233 : bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity)
302 : : {
303 [ + + ]: 10167233 : if (polarity)
304 : : {
305 : 5337708 : return d_out.propagate(equality);
306 : : }
307 : 4829525 : return d_out.propagate(equality.notNode());
308 : : }
309 : :
310 : 16120050 : void SharedTermsDatabase::checkForConflict()
311 : : {
312 [ + + ]: 16120050 : if (!d_inConflict)
313 : : {
314 : 16096569 : return;
315 : : }
316 : 23481 : d_inConflict = false;
317 : 23481 : TrustNode trnc;
318 [ + + ]: 23481 : if (d_pfee != nullptr)
319 : : {
320 : 7466 : Node conflict = d_conflictLHS.eqNode(d_conflictRHS);
321 [ + - ]: 7466 : conflict = d_conflictPolarity ? conflict : conflict.notNode();
322 : 7466 : trnc = d_pfee->assertConflict(conflict);
323 : 7466 : }
324 : : else
325 : : {
326 : : // standard explain
327 : 16015 : std::vector<TNode> assumptions;
328 : 16015 : d_equalityEngine->explainEquality(
329 : 16015 : d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions);
330 : 16015 : Node conflictNode = nodeManager()->mkAnd(assumptions);
331 : 16015 : trnc = TrustNode::mkTrustConflict(conflictNode, nullptr);
332 : 16015 : }
333 : 23481 : d_theoryEngine->conflict(
334 : : trnc, InferenceId::EQ_CONSTANT_MERGE, THEORY_BUILTIN);
335 : 23481 : d_conflictLHS = d_conflictRHS = Node::null();
336 : 23481 : }
337 : :
338 : 0 : bool SharedTermsDatabase::isKnown(TNode literal) const
339 : : {
340 : 0 : Assert(d_equalityEngine != nullptr);
341 : 0 : bool polarity = literal.getKind() != Kind::NOT;
342 [ - - ]: 0 : TNode equality = polarity ? literal : literal[0];
343 [ - - ]: 0 : if (polarity)
344 : : {
345 : 0 : return d_equalityEngine->areEqual(equality[0], equality[1]);
346 : : }
347 : : else
348 : : {
349 : 0 : return d_equalityEngine->areDisequal(equality[0], equality[1], false);
350 : : }
351 : 0 : }
352 : :
353 : 235784 : TrustNode SharedTermsDatabase::explain(TNode literal) const
354 : : {
355 [ + + ]: 235784 : if (d_pfee != nullptr)
356 : : {
357 : : // use the proof equality engine if it exists
358 : 107030 : return d_pfee->explain(literal);
359 : : }
360 : : // otherwise, explain without proofs
361 : 128754 : Node exp = d_equalityEngine->mkExplainLit(literal);
362 : : // no proof generator
363 : 128754 : return TrustNode::mkTrustPropExp(literal, exp, nullptr);
364 : 128754 : }
365 : :
366 : : } // namespace cvc5::internal
|
