GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_id.cpp Lines: 67 78 85.9 %
Date: 2021-03-23 Branches: 56 97 57.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_id.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Aina Niemetz, Mudathir Mohamed
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "theory/theory_id.h"
19
20
#include <sstream>
21
22
#include "base/check.h"
23
#include "lib/ffs.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
207988236
TheoryId& operator++(TheoryId& id)
29
{
30
207988236
  return id = static_cast<TheoryId>(static_cast<int>(id) + 1);
31
}
32
33
3027473
std::ostream& operator<<(std::ostream& out, TheoryId theoryId)
34
{
35
3027473
  switch (theoryId)
36
  {
37
427733
    case THEORY_BUILTIN: out << "THEORY_BUILTIN"; break;
38
33418
    case THEORY_BOOL: out << "THEORY_BOOL"; break;
39
670272
    case THEORY_UF: out << "THEORY_UF"; break;
40
828208
    case THEORY_ARITH: out << "THEORY_ARITH"; break;
41
251177
    case THEORY_BV: out << "THEORY_BV"; break;
42
6763
    case THEORY_FP: out << "THEORY_FP"; break;
43
160845
    case THEORY_ARRAYS: out << "THEORY_ARRAYS"; break;
44
384932
    case THEORY_DATATYPES: out << "THEORY_DATATYPES"; break;
45
    case THEORY_SAT_SOLVER: out << "THEORY_SAT_SOLVER"; break;
46
1557
    case THEORY_SEP: out << "THEORY_SEP"; break;
47
42962
    case THEORY_SETS: out << "THEORY_SETS"; break;
48
8463
    case THEORY_BAGS: out << "THEORY_BAGS"; break;
49
210223
    case THEORY_STRINGS: out << "THEORY_STRINGS"; break;
50
920
    case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break;
51
52
    default: out << "UNKNOWN_THEORY"; break;
53
  }
54
3027473
  return out;
55
}
56
57
1061972
std::string getStatsPrefix(TheoryId theoryId)
58
{
59
1061972
  switch (theoryId)
60
  {
61
81039
    case THEORY_BUILTIN: return "theory::builtin"; break;
62
81027
    case THEORY_BOOL: return "theory::bool"; break;
63
81027
    case THEORY_UF: return "theory::uf"; break;
64
81027
    case THEORY_ARITH: return "theory::arith"; break;
65
90014
    case THEORY_BV: return "theory::bv"; break;
66
80973
    case THEORY_FP: return "theory::fp"; break;
67
81027
    case THEORY_ARRAYS: return "theory::arrays"; break;
68
80973
    case THEORY_DATATYPES: return "theory::datatypes"; break;
69
80973
    case THEORY_SEP: return "theory::sep"; break;
70
80973
    case THEORY_SETS: return "theory::sets"; break;
71
80973
    case THEORY_BAGS: return "theory::bags"; break;
72
80973
    case THEORY_STRINGS: return "theory::strings"; break;
73
80973
    case THEORY_QUANTIFIERS: return "theory::quantifiers"; break;
74
75
    default: break;
76
  }
77
  return "unknown";
78
}
79
80
67728766
TheoryId TheoryIdSetUtil::setPop(TheoryIdSet& set)
81
{
82
67728766
  uint32_t i = ffs(set);  // Find First Set (bit)
83
67728766
  if (i == 0)
84
  {
85
9769050
    return THEORY_LAST;
86
  }
87
57959716
  TheoryId id = static_cast<TheoryId>(i - 1);
88
57959716
  set = setRemove(id, set);
89
57959716
  return id;
90
}
91
92
size_t TheoryIdSetUtil::setSize(TheoryIdSet set)
93
{
94
  size_t count = 0;
95
  while (setPop(set) != THEORY_LAST)
96
  {
97
    ++count;
98
  }
99
  return count;
100
}
101
102
3651593
size_t TheoryIdSetUtil::setIndex(TheoryId id, TheoryIdSet set)
103
{
104
3651593
  Assert(setContains(id, set));
105
3651593
  size_t count = 0;
106
13196843
  while (setPop(set) != id)
107
  {
108
4772625
    ++count;
109
  }
110
3651593
  return count;
111
}
112
113
91955382
TheoryIdSet TheoryIdSetUtil::setInsert(TheoryId theory, TheoryIdSet set)
114
{
115
91955382
  return set | (1 << theory);
116
}
117
118
59390163
TheoryIdSet TheoryIdSetUtil::setRemove(TheoryId theory, TheoryIdSet set)
119
{
120
59390163
  return setDifference(set, setInsert(theory));
121
}
122
123
258923048
bool TheoryIdSetUtil::setContains(TheoryId theory, TheoryIdSet set)
124
{
125
258923048
  return set & (1 << theory);
126
}
127
128
TheoryIdSet TheoryIdSetUtil::setComplement(TheoryIdSet a)
129
{
130
  return (~a) & AllTheories;
131
}
132
133
21074013
TheoryIdSet TheoryIdSetUtil::setIntersection(TheoryIdSet a, TheoryIdSet b)
134
{
135
21074013
  return a & b;
136
}
137
138
8030387
TheoryIdSet TheoryIdSetUtil::setUnion(TheoryIdSet a, TheoryIdSet b)
139
{
140
8030387
  return a | b;
141
}
142
143
145646220
TheoryIdSet TheoryIdSetUtil::setDifference(TheoryIdSet a, TheoryIdSet b)
144
{
145
145646220
  return (~b) & a;
146
}
147
148
1274546
std::string TheoryIdSetUtil::setToString(TheoryIdSet theorySet)
149
{
150
2549092
  std::stringstream ss;
151
1274546
  ss << "[";
152
17843644
  for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++theoryId)
153
  {
154
16569098
    TheoryId tid = static_cast<TheoryId>(theoryId);
155
16569098
    if (setContains(tid, theorySet))
156
    {
157
2314199
      ss << tid << " ";
158
    }
159
  }
160
1274546
  ss << "]";
161
2549092
  return ss.str();
162
}
163
164
}  // namespace theory
165
}  // namespace CVC4