Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Dejan Jovanovic, Morgan Deters
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * [[ Add lengthier description here ]]
14 : : * \todo document this file
15 : : */
16 : :
17 : : #include "theory/shared_terms_database.h"
18 : :
19 : : #include "options/theory_options.h"
20 : : #include "theory/theory_engine.h"
21 : :
22 : : using namespace std;
23 : : using namespace cvc5::internal::theory;
24 : :
25 : : namespace cvc5::internal {
26 : :
27 : 49244 : SharedTermsDatabase::SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine)
28 : : : EnvObj(env),
29 : : ContextNotifyObj(env.getContext()),
30 : : d_statSharedTerms(
31 : 49244 : statisticsRegistry().registerInt("theory::shared_terms")),
32 : 0 : d_addedSharedTermsSize(env.getContext(), 0),
33 : : d_termsToTheories(env.getContext()),
34 : : d_alreadyNotifiedMap(env.getContext()),
35 : : d_registeredEqualities(env.getContext()),
36 : : d_EENotify(*this),
37 : : d_theoryEngine(theoryEngine),
38 : 0 : d_inConflict(env.getContext(), false),
39 : : d_conflictPolarity(),
40 : : d_equalityEngine(nullptr),
41 : : d_pfee(nullptr),
42 : 98488 : d_out(theoryEngine->theoryOf(THEORY_BUILTIN)->getOutputChannel())
43 : : {
44 : 49244 : }
45 : :
46 : 49244 : void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
47 : : {
48 [ - + ][ - + ]: 49244 : Assert(ee != nullptr);
[ - - ]
49 : 49244 : d_equalityEngine = ee;
50 : : // if proofs are enabled, make the proof equality engine if necessary
51 [ + + ]: 49244 : if (d_env.isTheoryProofProducing())
52 : : {
53 : 10455 : d_pfee = d_equalityEngine->getProofEqualityEngine();
54 [ + + ]: 10455 : if (d_pfee == nullptr)
55 : : {
56 : 10424 : d_pfeeAlloc = std::make_unique<eq::ProofEqEngine>(d_env, *ee);
57 : 10424 : d_pfee = d_pfeeAlloc.get();
58 : 10424 : d_equalityEngine->setProofEqualityEngine(d_pfee);
59 : : }
60 : : }
61 : 49244 : }
62 : :
63 : 49244 : bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi)
64 : : {
65 : 49244 : esi.d_notify = &d_EENotify;
66 : 49244 : esi.d_name = "shared::ee";
67 : 49244 : return true;
68 : : }
69 : :
70 : 871578 : void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
71 [ - + ][ - + ]: 871578 : Assert(d_equalityEngine != nullptr);
[ - - ]
72 : 871578 : d_registeredEqualities.insert(equality);
73 [ + + ]: 871578 : if (d_theoryEngine->hasSatValue(equality))
74 : : {
75 : : // don't need to propagate what is already asserted
76 : 16475 : return;
77 : : }
78 : 855103 : d_equalityEngine->addTriggerPredicate(equality);
79 : 855103 : checkForConflict();
80 : : }
81 : :
82 : 2379840 : void SharedTermsDatabase::addSharedTerm(TNode atom,
83 : : TNode term,
84 : : TheoryIdSet theories)
85 : : {
86 [ + - ]: 4759670 : Trace("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", "
87 [ - + ][ - - ]: 2379840 : << term << ", " << TheoryIdSetUtil::setToString(theories)
88 : 2379840 : << ")" << std::endl;
89 : :
90 : 4759670 : std::pair<TNode, TNode> search_pair(atom, term);
91 : 2379840 : SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
92 [ + + ]: 2379840 : if (find == d_termsToTheories.end()) {
93 : : // First time for this term and this atom
94 : 2374390 : d_atomsToTerms[atom].push_back(term);
95 : 2374390 : d_addedSharedTerms.push_back(atom);
96 : 2374390 : d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
97 : 2374390 : d_termsToTheories[search_pair] = theories;
98 : : } else {
99 [ - + ][ - + ]: 5449 : Assert(theories != (*find).second);
[ - - ]
100 : 10898 : d_termsToTheories[search_pair] =
101 : 16347 : TheoryIdSetUtil::setUnion(theories, (*find).second);
102 : : }
103 : 2379840 : }
104 : :
105 : 9484000 : SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::begin(TNode atom) const {
106 [ - + ][ - + ]: 9484000 : Assert(hasSharedTerms(atom));
[ - - ]
107 : 9484000 : return d_atomsToTerms.find(atom)->second.begin();
108 : : }
109 : :
110 : 9484000 : SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::end(TNode atom) const {
111 [ - + ][ - + ]: 9484000 : Assert(hasSharedTerms(atom));
[ - - ]
112 : 9484000 : return d_atomsToTerms.find(atom)->second.end();
113 : : }
114 : :
115 : 35066500 : bool SharedTermsDatabase::hasSharedTerms(TNode atom) const {
116 : 35066500 : return d_atomsToTerms.find(atom) != d_atomsToTerms.end();
117 : : }
118 : :
119 : 14778200 : void SharedTermsDatabase::backtrack() {
120 [ + + ]: 17152100 : for (int i = d_addedSharedTerms.size() - 1, i_end = (int)d_addedSharedTermsSize; i >= i_end; -- i) {
121 : 4747760 : TNode atom = d_addedSharedTerms[i];
122 : 2373880 : shared_terms_list& list = d_atomsToTerms[atom];
123 : 2373880 : list.pop_back();
124 [ + + ]: 2373880 : if (list.empty()) {
125 : 882241 : d_atomsToTerms.erase(atom);
126 : : }
127 : : }
128 : 14778200 : d_addedSharedTerms.resize(d_addedSharedTermsSize);
129 : 14778200 : }
130 : :
131 : 23512700 : TheoryIdSet SharedTermsDatabase::getTheoriesToNotify(TNode atom,
132 : : TNode term) const
133 : : {
134 : : // Get the theories that share this term from this atom
135 : 47025500 : std::pair<TNode, TNode> search_pair(atom, term);
136 : 23512700 : SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
137 [ - + ][ - + ]: 23512700 : Assert(find != d_termsToTheories.end());
[ - - ]
138 : :
139 : : // Get the theories that were already notified
140 : 23512700 : TheoryIdSet alreadyNotified = 0;
141 : 23512700 : AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
142 [ + + ]: 23512700 : if (theoriesFind != d_alreadyNotifiedMap.end()) {
143 : 21753500 : alreadyNotified = (*theoriesFind).second;
144 : : }
145 : :
146 : : // Return the ones that haven't been notified yet
147 : 47025500 : return TheoryIdSetUtil::setDifference((*find).second, alreadyNotified);
148 : : }
149 : :
150 : 0 : TheoryIdSet SharedTermsDatabase::getNotifiedTheories(TNode term) const
151 : : {
152 : : // Get the theories that were already notified
153 : 0 : AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
154 [ - - ]: 0 : if (theoriesFind != d_alreadyNotifiedMap.end()) {
155 : 0 : return (*theoriesFind).second;
156 : : } else {
157 : 0 : return 0;
158 : : }
159 : : }
160 : :
161 : 6075770 : bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNode b, bool value)
162 : : {
163 [ + - ][ - - ]: 6075770 : Trace("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory << "," << a << "," << b << ", " << (value ? "true" : "false") << ")" << endl;
164 : :
165 [ - + ]: 6075770 : if (d_inConflict) {
166 : 0 : return false;
167 : : }
168 : :
169 : : // Propagate away
170 : 6075770 : Node equality = a.eqNode(b);
171 [ + + ]: 6075770 : if (value) {
172 : 4153280 : d_theoryEngine->assertToTheory(equality, equality, theory, THEORY_BUILTIN);
173 : : } else {
174 : 1922480 : d_theoryEngine->assertToTheory(equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN);
175 : : }
176 : :
177 : : // As you were
178 : 6075770 : return true;
179 : : }
180 : :
181 : 23512700 : void SharedTermsDatabase::markNotified(TNode term, TheoryIdSet theories)
182 : : {
183 : : // Find out if there are any new theories that were notified about this term
184 : 23512700 : TheoryIdSet alreadyNotified = 0;
185 : 23512700 : AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
186 [ + + ]: 23512700 : if (theoriesFind != d_alreadyNotifiedMap.end()) {
187 : 21753500 : alreadyNotified = (*theoriesFind).second;
188 : : }
189 : : TheoryIdSet newlyNotified =
190 : 23512700 : TheoryIdSetUtil::setDifference(theories, alreadyNotified);
191 : :
192 : : // If no new theories were notified, we are done
193 [ + + ]: 23512700 : if (newlyNotified == 0) {
194 : 21730600 : return;
195 : : }
196 : :
197 [ + - ]: 1782150 : Trace("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl;
198 : :
199 : : // First update the set of notified theories for this term
200 : 3564310 : d_alreadyNotifiedMap[term] =
201 : 1782150 : TheoryIdSetUtil::setUnion(newlyNotified, alreadyNotified);
202 : :
203 [ - + ]: 1782150 : if (d_equalityEngine == nullptr)
204 : : {
205 : : // if we are not assigned an equality engine, there is nothing to do
206 : 0 : return;
207 : : }
208 : :
209 : : // Mark the shared terms in the equality engine
210 : : theory::TheoryId currentTheory;
211 : 5347940 : while ((currentTheory = TheoryIdSetUtil::setPop(newlyNotified))
212 [ + + ]: 5347940 : != THEORY_LAST)
213 : : {
214 : 3565780 : d_equalityEngine->addTriggerTerm(term, currentTheory);
215 : : }
216 : :
217 : : // Check for any conflits
218 : 1782150 : checkForConflict();
219 : : }
220 : :
221 : 2045830 : bool SharedTermsDatabase::areEqual(TNode a, TNode b) const {
222 [ - + ][ - + ]: 2045830 : Assert(d_equalityEngine != nullptr);
[ - - ]
223 : 2045830 : if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
224 : : {
225 : 2045830 : return d_equalityEngine->areEqual(a, b);
226 : : } else {
227 : 0 : Assert(d_equalityEngine->hasTerm(a) || a.isConst());
228 : 0 : Assert(d_equalityEngine->hasTerm(b) || b.isConst());
229 : : // since one (or both) of them is a constant, and the other is in the equality engine, they are not same
230 : 0 : return false;
231 : : }
232 : : }
233 : :
234 : 2006610 : bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const {
235 [ - + ][ - + ]: 2006610 : Assert(d_equalityEngine != nullptr);
[ - - ]
236 : 2006610 : if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
237 : : {
238 : 2006610 : return d_equalityEngine->areDisequal(a, b, false);
239 : : } else {
240 : 0 : Assert(d_equalityEngine->hasTerm(a) || a.isConst());
241 : 0 : Assert(d_equalityEngine->hasTerm(b) || b.isConst());
242 : : // one (or both) are in the equality engine
243 : 0 : return false;
244 : : }
245 : : }
246 : :
247 : 0 : theory::eq::EqualityEngine* SharedTermsDatabase::getEqualityEngine()
248 : : {
249 : 0 : return d_equalityEngine;
250 : : }
251 : :
252 : 10772800 : void SharedTermsDatabase::assertShared(TNode n, bool polarity, TNode reason)
253 : : {
254 [ - + ][ - + ]: 10772800 : Assert(d_equalityEngine != nullptr);
[ - - ]
255 [ + - ]: 21545500 : Trace("shared-terms-database::assert")
256 : 0 : << "SharedTermsDatabase::assertShared(" << n << ", "
257 [ - - ]: 10772800 : << (polarity ? "true" : "false") << ", " << reason << ")" << endl;
258 : : // Add it to the equality engine
259 [ + - ]: 10772800 : if (n.getKind() == Kind::EQUAL)
260 : : {
261 : 10772800 : d_equalityEngine->assertEquality(n, polarity, reason);
262 : : }
263 : : else
264 : : {
265 : 0 : d_equalityEngine->assertPredicate(n, polarity, reason);
266 : : }
267 : : // Check for conflict
268 : 10772800 : checkForConflict();
269 : 10772800 : }
270 : :
271 : 8308110 : bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity) {
272 [ + + ]: 8308110 : if (polarity) {
273 : 3233030 : return d_out.propagate(equality);
274 : : }
275 : 5075080 : return d_out.propagate(equality.notNode());
276 : : }
277 : :
278 : 13410000 : void SharedTermsDatabase::checkForConflict()
279 : : {
280 [ + + ]: 13410000 : if (!d_inConflict)
281 : : {
282 : 13387400 : return;
283 : : }
284 : 22587 : d_inConflict = false;
285 : 22587 : TrustNode trnc;
286 [ + + ]: 22587 : if (d_pfee != nullptr)
287 : : {
288 : 6276 : Node conflict = d_conflictLHS.eqNode(d_conflictRHS);
289 [ + - ]: 6276 : conflict = d_conflictPolarity ? conflict : conflict.notNode();
290 : 6276 : trnc = d_pfee->assertConflict(conflict);
291 : : }
292 : : else
293 : : {
294 : : // standard explain
295 : 32622 : std::vector<TNode> assumptions;
296 : 16311 : d_equalityEngine->explainEquality(
297 : 16311 : d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions);
298 : 16311 : Node conflictNode = nodeManager()->mkAnd(assumptions);
299 : 16311 : trnc = TrustNode::mkTrustConflict(conflictNode, nullptr);
300 : : }
301 : 22587 : d_theoryEngine->conflict(
302 : : trnc, InferenceId::EQ_CONSTANT_MERGE, THEORY_BUILTIN);
303 : 22587 : d_conflictLHS = d_conflictRHS = Node::null();
304 : : }
305 : :
306 : 0 : bool SharedTermsDatabase::isKnown(TNode literal) const {
307 : 0 : Assert(d_equalityEngine != nullptr);
308 : 0 : bool polarity = literal.getKind() != Kind::NOT;
309 [ - - ]: 0 : TNode equality = polarity ? literal : literal[0];
310 [ - - ]: 0 : if (polarity) {
311 : 0 : return d_equalityEngine->areEqual(equality[0], equality[1]);
312 : : } else {
313 : 0 : return d_equalityEngine->areDisequal(equality[0], equality[1], false);
314 : : }
315 : : }
316 : :
317 : 165932 : TrustNode SharedTermsDatabase::explain(TNode literal) const
318 : : {
319 [ + + ]: 165932 : if (d_pfee != nullptr)
320 : : {
321 : : // use the proof equality engine if it exists
322 : 70052 : return d_pfee->explain(literal);
323 : : }
324 : : // otherwise, explain without proofs
325 : 95880 : Node exp = d_equalityEngine->mkExplainLit(literal);
326 : : // no proof generator
327 : 95880 : return TrustNode::mkTrustPropExp(literal, exp, nullptr);
328 : : }
329 : :
330 : : } // namespace cvc5::internal
|
