Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/shared_terms_database.cpp	Lines:	133	156	85.3 %
Date:	2021-11-05	Branches:	228	704	32.4 %


/******************************************************************************
 * 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(Env& env, TheoryEngine* theoryEngine)
    : ContextNotifyObj(env.getContext()),
      d_env(env),
      d_statSharedTerms(
          smtStatisticsRegistry().registerInt("theory::shared_terms")),
      d_addedSharedTermsSize(env.getContext(), 0),
      d_termsToTheories(env.getContext()),
      d_alreadyNotifiedMap(env.getContext()),
      d_registeredEqualities(env.getContext()),
      d_EENotify(*this),
      d_theoryEngine(theoryEngine),
      d_inConflict(env.getContext(), false),
      d_conflictPolarity(),
      d_equalityEngine(nullptr),
      d_pfee(nullptr)
{
}

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_env.isTheoryProofProducing())
  {
    d_pfee = d_equalityEngine->getProofEqualityEngine();
    if (d_pfee == nullptr)
    {
      d_pfeeAlloc = std::make_unique<eq::ProofEqEngine>(d_env, *ee);
      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	15271	SharedTermsDatabase::SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine)
28		: ContextNotifyObj(env.getContext()),
29		d_env(env),
30		d_statSharedTerms(
31	30542	smtStatisticsRegistry().registerInt("theory::shared_terms")),
32		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		d_inConflict(env.getContext(), false),
39		d_conflictPolarity(),
40		d_equalityEngine(nullptr),
41	45813	d_pfee(nullptr)
42		{
43	15271	}
44
45	15271	void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
46		{
47	15271	Assert(ee != nullptr);
48	15271	d_equalityEngine = ee;
49		// if proofs are enabled, make the proof equality engine if necessary
50	15271	if (d_env.isTheoryProofProducing())
51		{
52	5372	d_pfee = d_equalityEngine->getProofEqualityEngine();
53	5372	if (d_pfee == nullptr)
54		{
55	5364	d_pfeeAlloc = std::make_unique<eq::ProofEqEngine>(d_env, *ee);
56	5364	d_pfee = d_pfeeAlloc.get();
57	5364	d_equalityEngine->setProofEqualityEngine(d_pfee);
58		}
59		}
60	15271	}
61
62	15271	bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi)
63		{
64	15271	esi.d_notify = &d_EENotify;
65	15271	esi.d_name = "shared::ee";
66	15271	return true;
67		}
68
69	522138	void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
70	522138	Assert(d_equalityEngine != nullptr);
71	522138	d_registeredEqualities.insert(equality);
72	522138	d_equalityEngine->addTriggerPredicate(equality);
73	522138	checkForConflict();
74	522138	}
75
76	1420568	void SharedTermsDatabase::addSharedTerm(TNode atom,
77		TNode term,
78		TheoryIdSet theories)
79		{
80	2841136	Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", "
81	2841136	<< term << ", " << TheoryIdSetUtil::setToString(theories)
82	1420568	<< ")" << std::endl;
83
84	2841136	std::pair<TNode, TNode> search_pair(atom, term);
85	1420568	SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
86	1420568	if (find == d_termsToTheories.end()) {
87		// First time for this term and this atom
88	1417647	d_atomsToTerms[atom].push_back(term);
89	1417647	d_addedSharedTerms.push_back(atom);
90	1417647	d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
91	1417647	d_termsToTheories[search_pair] = theories;
92		} else {
93	2921	Assert(theories != (*find).second);
94	2921	d_termsToTheories[search_pair] =
95	5842	TheoryIdSetUtil::setUnion(theories, (*find).second);
96		}
97	1420568	}
98
99	8081479	SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::begin(TNode atom) const {
100	8081479	Assert(hasSharedTerms(atom));
101	8081479	return d_atomsToTerms.find(atom)->second.begin();
102		}
103
104	8081479	SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::end(TNode atom) const {
105	8081479	Assert(hasSharedTerms(atom));
106	8081479	return d_atomsToTerms.find(atom)->second.end();
107		}
108
109	27531874	bool SharedTermsDatabase::hasSharedTerms(TNode atom) const {
110	27531874	return d_atomsToTerms.find(atom) != d_atomsToTerms.end();
111		}
112
113	3755300	void SharedTermsDatabase::backtrack() {
114	5172947	for (int i = d_addedSharedTerms.size() - 1, i_end = (int)d_addedSharedTermsSize; i >= i_end; -- i) {
115	2835294	TNode atom = d_addedSharedTerms[i];
116	1417647	shared_terms_list& list = d_atomsToTerms[atom];
117	1417647	list.pop_back();
118	1417647	if (list.empty()) {
119	550560	d_atomsToTerms.erase(atom);
120		}
121		}
122	3755300	d_addedSharedTerms.resize(d_addedSharedTermsSize);
123	3755300	}
124
125	21132880	TheoryIdSet SharedTermsDatabase::getTheoriesToNotify(TNode atom,
126		TNode term) const
127		{
128		// Get the theories that share this term from this atom
129	42265760	std::pair<TNode, TNode> search_pair(atom, term);
130	21132880	SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
131	21132880	Assert(find != d_termsToTheories.end());
132
133		// Get the theories that were already notified
134	21132880	TheoryIdSet alreadyNotified = 0;
135	21132880	AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
136	21132880	if (theoriesFind != d_alreadyNotifiedMap.end()) {
137	19946925	alreadyNotified = (*theoriesFind).second;
138		}
139
140		// Return the ones that haven't been notified yet
141	42265760	return TheoryIdSetUtil::setDifference((*find).second, alreadyNotified);
142		}
143
144		TheoryIdSet SharedTermsDatabase::getNotifiedTheories(TNode term) const
145		{
146		// Get the theories that were already notified
147		AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
148		if (theoriesFind != d_alreadyNotifiedMap.end()) {
149		return (*theoriesFind).second;
150		} else {
151		return 0;
152		}
153		}
154
155	4843329	bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNode b, bool value)
156		{
157	4843329	Debug("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory << "," << a << "," << b << ", " << (value ? "true" : "false") << ")" << endl;
158
159	4843329	if (d_inConflict) {
160		return false;
161		}
162
163		// Propagate away
164	9686658	Node equality = a.eqNode(b);
165	4843329	if (value) {
166	2937726	d_theoryEngine->assertToTheory(equality, equality, theory, THEORY_BUILTIN);
167		} else {
168	1905603	d_theoryEngine->assertToTheory(equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN);
169		}
170
171		// As you were
172	4843329	return true;
173		}
174
175	21132880	void SharedTermsDatabase::markNotified(TNode term, TheoryIdSet theories)
176		{
177		// Find out if there are any new theories that were notified about this term
178	21132880	TheoryIdSet alreadyNotified = 0;
179	21132880	AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
180	21132880	if (theoriesFind != d_alreadyNotifiedMap.end()) {
181	19946925	alreadyNotified = (*theoriesFind).second;
182		}
183		TheoryIdSet newlyNotified =
184	21132880	TheoryIdSetUtil::setDifference(theories, alreadyNotified);
185
186		// If no new theories were notified, we are done
187	21132880	if (newlyNotified == 0) {
188	39791802	return;
189		}
190
191	1236979	Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl;
192
193		// First update the set of notified theories for this term
194	1236979	d_alreadyNotifiedMap[term] =
195	2473958	TheoryIdSetUtil::setUnion(newlyNotified, alreadyNotified);
196
197	1236979	if (d_equalityEngine == nullptr)
198		{
199		// if we are not assigned an equality engine, there is nothing to do
200		return;
201		}
202
203		// Mark the shared terms in the equality engine
204		theory::TheoryId currentTheory;
205	2470265	while ((currentTheory = TheoryIdSetUtil::setPop(newlyNotified))
206	3707244	!= THEORY_LAST)
207		{
208	2470265	d_equalityEngine->addTriggerTerm(term, currentTheory);
209		}
210
211		// Check for any conflits
212	1236979	checkForConflict();
213		}
214
215	1129641	bool SharedTermsDatabase::areEqual(TNode a, TNode b) const {
216	1129641	Assert(d_equalityEngine != nullptr);
217	1129641	if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
218		{
219	1129641	return d_equalityEngine->areEqual(a, b);
220		} else {
221		Assert(d_equalityEngine->hasTerm(a) \|\| a.isConst());
222		Assert(d_equalityEngine->hasTerm(b) \|\| b.isConst());
223		// since one (or both) of them is a constant, and the other is in the equality engine, they are not same
224		return false;
225		}
226		}
227
228	954867	bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const {
229	954867	Assert(d_equalityEngine != nullptr);
230	954867	if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
231		{
232	954867	return d_equalityEngine->areDisequal(a, b, false);
233		} else {
234		Assert(d_equalityEngine->hasTerm(a) \|\| a.isConst());
235		Assert(d_equalityEngine->hasTerm(b) \|\| b.isConst());
236		// one (or both) are in the equality engine
237		return false;
238		}
239		}
240
241		theory::eq::EqualityEngine* SharedTermsDatabase::getEqualityEngine()
242		{
243		return d_equalityEngine;
244		}
245
246	7607232	void SharedTermsDatabase::assertShared(TNode n, bool polarity, TNode reason)
247		{
248	7607232	Assert(d_equalityEngine != nullptr);
249	15214464	Debug("shared-terms-database::assert")
250	7607232	<< "SharedTermsDatabase::assertShared(" << n << ", "
251	7607232	<< (polarity ? "true" : "false") << ", " << reason << ")" << endl;
252		// Add it to the equality engine
253	7607232	if (n.getKind() == kind::EQUAL)
254		{
255	7607232	d_equalityEngine->assertEquality(n, polarity, reason);
256		}
257		else
258		{
259		d_equalityEngine->assertPredicate(n, polarity, reason);
260		}
261		// Check for conflict
262	7607232	checkForConflict();
263	7607232	}
264
265	6021894	bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity) {
266	6021894	if (polarity) {
267	2309854	d_theoryEngine->propagate(equality, THEORY_BUILTIN);
268		} else {
269	3712040	d_theoryEngine->propagate(equality.notNode(), THEORY_BUILTIN);
270		}
271	6021894	return true;
272		}
273
274	9366349	void SharedTermsDatabase::checkForConflict()
275		{
276	9366349	if (!d_inConflict)
277		{
278	9352119	return;
279		}
280	14230	d_inConflict = false;
281	28460	TrustNode trnc;
282	14230	if (d_pfee != nullptr)
283		{
284	2066	Node conflict = d_conflictLHS.eqNode(d_conflictRHS);
285	1033	conflict = d_conflictPolarity ? conflict : conflict.notNode();
286	1033	trnc = d_pfee->assertConflict(conflict);
287		}
288		else
289		{
290		// standard explain
291	26394	std::vector<TNode> assumptions;
292	26394	d_equalityEngine->explainEquality(
293	13197	d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions);
294	26394	Node conflictNode = NodeManager::currentNM()->mkAnd(assumptions);
295	13197	trnc = TrustNode::mkTrustConflict(conflictNode, nullptr);
296		}
297	14230	d_theoryEngine->conflict(trnc, THEORY_BUILTIN);
298	14230	d_conflictLHS = d_conflictRHS = Node::null();
299		}
300
301		bool SharedTermsDatabase::isKnown(TNode literal) const {
302		Assert(d_equalityEngine != nullptr);
303		bool polarity = literal.getKind() != kind::NOT;
304		TNode equality = polarity ? literal : literal[0];
305		if (polarity) {
306		return d_equalityEngine->areEqual(equality[0], equality[1]);
307		} else {
308		return d_equalityEngine->areDisequal(equality[0], equality[1], false);
309		}
310		}
311
312	141429	TrustNode SharedTermsDatabase::explain(TNode literal) const
313		{
314	141429	if (d_pfee != nullptr)
315		{
316		// use the proof equality engine if it exists
317	15104	return d_pfee->explain(literal);
318		}
319		// otherwise, explain without proofs
320	252650	Node exp = d_equalityEngine->mkExplainLit(literal);
321		// no proof generator
322	126325	return TrustNode::mkTrustPropExp(literal, exp, nullptr);
323		}
324
325	31125	} // namespace cvc5