Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/shared_terms_database.cpp	Lines:	135	158	85.4 %
Date:	2021-08-20	Branches:	224	696	32.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "theory/shared_terms_database.h"

#include "smt/smt_statistics_registry.h"
#include "theory/theory_engine.h"

using namespace std;
using namespace cvc5::theory;

namespace cvc5 {

SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
                                         context::Context* context,
                                         context::UserContext* userContext,
                                         ProofNodeManager* pnm)
    : ContextNotifyObj(context),
      d_statSharedTerms(
          smtStatisticsRegistry().registerInt("theory::shared_terms")),
      d_addedSharedTermsSize(context, 0),
      d_termsToTheories(context),
      d_alreadyNotifiedMap(context),
      d_registeredEqualities(context),
      d_EENotify(*this),
      d_theoryEngine(theoryEngine),
      d_inConflict(context, false),
      d_conflictPolarity(),
      d_satContext(context),
      d_userContext(userContext),
      d_equalityEngine(nullptr),
      d_pfee(nullptr),
      d_pnm(pnm)
{
}

void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
{
  Assert(ee != nullptr);
  d_equalityEngine = ee;
  // if proofs are enabled, make the proof equality engine if necessary
  if (d_pnm != nullptr)
  {
    d_pfee = d_equalityEngine->getProofEqualityEngine();
    if (d_pfee == nullptr)
    {
      d_pfeeAlloc.reset(
          new eq::ProofEqEngine(d_satContext, d_userContext, *ee, d_pnm));
      d_pfee = d_pfeeAlloc.get();
      d_equalityEngine->setProofEqualityEngine(d_pfee);
    }
  }
}

bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi)
{
  esi.d_notify = &d_EENotify;
  esi.d_name = "shared::ee";
  return true;
}

void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
  Assert(d_equalityEngine != nullptr);
  d_registeredEqualities.insert(equality);
  d_equalityEngine->addTriggerPredicate(equality);
  checkForConflict();
}

void SharedTermsDatabase::addSharedTerm(TNode atom,
                                        TNode term,
                                        TheoryIdSet theories)
{
  Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", "
                    << term << ", " << TheoryIdSetUtil::setToString(theories)
                    << ")" << std::endl;

  std::pair<TNode, TNode> search_pair(atom, term);
  SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
  if (find == d_termsToTheories.end()) {
    // First time for this term and this atom
    d_atomsToTerms[atom].push_back(term);
    d_addedSharedTerms.push_back(atom);
    d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
    d_termsToTheories[search_pair] = theories;
  } else {
    Assert(theories != (*find).second);
    d_termsToTheories[search_pair] =
        TheoryIdSetUtil::setUnion(theories, (*find).second);
  }
}

SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::begin(TNode atom) const {
  Assert(hasSharedTerms(atom));
  return d_atomsToTerms.find(atom)->second.begin();
}

SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::end(TNode atom) const {
  Assert(hasSharedTerms(atom));
  return d_atomsToTerms.find(atom)->second.end();
}

bool SharedTermsDatabase::hasSharedTerms(TNode atom) const {
  return d_atomsToTerms.find(atom) != d_atomsToTerms.end();
}

void SharedTermsDatabase::backtrack() {
  for (int i = d_addedSharedTerms.size() - 1, i_end = (int)d_addedSharedTermsSize; i >= i_end; -- i) {
    TNode atom = d_addedSharedTerms[i];
    shared_terms_list& list = d_atomsToTerms[atom];
    list.pop_back();
    if (list.empty()) {
      d_atomsToTerms.erase(atom);
    }
  }
  d_addedSharedTerms.resize(d_addedSharedTermsSize);
}

TheoryIdSet SharedTermsDatabase::getTheoriesToNotify(TNode atom,
                                                     TNode term) const
{
  // Get the theories that share this term from this atom
  std::pair<TNode, TNode> search_pair(atom, term);
  SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
  Assert(find != d_termsToTheories.end());

  // Get the theories that were already notified
  TheoryIdSet alreadyNotified = 0;
  AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
  if (theoriesFind != d_alreadyNotifiedMap.end()) {
    alreadyNotified = (*theoriesFind).second;
  }

  // Return the ones that haven't been notified yet
  return TheoryIdSetUtil::setDifference((*find).second, alreadyNotified);
}

TheoryIdSet SharedTermsDatabase::getNotifiedTheories(TNode term) const
{
  // Get the theories that were already notified
  AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
  if (theoriesFind != d_alreadyNotifiedMap.end()) {
    return (*theoriesFind).second;
  } else {
    return 0;
  }
}

bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNode b, bool value)
{
  Debug("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory << "," << a << "," << b << ", " << (value ? "true" : "false") << ")" << endl;

  if (d_inConflict) {
    return false;
  }

  // Propagate away
  Node equality = a.eqNode(b);
  if (value) {
    d_theoryEngine->assertToTheory(equality, equality, theory, THEORY_BUILTIN);
  } else {
    d_theoryEngine->assertToTheory(equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN);
  }

  // As you were
  return true;
}

void SharedTermsDatabase::markNotified(TNode term, TheoryIdSet theories)
{
  // Find out if there are any new theories that were notified about this term
  TheoryIdSet alreadyNotified = 0;
  AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
  if (theoriesFind != d_alreadyNotifiedMap.end()) {
    alreadyNotified = (*theoriesFind).second;
  }
  TheoryIdSet newlyNotified =
      TheoryIdSetUtil::setDifference(theories, alreadyNotified);

  // If no new theories were notified, we are done
  if (newlyNotified == 0) {
    return;
  }

  Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl;

  // First update the set of notified theories for this term
  d_alreadyNotifiedMap[term] =
      TheoryIdSetUtil::setUnion(newlyNotified, alreadyNotified);

  if (d_equalityEngine == nullptr)
  {
    // if we are not assigned an equality engine, there is nothing to do
    return;
  }

  // Mark the shared terms in the equality engine
  theory::TheoryId currentTheory;
  while ((currentTheory = TheoryIdSetUtil::setPop(newlyNotified))
         != THEORY_LAST)
  {
    d_equalityEngine->addTriggerTerm(term, currentTheory);
  }

  // Check for any conflits
  checkForConflict();
}

bool SharedTermsDatabase::areEqual(TNode a, TNode b) const {
  Assert(d_equalityEngine != nullptr);
  if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
  {
    return d_equalityEngine->areEqual(a, b);
  } else {
    Assert(d_equalityEngine->hasTerm(a) || a.isConst());
    Assert(d_equalityEngine->hasTerm(b) || b.isConst());
    // since one (or both) of them is a constant, and the other is in the equality engine, they are not same
    return false;
  }
}

bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const {
  Assert(d_equalityEngine != nullptr);
  if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
  {
    return d_equalityEngine->areDisequal(a, b, false);
  } else {
    Assert(d_equalityEngine->hasTerm(a) || a.isConst());
    Assert(d_equalityEngine->hasTerm(b) || b.isConst());
    // one (or both) are in the equality engine
    return false;
  }
}

theory::eq::EqualityEngine* SharedTermsDatabase::getEqualityEngine()
{
  return d_equalityEngine;
}

void SharedTermsDatabase::assertShared(TNode n, bool polarity, TNode reason)
{
  Assert(d_equalityEngine != nullptr);
  Debug("shared-terms-database::assert")
      << "SharedTermsDatabase::assertShared(" << n << ", "
      << (polarity ? "true" : "false") << ", " << reason << ")" << endl;
  // Add it to the equality engine
  if (n.getKind() == kind::EQUAL)
  {
    d_equalityEngine->assertEquality(n, polarity, reason);
  }
  else
  {
    d_equalityEngine->assertPredicate(n, polarity, reason);
  }
  // Check for conflict
  checkForConflict();
}

bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity) {
  if (polarity) {
    d_theoryEngine->propagate(equality, THEORY_BUILTIN);
  } else {
    d_theoryEngine->propagate(equality.notNode(), THEORY_BUILTIN);
  }
  return true;
}

void SharedTermsDatabase::checkForConflict()
{
  if (!d_inConflict)
  {
    return;
  }
  d_inConflict = false;
  TrustNode trnc;
  if (d_pfee != nullptr)
  {
    Node conflict = d_conflictLHS.eqNode(d_conflictRHS);
    conflict = d_conflictPolarity ? conflict : conflict.notNode();
    trnc = d_pfee->assertConflict(conflict);
  }
  else
  {
    // standard explain
    std::vector<TNode> assumptions;
    d_equalityEngine->explainEquality(
        d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions);
    Node conflictNode = NodeManager::currentNM()->mkAnd(assumptions);
    trnc = TrustNode::mkTrustConflict(conflictNode, nullptr);
  }
  d_theoryEngine->conflict(trnc, THEORY_BUILTIN);
  d_conflictLHS = d_conflictRHS = Node::null();
}

bool SharedTermsDatabase::isKnown(TNode literal) const {
  Assert(d_equalityEngine != nullptr);
  bool polarity = literal.getKind() != kind::NOT;
  TNode equality = polarity ? literal : literal[0];
  if (polarity) {
    return d_equalityEngine->areEqual(equality[0], equality[1]);
  } else {
    return d_equalityEngine->areDisequal(equality[0], equality[1], false);
  }
}

TrustNode SharedTermsDatabase::explain(TNode literal) const
{
  if (d_pfee != nullptr)
  {
    // use the proof equality engine if it exists
    return d_pfee->explain(literal);
  }
  // otherwise, explain without proofs
  Node exp = d_equalityEngine->mkExplainLit(literal);
  // no proof generator
  return TrustNode::mkTrustPropExp(literal, exp, nullptr);
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
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-2021 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 "smt/smt_statistics_registry.h"
20		#include "theory/theory_engine.h"
21
22		using namespace std;
23		using namespace cvc5::theory;
24
25		namespace cvc5 {
26
27	9856	SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
28		context::Context* context,
29		context::UserContext* userContext,
30	9856	ProofNodeManager* pnm)
31		: ContextNotifyObj(context),
32		d_statSharedTerms(
33	19712	smtStatisticsRegistry().registerInt("theory::shared_terms")),
34		d_addedSharedTermsSize(context, 0),
35		d_termsToTheories(context),
36		d_alreadyNotifiedMap(context),
37		d_registeredEqualities(context),
38		d_EENotify(*this),
39		d_theoryEngine(theoryEngine),
40		d_inConflict(context, false),
41		d_conflictPolarity(),
42		d_satContext(context),
43		d_userContext(userContext),
44		d_equalityEngine(nullptr),
45		d_pfee(nullptr),
46	29568	d_pnm(pnm)
47		{
48	9856	}
49
50	9856	void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
51		{
52	9856	Assert(ee != nullptr);
53	9856	d_equalityEngine = ee;
54		// if proofs are enabled, make the proof equality engine if necessary
55	9856	if (d_pnm != nullptr)
56		{
57	1246	d_pfee = d_equalityEngine->getProofEqualityEngine();
58	1246	if (d_pfee == nullptr)
59		{
60	2478	d_pfeeAlloc.reset(
61	1239	new eq::ProofEqEngine(d_satContext, d_userContext, *ee, d_pnm));
62	1239	d_pfee = d_pfeeAlloc.get();
63	1239	d_equalityEngine->setProofEqualityEngine(d_pfee);
64		}
65		}
66	9856	}
67
68	9856	bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi)
69		{
70	9856	esi.d_notify = &d_EENotify;
71	9856	esi.d_name = "shared::ee";
72	9856	return true;
73		}
74
75	439976	void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
76	439976	Assert(d_equalityEngine != nullptr);
77	439976	d_registeredEqualities.insert(equality);
78	439976	d_equalityEngine->addTriggerPredicate(equality);
79	439976	checkForConflict();
80	439976	}
81
82	1134721	void SharedTermsDatabase::addSharedTerm(TNode atom,
83		TNode term,
84		TheoryIdSet theories)
85		{
86	2269442	Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", "
87	2269442	<< term << ", " << TheoryIdSetUtil::setToString(theories)
88	1134721	<< ")" << std::endl;
89
90	2269442	std::pair<TNode, TNode> search_pair(atom, term);
91	1134721	SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
92	1134721	if (find == d_termsToTheories.end()) {
93		// First time for this term and this atom
94	1131880	d_atomsToTerms[atom].push_back(term);
95	1131880	d_addedSharedTerms.push_back(atom);
96	1131880	d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
97	1131880	d_termsToTheories[search_pair] = theories;
98		} else {
99	2841	Assert(theories != (*find).second);
100	2841	d_termsToTheories[search_pair] =
101	5682	TheoryIdSetUtil::setUnion(theories, (*find).second);
102		}
103	1134721	}
104
105	5026742	SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::begin(TNode atom) const {
106	5026742	Assert(hasSharedTerms(atom));
107	5026742	return d_atomsToTerms.find(atom)->second.begin();
108		}
109
110	5026742	SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::end(TNode atom) const {
111	5026742	Assert(hasSharedTerms(atom));
112	5026742	return d_atomsToTerms.find(atom)->second.end();
113		}
114
115	17675134	bool SharedTermsDatabase::hasSharedTerms(TNode atom) const {
116	17675134	return d_atomsToTerms.find(atom) != d_atomsToTerms.end();
117		}
118
119	3104111	void SharedTermsDatabase::backtrack() {
120	4235991	for (int i = d_addedSharedTerms.size() - 1, i_end = (int)d_addedSharedTermsSize; i >= i_end; -- i) {
121	2263760	TNode atom = d_addedSharedTerms[i];
122	1131880	shared_terms_list& list = d_atomsToTerms[atom];
123	1131880	list.pop_back();
124	1131880	if (list.empty()) {
125	448964	d_atomsToTerms.erase(atom);
126		}
127		}
128	3104111	d_addedSharedTerms.resize(d_addedSharedTermsSize);
129	3104111	}
130
131	13006576	TheoryIdSet SharedTermsDatabase::getTheoriesToNotify(TNode atom,
132		TNode term) const
133		{
134		// Get the theories that share this term from this atom
135	26013152	std::pair<TNode, TNode> search_pair(atom, term);
136	13006576	SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
137	13006576	Assert(find != d_termsToTheories.end());
138
139		// Get the theories that were already notified
140	13006576	TheoryIdSet alreadyNotified = 0;
141	13006576	AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
142	13006576	if (theoriesFind != d_alreadyNotifiedMap.end()) {
143	12092466	alreadyNotified = (*theoriesFind).second;
144		}
145
146		// Return the ones that haven't been notified yet
147	26013152	return TheoryIdSetUtil::setDifference((*find).second, alreadyNotified);
148		}
149
150		TheoryIdSet SharedTermsDatabase::getNotifiedTheories(TNode term) const
151		{
152		// Get the theories that were already notified
153		AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
154		if (theoriesFind != d_alreadyNotifiedMap.end()) {
155		return (*theoriesFind).second;
156		} else {
157		return 0;
158		}
159		}
160
161	3494632	bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNode b, bool value)
162		{
163	3494632	Debug("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory << "," << a << "," << b << ", " << (value ? "true" : "false") << ")" << endl;
164
165	3494632	if (d_inConflict) {
166		return false;
167		}
168
169		// Propagate away
170	6989264	Node equality = a.eqNode(b);
171	3494632	if (value) {
172	2360299	d_theoryEngine->assertToTheory(equality, equality, theory, THEORY_BUILTIN);
173		} else {
174	1134333	d_theoryEngine->assertToTheory(equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN);
175		}
176
177		// As you were
178	3494632	return true;
179		}
180
181	13006576	void SharedTermsDatabase::markNotified(TNode term, TheoryIdSet theories)
182		{
183		// Find out if there are any new theories that were notified about this term
184	13006576	TheoryIdSet alreadyNotified = 0;
185	13006576	AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
186	13006576	if (theoriesFind != d_alreadyNotifiedMap.end()) {
187	12092466	alreadyNotified = (*theoriesFind).second;
188		}
189		TheoryIdSet newlyNotified =
190	13006576	TheoryIdSetUtil::setDifference(theories, alreadyNotified);
191
192		// If no new theories were notified, we are done
193	13006576	if (newlyNotified == 0) {
194	24163462	return;
195		}
196
197	924845	Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl;
198
199		// First update the set of notified theories for this term
200	924845	d_alreadyNotifiedMap[term] =
201	1849690	TheoryIdSetUtil::setUnion(newlyNotified, alreadyNotified);
202
203	924845	if (d_equalityEngine == nullptr)
204		{
205		// if we are not assigned an equality engine, there is nothing to do
206		return;
207		}
208
209		// Mark the shared terms in the equality engine
210		theory::TheoryId currentTheory;
211	1859938	while ((currentTheory = TheoryIdSetUtil::setPop(newlyNotified))
212	2784783	!= THEORY_LAST)
213		{
214	1859938	d_equalityEngine->addTriggerTerm(term, currentTheory);
215		}
216
217		// Check for any conflits
218	924845	checkForConflict();
219		}
220
221	1261371	bool SharedTermsDatabase::areEqual(TNode a, TNode b) const {
222	1261371	Assert(d_equalityEngine != nullptr);
223	1261371	if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
224		{
225	1261371	return d_equalityEngine->areEqual(a, b);
226		} else {
227		Assert(d_equalityEngine->hasTerm(a) \|\| a.isConst());
228		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		return false;
231		}
232		}
233
234	1083821	bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const {
235	1083821	Assert(d_equalityEngine != nullptr);
236	1083821	if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
237		{
238	1083821	return d_equalityEngine->areDisequal(a, b, false);
239		} else {
240		Assert(d_equalityEngine->hasTerm(a) \|\| a.isConst());
241		Assert(d_equalityEngine->hasTerm(b) \|\| b.isConst());
242		// one (or both) are in the equality engine
243		return false;
244		}
245		}
246
247		theory::eq::EqualityEngine* SharedTermsDatabase::getEqualityEngine()
248		{
249		return d_equalityEngine;
250		}
251
252	5976844	void SharedTermsDatabase::assertShared(TNode n, bool polarity, TNode reason)
253		{
254	5976844	Assert(d_equalityEngine != nullptr);
255	11953688	Debug("shared-terms-database::assert")
256	5976844	<< "SharedTermsDatabase::assertShared(" << n << ", "
257	5976844	<< (polarity ? "true" : "false") << ", " << reason << ")" << endl;
258		// Add it to the equality engine
259	5976844	if (n.getKind() == kind::EQUAL)
260		{
261	5976844	d_equalityEngine->assertEquality(n, polarity, reason);
262		}
263		else
264		{
265		d_equalityEngine->assertPredicate(n, polarity, reason);
266		}
267		// Check for conflict
268	5976844	checkForConflict();
269	5976844	}
270
271	4556901	bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity) {
272	4556901	if (polarity) {
273	1862802	d_theoryEngine->propagate(equality, THEORY_BUILTIN);
274		} else {
275	2694099	d_theoryEngine->propagate(equality.notNode(), THEORY_BUILTIN);
276		}
277	4556901	return true;
278		}
279
280	7341665	void SharedTermsDatabase::checkForConflict()
281		{
282	7341665	if (!d_inConflict)
283		{
284	7329323	return;
285		}
286	12342	d_inConflict = false;
287	24684	TrustNode trnc;
288	12342	if (d_pfee != nullptr)
289		{
290	1886	Node conflict = d_conflictLHS.eqNode(d_conflictRHS);
291	943	conflict = d_conflictPolarity ? conflict : conflict.notNode();
292	943	trnc = d_pfee->assertConflict(conflict);
293		}
294		else
295		{
296		// standard explain
297	22798	std::vector<TNode> assumptions;
298	22798	d_equalityEngine->explainEquality(
299	11399	d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions);
300	22798	Node conflictNode = NodeManager::currentNM()->mkAnd(assumptions);
301	11399	trnc = TrustNode::mkTrustConflict(conflictNode, nullptr);
302		}
303	12342	d_theoryEngine->conflict(trnc, THEORY_BUILTIN);
304	12342	d_conflictLHS = d_conflictRHS = Node::null();
305		}
306
307		bool SharedTermsDatabase::isKnown(TNode literal) const {
308		Assert(d_equalityEngine != nullptr);
309		bool polarity = literal.getKind() != kind::NOT;
310		TNode equality = polarity ? literal : literal[0];
311		if (polarity) {
312		return d_equalityEngine->areEqual(equality[0], equality[1]);
313		} else {
314		return d_equalityEngine->areDisequal(equality[0], equality[1], false);
315		}
316		}
317
318	123522	TrustNode SharedTermsDatabase::explain(TNode literal) const
319		{
320	123522	if (d_pfee != nullptr)
321		{
322		// use the proof equality engine if it exists
323	14172	return d_pfee->explain(literal);
324		}
325		// otherwise, explain without proofs
326	218700	Node exp = d_equalityEngine->mkExplainLit(literal);
327		// no proof generator
328	109350	return TrustNode::mkTrustPropExp(literal, exp, nullptr);
329		}
330
331	29358	} // namespace cvc5