-
Notifications
You must be signed in to change notification settings - Fork 0
/
main.cpp
168 lines (135 loc) · 3.55 KB
/
main.cpp
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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
#include <fstream>
#include <iostream>
#include <cstring>
#include <getopt.h>
#include "aag.h"
#include "translate.h"
#include "dimacs.h"
struct Env {
int K = -1;
int Debug = 0;
std::istream *inputstream = &std::cin;
std::ifstream file;
bool ParserTest = false;
bool ShowProof = false;
bool PrintDIMACS = false;
bool Interpolation = false;
};
const char USAGE[] =
" -k <steps> [-d <level>] [-f <file>] [--parse-only]\n\n"
"-d[level] include debug output (optionally, specify debug level)\n"
"--dimacs print CNF of classical BMC check in DIMACS format\n"
"-k <steps> # of steps the model checker will unwind (default k=0)\n"
"-f <file path> read from a file instead of console\n"
"-p | --proof show proof\n"
"--parse-only Only parse ASCII AIGer file (for testing)\n";
auto usage(const char *prog) -> void
{
std::cout << "Usage: " << prog << USAGE << std::endl;
}
auto parseArgs(int argc, char **argv) -> Env
{
static option long_options[] = {{"parse-only", no_argument, 0, 0},
{"help", no_argument, 0, 0},
{"dimacs", no_argument, 0, 0},
{"proof", no_argument, 0, 'p'},
{"interpolate", no_argument, 0, 'i'},
{0, 0, 0, 0}};
Env e;
while (1) {
int option_index = 0, c;
c = getopt_long(argc, argv, "d::f:ik:p", long_options, &option_index);
if (c == -1)
break;
switch (c + (c == 0 ? option_index : 0)) {
case 0: // --parse-only
e.ParserTest = true;
break;
case 1: // --help
usage(argv[0]);
exit(0);
break;
case 2: // --dimacs
e.PrintDIMACS = true;
break;
case 'd':
if (optarg == nullptr) {
e.Debug = 1;
break;
}
e.Debug = atoi(optarg);
if (e.Debug <= 0) {
e.Debug = 1;
}
break;
case 'i':
e.Interpolation = true;
break;
case 'k':
e.K = atoi(optarg);
break;
case 'f':
if (strcmp(optarg, "-") == 0) {
break;
}
e.file.open(optarg);
if (e.file.fail()) {
std::cout << "error: cannot open file '" << optarg << "'"
<< std::endl;
exit(1);
}
e.inputstream = &e.file;
break;
case 'p':
e.ShowProof = true;
break;
}
}
if (e.K < 0 && !e.ParserTest && !e.Interpolation) {
usage(argv[0]);
std::cout << "Parameter k was not given" << std::endl;
exit(0);
}
return e;
}
auto main(int argc, char **argv) -> int
{
auto env = parseArgs(argc, argv);
auto aig = AIG::FromStream(*env.inputstream);
if (env.ParserTest) {
return 0;
}
if (aig.outputs.size() == 0) {
std::cout << "Model has no outputs. Bad states cannot be detected." << std::endl;
std::cout << "Exiting." << std::endl;
return 0;
}
std::cout << "outputs " << aig.outputs.size() << std::endl;
std::cout << "K = " << env.K << std::endl;
try {
if(env.PrintDIMACS) {
if (env.Interpolation) {
std::cout << "Cannot print DIMACS for interpolation method, sry." << std::endl;
return 0;
}
DimacsCNFer cnfer(std::cout);
AIGtoSATer ats{aig};
VarTranslator vars(&cnfer, aig.lastLit, env.K);
ats.toSAT(cnfer, vars, env.K);
return 0;
}
AIGtoSATer ats{aig};
if(env.Interpolation)
ats.enableInterpolation();
auto result = ats.check(env.K);
assert(result == AIGtoSATer::OK || result == AIGtoSATer::FAIL);
std::cout << std::endl << (result == AIGtoSATer::FAIL ? "FAIL" : "OK") << std::endl;
}catch(TranslationError& err) {
std::cout << "translation error: " << err.what() << std::endl << std::endl;
return 1;
}catch(std::exception& err) {
std::cout << "error: " << err.what() << std::endl << std::endl;
return 1;
}
return 0;
}