Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/ee_manager_central.cpp	Lines:	126	141	89.4 %
Date:	2021-09-07	Branches:	192	442	43.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Equality engine manager for central equality engine architecture
 */

#include "theory/ee_manager_central.h"

#include "theory/quantifiers_engine.h"
#include "theory/shared_solver.h"
#include "theory/theory_engine.h"
#include "theory/theory_state.h"

namespace cvc5 {
namespace theory {

EqEngineManagerCentral::EqEngineManagerCentral(TheoryEngine& te,
                                               SharedSolver& shs,
                                               ProofNodeManager* pnm)
    : EqEngineManager(te, shs),
      d_masterEENotify(nullptr),
      d_masterEqualityEngine(nullptr),
      d_centralEENotify(*this),
      d_centralEqualityEngine(
          d_centralEENotify, te.getSatContext(), "central::ee", true)
{
  for (TheoryId theoryId = theory::THEORY_FIRST;
       theoryId != theory::THEORY_LAST;
       ++theoryId)
  {
    d_theoryNotify[theoryId] = nullptr;
  }
  if (pnm != nullptr)
  {
    d_centralPfee.reset(new eq::ProofEqEngine(d_te.getSatContext(),
                                              d_te.getUserContext(),
                                              d_centralEqualityEngine,
                                              pnm));
    d_centralEqualityEngine.setProofEqualityEngine(d_centralPfee.get());
  }
}

EqEngineManagerCentral::~EqEngineManagerCentral() {}

void EqEngineManagerCentral::initializeTheories()
{
  context::Context* c = d_te.getSatContext();
  // initialize the shared solver
  EeSetupInfo esis;
  if (d_sharedSolver.needsEqualityEngine(esis))
  {
    // the shared solver uses central equality engine
    d_sharedSolver.setEqualityEngine(&d_centralEqualityEngine);
  }
  else
  {
    Unreachable() << "Expected shared solver to use equality engine";
  }
  // whether to use master equality engine as central
  bool masterEqToCentral = true;
  // setup info for each theory
  std::map<TheoryId, EeSetupInfo> esiMap;
  // set of theories that need equality engines
  std::unordered_set<TheoryId> eeTheories;
  const LogicInfo& logicInfo = d_te.getLogicInfo();
  for (TheoryId theoryId = theory::THEORY_FIRST;
       theoryId != theory::THEORY_LAST;
       ++theoryId)
  {
    Theory* t = d_te.theoryOf(theoryId);
    if (t == nullptr)
    {
      // theory not active, skip
      continue;
    }
    if (!t->needsEqualityEngine(esiMap[theoryId]))
    {
      // theory said it doesn't need an equality engine, skip
      continue;
    }
    // otherwise add it to the set of equality engine theories
    eeTheories.insert(theoryId);
    // if the logic has a theory that does not use central equality engine,
    // we can't use the central equality engine for the master equality
    // engine
    if (theoryId != THEORY_QUANTIFIERS && logicInfo.isTheoryEnabled(theoryId)
        && !Theory::usesCentralEqualityEngine(theoryId))
    {
      Trace("ee-central") << "Must use separate master equality engine due to "
                          << theoryId << std::endl;
      masterEqToCentral = false;
    }
  }

  // initialize the master equality engine, which may be the central equality
  // engine
  if (logicInfo.isQuantified())
  {
    // construct the master equality engine
    Assert(d_masterEqualityEngine == nullptr);
    QuantifiersEngine* qe = d_te.getQuantifiersEngine();
    Assert(qe != nullptr);
    d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe));
    if (!masterEqToCentral)
    {
      d_masterEqualityEngineAlloc.reset(new eq::EqualityEngine(
          *d_masterEENotify.get(), d_te.getSatContext(), "master::ee", false));
      d_masterEqualityEngine = d_masterEqualityEngineAlloc.get();
    }
    else
    {
      Trace("ee-central")
          << "Master equality engine is the central equality engine"
          << std::endl;
      d_masterEqualityEngine = &d_centralEqualityEngine;
      d_centralEENotify.d_newClassNotify.push_back(d_masterEENotify.get());
    }
  }

  // allocate equality engines per theory
  for (TheoryId theoryId = theory::THEORY_FIRST;
       theoryId != theory::THEORY_LAST;
       ++theoryId)
  {
    Trace("ee-central") << "Setup equality engine for " << theoryId
                        << std::endl;
    // always allocate an object in d_einfo here
    EeTheoryInfo& eet = d_einfo[theoryId];
    if (eeTheories.find(theoryId) == eeTheories.end())
    {
      Trace("ee-central") << "..." << theoryId << " does not need ee"
                          << std::endl;
      continue;
    }
    Theory* t = d_te.theoryOf(theoryId);
    Assert(t != nullptr);
    Assert(esiMap.find(theoryId) != esiMap.end());
    EeSetupInfo& esi = esiMap[theoryId];
    if (esi.d_useMaster)
    {
      Trace("ee-central") << "...uses master" << std::endl;
      // the theory said it wants to use the master equality engine
      eet.d_usedEe = d_masterEqualityEngine;
      continue;
    }
    // set the notify
    eq::EqualityEngineNotify* notify = esi.d_notify;
    d_theoryNotify[theoryId] = notify;
    // split on whether integrated, or whether asked for master
    if (t->usesCentralEqualityEngine())
    {
      Trace("ee-central") << "...uses central" << std::endl;
      // the theory uses the central equality engine
      eet.d_usedEe = &d_centralEqualityEngine;
      if (logicInfo.isTheoryEnabled(theoryId))
      {
        // add to vectors for the kinds of notifications
        if (esi.needsNotifyNewClass())
        {
          d_centralEENotify.d_newClassNotify.push_back(notify);
        }
        if (esi.needsNotifyMerge())
        {
          d_centralEENotify.d_mergeNotify.push_back(notify);
        }
        if (esi.needsNotifyDisequal())
        {
          d_centralEENotify.d_disequalNotify.push_back(notify);
        }
      }
      continue;
    }
    Trace("ee-central") << "...uses new" << std::endl;
    eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
    // the theory uses the equality engine
    eet.d_usedEe = eet.d_allocEe.get();
    if (!masterEqToCentral)
    {
      // set the master equality engine of the theory's equality engine
      eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine);
    }
  }

  // set the master equality engine of the theory's equality engine
  if (!masterEqToCentral)
  {
    d_centralEqualityEngine.setMasterEqualityEngine(d_masterEqualityEngine);
  }
}

void EqEngineManagerCentral::notifyBuildingModel() {}

EqEngineManagerCentral::CentralNotifyClass::CentralNotifyClass(
    EqEngineManagerCentral& eemc)
    : d_eemc(eemc), d_mNotify(nullptr), d_quantEngine(nullptr)
{
}

bool EqEngineManagerCentral::CentralNotifyClass::eqNotifyTriggerPredicate(
    TNode predicate, bool value)
{
  Trace("eem-central") << "eqNotifyTriggerPredicate: " << predicate
                       << std::endl;
  return d_eemc.eqNotifyTriggerPredicate(predicate, value);
}

bool EqEngineManagerCentral::CentralNotifyClass::eqNotifyTriggerTermEquality(
    TheoryId tag, TNode t1, TNode t2, bool value)
{
  Trace("eem-central") << "eqNotifyTriggerTermEquality: " << t1 << " " << t2
                       << value << ", tag = " << tag << std::endl;
  return d_eemc.eqNotifyTriggerTermEquality(tag, t1, t2, value);
}

void EqEngineManagerCentral::CentralNotifyClass::eqNotifyConstantTermMerge(
    TNode t1, TNode t2)
{
  Trace("eem-central") << "eqNotifyConstantTermMerge: " << t1 << " " << t2
                       << std::endl;
  d_eemc.eqNotifyConstantTermMerge(t1, t2);
}

void EqEngineManagerCentral::CentralNotifyClass::eqNotifyNewClass(TNode t)
{
  Trace("eem-central") << "...eqNotifyNewClass " << t << std::endl;
  // notify all theories that have new equivalence class notifications
  for (eq::EqualityEngineNotify* notify : d_newClassNotify)
  {
    notify->eqNotifyNewClass(t);
  }
}

void EqEngineManagerCentral::CentralNotifyClass::eqNotifyMerge(TNode t1,
                                                               TNode t2)
{
  Trace("eem-central") << "...eqNotifyMerge " << t1 << ", " << t2 << std::endl;
  // notify all theories that have merge notifications
  for (eq::EqualityEngineNotify* notify : d_mergeNotify)
  {
    notify->eqNotifyMerge(t1, t2);
  }
}

void EqEngineManagerCentral::CentralNotifyClass::eqNotifyDisequal(TNode t1,
                                                                  TNode t2,
                                                                  TNode reason)
{
  Trace("eem-central") << "...eqNotifyDisequal " << t1 << ", " << t2
                       << std::endl;
  // notify all theories that have disequal notifications
  for (eq::EqualityEngineNotify* notify : d_disequalNotify)
  {
    notify->eqNotifyDisequal(t1, t2, reason);
  }
}

bool EqEngineManagerCentral::eqNotifyTriggerPredicate(TNode predicate,
                                                      bool value)
{
  // always propagate with the shared solver
  Trace("eem-central") << "...propagate " << predicate << ", " << value
                       << " with shared solver" << std::endl;
  return d_sharedSolver.propagateLit(predicate, value);
}

bool EqEngineManagerCentral::eqNotifyTriggerTermEquality(TheoryId tag,
                                                         TNode a,
                                                         TNode b,
                                                         bool value)
{
  // propagate to theory engine
  bool ok = d_sharedSolver.propagateLit(a.eqNode(b), value);
  if (!ok)
  {
    return false;
  }
  // no need to propagate shared term equalities to the UF theory
  if (tag == THEORY_UF)
  {
    return true;
  }
  // propagate shared equality
  return d_sharedSolver.propagateSharedEquality(tag, a, b, value);
}

void EqEngineManagerCentral::eqNotifyConstantTermMerge(TNode t1, TNode t2)
{
  Node lit = t1.eqNode(t2);
  Node conflict = d_centralEqualityEngine.mkExplainLit(lit);
  Trace("eem-central") << "...explained conflict of " << lit << " ... "
                       << conflict << std::endl;
  d_sharedSolver.sendConflict(TrustNode::mkTrustConflict(conflict),
                              InferenceId::EQ_CONSTANT_MERGE);
  return;
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
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-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		* Equality engine manager for central equality engine architecture
14		*/
15
16		#include "theory/ee_manager_central.h"
17
18		#include "theory/quantifiers_engine.h"
19		#include "theory/shared_solver.h"
20		#include "theory/theory_engine.h"
21		#include "theory/theory_state.h"
22
23		namespace cvc5 {
24		namespace theory {
25
26	35	EqEngineManagerCentral::EqEngineManagerCentral(TheoryEngine& te,
27		SharedSolver& shs,
28	35	ProofNodeManager* pnm)
29		: EqEngineManager(te, shs),
30		d_masterEENotify(nullptr),
31		d_masterEqualityEngine(nullptr),
32		d_centralEENotify(*this),
33		d_centralEqualityEngine(
34	35	d_centralEENotify, te.getSatContext(), "central::ee", true)
35		{
36	490	for (TheoryId theoryId = theory::THEORY_FIRST;
37	490	theoryId != theory::THEORY_LAST;
38		++theoryId)
39		{
40	455	d_theoryNotify[theoryId] = nullptr;
41		}
42	35	if (pnm != nullptr)
43		{
44	14	d_centralPfee.reset(new eq::ProofEqEngine(d_te.getSatContext(),
45	7	d_te.getUserContext(),
46		d_centralEqualityEngine,
47	7	pnm));
48	7	d_centralEqualityEngine.setProofEqualityEngine(d_centralPfee.get());
49		}
50	35	}
51
52	70	EqEngineManagerCentral::~EqEngineManagerCentral() {}
53
54	35	void EqEngineManagerCentral::initializeTheories()
55		{
56	35	context::Context* c = d_te.getSatContext();
57		// initialize the shared solver
58	70	EeSetupInfo esis;
59	35	if (d_sharedSolver.needsEqualityEngine(esis))
60		{
61		// the shared solver uses central equality engine
62	35	d_sharedSolver.setEqualityEngine(&d_centralEqualityEngine);
63		}
64		else
65		{
66		Unreachable() << "Expected shared solver to use equality engine";
67		}
68		// whether to use master equality engine as central
69	35	bool masterEqToCentral = true;
70		// setup info for each theory
71	70	std::map<TheoryId, EeSetupInfo> esiMap;
72		// set of theories that need equality engines
73	70	std::unordered_set<TheoryId> eeTheories;
74	35	const LogicInfo& logicInfo = d_te.getLogicInfo();
75	490	for (TheoryId theoryId = theory::THEORY_FIRST;
76	490	theoryId != theory::THEORY_LAST;
77		++theoryId)
78		{
79	455	Theory* t = d_te.theoryOf(theoryId);
80	455	if (t == nullptr)
81		{
82		// theory not active, skip
83		continue;
84		}
85	455	if (!t->needsEqualityEngine(esiMap[theoryId]))
86		{
87		// theory said it doesn't need an equality engine, skip
88	70	continue;
89		}
90		// otherwise add it to the set of equality engine theories
91	385	eeTheories.insert(theoryId);
92		// if the logic has a theory that does not use central equality engine,
93		// we can't use the central equality engine for the master equality
94		// engine
95	1120	if (theoryId != THEORY_QUANTIFIERS && logicInfo.isTheoryEnabled(theoryId)
96	735	&& !Theory::usesCentralEqualityEngine(theoryId))
97		{
98		Trace("ee-central") << "Must use separate master equality engine due to "
99		<< theoryId << std::endl;
100		masterEqToCentral = false;
101		}
102		}
103
104		// initialize the master equality engine, which may be the central equality
105		// engine
106	35	if (logicInfo.isQuantified())
107		{
108		// construct the master equality engine
109	35	Assert(d_masterEqualityEngine == nullptr);
110	35	QuantifiersEngine* qe = d_te.getQuantifiersEngine();
111	35	Assert(qe != nullptr);
112	35	d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe));
113	35	if (!masterEqToCentral)
114		{
115		d_masterEqualityEngineAlloc.reset(new eq::EqualityEngine(
116		*d_masterEENotify.get(), d_te.getSatContext(), "master::ee", false));
117		d_masterEqualityEngine = d_masterEqualityEngineAlloc.get();
118		}
119		else
120		{
121	70	Trace("ee-central")
122	35	<< "Master equality engine is the central equality engine"
123	35	<< std::endl;
124	35	d_masterEqualityEngine = &d_centralEqualityEngine;
125	35	d_centralEENotify.d_newClassNotify.push_back(d_masterEENotify.get());
126		}
127		}
128
129		// allocate equality engines per theory
130	490	for (TheoryId theoryId = theory::THEORY_FIRST;
131	490	theoryId != theory::THEORY_LAST;
132		++theoryId)
133		{
134	910	Trace("ee-central") << "Setup equality engine for " << theoryId
135	455	<< std::endl;
136		// always allocate an object in d_einfo here
137	455	EeTheoryInfo& eet = d_einfo[theoryId];
138	525	if (eeTheories.find(theoryId) == eeTheories.end())
139		{
140	140	Trace("ee-central") << "..." << theoryId << " does not need ee"
141	70	<< std::endl;
142	525	continue;
143		}
144	385	Theory* t = d_te.theoryOf(theoryId);
145	385	Assert(t != nullptr);
146	385	Assert(esiMap.find(theoryId) != esiMap.end());
147	385	EeSetupInfo& esi = esiMap[theoryId];
148	420	if (esi.d_useMaster)
149		{
150	35	Trace("ee-central") << "...uses master" << std::endl;
151		// the theory said it wants to use the master equality engine
152	35	eet.d_usedEe = d_masterEqualityEngine;
153	35	continue;
154		}
155		// set the notify
156	350	eq::EqualityEngineNotify* notify = esi.d_notify;
157	350	d_theoryNotify[theoryId] = notify;
158		// split on whether integrated, or whether asked for master
159	700	if (t->usesCentralEqualityEngine())
160		{
161	350	Trace("ee-central") << "...uses central" << std::endl;
162		// the theory uses the central equality engine
163	350	eet.d_usedEe = &d_centralEqualityEngine;
164	350	if (logicInfo.isTheoryEnabled(theoryId))
165		{
166		// add to vectors for the kinds of notifications
167	350	if (esi.needsNotifyNewClass())
168		{
169	140	d_centralEENotify.d_newClassNotify.push_back(notify);
170		}
171	350	if (esi.needsNotifyMerge())
172		{
173	175	d_centralEENotify.d_mergeNotify.push_back(notify);
174		}
175	350	if (esi.needsNotifyDisequal())
176		{
177	70	d_centralEENotify.d_disequalNotify.push_back(notify);
178		}
179		}
180	350	continue;
181		}
182		Trace("ee-central") << "...uses new" << std::endl;
183		eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
184		// the theory uses the equality engine
185		eet.d_usedEe = eet.d_allocEe.get();
186		if (!masterEqToCentral)
187		{
188		// set the master equality engine of the theory's equality engine
189		eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine);
190		}
191		}
192
193		// set the master equality engine of the theory's equality engine
194	35	if (!masterEqToCentral)
195		{
196		d_centralEqualityEngine.setMasterEqualityEngine(d_masterEqualityEngine);
197		}
198	35	}
199
200		void EqEngineManagerCentral::notifyBuildingModel() {}
201
202	35	EqEngineManagerCentral::CentralNotifyClass::CentralNotifyClass(
203	35	EqEngineManagerCentral& eemc)
204	35	: d_eemc(eemc), d_mNotify(nullptr), d_quantEngine(nullptr)
205		{
206	35	}
207
208	6622	bool EqEngineManagerCentral::CentralNotifyClass::eqNotifyTriggerPredicate(
209		TNode predicate, bool value)
210		{
211	13244	Trace("eem-central") << "eqNotifyTriggerPredicate: " << predicate
212	6622	<< std::endl;
213	6622	return d_eemc.eqNotifyTriggerPredicate(predicate, value);
214		}
215
216	8306	bool EqEngineManagerCentral::CentralNotifyClass::eqNotifyTriggerTermEquality(
217		TheoryId tag, TNode t1, TNode t2, bool value)
218		{
219	16612	Trace("eem-central") << "eqNotifyTriggerTermEquality: " << t1 << " " << t2
220	8306	<< value << ", tag = " << tag << std::endl;
221	8306	return d_eemc.eqNotifyTriggerTermEquality(tag, t1, t2, value);
222		}
223
224	28	void EqEngineManagerCentral::CentralNotifyClass::eqNotifyConstantTermMerge(
225		TNode t1, TNode t2)
226		{
227	56	Trace("eem-central") << "eqNotifyConstantTermMerge: " << t1 << " " << t2
228	28	<< std::endl;
229	28	d_eemc.eqNotifyConstantTermMerge(t1, t2);
230	28	}
231
232	6018	void EqEngineManagerCentral::CentralNotifyClass::eqNotifyNewClass(TNode t)
233		{
234	6018	Trace("eem-central") << "...eqNotifyNewClass " << t << std::endl;
235		// notify all theories that have new equivalence class notifications
236	36108	for (eq::EqualityEngineNotify* notify : d_newClassNotify)
237		{
238	30090	notify->eqNotifyNewClass(t);
239		}
240	6018	}
241
242	11183	void EqEngineManagerCentral::CentralNotifyClass::eqNotifyMerge(TNode t1,
243		TNode t2)
244		{
245	11183	Trace("eem-central") << "...eqNotifyMerge " << t1 << ", " << t2 << std::endl;
246		// notify all theories that have merge notifications
247	67098	for (eq::EqualityEngineNotify* notify : d_mergeNotify)
248		{
249	55915	notify->eqNotifyMerge(t1, t2);
250		}
251	11183	}
252
253	320	void EqEngineManagerCentral::CentralNotifyClass::eqNotifyDisequal(TNode t1,
254		TNode t2,
255		TNode reason)
256		{
257	640	Trace("eem-central") << "...eqNotifyDisequal " << t1 << ", " << t2
258	320	<< std::endl;
259		// notify all theories that have disequal notifications
260	960	for (eq::EqualityEngineNotify* notify : d_disequalNotify)
261		{
262	640	notify->eqNotifyDisequal(t1, t2, reason);
263		}
264	320	}
265
266	6622	bool EqEngineManagerCentral::eqNotifyTriggerPredicate(TNode predicate,
267		bool value)
268		{
269		// always propagate with the shared solver
270	13244	Trace("eem-central") << "...propagate " << predicate << ", " << value
271	6622	<< " with shared solver" << std::endl;
272	6622	return d_sharedSolver.propagateLit(predicate, value);
273		}
274
275	8306	bool EqEngineManagerCentral::eqNotifyTriggerTermEquality(TheoryId tag,
276		TNode a,
277		TNode b,
278		bool value)
279		{
280		// propagate to theory engine
281	8306	bool ok = d_sharedSolver.propagateLit(a.eqNode(b), value);
282	8306	if (!ok)
283		{
284	26	return false;
285		}
286		// no need to propagate shared term equalities to the UF theory
287	8280	if (tag == THEORY_UF)
288		{
289	3523	return true;
290		}
291		// propagate shared equality
292	4757	return d_sharedSolver.propagateSharedEquality(tag, a, b, value);
293		}
294
295	28	void EqEngineManagerCentral::eqNotifyConstantTermMerge(TNode t1, TNode t2)
296		{
297	56	Node lit = t1.eqNode(t2);
298	56	Node conflict = d_centralEqualityEngine.mkExplainLit(lit);
299	56	Trace("eem-central") << "...explained conflict of " << lit << " ... "
300	28	<< conflict << std::endl;
301	28	d_sharedSolver.sendConflict(TrustNode::mkTrustConflict(conflict),
302		InferenceId::EQ_CONSTANT_MERGE);
303	56	return;
304		}
305
306		} // namespace theory
307	29502	} // namespace cvc5