GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/base/configuration.cpp Lines: 118 164 72.0 %
Date: 2021-03-22 Branches: 113 322 35.1 %

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