1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
|
/********************* */
/*! \file ee_manager_distributed.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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.\endverbatim
**
** \brief Management of a distributed approach for equality sharing.
**/
#include "theory/ee_manager_distributed.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
namespace CVC4 {
namespace theory {
EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te)
: d_te(te), d_masterEENotify(nullptr)
{
}
EqEngineManagerDistributed::~EqEngineManagerDistributed()
{
// pop the model context which we pushed on initialization
d_modelEeContext.pop();
}
void EqEngineManagerDistributed::initializeTheories()
{
context::Context* c = d_te.getSatContext();
// allocate equality engines per theory
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;
}
// always allocate an object in d_einfo here
EeTheoryInfo& eet = d_einfo[theoryId];
EeSetupInfo esi;
if (!t->needsEqualityEngine(esi))
{
// theory said it doesn't need an equality engine, skip
continue;
}
// allocate the equality engine
eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
// the theory uses the equality engine
eet.d_usedEe = eet.d_allocEe.get();
}
const LogicInfo& logicInfo = d_te.getLogicInfo();
if (logicInfo.isQuantified())
{
// construct the master equality engine
Assert(d_masterEqualityEngine == nullptr);
QuantifiersEngine* qe = d_te.getQuantifiersEngine();
Assert(qe != nullptr);
d_masterEENotify.reset(new MasterNotifyClass(qe));
d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
d_te.getSatContext(),
"theory::master",
false));
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;
}
EeTheoryInfo& eet = d_einfo[theoryId];
// Get the allocated equality engine, and connect it to the master
// equality engine.
eq::EqualityEngine* eeAlloc = eet.d_allocEe.get();
if (eeAlloc != nullptr)
{
// set the master equality engine of the theory's equality engine
eeAlloc->setMasterEqualityEngine(d_masterEqualityEngine.get());
}
}
}
}
void EqEngineManagerDistributed::initializeModel(
TheoryModel* m, eq::EqualityEngineNotify* notify)
{
Assert(m != nullptr);
// initialize the model equality engine
EeSetupInfo esim;
if (m->needsEqualityEngine(esim))
{
// use the provided notification object
esim.d_notify = notify;
d_modelEqualityEngine.reset(
allocateEqualityEngine(esim, &d_modelEeContext));
m->setEqualityEngine(d_modelEqualityEngine.get());
}
else
{
AlwaysAssert(false) << "Expected model to use equality engine";
}
m->finishInit();
// We push a context during initialization since the model is cleared during
// collectModelInfo using pop/push.
d_modelEeContext.push();
}
void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t)
{
// adds t to the quantifiers term database
d_quantEngine->eqNotifyNewClass(t);
}
context::Context* EqEngineManagerDistributed::getModelEqualityEngineContext()
{
return &d_modelEeContext;
}
eq::EqualityEngine* EqEngineManagerDistributed::getModelEqualityEngine()
{
return d_modelEqualityEngine.get();
}
eq::EqualityEngine* EqEngineManagerDistributed::getCoreEqualityEngine()
{
return d_masterEqualityEngine.get();
}
eq::EqualityEngine* EqEngineManagerDistributed::allocateEqualityEngine(
EeSetupInfo& esi, context::Context* c)
{
if (esi.d_notify != nullptr)
{
return new eq::EqualityEngine(
*esi.d_notify, c, esi.d_name, esi.d_constantsAreTriggers);
}
// the theory doesn't care about explicit notifications
return new eq::EqualityEngine(c, esi.d_name, esi.d_constantsAreTriggers);
}
} // namespace theory
} // namespace CVC4
|
