1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz, Mudathir Mohamed |
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 |
|
* [[ Add one-line brief description here ]] |
14 |
|
* |
15 |
|
* [[ Add lengthier description here ]] |
16 |
|
* \todo document this file |
17 |
|
*/ |
18 |
|
|
19 |
|
#include "theory/theory_id.h" |
20 |
|
|
21 |
|
#include <sstream> |
22 |
|
|
23 |
|
#include "base/check.h" |
24 |
|
#include "lib/ffs.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace theory { |
28 |
|
|
29 |
162171815 |
TheoryId& operator++(TheoryId& id) |
30 |
|
{ |
31 |
162171815 |
return id = static_cast<TheoryId>(static_cast<int>(id) + 1); |
32 |
|
} |
33 |
|
|
34 |
3033620 |
std::ostream& operator<<(std::ostream& out, TheoryId theoryId) |
35 |
|
{ |
36 |
3033620 |
switch (theoryId) |
37 |
|
{ |
38 |
356180 |
case THEORY_BUILTIN: out << "THEORY_BUILTIN"; break; |
39 |
33861 |
case THEORY_BOOL: out << "THEORY_BOOL"; break; |
40 |
681899 |
case THEORY_UF: out << "THEORY_UF"; break; |
41 |
842154 |
case THEORY_ARITH: out << "THEORY_ARITH"; break; |
42 |
274681 |
case THEORY_BV: out << "THEORY_BV"; break; |
43 |
5934 |
case THEORY_FP: out << "THEORY_FP"; break; |
44 |
176757 |
case THEORY_ARRAYS: out << "THEORY_ARRAYS"; break; |
45 |
386648 |
case THEORY_DATATYPES: out << "THEORY_DATATYPES"; break; |
46 |
|
case THEORY_SAT_SOLVER: out << "THEORY_SAT_SOLVER"; break; |
47 |
1793 |
case THEORY_SEP: out << "THEORY_SEP"; break; |
48 |
53229 |
case THEORY_SETS: out << "THEORY_SETS"; break; |
49 |
8944 |
case THEORY_BAGS: out << "THEORY_BAGS"; break; |
50 |
210431 |
case THEORY_STRINGS: out << "THEORY_STRINGS"; break; |
51 |
1109 |
case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break; |
52 |
|
|
53 |
|
default: out << "UNKNOWN_THEORY"; break; |
54 |
|
} |
55 |
3033620 |
return out; |
56 |
|
} |
57 |
|
|
58 |
1247823 |
std::string getStatsPrefix(TheoryId theoryId) |
59 |
|
{ |
60 |
1247823 |
switch (theoryId) |
61 |
|
{ |
62 |
95300 |
case THEORY_BUILTIN: return "theory::builtin::"; break; |
63 |
95288 |
case THEORY_BOOL: return "theory::bool::"; break; |
64 |
95288 |
case THEORY_UF: return "theory::uf::"; break; |
65 |
95288 |
case THEORY_ARITH: return "theory::arith::"; break; |
66 |
104733 |
case THEORY_BV: return "theory::bv::"; break; |
67 |
95234 |
case THEORY_FP: return "theory::fp::"; break; |
68 |
95288 |
case THEORY_ARRAYS: return "theory::arrays::"; break; |
69 |
95234 |
case THEORY_DATATYPES: return "theory::datatypes::"; break; |
70 |
95234 |
case THEORY_SEP: return "theory::sep::"; break; |
71 |
95234 |
case THEORY_SETS: return "theory::sets::"; break; |
72 |
95234 |
case THEORY_BAGS: return "theory::bags::"; break; |
73 |
95234 |
case THEORY_STRINGS: return "theory::strings::"; break; |
74 |
95234 |
case THEORY_QUANTIFIERS: return "theory::quantifiers::"; break; |
75 |
|
|
76 |
|
default: break; |
77 |
|
} |
78 |
|
return "unknown::"; |
79 |
|
} |
80 |
|
|
81 |
52633591 |
TheoryId TheoryIdSetUtil::setPop(TheoryIdSet& set) |
82 |
|
{ |
83 |
52633591 |
uint32_t i = ffs(set); // Find First Set (bit) |
84 |
52633591 |
if (i == 0) |
85 |
|
{ |
86 |
8256246 |
return THEORY_LAST; |
87 |
|
} |
88 |
44377345 |
TheoryId id = static_cast<TheoryId>(i - 1); |
89 |
44377345 |
set = setRemove(id, set); |
90 |
44377345 |
return id; |
91 |
|
} |
92 |
|
|
93 |
|
size_t TheoryIdSetUtil::setSize(TheoryIdSet set) |
94 |
|
{ |
95 |
|
size_t count = 0; |
96 |
|
while (setPop(set) != THEORY_LAST) |
97 |
|
{ |
98 |
|
++count; |
99 |
|
} |
100 |
|
return count; |
101 |
|
} |
102 |
|
|
103 |
3321596 |
size_t TheoryIdSetUtil::setIndex(TheoryId id, TheoryIdSet set) |
104 |
|
{ |
105 |
3321596 |
Assert(setContains(id, set)); |
106 |
3321596 |
size_t count = 0; |
107 |
11413344 |
while (setPop(set) != id) |
108 |
|
{ |
109 |
4045874 |
++count; |
110 |
|
} |
111 |
3321596 |
return count; |
112 |
|
} |
113 |
|
|
114 |
74737224 |
TheoryIdSet TheoryIdSetUtil::setInsert(TheoryId theory, TheoryIdSet set) |
115 |
|
{ |
116 |
74737224 |
return set | (1 << theory); |
117 |
|
} |
118 |
|
|
119 |
45518003 |
TheoryIdSet TheoryIdSetUtil::setRemove(TheoryId theory, TheoryIdSet set) |
120 |
|
{ |
121 |
45518003 |
return setDifference(set, setInsert(theory)); |
122 |
|
} |
123 |
|
|
124 |
213254062 |
bool TheoryIdSetUtil::setContains(TheoryId theory, TheoryIdSet set) |
125 |
|
{ |
126 |
213254062 |
return set & (1 << theory); |
127 |
|
} |
128 |
|
|
129 |
|
TheoryIdSet TheoryIdSetUtil::setComplement(TheoryIdSet a) |
130 |
|
{ |
131 |
|
return (~a) & AllTheories; |
132 |
|
} |
133 |
|
|
134 |
17918216 |
TheoryIdSet TheoryIdSetUtil::setIntersection(TheoryIdSet a, TheoryIdSet b) |
135 |
|
{ |
136 |
17918216 |
return a & b; |
137 |
|
} |
138 |
|
|
139 |
7821418 |
TheoryIdSet TheoryIdSetUtil::setUnion(TheoryIdSet a, TheoryIdSet b) |
140 |
|
{ |
141 |
7821418 |
return a | b; |
142 |
|
} |
143 |
|
|
144 |
117619826 |
TheoryIdSet TheoryIdSetUtil::setDifference(TheoryIdSet a, TheoryIdSet b) |
145 |
|
{ |
146 |
117619826 |
return (~b) & a; |
147 |
|
} |
148 |
|
|
149 |
1349742 |
std::string TheoryIdSetUtil::setToString(TheoryIdSet theorySet) |
150 |
|
{ |
151 |
2699484 |
std::stringstream ss; |
152 |
1349742 |
ss << "["; |
153 |
18896388 |
for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++theoryId) |
154 |
|
{ |
155 |
17546646 |
TheoryId tid = static_cast<TheoryId>(theoryId); |
156 |
17546646 |
if (setContains(tid, theorySet)) |
157 |
|
{ |
158 |
2436924 |
ss << tid << " "; |
159 |
|
} |
160 |
|
} |
161 |
1349742 |
ss << "]"; |
162 |
2699484 |
return ss.str(); |
163 |
|
} |
164 |
|
|
165 |
|
} // namespace theory |
166 |
|
} // namespace cvc5 |