zchaff64/cnf_stats.cpp

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