1 /*************************************************************
2 MiniSat --- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3 CryptoMiniSat --- Copyright (c) 2014, Mate Soos
4
5 Permission is hereby granted, free of charge, to any person obtaining a copy
6 of this software and associated documentation files (the "Software"), to deal
7 in the Software without restriction, including without limitation the rights
8 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9 copies of the Software, and to permit persons to whom the Software is
10 furnished to do so, subject to the following conditions:
11
12 The above copyright notice and this permission notice shall be included in
13 all copies or substantial portions of the Software.
14
15 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
21 THE SOFTWARE.
22 ***************************************************************/
23
24 #include <ctime>
25 #include <cstring>
26 #include <errno.h>
27 #include <iostream>
28 #include <stdlib.h>
main(int argc,char ** argv)29 #include <string.h>
30
31 using std::cout;
32 using std::endl;
33
34 #include <signal.h>
35 #include "time_mem.h"
36 #include "main_common.h"
37
38 #include "solverconf.h"
39 #include "cryptominisat5/cryptominisat.h"
40 #include "dimacsparser.h"
41
42 #if defined(_MSC_VER)
43 #pragma warning(push)
44 #pragma warning(disable:4706) // Assignment within conditional expression
45 // -- used in parsing args
46 #endif
47
48 using namespace CMSat;
49
50 SATSolver* solver;
51
52 static void SIGINT_handler(int) {
53 cout << "\n*** INTERRUPTED ***\n";
54 solver->add_in_partial_solving_stats();
55 solver->print_stats();
56 cout << "\n*** INTERRUPTED ***\n";
57 exit(1);
58 }
59
60 class Main: public MainCommon {
61 public:
62
63 void printVersionInfo()
64 {
65 cout << solver->get_text_version_info() << endl;
66 }
67
68 void printUsage(const char** argv)
69 {
70 cout << "Usage: "
71 << argv[0] << " [options] <input-file> where input is plain DIMACS.\n";
72 cout << "Options:\n";
73 cout << " --verb = [0...] Sets verbosity level. Anything higher\n";
74 cout << " than 2 will give debug log\n";
75 cout << " --drat = {fname} DRAT dumped to file\n";
76 cout << " --sls = {walksat,yalsat} Which SLS solver to use\n";
77 cout << " --threads = [1...] Sets number of threads\n";
78 cout << "\n";
79 }
80
81 const char* hasPrefix(const char* str, const char* prefix)
82 {
83 int len = strlen(prefix);
84 if (strncmp(str, prefix, len) == 0)
85 return str + len;
86 else
87 return NULL;
88 }
89
90 int main(int argc, const char** argv) {
91 conf.verbosity = 1;
92
93 int i, j;
94 for (i = j = 0; i < argc; i++){
95 const char* value;
96 if ((value = hasPrefix(argv[i], "--drat="))){
97 dratfilname = std::string(value);
98 handle_drat_option();
99 }else if ((value = hasPrefix(argv[i], "--verb="))){
100 long int verbosity = (int)strtol(value, NULL, 10);
101 if (verbosity == 0 && errno == EINVAL){
102 cout << "ERROR! illegal verbosity level" << value << endl;
103 exit(0);
104 }
105 conf.verbosity = verbosity;
106 }else if ((value = hasPrefix(argv[i], "--simdrat="))){
107 int drat_sim = (int)strtol(value, NULL, 10);
108 conf.simulate_drat = drat_sim;
109 }else if ((value = hasPrefix(argv[i], "--threads="))){
110 num_threads = (int)strtol(value, NULL, 10);
111 if (num_threads == 0 && errno == EINVAL){
112 cout << "ERROR! illegal threads " << value << endl;
113 exit(0);
114 }
115 if (num_threads > 16) {
116 conf.var_and_mem_out_mult *= 0.4;
117 }
118 }else if ((value = hasPrefix(argv[i], "--bva="))){
119 conf.do_bva = (int)strtol(value, NULL, 10);
120 }else if ((value = hasPrefix(argv[i], "--sls="))){
121 std::string sls;
122 sls = argv[i];
123 sls = sls.substr(6, 100);
124 conf.which_sls = sls;
125 cout << "c using SLS: '" << sls << "'" << endl;
126 }else if ((value = hasPrefix(argv[i], "--reconf="))){
127 long int reconf = (int)strtol(value, NULL, 10);
128 if (reconf == 0 && errno == EINVAL){
129 cout << "ERROR! illegal threads " << value << endl;
130 exit(0);
131 }
132 conf.reconfigure_val = reconf;
133 }else if (strcmp(argv[i], "--zero-exit-status") == 0){
134 zero_exit_status = true;
135 }else if (strcmp(argv[i], "--version") == 0){
136 printVersionInfo();
137 exit(0);
138 } else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "-help") == 0 || strcmp(argv[i], "--help") == 0){
139 printUsage(argv);
140 exit(0);
141
142 }else if (strncmp(argv[i], "-", 1) == 0){
143 cout << "ERROR! unknown flag: " << argv[i] << endl;
144 exit(0);
145
146 }else
147 argv[j++] = argv[i];
148 }
149 argc = j;
150
151 SATSolver S(&conf);
152 solver = &S;
153 if (dratf) {
154 solver->set_drat(dratf, false);
155 if (num_threads > 1) {
156 cout << "ERROR: Cannot have DRAT and multiple threads." << endl;
157 exit(-1);
158 }
159 }
160 solver->set_num_threads(num_threads);
161
162 if (conf.verbosity) {
163 printVersionInfo();
164 cout << "c NOTE: this is a SIMPLIFIED executable. For the full experience, you need to compile/obtain/use the 'cryptominisat5' executable. To compile that, you need the boost libraries. Please read the README." << endl;
165 }
166 double cpu_time = cpuTime();
167
168 solver = &S;
169 signal(SIGINT,SIGINT_handler);
170 #if !defined (_WIN32)
171 signal(SIGHUP,SIGINT_handler);
172 #endif
173
174 if (argc == 1) {
175 cout << "Reading from standard input... Use '-h' or '--help' for help.\n";
176 #ifndef USE_ZLIB
177 FILE* in = stdin;
178 DimacsParser<StreamBuffer<FILE*, FN>, SATSolver> parser(solver, NULL, conf.verbosity);
179 #else
180 gzFile in = gzdopen(0, "rb"); //opens stdin, which is 0
181 DimacsParser<StreamBuffer<gzFile, GZ>, SATSolver> parser(solver, NULL, conf.verbosity);
182 #endif
183
184 if (!parser.parse_DIMACS(in, false)) {
185 exit(-1);
186 }
187
188 #ifndef USE_ZLIB
189 fclose(in);
190 #else
191 gzclose(in);
192 #endif
193 } else {
194 #ifndef USE_ZLIB
195 FILE* in = fopen(argv[1], "rb");
196 #else
197 gzFile in = gzopen(argv[1], "rb");
198 #endif
199
200 if (in == NULL) {
201 std::cout << "ERROR! Could not open file: ";
202 std::cout << argv[1] << " reason: " << strerror(errno);
203 std::cout << std::endl;
204 std::exit(1);
205 }
206
207 #ifndef USE_ZLIB
208 DimacsParser<StreamBuffer<FILE*, FN>, SATSolver> parser(solver, NULL, conf.verbosity);
209 #else
210 DimacsParser<StreamBuffer<gzFile, GZ>, SATSolver> parser(solver, NULL, conf.verbosity);
211 #endif
212
213 if (!parser.parse_DIMACS(in, false)) {
214 exit(-1);
215 }
216
217 #ifndef USE_ZLIB
218 fclose(in);
219 #else
220 gzclose(in);
221 #endif
222 }
223
224 double parse_time = cpuTime() - cpu_time;
225 if (conf.verbosity) {
226 cout << "c Parsing time: "
227 << std::fixed << std::setprecision(2) << parse_time << " s" << endl;
228 }
229
230 lbool ret = S.solve();
231 if (conf.verbosity) {
232 S.print_stats();
233 }
234
235 if (ret == l_True) {
236 cout << "s SATISFIABLE" << endl;
237 } else if (ret == l_False) {
238 cout << "s UNSATISFIABLE"<< endl;
239 }
240
241 if (ret == l_True) {
242 print_model(solver, &std::cout);
243 }
244
245 if (dratf) {
246 *dratf << std::flush;
247 if (dratf != &std::cout) {
248 delete dratf;
249 }
250 }
251
252 if (zero_exit_status)
253 return 0;
254 else {
255 return ret == l_True ? 10 : 20;
256 }
257 }
258 };
259
260 int main(int argc, const char** argv)
261 {
262 Main m;
263 return m.main(argc, argv);
264 }
265
266 #if defined(_MSC_VER)
267 #pragma warning(pop)
268 #endif
269