@@ -13,15 +13,16 @@ void DispatcherGraph::addDispatcher(ClauseDispatcher *dispatcher) {
13
13
if (contains (dispatcher)) {
14
14
throw " Error: dispatcher already exists in graph" ;
15
15
}
16
- if (!symbols .empty ()) {
16
+ if (!symbolsToClauseDispatchersMap .empty ()) {
17
17
ensureHasOneCommonSymbolWith (dispatcher);
18
18
}
19
19
adjacencyList[dispatcher] = EDGES ();
20
20
for (const auto &symbol : dispatcher->getSymbols ()) {
21
21
if (!contains (symbol)) {
22
- symbols [symbol] = CLAUSE_DISPATCHER_SET ();
22
+ symbolsToClauseDispatchersMap [symbol] = CLAUSE_DISPATCHER_SET ();
23
23
}
24
- for (const auto &associatedDispatcher : symbols[symbol]) {
24
+ for (const auto &associatedDispatcher :
25
+ symbolsToClauseDispatchersMap[symbol]) {
25
26
int weight = countCommonSymbols (dispatcher, associatedDispatcher) * 2 ;
26
27
adjacencyList.at (dispatcher)
27
28
.insert (Edge{
@@ -35,7 +36,8 @@ void DispatcherGraph::addDispatcher(ClauseDispatcher *dispatcher) {
35
36
weight,
36
37
});
37
38
}
38
- symbols.at (symbol).insert (dispatcher);
39
+ symbolsToClauseDispatchersMap.at (symbol).insert (dispatcher);
40
+ symbols.insert (symbol);
39
41
}
40
42
totalPriority += dispatcher->dispatchPriority ();
41
43
}
@@ -53,7 +55,7 @@ int DispatcherGraph::countCommonSymbols(ClauseDispatcher *first,
53
55
54
56
void DispatcherGraph::ensureSymbolsNotContainedInOtherGraph (
55
57
const DispatcherGraph *otherGraph) const {
56
- for (const auto &symbolPair : symbols ) {
58
+ for (const auto &symbolPair : symbolsToClauseDispatchersMap ) {
57
59
if (otherGraph->contains (symbolPair.first )) {
58
60
throw " ERROR: There exists common symbol between the two graphs" ;
59
61
}
@@ -63,7 +65,7 @@ void DispatcherGraph::ensureSymbolsNotContainedInOtherGraph(
63
65
void DispatcherGraph::ensureHasOneCommonSymbolWith (
64
66
ClauseDispatcher *dispatcher) const {
65
67
for (const auto &symbol : dispatcher->getSymbols ()) {
66
- if (mapContains (symbols , symbol)) {
68
+ if (mapContains (symbolsToClauseDispatchersMap , symbol)) {
67
69
return ;
68
70
}
69
71
}
@@ -80,15 +82,18 @@ void DispatcherGraph::merge(DispatcherGraph &otherGraph,
80
82
for (const auto &[clause, edges] : otherGraph.adjacencyList ) {
81
83
adjacencyList[clause].insert (edges.begin (), edges.end ());
82
84
}
83
- for (const auto &[symbol, clauses] : otherGraph.symbols ) {
84
- symbols[symbol].insert (clauses.begin (), clauses.end ());
85
+ for (const auto &[symbol, clauses] :
86
+ otherGraph.symbolsToClauseDispatchersMap ) {
87
+ symbolsToClauseDispatchersMap[symbol].insert (clauses.begin (),
88
+ clauses.end ());
85
89
}
86
90
totalPriority += otherGraph.totalPriority ;
91
+ symbols.insert (otherGraph.symbols .begin (), otherGraph.symbols .end ());
87
92
addDispatcher (dispatcher);
88
93
}
89
94
90
95
bool DispatcherGraph::contains (SYMBOL symbol) const {
91
- return mapContains (symbols , symbol);
96
+ return mapContains (symbolsToClauseDispatchersMap , symbol);
92
97
}
93
98
94
99
bool DispatcherGraph::contains (ClauseDispatcher *clauseDispatcher) const {
@@ -97,7 +102,8 @@ bool DispatcherGraph::contains(ClauseDispatcher *clauseDispatcher) const {
97
102
98
103
int DispatcherGraph::priority () { return totalPriority; }
99
104
100
- EvaluationTable DispatcherGraph::evaluate () {
105
+ EvaluationTable
106
+ DispatcherGraph::evaluate (std::unordered_set<SYMBOL> selectedSymbols) {
101
107
typedef std::pair<int , ClauseDispatcher *> PQ_NODE;
102
108
auto compare = [](PQ_NODE &node1, PQ_NODE &node2) {
103
109
return node1.first < node2.first ;
@@ -135,6 +141,22 @@ EvaluationTable DispatcherGraph::evaluate() {
135
141
if (table.rowCount () == 0 ) {
136
142
return table;
137
143
}
144
+ auto symbolDeleted = false ;
145
+ for (const auto &symbol : dispatcher->getSymbols ()) {
146
+ if (mapContains (symbolsToClauseDispatchersMap, symbol) &&
147
+ setContains (symbolsToClauseDispatchersMap.at (symbol), dispatcher)) {
148
+ symbolsToClauseDispatchersMap.at (symbol).erase (dispatcher);
149
+ if (symbolsToClauseDispatchersMap.at (symbol).empty () &&
150
+ !setContains (selectedSymbols, symbol)) {
151
+ symbols.erase (symbol);
152
+ symbolDeleted = true ;
153
+ symbolsToClauseDispatchersMap.erase (symbol);
154
+ }
155
+ }
156
+ }
157
+ if (symbolDeleted)
158
+ table = table.sliceSymbols (symbols);
159
+
138
160
for (const auto &e : adjacencyList.at (dispatcher)) {
139
161
int pqWeight = e.weight + e.neighbour ->dispatchPriority ();
140
162
pq.push (PQ_NODE{pqWeight, e.neighbour });
@@ -145,5 +167,6 @@ EvaluationTable DispatcherGraph::evaluate() {
145
167
};
146
168
147
169
bool DispatcherGraph::operator ==(const DispatcherGraph &other) const {
148
- return adjacencyList == other.adjacencyList && symbols == other.symbols ;
170
+ return adjacencyList == other.adjacencyList &&
171
+ symbolsToClauseDispatchersMap == other.symbolsToClauseDispatchersMap ;
149
172
}
0 commit comments