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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
#include <cstdio>
#include <cstdlib>
#include <new>
#include <unistd.h>
#include <string.h>
#include <stdint.h>
#include <time.h>
#include <getopt.h>
#include "config.h"
#include "main.h"
#include "util/exception.h"
#include "usage.h"
#include "about.h"
using namespace std;
using namespace CVC4;
namespace CVC4 {
namespace Main {
static const char lang_help[] = "\
Languages currently supported to the -L / --lang option:\n\
auto attempt to automatically determine the input language\n\
pl | cvc4 CVC4 presentation language\n\
smt | smtlib SMT-LIB format\n\
";
enum Language {
AUTO = 0,
PL,
SMTLIB,
};/* enum Language */
enum OptionValue {
SMTCOMP = 256, /* no clash with char options */
STATS
};/* enum OptionValue */
static struct option cmdlineOptions[] = {
// name, has_arg, *flag, val
{ "help" , no_argument , NULL, 'h' },
{ "version", no_argument , NULL, 'V' },
{ "verbose", no_argument , NULL, 'v' },
{ "quiet" , no_argument , NULL, 'q' },
{ "lang" , required_argument, NULL, 'L' },
{ "debug" , required_argument, NULL, 'd' },
{ "smtcomp", no_argument , NULL, SMTCOMP },
{ "stats" , no_argument , NULL, STATS }
};
int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) {
const char *progName = argv[0];
int c;
// find the base name of the program
const char *x = strrchr(progName, '/');
if(x != NULL)
progName = x + 1;
opts->binary_name = string(progName);
while((c = getopt_long(argc, argv, "+:hVvL:", cmdlineOptions, NULL)) != -1) {
switch(c) {
case 'h':
printf(usage, opts->binary_name.c_str());
exit(1);
break;
case 'V':
fputs(about, stdout);
break;
case 'v':
++opts->verbosity;
break;
case 'q':
--opts->verbosity;
break;
case 'L':
if(!strcmp(argv[optind], "cvc4") || !strcmp(argv[optind], "pl")) {
opts->lang = PL;
break;
} else if(!strcmp(argv[optind], "smtlib") || !strcmp(argv[optind], "smt")) {
opts->lang = SMTLIB;
break;
} else if(!strcmp(argv[optind], "auto")) {
opts->lang = AUTO;
break;
}
if(strcmp(argv[optind], "help"))
throw new OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help.");
fputs(lang_help, stdout);
exit(1);
case STATS:
opts->statistics = true;
break;
case SMTCOMP:
// silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input)
opts->smtcomp_mode = true;
opts->verbosity = -1;
opts->lang = SMTLIB;
break;
case '?':
throw new OptionException(string("can't understand option: `") + argv[optind] + "'");
case ':':
throw new OptionException(string("option `") + argv[optind] + "' missing its required argument");
default:
throw new OptionException(string("can't understand option: `") + argv[optind] + "'");
}
}
return optind;
}
}/* CVC4::Main namespace */
}/* CVC4 namespace */
|
