1 /*****************************************************************************
2 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3 CryptoMiniSat -- Copyright (c) 2009 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 #ifndef DIMACSPARSER_H
25 #define DIMACSPARSER_H
26
27 #include <string.h>
28 #include "streambuffer.h"
29 #include <cstdlib>
30 #include <cmath>
31
32 using namespace CMSat;
33 using std::vector;
34
35 template <class C, class S>
36 class DimacsParser
37 {
38 public:
39 DimacsParser(S* solver, const std::string* debugLib, unsigned _verbosity);
40
41 template <class T> bool parse_DIMACS(
42 T input_stream,
43 const bool strict_header,
44 uint32_t offset_vars = 0);
45 uint64_t max_var = std::numeric_limits<uint64_t>::max();
46 vector<uint32_t> sampling_vars;
47 vector<double> weights;
48 const std::string dimacs_spec = "http://www.satcompetition.org/2009/format-benchmarks2009.html";
49 const std::string please_read_dimacs = "\nPlease read DIMACS specification at http://www.satcompetition.org/2009/format-benchmarks2009.html";
50
51 private:
52 bool parse_DIMACS_main(C& in);
53 bool readClause(C& in);
54 bool parse_and_add_clause(C& in);
55 bool parse_and_add_xor_clause(C& in);
56 bool match(C& in, const char* str);
57 bool parse_header(C& in);
58 bool parseComments(C& in, const std::string& str);
59 std::string stringify(uint32_t x) const;
60
61 #ifdef DEBUG_DIMACSPARSER_CMS
62 bool parseWeight(C& in);
63 bool parse_solve_simp_comment(C& in, const bool solve);
64 void write_solution_to_debuglib_file(const lbool ret) const;
65 #endif
66
67 bool parseIndependentSet(C& in);
68 std::string get_debuglib_fname() const;
69
70
71 S* solver;
72 std::string debugLib;
73 unsigned verbosity;
74 bool pcnf = false;
75 unsigned num_vp = 0; //how many vp's have we seen
76
77 //Stat
78 size_t lineNum;
79
80 //Printing partial solutions to debugLibPart1..N.output when "debugLib" is set to TRUE
81 uint32_t debugLibPart = 1;
82
83 //check header strictly
84 bool strict_header = false;
85 bool header_found = false;
86 int num_header_vars = 0;
87 int num_header_cls = 0;
88 uint32_t offset_vars = 0;
89
90 //Reduce temp overhead
91 vector<Lit> lits;
92 vector<uint32_t> vars;
93
94 size_t norm_clauses_added = 0;
95 size_t xor_clauses_added = 0;
96 };
97
98 #include <sstream>
99 #include <iostream>
100 #include <iomanip>
101 #include <vector>
102 #include <fstream>
103 #include <complex>
104 #include <cassert>
105
106 using std::vector;
107 using std::cout;
108 using std::endl;
109
110 template<class C, class S>
DimacsParser(S * _solver,const std::string * _debugLib,unsigned _verbosity)111 DimacsParser<C, S>::DimacsParser(
112 S* _solver
113 , const std::string* _debugLib
114 , unsigned _verbosity
115 ):
116 solver(_solver)
117 , verbosity(_verbosity)
118 , lineNum(0)
119 {
120 if (_debugLib) {
121 debugLib = *_debugLib;
122 }
123 }
124
125 template<class C, class S>
stringify(uint32_t x)126 std::string DimacsParser<C, S>::stringify(uint32_t x) const
127 {
128 std::ostringstream o;
129 o << x;
130 return o.str();
131 }
132
133 template<class C, class S>
readClause(C & in)134 bool DimacsParser<C, S>::readClause(C& in)
135 {
136 int32_t parsed_lit;
137 uint32_t var;
138 for (;;) {
139 if (!in.parseInt(parsed_lit, lineNum)) {
140 return false;
141 }
142 if (parsed_lit == 0) {
143 break;
144 }
145
146 var = std::abs(parsed_lit)-1;
147 var += offset_vars;
148
149 if (var > max_var) {
150 std::cerr
151 << "ERROR! "
152 << "Variable requested is too large for DIMACS parser parameter: "
153 << var << endl
154 << "--> At line " << lineNum+1
155 << please_read_dimacs
156 << endl;
157 return false;
158 }
159
160 if (var >= (1ULL<<28)) {
161 std::cerr
162 << "ERROR! "
163 << "Variable requested is far too large: " << var + 1 << endl
164 << "--> At line " << lineNum+1
165 << please_read_dimacs
166 << endl;
167 return false;
168 }
169
170 if (strict_header && !header_found) {
171 std::cerr
172 << "ERROR! "
173 << "DIMACS header ('p cnf vars cls') never found!" << endl;
174 return false;
175 }
176
177 if ((int)var >= num_header_vars && strict_header) {
178 std::cerr
179 << "ERROR! "
180 << "Variable requested is larger than the header told us." << endl
181 << " -> var is : " << var + 1 << endl
182 << " -> header told us maximum will be : " << num_header_vars << endl
183 << " -> At line " << lineNum+1
184 << endl;
185 return false;
186 }
187
188 if (var >= solver->nVars()) {
189 assert(!strict_header);
190 solver->new_vars(var - solver->nVars() +1);
191 }
192
193 lits.push_back( (parsed_lit > 0) ? Lit(var, false) : Lit(var, true) );
194 if (*in != ' ') {
195 std::cerr
196 << "ERROR! "
197 << "After last element on the line must be 0" << endl
198 << "--> At line " << lineNum+1
199 << please_read_dimacs
200 << endl
201 << endl;
202 return false;
203 }
204 }
205
206 return true;
207 }
208
209 template<class C, class S>
match(C & in,const char * str)210 bool DimacsParser<C, S>::match(C& in, const char* str)
211 {
212 for (; *str != 0; ++str, ++in)
213 if (*str != *in)
214 return false;
215 return true;
216 }
217
218 #ifdef DEBUG_DIMACSPARSER_CMS
219 template<class C, class S>
parseWeight(C & in)220 bool DimacsParser<C, S>::parseWeight(C& in)
221 {
222 if (match(in, "w ")) {
223 int32_t slit;
224 double weight;
225 if (in.parseInt(slit, lineNum)
226 && in.parseDouble(weight, lineNum)
227 ) {
228 if (slit == 0) {
229 cout << "ERROR: Cannot define weight of literal 0!" << endl;
230 exit(-1);
231 }
232 uint32_t var = std::abs(slit)-1;
233 bool sign = slit < 0;
234 Lit lit = Lit(var, sign);
235 solver->set_var_weight(lit, weight);
236 //cout << "lit: " << lit << " weight: " << std::setprecision(12) << weight << endl;
237 if (weight < 0) {
238 cout << "ERROR: while definint weight, variable " << var+1 << " has is negative weight: " << weight << " -- line " << lineNum << endl;
239 exit(-1);
240 }
241 return true;
242 } else {
243 cout << "ERROR: weight is incorrect on line " << lineNum << endl;
244 exit(-1);
245 }
246 } else {
247 cout << "ERROR: weight is not given on line " << lineNum << endl;
248 exit(-1);
249 }
250 return true;
251 }
252 #endif
253
254 template<class C, class S>
parse_header(C & in)255 bool DimacsParser<C, S>::parse_header(C& in)
256 {
257 ++in;
258 in.skipWhitespace();
259 std::string str;
260 in.parseString(str);
261 if (str == "cnf" || str == "pcnf") {
262 pcnf = (str == "pcnf");
263 if (pcnf && verbosity) {
264 cout << "c parsing pcnf" << endl;
265 }
266 if (header_found && strict_header) {
267 std::cerr << "ERROR: CNF header ('p cnf vars cls') found twice in file! Exiting." << endl;
268 exit(-1);
269 }
270 header_found = true;
271
272 if (!in.parseInt(num_header_vars, lineNum)
273 || !in.parseInt(num_header_cls, lineNum)
274 ) {
275 return false;
276 }
277 if (verbosity) {
278 cout << "c -- header says num vars: " << std::setw(12) << num_header_vars << endl;
279 cout << "c -- header says num clauses:" << std::setw(12) << num_header_cls << endl;
280 }
281 if (num_header_vars < 0) {
282 std::cerr << "ERROR: Number of variables in header cannot be less than 0" << endl;
283 return false;
284 }
285 if (num_header_cls < 0) {
286 std::cerr << "ERROR: Number of clauses in header cannot be less than 0" << endl;
287 return false;
288 }
289 num_header_vars += offset_vars;
290
291 if (solver->nVars() < (size_t)num_header_vars) {
292 solver->new_vars(num_header_vars-solver->nVars());
293 }
294 } else {
295 std::cerr
296 << "PARSE ERROR! Unexpected char (hex: " << std::hex
297 << std::setw(2)
298 << std::setfill('0')
299 << "0x" << *in
300 << std::setfill(' ')
301 << std::dec
302 << ")"
303 << " At line " << lineNum+1
304 << "' in the header"
305 << please_read_dimacs
306 << endl;
307 return false;
308 }
309
310 return true;
311 }
312
313 template<class C, class S>
get_debuglib_fname()314 std::string DimacsParser<C, S>::get_debuglib_fname() const
315 {
316 std::string sol_fname = debugLib + "-debugLibPart" + stringify(debugLibPart) +".output";
317 return sol_fname;
318 }
319
320 #ifdef DEBUG_DIMACSPARSER_CMS
321 template<class C, class S>
parse_solve_simp_comment(C & in,const bool solve)322 bool DimacsParser<C, S>::parse_solve_simp_comment(C& in, const bool solve)
323 {
324 vector<Lit> assumps;
325 in.skipWhitespace();
326 while(*in != ')') {
327 int lit;
328 if (!in.parseInt(lit, lineNum)) {
329 return false;
330 }
331 assumps.push_back(Lit(std::abs(lit)-1, lit < 0));
332 in.skipWhitespace();
333 }
334
335 if (verbosity) {
336 cout
337 << "c -----------> Solver::"
338 << (solve ? "solve" : "simplify")
339 <<" called (number: "
340 << std::setw(3) << debugLibPart << ") with assumps :";
341 for(Lit lit: assumps) {
342 cout << lit << " ";
343 }
344 cout << "<-----------" << endl;
345 }
346
347 lbool ret;
348 if (solve) {
349 if (verbosity) {
350 cout << "c Solution will be written to: "
351 << get_debuglib_fname() << endl;
352 }
353 ret = solver->solve(&assumps);
354 write_solution_to_debuglib_file(ret);
355 debugLibPart++;
356 } else {
357 ret = solver->simplify(&assumps);
358 }
359
360 if (verbosity >= 6) {
361 cout << "c Parsed Solver::"
362 << (solve ? "solve" : "simplify")
363 << endl;
364 }
365 return true;
366 }
367
368 template<class C, class S>
write_solution_to_debuglib_file(const lbool ret)369 void DimacsParser<C, S>::write_solution_to_debuglib_file(const lbool ret) const
370 {
371 //Open file for writing
372 std::string s = get_debuglib_fname();
373 std::ofstream partFile;
374 partFile.open(s.c_str());
375 if (!partFile) {
376 std::cerr << "ERROR: Cannot open part file '" << s << "'";
377 std::exit(-1);
378 }
379
380 //Output to part file the result
381 if (ret == l_True) {
382 partFile << "s SATISFIABLE\n";
383 partFile << "v ";
384 for (uint32_t i = 0; i != solver->nVars(); i++) {
385 if (solver->get_model()[i] != l_Undef)
386 partFile
387 << ((solver->get_model()[i]==l_True) ? "" : "-")
388 << (i+1) << " ";
389 }
390 partFile << "0\n";
391 } else if (ret == l_False) {
392 partFile << "conflict ";
393 for (Lit lit: solver->get_conflict()) {
394 partFile << lit << " ";
395 }
396 partFile
397 << "\ns UNSAT\n";
398 } else if (ret == l_Undef) {
399 cout << "c timeout, exiting" << endl;
400 std::exit(15);
401 } else {
402 assert(false);
403 }
404 partFile.close();
405 }
406 #endif
407
408 template<class C, class S>
parseComments(C & in,const std::string & str)409 bool DimacsParser<C, S>::parseComments(C& in, const std::string& str)
410 {
411 #ifdef DEBUG_DIMACSPARSER_CMS
412 if (!debugLib.empty() && str.substr(0, 13) == "Solver::solve") {
413 if (!parse_solve_simp_comment(in, true)) {
414 return false;
415 }
416 } else if (!debugLib.empty() && str.substr(0, 16) == "Solver::simplify") {
417 if (!parse_solve_simp_comment(in, false)) {
418 return false;
419 }
420 } else
421 #endif
422 if (!debugLib.empty() && str == "Solver::new_var()") {
423 solver->new_var();
424
425 if (verbosity >= 6) {
426 cout << "c Parsed Solver::new_var()" << endl;
427 }
428 } else if (!debugLib.empty() && str == "Solver::new_vars(") {
429 in.skipWhitespace();
430 int n;
431 if (!in.parseInt(n, lineNum)) {
432 return false;
433 }
434 solver->new_vars(n);
435
436 if (verbosity >= 6) {
437 cout << "c Parsed Solver::new_vars( " << n << " )" << endl;
438 }
439 } else if (str == "ind") {
440 if (pcnf) {
441 //nothing
442 } else {
443 if (!parseIndependentSet(in)) {
444 return false;
445 }
446 }
447 } else {
448 if (verbosity >= 6) {
449 cout
450 << "didn't understand in CNF file comment line:"
451 << "'c " << str << "'"
452 << endl;
453 }
454 }
455 in.skipLine();
456 lineNum++;
457 return true;
458 }
459
460 template<class C, class S>
parse_and_add_clause(C & in)461 bool DimacsParser<C, S>::parse_and_add_clause(C& in)
462 {
463 lits.clear();
464 if (!readClause(in)) {
465 return false;
466 }
467 in.skipWhitespace();
468 if (!in.skipEOL(lineNum)) {
469 return false;
470 }
471 lineNum++;
472 solver->add_clause(lits);
473 norm_clauses_added++;
474 return true;
475 }
476
477 template<class C, class S>
parse_and_add_xor_clause(C & in)478 bool DimacsParser<C, S>::parse_and_add_xor_clause(C& in)
479 {
480 lits.clear();
481 if (!readClause(in)) {
482 return false;
483 }
484 if (!in.skipEOL(lineNum)) {
485 return false;
486 }
487 lineNum++;
488 if (lits.empty())
489 return true;
490
491 bool rhs = true;
492 vars.clear();
493 for(Lit& lit: lits) {
494 vars.push_back(lit.var());
495 if (lit.sign()) {
496 rhs ^= true;
497 }
498 }
499 solver->add_xor_clause(vars, rhs);
500 xor_clauses_added++;
501 return true;
502 }
503
504 template<class C, class S>
parse_DIMACS_main(C & in)505 bool DimacsParser<C, S>::parse_DIMACS_main(C& in)
506 {
507 std::string str;
508
509 for (;;) {
510 in.skipWhitespace();
511 switch (*in) {
512 case EOF:
513 return true;
514 case 'p':
515 if (!parse_header(in)) {
516 return false;
517 }
518 in.skipLine();
519 lineNum++;
520 break;
521 case 'v':
522 in.parseString(str);
523 assert(str == "vp");
524 if (!pcnf) {
525 in.skipLine();
526 } else {
527 if (num_vp == 0) {
528 sampling_vars.clear();
529 }
530 num_vp++;
531 if (!parseIndependentSet(in)) {
532 return false;
533 }
534 }
535 break;
536
537 #ifdef DEBUG_DIMACSPARSER_CMS
538 case 'w':
539 if (!parseWeight(in)) {
540 return false;
541 }
542 in.skipLine();
543 lineNum++;
544 break;
545 #endif
546 case 'c':
547 ++in;
548 in.parseString(str);
549 if (!parseComments(in, str)) {
550 return false;
551 }
552 break;
553 case 'x':
554 ++in;
555 if (!parse_and_add_xor_clause(in)) {
556 return false;
557 }
558 break;
559 case '\n':
560 if (verbosity) {
561 std::cout
562 << "c WARNING: Empty line at line number " << lineNum+1
563 << " -- this is not part of the DIMACS specifications ("
564 << dimacs_spec << "). Ignoring."
565 << endl;
566 }
567 in.skipLine();
568 lineNum++;
569 break;
570 default:
571 if (!parse_and_add_clause(in)) {
572 return false;
573 }
574 break;
575 }
576 }
577
578 return true;
579 }
580
581 template <class C, class S>
582 template <class T>
parse_DIMACS(T input_stream,const bool _strict_header,uint32_t _offset_vars)583 bool DimacsParser<C, S>::parse_DIMACS(
584 T input_stream,
585 const bool _strict_header,
586 uint32_t _offset_vars)
587 {
588 debugLibPart = 1;
589 strict_header = _strict_header;
590 offset_vars = _offset_vars;
591 const uint32_t origNumVars = solver->nVars();
592
593 C in(input_stream);
594 if ( !parse_DIMACS_main(in)) {
595 return false;
596 }
597
598 if (verbosity) {
599 cout
600 << "c -- clauses added: " << norm_clauses_added << endl
601 << "c -- xor clauses added: " << xor_clauses_added << endl
602 << "c -- vars added " << (solver->nVars() - origNumVars)
603 << endl;
604 }
605
606 return true;
607 }
608
609 template <class C, class S>
parseIndependentSet(C & in)610 bool DimacsParser<C, S>::parseIndependentSet(C& in)
611 {
612 int32_t parsed_lit;
613 for (;;) {
614 if (!in.parseInt(parsed_lit, lineNum)) {
615 return false;
616 }
617 if (parsed_lit == 0) {
618 break;
619 }
620 uint32_t var = std::abs(parsed_lit) - 1;
621 sampling_vars.push_back(var);
622 }
623 return true;
624 }
625
626 #endif //DIMACSPARSER_H
627