Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/ee_manager_central.cpp	Lines:	125	140	89.3 %
Date:	2021-11-06	Branches:	190	432	44.0 %


/******************************************************************************
 * 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 "smt/env.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(Env& env,
                                               TheoryEngine& te,
                                               SharedSolver& shs)
    : EqEngineManager(env, te, shs),
      d_masterEENotify(nullptr),
      d_masterEqualityEngine(nullptr),
      d_centralEENotify(*this),
      d_centralEqualityEngine(
          env, context(), d_centralEENotify, "central::ee", true)
{
  for (TheoryId theoryId = theory::THEORY_FIRST;
       theoryId != theory::THEORY_LAST;
       ++theoryId)
  {
    d_theoryNotify[theoryId] = nullptr;
  }
  if (env.isTheoryProofProducing())
  {
    d_centralPfee =
        std::make_unique<eq::ProofEqEngine>(env, d_centralEqualityEngine);
    d_centralEqualityEngine.setProofEqualityEngine(d_centralPfee.get());
  }
}

EqEngineManagerCentral::~EqEngineManagerCentral() {}

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