source: vis_dev/zchaff/cnf_stats.cpp @ 77

Last change on this file since 77 was 10, checked in by cecile, 13 years ago

Zchaff

File size: 3.2 KB
Line 
1#include <iostream>
2#include <fstream>
3#include <cstdlib>
4#include <cstdio>
5#include <cstring>
6
7
8#include <set>
9#include <vector>
10#include <assert.h>
11
12using namespace std;
13
14const int MAX_WORD_LENGTH       = 64;
15const int MAX_LINE_LENGTH       = 256000;
16
17int main(int argc, char** argv) {
18  assert(argc == 2);
19  char * filename = argv[1];
20  int line_num = 0;
21  char line_buffer[MAX_LINE_LENGTH];
22  char word_buffer[MAX_WORD_LENGTH];
23  set<int> clause_vars;
24  set<int> clause_lits;
25  int num_cls = 0;
26  vector<bool> variables;
27  int var_num;
28  int cl_num;
29  ifstream inp(filename, ios::in);
30  if (!inp) {
31    cerr << "Can't open input file" << endl;
32    exit(1);
33  }
34  while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
35    ++line_num;
36    if (line_buffer[0] == 'c') {
37      continue;
38    }
39    else if (line_buffer[0] == 'p') {
40      int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);
41      if (arg < 2) {
42        cerr << "Unable to read number of variables and clauses"
43             << "at line " << line_num << endl;
44        exit(3);
45      }
46      variables.resize(var_num + 1);
47      for (int i = 0; i < var_num + 1; ++i)
48        variables[i] = false;
49    } else {                             // Clause definition or continuation
50      char *lp = line_buffer;
51      do {
52        char *wp = word_buffer;
53        while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
54          lp++;
55        }
56        while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
57          *(wp++) = *(lp++);
58        }
59        *wp = '\0';                                 // terminate string
60
61        if (strlen(word_buffer) != 0) {     // check if number is there
62          int var_idx = atoi(word_buffer);
63          int sign = 0;
64
65          if (var_idx != 0) {
66            if (var_idx < 0) {
67              var_idx = -var_idx;
68              sign = 1;
69            }
70            clause_vars.insert(var_idx);
71            clause_lits.insert((var_idx << 1) + sign);
72          } else {
73            // add this clause
74            if (clause_vars.size() != 0 &&
75                clause_vars.size() == clause_lits.size()) {
76              vector <int> temp;
77              for (set<int>::iterator itr = clause_lits.begin();
78                itr != clause_lits.end(); ++itr)
79                temp.push_back(*itr);
80              for (unsigned i = 0; i < temp.size(); ++i)
81                variables[temp[i]>>1] = true;
82              ++num_cls;
83            } else {
84              cout << "Literals of both polarity at line "
85                   << line_num << ", clause skipped " << endl;
86            }
87            // it contain var of both polarity, so is automatically
88            // satisfied, just skip it
89            clause_lits.clear();
90            clause_vars.clear();
91          }
92        }
93      }
94      while (*lp);
95    }
96  }
97  if (!inp.eof()) {
98    cerr << "Input line " << line_num <<  " too long. Unable to continue..."
99         << endl;
100    exit(2);
101  }
102  assert(clause_vars.size() == 0);
103  int num_vars  = 0;
104  for (unsigned i = 0; i < variables.size(); ++i) {
105    if (variables[i])
106      ++num_vars;
107  }
108  cout <<"Statistics of CNF file:\t\t" <<  filename << "\n"
109     <<" Claim:\t\t Cl: " << cl_num << "\t Var: " << var_num << "\n"
110     <<" Actual:\t Cl: " << num_cls << "\t Var: " << num_vars << endl;
111  return 0;
112}
Note: See TracBrowser for help on using the repository browser.