Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/base/configuration.cpp	Lines:	112	148	75.7 %
Date:	2021-05-24	Branches:	121	308	39.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Aina Niemetz, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of Configuration class, which provides compile-time
 * configuration information about the cvc5 library.
 */
#include "base/configuration.h"

#include <stdlib.h>
#include <string.h>

#include <sstream>
#include <string>

#include "base/configuration_private.h"
#include "base/cvc5config.h"

#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
#  include "base/Debug_tags.h"
#endif /* CVC5_DEBUG && CVC5_TRACING */

#ifdef CVC5_TRACING
#  include "base/Trace_tags.h"
#endif /* CVC5_TRACING */

using namespace std;

namespace cvc5 {

string Configuration::getName() { return CVC5_PACKAGE_NAME; }

bool Configuration::isDebugBuild() {
  return IS_DEBUG_BUILD;
}

bool Configuration::isTracingBuild() {
  return IS_TRACING_BUILD;
}

bool Configuration::isDumpingBuild() {
  return IS_DUMPING_BUILD && !IS_MUZZLED_BUILD;
}

bool Configuration::isMuzzledBuild() {
  return IS_MUZZLED_BUILD;
}

bool Configuration::isAssertionBuild() {
  return IS_ASSERTIONS_BUILD;
}

bool Configuration::isCoverageBuild() {
  return IS_COVERAGE_BUILD;
}

bool Configuration::isProfilingBuild() {
  return IS_PROFILING_BUILD;
}

bool Configuration::isAsanBuild() { return IS_ASAN_BUILD; }

bool Configuration::isUbsanBuild() { return IS_UBSAN_BUILD; }

bool Configuration::isTsanBuild() { return IS_TSAN_BUILD; }

bool Configuration::isCompetitionBuild() {
  return IS_COMPETITION_BUILD;
}

bool Configuration::isStaticBuild()
{
#if defined(CVC5_STATIC_BUILD)
  return true;
#else
  return false;
#endif
}

string Configuration::getPackageName() { return CVC5_PACKAGE_NAME; }

string Configuration::getVersionString() { return CVC5_RELEASE_STRING; }

unsigned Configuration::getVersionMajor() { return CVC5_MAJOR; }

unsigned Configuration::getVersionMinor() { return CVC5_MINOR; }

unsigned Configuration::getVersionRelease() { return CVC5_RELEASE; }

std::string Configuration::getVersionExtra() { return CVC5_EXTRAVERSION; }

std::string Configuration::copyright() {
  std::stringstream ss;
  ss << "Copyright (c) 2009-2020 by the authors and their institutional\n"
     << "affiliations listed at http://cvc4.cs.stanford.edu/authors\n\n";

  if (Configuration::licenseIsGpl()) {
    ss << "This build of cvc5 uses GPLed libraries, and is thus covered by\n"
       << "the GNU General Public License (GPL) version 3.  Versions of cvc5\n"
       << "are available that are covered by the (modified) BSD license. If\n"
       << "you want to license cvc5 under this license, please configure cvc5\n"
       << "with the \"--no-gpl\" option before building from sources.\n\n";
  } else {
    ss << "cvc5 is open-source and is covered by the BSD license (modified)."
       << "\n\n";
  }

  ss << "THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.\n"
     << "USE AT YOUR OWN RISK.\n\n";

  ss << "cvc5 incorporates code from ANTLR3 (http://www.antlr.org).\n"
     << "See licenses/antlr3-LICENSE for copyright and licensing information."
     << "\n\n";

  if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical()
      || Configuration::isBuiltWithCryptominisat()
      || Configuration::isBuiltWithKissat()
      || Configuration::isBuiltWithSymFPU()
      || Configuration::isBuiltWithEditline())
  {
    ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
       << "third party libraries.\n\n";
    if (Configuration::isBuiltWithAbc()) {
      ss << "  ABC - A System for Sequential Synthesis and Verification\n"
         << "  See http://bitbucket.org/alanmi/abc for copyright and\n"
         << "  licensing information.\n\n";
    }
    if (Configuration::isBuiltWithCadical())
    {
      ss << "  CaDiCaL - Simplified Satisfiability Solver\n"
         << "  See https://github.com/arminbiere/cadical for copyright "
         << "information.\n\n";
    }
    if (Configuration::isBuiltWithCryptominisat())
    {
      ss << "  CryptoMiniSat - An Advanced SAT Solver\n"
         << "  See https://github.com/msoos/cryptominisat for copyright "
         << "information.\n\n";
    }
    if (Configuration::isBuiltWithKissat())
    {
      ss << "  Kissat - Simplified Satisfiability Solver\n"
         << "  See https://fmv.jku.at/kissat for copyright "
         << "information.\n\n";
    }
    if (Configuration::isBuiltWithSymFPU())
    {
      ss << "  SymFPU - The Symbolic Floating Point Unit\n"
         << "  See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
         << "information.\n\n";
    }
    if (Configuration::isBuiltWithEditline())
    {
      ss << "  Editline Library\n"
         << "  See https://thrysoee.dk/editline\n"
         << "  for copyright information.\n\n";
    }
  }

  if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly())
  {
    ss << "This version of cvc5 is linked against the following third party\n"
       << "libraries covered by the LGPLv3 license.\n"
       << "See licenses/lgpl-3.0.txt for more information.\n\n";
    if (Configuration::isBuiltWithGmp()) {
      ss << "  GMP - Gnu Multi Precision Arithmetic Library\n"
         << "  See http://gmplib.org for copyright information.\n\n";
    }
    if (Configuration::isBuiltWithPoly())
    {
      ss << "  LibPoly polynomial library\n"
         << "  See https://github.com/SRI-CSL/libpoly for copyright and\n"
         << "  licensing information.\n\n";
    }
    if (Configuration::isStaticBuild())
    {
      ss << "cvc5 is statically linked against these libraries. To recompile\n"
            "this version of cvc5 with different versions of these libraries\n"
            "follow the instructions on "
            "https://github.com/CVC4/CVC4/blob/master/INSTALL.md\n\n";
    }
  }

  if (Configuration::isBuiltWithCln()
      || Configuration::isBuiltWithGlpk ()) {
    ss << "This version of cvc5 is linked against the following third party\n"
       << "libraries covered by the GPLv3 license.\n"
       << "See licenses/gpl-3.0.txt for more information.\n\n";
    if (Configuration::isBuiltWithCln()) {
      ss << "  CLN - Class Library for Numbers\n"
         << "  See http://www.ginac.de/CLN for copyright information.\n\n";
    }
    if (Configuration::isBuiltWithGlpk()) {
      ss << "  glpk-cut-log -  a modified version of GPLK, "
         << "the GNU Linear Programming Kit\n"
         << "  See http://github.com/timothy-king/glpk-cut-log for copyright"
         << "information\n\n";
    }
  }

  ss << "See the file COPYING (distributed with the source code, and with\n"
     << "all binaries) for the full cvc5 copyright, licensing, and (lack of)\n"
     << "warranty information.\n";
  return ss.str();
}

std::string Configuration::about() {
  std::stringstream ss;
  ss << "This is cvc5 version " << CVC5_RELEASE_STRING;
  if (Configuration::isGitBuild()) {
    ss << " [" << Configuration::getGitId() << "]";
  }
  ss << "\ncompiled with " << Configuration::getCompiler()
     << "\non " << Configuration::getCompiledDateTime() << "\n\n";
  ss << Configuration::copyright ();
  return ss.str();
}

bool Configuration::licenseIsGpl() {
  return IS_GPL_BUILD;
}

bool Configuration::isBuiltWithGmp() {
  return IS_GMP_BUILD;
}

bool Configuration::isBuiltWithCln() {
  return IS_CLN_BUILD;
}

bool Configuration::isBuiltWithGlpk() {
  return IS_GLPK_BUILD;
}

bool Configuration::isBuiltWithAbc() {
  return IS_ABC_BUILD;
}

bool Configuration::isBuiltWithCadical() { return IS_CADICAL_BUILD; }

bool Configuration::isBuiltWithCryptominisat() {
  return IS_CRYPTOMINISAT_BUILD;
}

bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; }

bool Configuration::isBuiltWithEditline() { return IS_EDITLINE_BUILD; }

bool Configuration::isBuiltWithPoly()
{
  return IS_POLY_BUILD;
}

bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; }

unsigned Configuration::getNumDebugTags() {
#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
  /* -1 because a NULL pointer is inserted as the last value */
  return (sizeof(Debug_tags) / sizeof(Debug_tags[0])) - 1;
#else  /* CVC5_DEBUG && CVC5_TRACING */
  return 0;
#endif /* CVC5_DEBUG && CVC5_TRACING */
}

char const* const* Configuration::getDebugTags() {
#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
  return Debug_tags;
#else  /* CVC5_DEBUG && CVC5_TRACING */
  static char const* no_tags[] = { NULL };
  return no_tags;
#endif /* CVC5_DEBUG && CVC5_TRACING */
}

int strcmpptr(const char **s1, const char **s2){
  return strcmp(*s1,*s2);
}

bool Configuration::isDebugTag(char const *tag){
#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
  unsigned ntags = getNumDebugTags();
  char const* const* tags = getDebugTags();
  for (unsigned i = 0; i < ntags; ++ i) {
    if (strcmp(tag, tags[i]) == 0) {
      return true;
    }
  }
#endif /* CVC5_DEBUG && CVC5_TRACING */
  return false;
}

unsigned Configuration::getNumTraceTags() {
#if CVC5_TRACING
  /* -1 because a NULL pointer is inserted as the last value */
  return sizeof(Trace_tags) / sizeof(Trace_tags[0]) - 1;
#else  /* CVC5_TRACING */
  return 0;
#endif /* CVC5_TRACING */
}

char const* const* Configuration::getTraceTags() {
#if CVC5_TRACING
  return Trace_tags;
#else  /* CVC5_TRACING */
  static char const* no_tags[] = { NULL };
  return no_tags;
#endif /* CVC5_TRACING */
}

bool Configuration::isTraceTag(char const * tag){
#if CVC5_TRACING
  unsigned ntags = getNumTraceTags();
  char const* const* tags = getTraceTags();
  for (unsigned i = 0; i < ntags; ++ i) {
    if (strcmp(tag, tags[i]) == 0) {
      return true;
    }
  }
#endif /* CVC5_TRACING */
  return false;
}

bool Configuration::isGitBuild() {
  return IS_GIT_BUILD;
}

const char* Configuration::getGitBranchName() {
  return GIT_BRANCH_NAME;
}

const char* Configuration::getGitCommit() {
  return GIT_COMMIT;
}

bool Configuration::hasGitModifications() {
  return GIT_HAS_MODIFICATIONS;
}

std::string Configuration::getGitId() {
  if(! isGitBuild()) {
    return "";
  }

  const char* branchName = getGitBranchName();
  if(*branchName == '\0') {
    branchName = "-";
  }

  stringstream ss;
  ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8)
     << (::cvc5::Configuration::hasGitModifications() ? " (with modifications)"
                                                      : "");
  return ss.str();
}

std::string Configuration::getCompiler() {
  stringstream ss;
#ifdef __GNUC__
  ss << "GCC";
#else /* __GNUC__ */
  ss << "unknown compiler";
#endif /* __GNUC__ */
#ifdef __VERSION__
  ss << " version " << __VERSION__;
#else /* __VERSION__ */
  ss << ", unknown version";
#endif /* __VERSION__ */
  return ss.str();
}

std::string Configuration::getCompiledDateTime() {
  return __DATE__ " " __TIME__;
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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