1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
/********************* */
/*! \file options_handlers.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
** Minor contributors (to current version): Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Custom handlers and predicates for main driver options
**
** Custom handlers and predicates for main driver options.
**/
#include "cvc4_private.h"
#ifndef __CVC4__MAIN__OPTIONS_HANDLERS_H
#define __CVC4__MAIN__OPTIONS_HANDLERS_H
namespace CVC4 {
namespace main {
inline void showConfiguration(std::string option, SmtEngine* smt) {
fputs(Configuration::about().c_str(), stdout);
printf("\n");
printf("version : %s\n", Configuration::getVersionString().c_str());
if(Configuration::isGitBuild()) {
const char* branchName = Configuration::getGitBranchName();
if(*branchName == '\0') {
branchName = "-";
}
printf("scm : git [%s %s%s]\n",
branchName,
std::string(Configuration::getGitCommit()).substr(0, 8).c_str(),
Configuration::hasGitModifications() ?
" (with modifications)" : "");
} else if(Configuration::isSubversionBuild()) {
printf("scm : svn [%s r%u%s]\n",
Configuration::getSubversionBranchName(),
Configuration::getSubversionRevision(),
Configuration::hasSubversionModifications() ?
" (with modifications)" : "");
} else {
printf("scm : no\n");
}
printf("\n");
printf("library : %u.%u.%u\n",
Configuration::getVersionMajor(),
Configuration::getVersionMinor(),
Configuration::getVersionRelease());
printf("\n");
printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no");
printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no");
printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no");
printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
printf("\n");
printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no");
printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no");
printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
exit(0);
}
inline void showDebugTags(std::string option, SmtEngine* smt) {
if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
printf("available tags:");
unsigned ntags = Configuration::getNumDebugTags();
char const* const* tags = Configuration::getDebugTags();
for(unsigned i = 0; i < ntags; ++ i) {
printf(" %s", tags[i]);
}
printf("\n");
} else if(! Configuration::isDebugBuild()) {
throw OptionException("debug tags not available in non-debug builds");
} else {
throw OptionException("debug tags not available in non-tracing builds");
}
exit(0);
}
inline void showTraceTags(std::string option, SmtEngine* smt) {
if(Configuration::isTracingBuild()) {
printf("available tags:");
unsigned ntags = Configuration::getNumTraceTags();
char const* const* tags = Configuration::getTraceTags();
for (unsigned i = 0; i < ntags; ++ i) {
printf(" %s", tags[i]);
}
printf("\n");
} else {
throw OptionException("trace tags not available in non-tracing build");
}
exit(0);
}
inline void threadN(std::string option, SmtEngine* smt) {
throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
}
}/* CVC4::main namespace */
}/* CVC4 namespace */
#endif /* __CVC4__MAIN__OPTIONS_HANDLERS_H */
|
