// =====================================================================================
//
//       Filename:  tran.cc
//
//    Description:  transform input of acts to cnf
//
//        Version:  1.0
//        Created:  2019年 01月 05日 星期六 07:43:30 CST
//       Revision:  none
//       Compiler:  g++
//
//         Author:  Jinkun Lin, jkunlin@gmail.com
//   Organization:  School of EECS, Peking University
//
// =====================================================================================
#include <fstream>
#include <iostream>
#include <map>
#include <sstream>
#include <string>
#include <vector>
using namespace std;

struct Literal {
  char sign;
  int value;
  Literal(char s, int v) : sign(s), value(v) {}
};

struct Clause {
  vector<Literal> lits;
};

int main(int argc, char const *argv[]) {
  if (argc != 2) {
    cout << "usage: " << endl;
    return 1;
  }
  ifstream infile(argv[1]);
  if (!infile) {
    cout << "infile error" << endl;
    return 1;
  }

  string line;
  while (getline(infile, line)) {
    if (line.find("Parameter") != line.npos) {
      break;
    }
  }

  map<string, int> parameter;
  vector<map<string, int>> value;
  int cur_pid = 0;
  int cur_vid = 0;
  string tmp_str;
  while (getline(infile, line)) {
    if (line.find("Constraint") != line.npos) {
      break;
    }
    istringstream is(line);

    string p;
    is >> p >> tmp_str;
    if (!is) {
      if (line.size() != 1) {
        abort();
      }
      continue;
    }
    parameter.insert(make_pair(p, cur_pid++));
    value.push_back(map<string, int>());

    string v;
    while (is >> v) {
      if (v[v.size() - 1] == ',') {
        v.pop_back();
      }
      value[parameter[p]].insert(make_pair(v, cur_vid++));
    }
  }

#ifndef NDEBUG
  // for (auto p_pair : parameter) {
  //   cout << p_pair.first << ": ";
  //   for (auto v_pair : value[p_pair.second]) {
  //     cout << v_pair.first << ", ";
  //   }
  //   cout << endl;
  // }
  //
  // for (auto p_pair : parameter) {
  //   cout << p_pair.second << ": ";
  //   for (auto v_pair : value[p_pair.second]) {
  //     cout << v_pair.second << ", ";
  //   }
  //   cout << endl;
  // }
  cout << 2 << endl;
  cout << parameter.size() << endl;
  auto iter = parameter.begin();
  cout << value[iter->second].size();
  for (++iter; iter != parameter.end(); ++iter) {
    cout << ' ' << value[iter->second].size();
  }
  cout << endl;
#endif

  vector<Clause> formular;
  char tmp_ch;
  while (getline(infile, line)) {
    istringstream is(line);
    is >> tmp_str >> tmp_ch;

    string p, v;
    char sign;
    Clause c;
    do {
      is >> p >> tmp_str >> tmp_ch;

      // sign
      if (tmp_str == "!=") {
        sign = '-';
      } else if (tmp_str == "=") {
        sign = '+';
      } else {
        cout << "error operator" << endl;
        return 1;
      }

      // value
      is >> v;
      if (v[v.size() - 1] == '"') {
        v.pop_back();
      } else if (v[v.size() - 1] == ')' && v[v.size() - 2] == '"') {
        v.pop_back();
        v.pop_back();
      } else {
        cout << "format error: " << v << endl;
        return 1;
      }

      c.lits.push_back(Literal(sign, value[parameter[p]][v]));

      // operator
      is >> tmp_str;
    } while (tmp_str == "||");
    formular.push_back(c);
  }

#ifndef NDEBUG
  cout << formular.size() << endl;
  for (auto c : formular) {
    cout << c.lits.size() << endl;
    cout << c.lits[0].sign << ' ' << c.lits[0].value;
    for (int i = 1; i < (int)c.lits.size(); ++i) {
      cout << ' ' << c.lits[i].sign << ' ' << c.lits[i].value;
    }
    cout << endl;
  }
#endif
  return 0;
}