12 const int MAX_WORD_LENGTH = 64;
13 const int MAX_LINE_LENGTH = 256000;
15 int main(int argc, char** argv) {
17 char * filename = argv[1];
19 char line_buffer[MAX_LINE_LENGTH];
20 char word_buffer[MAX_WORD_LENGTH];
24 vector<bool> variables;
27 ifstream inp(filename, ios::in);
29 cerr << "Can't open input file" << endl;
32 while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
34 if (line_buffer[0] == 'c') {
37 else if (line_buffer[0] == 'p') {
38 int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);
40 cerr << "Unable to read number of variables and clauses"
41 << "at line " << line_num << endl;
44 variables.resize(var_num + 1);
45 for (int i = 0; i < var_num + 1; ++i)
47 } else { // Clause definition or continuation
48 char *lp = line_buffer;
50 char *wp = word_buffer;
51 while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
54 while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
57 *wp = '\0'; // terminate string
59 if (strlen(word_buffer) != 0) { // check if number is there
60 int var_idx = atoi(word_buffer);
68 clause_vars.insert(var_idx);
69 clause_lits.insert((var_idx << 1) + sign);
72 if (clause_vars.size() != 0 &&
73 clause_vars.size() == clause_lits.size()) {
75 for (set<int>::iterator itr = clause_lits.begin();
76 itr != clause_lits.end(); ++itr)
78 for (unsigned i = 0; i < temp.size(); ++i)
79 variables[temp[i]>>1] = true;
82 cout << "Literals of both polarity at line "
83 << line_num << ", clause skipped " << endl;
85 // it contain var of both polarity, so is automatically
86 // satisfied, just skip it
96 cerr << "Input line " << line_num << " too long. Unable to continue..."
100 assert(clause_vars.size() == 0);
102 for (unsigned i = 0; i < variables.size(); ++i) {
106 cout <<"Statistics of CNF file:\t\t" << filename << "\n"
107 <<" Claim:\t\t Cl: " << cl_num << "\t Var: " << var_num << "\n"
108 <<" Actual:\t Cl: " << num_cls << "\t Var: " << num_vars << endl;