GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/base/configuration.cpp Lines: 109 143 76.2 %
Date: 2021-08-17 Branches: 117 292 40.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 <sstream>
22
#include <string>
23
24
#include "base/configuration_private.h"
25
#include "base/cvc5config.h"
26
27
#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
28
#  include "base/Debug_tags.h"
29
#endif /* CVC5_DEBUG && CVC5_TRACING */
30
31
#ifdef CVC5_TRACING
32
#  include "base/Trace_tags.h"
33
#endif /* CVC5_TRACING */
34
35
using namespace std;
36
37
namespace cvc5 {
38
39
3
string Configuration::getName() { return CVC5_PACKAGE_NAME; }
40
41
330245
bool Configuration::isDebugBuild() {
42
330245
  return IS_DEBUG_BUILD;
43
}
44
45
2610
bool Configuration::isTracingBuild() {
46
2610
  return IS_TRACING_BUILD;
47
}
48
49
2611
bool Configuration::isDumpingBuild() {
50
2611
  return IS_DUMPING_BUILD && !IS_MUZZLED_BUILD;
51
}
52
53
8943
bool Configuration::isMuzzledBuild() {
54
8943
  return IS_MUZZLED_BUILD;
55
}
56
57
2872711
bool Configuration::isAssertionBuild() {
58
2872711
  return IS_ASSERTIONS_BUILD;
59
}
60
61
2610
bool Configuration::isCoverageBuild() {
62
2610
  return IS_COVERAGE_BUILD;
63
}
64
65
2610
bool Configuration::isProfilingBuild() {
66
2610
  return IS_PROFILING_BUILD;
67
}
68
69
2608
bool Configuration::isAsanBuild() { return IS_ASAN_BUILD; }
70
71
2608
bool Configuration::isUbsanBuild() { return IS_UBSAN_BUILD; }
72
73
2608
bool Configuration::isTsanBuild() { return IS_TSAN_BUILD; }
74
75
2608
bool Configuration::isCompetitionBuild() {
76
2608
  return IS_COMPETITION_BUILD;
77
}
78
79
2611
bool Configuration::isStaticBuild()
80
{
81
#if defined(CVC5_STATIC_BUILD)
82
2611
  return true;
83
#else
84
  return false;
85
#endif
86
}
87
88
2
string Configuration::getPackageName() { return CVC5_PACKAGE_NAME; }
89
90
2611
string Configuration::getVersionString() { return CVC5_RELEASE_STRING; }
91
92
2610
unsigned Configuration::getVersionMajor() { return CVC5_MAJOR; }
93
94
2610
unsigned Configuration::getVersionMinor() { return CVC5_MINOR; }
95
96
2610
unsigned Configuration::getVersionRelease() { return CVC5_RELEASE; }
97
98
std::string Configuration::getVersionExtra() { return CVC5_EXTRAVERSION; }
99
100
2611
std::string Configuration::copyright() {
101
5222
  std::stringstream ss;
102
  ss << "Copyright (c) 2009-2021 by the authors and their institutional\n"
103
2611
     << "affiliations listed at https://cvc5.github.io/people.html\n\n";
104
105
2611
  if (Configuration::licenseIsGpl()) {
106
    ss << "This build of cvc5 uses GPLed libraries, and is thus covered by\n"
107
       << "the GNU General Public License (GPL) version 3.  Versions of cvc5\n"
108
       << "are available that are covered by the (modified) BSD license. If\n"
109
       << "you want to license cvc5 under this license, please configure cvc5\n"
110
2611
       << "with the \"--no-gpl\" option before building from sources.\n\n";
111
  } else {
112
    ss << "cvc5 is open-source and is covered by the BSD license (modified)."
113
       << "\n\n";
114
  }
115
116
  ss << "THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.\n"
117
2611
     << "USE AT YOUR OWN RISK.\n\n";
118
119
  ss << "cvc5 incorporates code from ANTLR3 (http://www.antlr.org).\n"
120
     << "See licenses/antlr3-LICENSE for copyright and licensing information."
121
2611
     << "\n\n";
122
123
  ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
124
2611
     << "third party libraries.\n\n";
125
126
  ss << "  CaDiCaL - Simplified Satisfiability Solver\n"
127
     << "  See https://github.com/arminbiere/cadical for copyright "
128
2611
     << "information.\n\n";
129
130
5222
  if (Configuration::isBuiltWithAbc()
131
2611
      || Configuration::isBuiltWithCryptominisat()
132
      || Configuration::isBuiltWithKissat()
133
2611
      || Configuration::isBuiltWithEditline())
134
  {
135
2611
    if (Configuration::isBuiltWithAbc()) {
136
      ss << "  ABC - A System for Sequential Synthesis and Verification\n"
137
         << "  See http://bitbucket.org/alanmi/abc for copyright and\n"
138
         << "  licensing information.\n\n";
139
    }
140
2611
    if (Configuration::isBuiltWithCryptominisat())
141
    {
142
      ss << "  CryptoMiniSat - An Advanced SAT Solver\n"
143
         << "  See https://github.com/msoos/cryptominisat for copyright "
144
2611
         << "information.\n\n";
145
    }
146
2611
    if (Configuration::isBuiltWithKissat())
147
    {
148
      ss << "  Kissat - Simplified Satisfiability Solver\n"
149
         << "  See https://fmv.jku.at/kissat for copyright "
150
         << "information.\n\n";
151
    }
152
2611
    if (Configuration::isBuiltWithEditline())
153
    {
154
      ss << "  Editline Library\n"
155
         << "  See https://thrysoee.dk/editline\n"
156
         << "  for copyright information.\n\n";
157
    }
158
  }
159
160
  ss << "  SymFPU - The Symbolic Floating Point Unit\n"
161
     << "  See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
162
2611
     << "information.\n\n";
163
164
2611
  if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly())
165
  {
166
    ss << "This version of cvc5 is linked against the following third party\n"
167
       << "libraries covered by the LGPLv3 license.\n"
168
2611
       << "See licenses/lgpl-3.0.txt for more information.\n\n";
169
2611
    if (Configuration::isBuiltWithGmp()) {
170
      ss << "  GMP - Gnu Multi Precision Arithmetic Library\n"
171
         << "  See http://gmplib.org for copyright information.\n\n";
172
    }
173
2611
    if (Configuration::isBuiltWithPoly())
174
    {
175
      ss << "  LibPoly polynomial library\n"
176
         << "  See https://github.com/SRI-CSL/libpoly for copyright and\n"
177
2611
         << "  licensing information.\n\n";
178
    }
179
2611
    if (Configuration::isStaticBuild())
180
    {
181
2611
      ss << "cvc5 is statically linked against these libraries. To recompile\n"
182
            "this version of cvc5 with different versions of these libraries\n"
183
            "follow the instructions on "
184
            "https://github.com/cvc5/cvc5/blob/master/INSTALL.md\n\n";
185
    }
186
  }
187
188
5222
  if (Configuration::isBuiltWithCln()
189
2611
      || Configuration::isBuiltWithGlpk ()) {
190
    ss << "This version of cvc5 is linked against the following third party\n"
191
       << "libraries covered by the GPLv3 license.\n"
192
2611
       << "See licenses/gpl-3.0.txt for more information.\n\n";
193
2611
    if (Configuration::isBuiltWithCln()) {
194
      ss << "  CLN - Class Library for Numbers\n"
195
2611
         << "  See http://www.ginac.de/CLN for copyright information.\n\n";
196
    }
197
2611
    if (Configuration::isBuiltWithGlpk()) {
198
      ss << "  glpk-cut-log - a modified version of GPLK, "
199
         << "the GNU Linear Programming Kit\n"
200
         << "  See http://github.com/timothy-king/glpk-cut-log for copyright"
201
         << " information\n\n";
202
    }
203
  }
204
205
  ss << "See the file COPYING (distributed with the source code, and with\n"
206
     << "all binaries) for the full cvc5 copyright, licensing, and (lack of)\n"
207
2611
     << "warranty information.\n";
208
5222
  return ss.str();
209
}
210
211
2611
std::string Configuration::about() {
212
5222
  std::stringstream ss;
213
2611
  ss << "This is cvc5 version " << CVC5_RELEASE_STRING;
214
2611
  if (Configuration::isGitBuild()) {
215
2611
    ss << " [" << Configuration::getGitId() << "]";
216
  }
217
5222
  ss << "\ncompiled with " << Configuration::getCompiler()
218
5222
     << "\non " << Configuration::getCompiledDateTime() << "\n\n";
219
2611
  ss << Configuration::copyright ();
220
5222
  return ss.str();
221
}
222
223
2611
bool Configuration::licenseIsGpl() {
224
2611
  return IS_GPL_BUILD;
225
}
226
227
7830
bool Configuration::isBuiltWithGmp() {
228
7830
  return IS_GMP_BUILD;
229
}
230
231
7830
bool Configuration::isBuiltWithCln() {
232
7830
  return IS_CLN_BUILD;
233
}
234
235
5219
bool Configuration::isBuiltWithGlpk() {
236
5219
  return IS_GLPK_BUILD;
237
}
238
239
7830
bool Configuration::isBuiltWithAbc() {
240
7830
  return IS_ABC_BUILD;
241
}
242
243
7840
bool Configuration::isBuiltWithCryptominisat() {
244
7840
  return IS_CRYPTOMINISAT_BUILD;
245
}
246
247
5219
bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; }
248
249
5219
bool Configuration::isBuiltWithEditline() { return IS_EDITLINE_BUILD; }
250
251
7830
bool Configuration::isBuiltWithPoly()
252
{
253
7830
  return IS_POLY_BUILD;
254
}
255
256
unsigned Configuration::getNumDebugTags() {
257
#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
258
  /* -1 because a NULL pointer is inserted as the last value */
259
  return (sizeof(Debug_tags) / sizeof(Debug_tags[0])) - 1;
260
#else  /* CVC5_DEBUG && CVC5_TRACING */
261
  return 0;
262
#endif /* CVC5_DEBUG && CVC5_TRACING */
263
}
264
265
char const* const* Configuration::getDebugTags() {
266
#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
267
  return Debug_tags;
268
#else  /* CVC5_DEBUG && CVC5_TRACING */
269
  static char const* no_tags[] = { NULL };
270
  return no_tags;
271
#endif /* CVC5_DEBUG && CVC5_TRACING */
272
}
273
274
int strcmpptr(const char **s1, const char **s2){
275
  return strcmp(*s1,*s2);
276
}
277
278
bool Configuration::isDebugTag(char const *tag){
279
#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
280
  unsigned ntags = getNumDebugTags();
281
  char const* const* tags = getDebugTags();
282
  for (unsigned i = 0; i < ntags; ++ i) {
283
    if (strcmp(tag, tags[i]) == 0) {
284
      return true;
285
    }
286
  }
287
#endif /* CVC5_DEBUG && CVC5_TRACING */
288
  return false;
289
}
290
291
unsigned Configuration::getNumTraceTags() {
292
#if CVC5_TRACING
293
  /* -1 because a NULL pointer is inserted as the last value */
294
  return sizeof(Trace_tags) / sizeof(Trace_tags[0]) - 1;
295
#else  /* CVC5_TRACING */
296
  return 0;
297
#endif /* CVC5_TRACING */
298
}
299
300
char const* const* Configuration::getTraceTags() {
301
#if CVC5_TRACING
302
  return Trace_tags;
303
#else  /* CVC5_TRACING */
304
  static char const* no_tags[] = { NULL };
305
  return no_tags;
306
#endif /* CVC5_TRACING */
307
}
308
309
bool Configuration::isTraceTag(char const * tag){
310
#if CVC5_TRACING
311
  unsigned ntags = getNumTraceTags();
312
  char const* const* tags = getTraceTags();
313
  for (unsigned i = 0; i < ntags; ++ i) {
314
    if (strcmp(tag, tags[i]) == 0) {
315
      return true;
316
    }
317
  }
318
#endif /* CVC5_TRACING */
319
  return false;
320
}
321
322
7830
bool Configuration::isGitBuild() {
323
7830
  return IS_GIT_BUILD;
324
}
325
326
5219
const char* Configuration::getGitBranchName() {
327
5219
  return GIT_BRANCH_NAME;
328
}
329
330
5219
const char* Configuration::getGitCommit() {
331
5219
  return GIT_COMMIT;
332
}
333
334
5219
bool Configuration::hasGitModifications() {
335
5219
  return GIT_HAS_MODIFICATIONS;
336
}
337
338
2611
std::string Configuration::getGitId() {
339
2611
  if(! isGitBuild()) {
340
    return "";
341
  }
342
343
2611
  const char* branchName = getGitBranchName();
344
2611
  if(*branchName == '\0') {
345
    branchName = "-";
346
  }
347
348
5222
  stringstream ss;
349
5222
  ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8)
350
5222
     << (::cvc5::Configuration::hasGitModifications() ? " (with modifications)"
351
7833
                                                      : "");
352
2611
  return ss.str();
353
}
354
355
2611
std::string Configuration::getCompiler() {
356
5222
  stringstream ss;
357
#ifdef __GNUC__
358
2611
  ss << "GCC";
359
#else /* __GNUC__ */
360
  ss << "unknown compiler";
361
#endif /* __GNUC__ */
362
#ifdef __VERSION__
363
2611
  ss << " version " << __VERSION__;
364
#else /* __VERSION__ */
365
  ss << ", unknown version";
366
#endif /* __VERSION__ */
367
5222
  return ss.str();
368
}
369
370
2611
std::string Configuration::getCompiledDateTime() {
371
2611
  return __DATE__ " " __TIME__;
372
}
373
374
}  // namespace cvc5