1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Tim King, Dejan Jovanovic, Morgan Deters |
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 |
|
* AttributeManager implementation. |
14 |
|
*/ |
15 |
|
#include "expr/attribute.h" |
16 |
|
|
17 |
|
#include <utility> |
18 |
|
|
19 |
|
#include "base/output.h" |
20 |
|
#include "expr/node_value.h" |
21 |
|
|
22 |
|
using namespace std; |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace expr { |
26 |
|
namespace attr { |
27 |
|
|
28 |
7966 |
AttributeManager::AttributeManager() : |
29 |
7966 |
d_inGarbageCollection(false) |
30 |
7966 |
{} |
31 |
|
|
32 |
62288354 |
bool AttributeManager::inGarbageCollection() const { |
33 |
62288354 |
return d_inGarbageCollection; |
34 |
|
} |
35 |
|
|
36 |
|
void AttributeManager::debugHook(int debugFlag) { |
37 |
|
/* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS! |
38 |
|
* debugHook() is an empty function for the purpose of debugging |
39 |
|
* the AttributeManager without recompiling all of cvc5. |
40 |
|
* Formally this is a nop. |
41 |
|
*/ |
42 |
|
} |
43 |
|
|
44 |
30776724 |
void AttributeManager::deleteAllAttributes(NodeValue* nv) { |
45 |
30776724 |
Assert(!inGarbageCollection()); |
46 |
30776724 |
d_bools.erase(nv); |
47 |
30776724 |
deleteFromTable(d_ints, nv); |
48 |
30776724 |
deleteFromTable(d_tnodes, nv); |
49 |
30776724 |
deleteFromTable(d_nodes, nv); |
50 |
30776724 |
deleteFromTable(d_types, nv); |
51 |
30776724 |
deleteFromTable(d_strings, nv); |
52 |
30776724 |
} |
53 |
|
|
54 |
7966 |
void AttributeManager::deleteAllAttributes() { |
55 |
7966 |
d_bools.clear(); |
56 |
7966 |
deleteAllFromTable(d_ints); |
57 |
7966 |
deleteAllFromTable(d_tnodes); |
58 |
7966 |
deleteAllFromTable(d_nodes); |
59 |
7966 |
deleteAllFromTable(d_types); |
60 |
7966 |
deleteAllFromTable(d_strings); |
61 |
7966 |
} |
62 |
|
|
63 |
|
void AttributeManager::deleteAttributes(const AttrIdVec& atids) { |
64 |
|
typedef std::map<uint64_t, std::vector< uint64_t> > AttrToVecMap; |
65 |
|
AttrToVecMap perTableIds; |
66 |
|
|
67 |
|
for(AttrIdVec::const_iterator it = atids.begin(), it_end = atids.end(); it != it_end; ++it) { |
68 |
|
const AttributeUniqueId& pair = *(*it); |
69 |
|
std::vector< uint64_t>& inTable = perTableIds[pair.getTableId()]; |
70 |
|
inTable.push_back(pair.getWithinTypeId()); |
71 |
|
} |
72 |
|
AttrToVecMap::iterator it = perTableIds.begin(), it_end = perTableIds.end(); |
73 |
|
for(; it != it_end; ++it) { |
74 |
|
Assert(((*it).first) <= LastAttrTable); |
75 |
|
AttrTableId tableId = (AttrTableId) ((*it).first); |
76 |
|
std::vector< uint64_t>& ids = (*it).second; |
77 |
|
std::sort(ids.begin(), ids.end()); |
78 |
|
|
79 |
|
switch(tableId) { |
80 |
|
case AttrTableBool: |
81 |
|
Unimplemented() << "delete attributes is unimplemented for bools"; |
82 |
|
break; |
83 |
|
case AttrTableUInt64: |
84 |
|
deleteAttributesFromTable(d_ints, ids); |
85 |
|
break; |
86 |
|
case AttrTableTNode: |
87 |
|
deleteAttributesFromTable(d_tnodes, ids); |
88 |
|
break; |
89 |
|
case AttrTableNode: |
90 |
|
deleteAttributesFromTable(d_nodes, ids); |
91 |
|
break; |
92 |
|
case AttrTableTypeNode: |
93 |
|
deleteAttributesFromTable(d_types, ids); |
94 |
|
break; |
95 |
|
case AttrTableString: |
96 |
|
deleteAttributesFromTable(d_strings, ids); |
97 |
|
break; |
98 |
|
|
99 |
|
case AttrTableCDBool: |
100 |
|
case AttrTableCDUInt64: |
101 |
|
case AttrTableCDTNode: |
102 |
|
case AttrTableCDNode: |
103 |
|
case AttrTableCDString: |
104 |
|
case AttrTableCDPointer: |
105 |
|
Unimplemented() << "CDAttributes cannot be deleted. Contact Tim/Morgan " |
106 |
|
"if this behavior is desired."; |
107 |
|
break; |
108 |
|
|
109 |
|
case LastAttrTable: |
110 |
|
default: |
111 |
|
Unreachable(); |
112 |
|
} |
113 |
|
} |
114 |
|
} |
115 |
|
|
116 |
|
} // namespace attr |
117 |
|
} // namespace expr |
118 |
29322 |
} // namespace cvc5 |