GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/base/configuration.cpp Lines: 92 106 86.8 %
Date: 2021-11-07 Branches: 101 246 41.1 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Morgan Deters, Aina Niemetz, Mathias Preiner
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 Configuration class, which provides compile-time
14
 * configuration information about the cvc5 library.
15
 */
16
#include "base/configuration.h"
17
18
#include <stdlib.h>
19
#include <string.h>
20
21
#include <algorithm>
22
#include <sstream>
23
#include <string>
24
25
#include "base/Debug_tags.h"
26
#include "base/Trace_tags.h"
27
#include "base/configuration_private.h"
28
#include "base/cvc5config.h"
29
30
using namespace std;
31
32
namespace cvc5 {
33
34
4
string Configuration::getName() { return CVC5_PACKAGE_NAME; }
35
36
317992
bool Configuration::isDebugBuild() {
37
317992
  return IS_DEBUG_BUILD;
38
}
39
40
2731
bool Configuration::isTracingBuild() {
41
2731
  return IS_TRACING_BUILD;
42
}
43
44
2728
bool Configuration::isDumpingBuild() {
45
2728
  return IS_DUMPING_BUILD && !IS_MUZZLED_BUILD;
46
}
47
48
416657
bool Configuration::isMuzzledBuild() {
49
416657
  return IS_MUZZLED_BUILD;
50
}
51
52
4748171
bool Configuration::isAssertionBuild() {
53
4748171
  return IS_ASSERTIONS_BUILD;
54
}
55
56
2730
bool Configuration::isCoverageBuild() {
57
2730
  return IS_COVERAGE_BUILD;
58
}
59
60
2730
bool Configuration::isProfilingBuild() {
61
2730
  return IS_PROFILING_BUILD;
62
}
63
64
2728
bool Configuration::isAsanBuild() { return IS_ASAN_BUILD; }
65
66
2728
bool Configuration::isUbsanBuild() { return IS_UBSAN_BUILD; }
67
68
2728
bool Configuration::isTsanBuild() { return IS_TSAN_BUILD; }
69
70
2728
bool Configuration::isCompetitionBuild() {
71
2728
  return IS_COMPETITION_BUILD;
72
}
73
74
2731
bool Configuration::isStaticBuild()
75
{
76
2731
  return CVC5_STATIC_BUILD;
77
}
78
79
2
string Configuration::getPackageName() { return CVC5_PACKAGE_NAME; }
80
81
8190
string Configuration::getVersionString() { return CVC5_FULL_VERSION; }
82
83
2731
std::string Configuration::copyright() {
84
5462
  std::stringstream ss;
85
  ss << "Copyright (c) 2009-2021 by the authors and their institutional\n"
86
2731
     << "affiliations listed at https://cvc5.github.io/people.html\n\n";
87
88
2731
  if (Configuration::licenseIsGpl()) {
89
    ss << "This build of cvc5 uses GPLed libraries, and is thus covered by\n"
90
       << "the GNU General Public License (GPL) version 3.  Versions of cvc5\n"
91
       << "are available that are covered by the (modified) BSD license. If\n"
92
       << "you want to license cvc5 under this license, please configure cvc5\n"
93
2731
       << "with the \"--no-gpl\" option before building from sources.\n\n";
94
  } else {
95
    ss << "cvc5 is open-source and is covered by the BSD license (modified)."
96
       << "\n\n";
97
  }
98
99
  ss << "THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.\n"
100
2731
     << "USE AT YOUR OWN RISK.\n\n";
101
102
  ss << "cvc5 incorporates code from ANTLR3 (http://www.antlr.org).\n"
103
     << "See licenses/antlr3-LICENSE for copyright and licensing information."
104
2731
     << "\n\n";
105
106
  ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
107
2731
     << "third party libraries.\n\n";
108
109
  ss << "  CaDiCaL - Simplified Satisfiability Solver\n"
110
     << "  See https://github.com/arminbiere/cadical for copyright "
111
2731
     << "information.\n\n";
112
113
5462
  if (Configuration::isBuiltWithCryptominisat()
114
      || Configuration::isBuiltWithKissat()
115
2731
      || Configuration::isBuiltWithEditline())
116
  {
117
2731
    if (Configuration::isBuiltWithCryptominisat())
118
    {
119
      ss << "  CryptoMiniSat - An Advanced SAT Solver\n"
120
         << "  See https://github.com/msoos/cryptominisat for copyright "
121
2731
         << "information.\n\n";
122
    }
123
2731
    if (Configuration::isBuiltWithKissat())
124
    {
125
      ss << "  Kissat - Simplified Satisfiability Solver\n"
126
         << "  See https://fmv.jku.at/kissat for copyright "
127
         << "information.\n\n";
128
    }
129
2731
    if (Configuration::isBuiltWithEditline())
130
    {
131
      ss << "  Editline Library\n"
132
         << "  See https://thrysoee.dk/editline\n"
133
         << "  for copyright information.\n\n";
134
    }
135
  }
136
137
  ss << "  SymFPU - The Symbolic Floating Point Unit\n"
138
     << "  See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
139
2731
     << "information.\n\n";
140
141
2731
  if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly())
142
  {
143
    ss << "This version of cvc5 is linked against the following third party\n"
144
       << "libraries covered by the LGPLv3 license.\n"
145
2731
       << "See licenses/lgpl-3.0.txt for more information.\n\n";
146
2731
    if (Configuration::isBuiltWithGmp()) {
147
      ss << "  GMP - Gnu Multi Precision Arithmetic Library\n"
148
         << "  See http://gmplib.org for copyright information.\n\n";
149
    }
150
2731
    if (Configuration::isBuiltWithPoly())
151
    {
152
      ss << "  LibPoly polynomial library\n"
153
         << "  See https://github.com/SRI-CSL/libpoly for copyright and\n"
154
2731
         << "  licensing information.\n\n";
155
    }
156
2731
    if (Configuration::isStaticBuild())
157
    {
158
      ss << "cvc5 is statically linked against these libraries. To recompile\n"
159
            "this version of cvc5 with different versions of these libraries\n"
160
            "follow the instructions on "
161
            "https://github.com/cvc5/cvc5/blob/master/INSTALL.md\n\n";
162
    }
163
  }
164
165
5462
  if (Configuration::isBuiltWithCln()
166
2731
      || Configuration::isBuiltWithGlpk ()) {
167
    ss << "This version of cvc5 is linked against the following third party\n"
168
       << "libraries covered by the GPLv3 license.\n"
169
2731
       << "See licenses/gpl-3.0.txt for more information.\n\n";
170
2731
    if (Configuration::isBuiltWithCln()) {
171
      ss << "  CLN - Class Library for Numbers\n"
172
2731
         << "  See http://www.ginac.de/CLN for copyright information.\n\n";
173
    }
174
2731
    if (Configuration::isBuiltWithGlpk()) {
175
      ss << "  glpk-cut-log - a modified version of GPLK, "
176
         << "the GNU Linear Programming Kit\n"
177
         << "  See http://github.com/timothy-king/glpk-cut-log for copyright"
178
         << " information\n\n";
179
    }
180
  }
181
182
  ss << "See the file COPYING (distributed with the source code, and with\n"
183
     << "all binaries) for the full cvc5 copyright, licensing, and (lack of)\n"
184
2731
     << "warranty information.\n";
185
5462
  return ss.str();
186
}
187
188
2731
std::string Configuration::about() {
189
5462
  std::stringstream ss;
190
2731
  ss << "This is cvc5 version " << getVersionString();
191
2731
  if (Configuration::isGitBuild()) {
192
2731
    ss << " [" << Configuration::getGitInfo() << "]";
193
  }
194
5462
  ss << "\ncompiled with " << Configuration::getCompiler()
195
5462
     << "\non " << Configuration::getCompiledDateTime() << "\n\n";
196
2731
  ss << Configuration::copyright ();
197
5462
  return ss.str();
198
}
199
200
2731
bool Configuration::licenseIsGpl() {
201
2731
  return IS_GPL_BUILD;
202
}
203
204
8190
bool Configuration::isBuiltWithGmp() {
205
8190
  return IS_GMP_BUILD;
206
}
207
208
8190
bool Configuration::isBuiltWithCln() {
209
8190
  return IS_CLN_BUILD;
210
}
211
212
5459
bool Configuration::isBuiltWithGlpk() {
213
5459
  return IS_GLPK_BUILD;
214
}
215
216
8200
bool Configuration::isBuiltWithCryptominisat() {
217
8200
  return IS_CRYPTOMINISAT_BUILD;
218
}
219
220
5459
bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; }
221
222
5459
bool Configuration::isBuiltWithEditline() { return IS_EDITLINE_BUILD; }
223
224
8190
bool Configuration::isBuiltWithPoly()
225
{
226
8190
  return IS_POLY_BUILD;
227
}
228
229
const std::vector<std::string>& Configuration::getDebugTags()
230
{
231
  return Debug_tags;
232
}
233
234
bool Configuration::isDebugTag(const std::string& tag)
235
{
236
  return std::find(Debug_tags.begin(), Debug_tags.end(), tag)
237
         != Debug_tags.end();
238
}
239
240
const std::vector<std::string>& Configuration::getTraceTags()
241
{
242
  return Trace_tags;
243
}
244
245
1
bool Configuration::isTraceTag(const std::string& tag)
246
{
247
2
  return std::find(Trace_tags.begin(), Trace_tags.end(), tag)
248
3
         != Trace_tags.end();
249
}
250
251
5459
bool Configuration::isGitBuild() {
252
5459
  return GIT_BUILD;
253
}
254
255
5459
std::string Configuration::getGitInfo() {
256
5459
  return CVC5_GIT_INFO;
257
}
258
259
2731
std::string Configuration::getCompiler() {
260
5462
  stringstream ss;
261
#ifdef __GNUC__
262
2731
  ss << "GCC";
263
#else /* __GNUC__ */
264
  ss << "unknown compiler";
265
#endif /* __GNUC__ */
266
#ifdef __VERSION__
267
2731
  ss << " version " << __VERSION__;
268
#else /* __VERSION__ */
269
  ss << ", unknown version";
270
#endif /* __VERSION__ */
271
5462
  return ss.str();
272
}
273
274
2731
std::string Configuration::getCompiledDateTime() {
275
2731
  return __DATE__ " " __TIME__;
276
}
277
278
31143
}  // namespace cvc5