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 |