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 |
11318 |
TriggerTrie::TriggerTrie() {} |
24 |
|
|
25 |
22630 |
TriggerTrie::~TriggerTrie() |
26 |
|
{ |
27 |
17487 |
for (size_t i = 0, ntriggers = d_tr.size(); i < ntriggers; i++) |
28 |
|
{ |
29 |
6172 |
delete d_tr[i]; |
30 |
|
} |
31 |
11315 |
} |
32 |
|
|
33 |
4980 |
inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes) |
34 |
|
{ |
35 |
9960 |
std::vector<Node> temp; |
36 |
4980 |
temp.insert(temp.begin(), nodes.begin(), nodes.end()); |
37 |
4980 |
std::sort(temp.begin(), temp.end()); |
38 |
4980 |
TriggerTrie* tt = this; |
39 |
5035 |
for (const Node& n : temp) |
40 |
|
{ |
41 |
5010 |
std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n); |
42 |
5010 |
if (itt == tt->d_children.end()) |
43 |
|
{ |
44 |
4955 |
return nullptr; |
45 |
|
} |
46 |
|
else |
47 |
|
{ |
48 |
55 |
tt = &(itt->second); |
49 |
|
} |
50 |
|
} |
51 |
25 |
return tt->d_tr.empty() ? nullptr : tt->d_tr[0]; |
52 |
|
} |
53 |
|
|
54 |
6172 |
void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t) |
55 |
|
{ |
56 |
12344 |
std::vector<Node> temp(nodes.begin(), nodes.end()); |
57 |
6172 |
std::sort(temp.begin(), temp.end()); |
58 |
6172 |
TriggerTrie* tt = this; |
59 |
12918 |
for (const Node& n : temp) |
60 |
|
{ |
61 |
6746 |
std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n); |
62 |
6746 |
if (itt == tt->d_children.end()) |
63 |
|
{ |
64 |
6738 |
TriggerTrie* ttn = &tt->d_children[n]; |
65 |
6738 |
tt = ttn; |
66 |
|
} |
67 |
|
else |
68 |
|
{ |
69 |
8 |
tt = &(itt->second); |
70 |
|
} |
71 |
|
} |
72 |
6172 |
tt->d_tr.push_back(t); |
73 |
6172 |
} |
74 |
|
|
75 |
|
} // namespace inst |
76 |
|
} // namespace quantifiers |
77 |
|
} // namespace theory |
78 |
22746 |
} // namespace cvc5 |