1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Tim King |
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 |
|
* Implementation of trigger trie class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/ematching/trigger_trie.h" |
17 |
|
|
18 |
|
namespace cvc5 { |
19 |
|
namespace theory { |
20 |
|
namespace quantifiers { |
21 |
|
namespace inst { |
22 |
|
|
23 |
25167 |
TriggerTrie::TriggerTrie() {} |
24 |
|
|
25 |
50328 |
TriggerTrie::~TriggerTrie() |
26 |
|
{ |
27 |
42197 |
for (size_t i = 0, ntriggers = d_tr.size(); i < ntriggers; i++) |
28 |
|
{ |
29 |
17033 |
delete d_tr[i]; |
30 |
|
} |
31 |
25164 |
} |
32 |
|
|
33 |
13267 |
inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes) |
34 |
|
{ |
35 |
26534 |
std::vector<Node> temp; |
36 |
13267 |
temp.insert(temp.begin(), nodes.begin(), nodes.end()); |
37 |
13267 |
std::sort(temp.begin(), temp.end()); |
38 |
13267 |
TriggerTrie* tt = this; |
39 |
13475 |
for (const Node& n : temp) |
40 |
|
{ |
41 |
13380 |
std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n); |
42 |
13380 |
if (itt == tt->d_children.end()) |
43 |
|
{ |
44 |
13172 |
return nullptr; |
45 |
|
} |
46 |
|
else |
47 |
|
{ |
48 |
208 |
tt = &(itt->second); |
49 |
|
} |
50 |
|
} |
51 |
95 |
return tt->d_tr.empty() ? nullptr : tt->d_tr[0]; |
52 |
|
} |
53 |
|
|
54 |
17033 |
void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t) |
55 |
|
{ |
56 |
34066 |
std::vector<Node> temp(nodes.begin(), nodes.end()); |
57 |
17033 |
std::sort(temp.begin(), temp.end()); |
58 |
17033 |
TriggerTrie* tt = this; |
59 |
35657 |
for (const Node& n : temp) |
60 |
|
{ |
61 |
18624 |
std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n); |
62 |
18624 |
if (itt == tt->d_children.end()) |
63 |
|
{ |
64 |
18590 |
TriggerTrie* ttn = &tt->d_children[n]; |
65 |
18590 |
tt = ttn; |
66 |
|
} |
67 |
|
else |
68 |
|
{ |
69 |
34 |
tt = &(itt->second); |
70 |
|
} |
71 |
|
} |
72 |
17033 |
tt->d_tr.push_back(t); |
73 |
17033 |
} |
74 |
|
|
75 |
|
} // namespace inst |
76 |
|
} // namespace quantifiers |
77 |
|
} // namespace theory |
78 |
29577 |
} // namespace cvc5 |