// version of zc2ms that works with original unmodified MiniSat 1.14p

#include <iostream>
#include <list>
#include <map>
#include <stack>
#include <set>
#include <vector>
#include <queue>
#include <ctime>
#include <unistd.h>
#include <signal.h>
#include <zlib.h>
#include "Global.h"
#include "Proof.h"
#include <fstream>
#include "Sort.h"
#include <string>
#include <sstream>

// Redfine if you want output to go somewhere else:
#define reportf(format, args...) ( printf(format , ## args), fflush(stdout) )

using namespace std;

enum enum_ty { ROOT, CL, VAR, CONF, DONE };
typedef vector<pair<enum_ty,vector<ClauseId> > > parsed_clauses; // if first=0,1,2,3 then root,CL,VAR,CONF


//=================================================================================================
// DIMACS Parser:
// DIMACS Parser and proof checker are from MiniSat 1.14p sources (MIT license reproduced below)
/*****************************************************************************************[Proof.C]
MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/

#define CHUNK_LIMIT 1048576

const int WORD_LEN      = 64000;

class StreamBuffer {
    gzFile  in;
    char    buf[CHUNK_LIMIT];
    int     pos;
    int     size;

    void assureLookahead() {
        if (pos >= size) {
            pos  = 0;
            size = gzread(in, buf, sizeof(buf)); } }

public:
    StreamBuffer(gzFile i) : in(i), pos(0), size(0) {
        assureLookahead(); }

    int  operator *  () { return (pos >= size) ? EOF : buf[pos]; }
    void operator ++ () { pos++; assureLookahead(); }
};

template<class B>
static void skipWhitespace(B& in) {
    while ((*in >= 9 && *in <= 13) || *in == 32)
        ++in; }

template<class B>
static void skipLine(B& in) {
    for (;;){
        if (*in == EOF) return;
        if (*in == '\n') { ++in; return; }
        ++in; } }

template<class B>
static int parseInt(B& in) {
    int     val = 0;
    bool    neg = false;
    skipWhitespace(in);
    if      (*in == '-') neg = true, ++in;
    else if (*in == '+') ++in;
    if (*in < '0' || *in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
    while (*in >= '0' && *in <= '9')
        val = val*10 + (*in - '0'),
        ++in;
    return neg ? -val : val; }

template<class B>
static void readClause(B& in, vector<int>& lits, int& numvars) {
    int     parsed_lit, var;
    lits.clear();
    for (;;){
        parsed_lit = parseInt(in);
        if (parsed_lit == 0) break;
        var = abs(parsed_lit)-1;
        while (var >= numvars) numvars++;
        lits.push_back( (parsed_lit > 0) ? var+var : var+var+1 );
    }
}

void vi2vl(const vector<int>& vi, vec<Lit>& vl) {
  int vsz = vi.size();
  for (int ii=0;ii<vsz;ii++)
    vl.push(Lit(vi[ii]>>1,vi[ii]&1));
}

template<class B>
static void parse_DIMACS_main(Proof& P, vec<vec<Lit> >& clauses, B& in,
                              parsed_clauses* pclauses, map<Lit,ClauseId>& units,
                              int& numvars, int& numclauses) {
    vector<int> lits;
    bool skip;
    for (;;){
      skip = false;
        skipWhitespace(in);
        if (*in == EOF)
            break;
        else if (*in == 'c' || *in == 'p')
            skipLine(in);
        else {
          readClause(in, lits, numvars);
          sort(lits.begin(),lits.end());
          lits.erase(unique(lits.begin(),lits.end()),lits.end()); //sortUnique(lits);
          for (int i = 0; i < lits.size()-1; i++) // skip trivial clause
            if (lits[i] == ((lits[i+1])^1)) {
              skip=true;
              break;
            }
          if (!skip) {
            if (lits.size()==1)
              units.insert(make_pair(Lit(lits[0]>>1,lits[0]&1),numclauses));
            pclauses->push_back(make_pair(ROOT,lits));
            vec<Lit> Lits;
            vi2vl(lits,Lits);
            clauses.push();
            Lits.copyTo(clauses.last());
            P.addRoot(Lits);
            numclauses++;
          }
        }
    }
}

// Inserts problem into solver.
//
static void parse_DIMACS(Proof& P, vec<vec<Lit> >& clauses, gzFile input_stream,
                         parsed_clauses* pclauses, map<Lit,ClauseId>& units,
                         int& numvars, int& numclauses) {
    StreamBuffer in(input_stream);
    parse_DIMACS_main(P, clauses, in, pclauses, units, numvars, numclauses);
}

// Simplistic proof-checker -- just to illustrate the use of 'ProofTraverser':

//#include "Sort.h"

static void resolve(vec<Lit>& main, vec<Lit>& other, Var x)
{
    Lit     p;
    bool    ok1 = false, ok2 = false;
    for (int i = 0; i < main.size(); i++){
        if (var(main[i]) == x){
            ok1 = true, p = main[i];
            main[i] = main.last();
            main.pop();
            break;
        }
    }

    for (int i = 0; i < other.size(); i++){
        if (var(other[i]) != x)
            main.push(other[i]);
        else{
            if (p != ~other[i])
                printf("PROOF ERROR! Resolved on variable with SAME polarity in both clauses: %d\n", x+1);
            ok2 = true;
        }
    }

    if (!ok1 || !ok2)
        printf("PROOF ERROR! Resolved on missing variable: %d\n", x+1);

    sortUnique(main);
}


struct Checker : public ProofTraverser {
    vec<vec<Lit> >  clauses;
  int res_count;
  Checker() { res_count = 0; }

    void root   (const vec<Lit>& c) {
      /*printf("%d: ROOT", clauses.size());
        for (int i = 0; i < c.size(); i++)
        printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); printf("\n");*/
        clauses.push();
        c.copyTo(clauses.last()); }

    void chain  (const vec<ClauseId>& cs, const vec<Var>& xs) {
      /*printf("%d: CHAIN %d", clauses.size(), cs[0]);
        for (int i = 0; i < xs.size(); i++)
        printf(" [%d] %d", xs[i]+1, cs[i+1]);*/
        clauses.push();
        vec<Lit>& c = clauses.last();
        clauses[cs[0]].copyTo(c);
        res_count+=xs.size();
        for (int i = 0; i < xs.size(); i++)
            resolve(c, clauses[cs[i+1]], xs[i]);
        /*printf(" =>"); for (int i = 0; i < c.size(); i++)
          printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); printf("\n");*/
        }

    void deleted(ClauseId c) {
        clauses[c].clear(); }
};


void checkProof(Proof* proof, ClauseId goal = ClauseId_NULL)
{
    Checker trav;
    proof->traverse(trav, goal);

    vec<Lit>& c = trav.clauses.last();
    printf("Final clause:");
    if (c.size() == 0)
        printf(" <empty>\n");
    else{
        for (int i = 0; i < c.size(); i++)
            printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1);
        printf("\n");
    }
    printf("Inferences: %d\n",trav.res_count);
}
//MIT license ends here
//=================================================================================================


//==========================================================================================
// zChaff trace parsing
// Follows Tjark Weber's documentation of the zChaff proof format (TPHOLs2005, track B)

void parse_zChaff(char * filename, int& numclauses,
                  parsed_clauses* pclauses, vector<int>& vars) {
  ifstream fin(filename);
  if (!fin) { cerr << "Error opening zChaff trace file " << filename << endl; exit(1); }
  istringstream iss;
  string line,stok;
  int itok;
  while (!fin.eof()) {
    getline(fin,line);
    iss.clear();
    iss.str(line);
    iss >> stok;
    if (stok=="CL:") {
      iss >> itok;  //clause id set by zChaff is ignored
      iss >> stok; assert(stok=="<=");
      vector<ClauseId> resolvents;
      while (!iss.eof()) {
        iss >> itok;
        resolvents.push_back(itok);
      }
      pclauses->push_back(make_pair(CL,resolvents));
      numclauses++;
    }
    else if (stok=="VAR:") {
      int vid; iss >> vid;
      iss >> stok; assert(stok=="L:");
      int level; iss >> level;
      iss >> stok; assert(stok=="V:");
      int value; iss >> value;
      assert((value ==0) || (value==1));
      iss >> stok; assert(stok=="A:");
      int ante; iss >> ante;
      // we don't parse the rest of the line
      vars[vid-1] = pclauses->size();
      vector<int> varv;
      varv.push_back(((vid-1)<<1)|(value?0:1));
      varv.push_back(ante);
      varv.push_back(level);
      pclauses->push_back(make_pair(VAR,varv));
      numclauses++;
    }
    else if (stok=="CONF:") {
      int conf_id; iss >> conf_id;
      // we don't parse the rest of the line
      vector<int> confv;
      confv.push_back(conf_id);
      pclauses->push_back(make_pair(CONF,confv));
      numclauses++;
    } else { cerr << "Unrecognized token\n"; exit(1); }
  }
}

//==========================================================================================

void printProofStats() {
      double  cpu_time = cpuTime();
      int64   mem_used = memUsed();
      if (mem_used!= 0) reportf("Memory used     : %.2f MB\n",
                                 (mem_used)/1048576.0);
      reportf("CPU time        : %g s\n", (cpu_time));
}

//==========================================================================================
// zChaff to MiniSat translation functions
// Follows Tjark Weber's documentation of the zChaff proof format (TPHOLs2005, track B)

class Z2M {
  vector<int> vartmp;
  vector<int> lu;
  vector<int> c2c;
  Proof& P;
  vec<vec<Lit> >& clauses;
  map<Lit,ClauseId>& units;
  vector<int>& vars;
  const int numclauses;
  const int numvars;
  parsed_clauses& pclauses;

  void update(vector<int>& ps, int lit, vector<int>& r1) {
    int flag = vartmp[lit>>1];
    if (flag==-1) { // lit not seen yet
      r1.push_back(lit);
      vartmp[lit>>1] = lit;
      lu.push_back(lit>>1);
    } else if (flag==(lit^1)) { // seen and now seen with opp sign: piv "second" occ
      vartmp[lit>>1]=lit; // switch vartmp to "second" occurrence
      ps.push_back(flag>>1); // record pivot in ps
    }
  }

  // calculate learnt clause, and fill in list of pivot vars
  void get_res(const vector<int>& resolvents,
               vec<Lit>& res, vector<int>& ps) {
    vector<int> r1;
    int rsz = resolvents.size();
    for (int ii=0;ii<rsz;ii++) {
      const vec<Lit>& cc = clauses[c2c[resolvents[ii]]];
      int csz = cc.size();
      for (int jj=0;jj<csz;jj++)
        update(ps,index(cc[jj]),r1);
    }
    int r1sz = r1.size();
    for (int ii=0;ii<r1sz;ii++) {
      int lit = r1[ii];
      if ((vartmp[lit>>1]^1)==lit) continue; // a "first" occ of pivot
      res.push(Lit(lit>>1,lit&1));
    }
    int lsz = lu.size();
    for (int ii=0;ii<lsz;ii++) vartmp[lu[ii]]=-1;
    lu.clear();
  }

  // create minisat chain for a "CL" line of zChaff proof trace
  int addChain(vector<int>& resolvents, int ci) {
    vec<Lit> res;
    vector<int> ps; // pivots
    get_res(resolvents,res,ps);
    assert(ps.size()==resolvents.size()-1);
    P.beginChain(c2c[resolvents[0]]);
    for (int ii=1; ii<resolvents.size();ii++)
      P.resolve(c2c[resolvents[ii]], ps[ii-1]);
    int idx = P.endChain();
    assert(idx==clauses.size());
    if (res.size()==1)
      units.insert(make_pair(res[0],ci));
    clauses.push();
    res.copyTo(clauses.last());
    return idx;
  }

  // create minisat chain for a "VAR" line of zChaff proof trace
  // each lit in ante has a corresponding unit clause with opposing sign,
  // which we can lookup via units
  // when all these unit clauses are resolved against the clause ante,
  // we get a unit clause which is the same as var vid with sign sgn
  int addVChain(int vid, bool sgn, int ante, int ci) {
    vec<Lit>& lits = clauses[c2c[ante]];
    Lit p(vid,sgn);
    P.beginChain(c2c[ante]);
    for (int i=0; i<lits.size();i++) {
      if (lits[i]==p) continue; // skip vid itself
      // pick up unit clause id corresponding to -ve of lit
      map<Lit,ClauseId>::iterator iter = units.find(~lits[i]);
      assert(iter!=units.end());
      P.resolve(c2c[iter->second], var(lits[i]));
    }
    int idx = P.endChain();
    assert(idx==clauses.size());
    units.insert(make_pair(p,ci));
    clauses.push();
    clauses.last().push(p);
    return idx;
  }

  // create minisat chain for "CONF" line of zChaff proof trace
  // this is more or less the same as writeVChain, except
  // that instead of deriving a unit clause we derive empty
  void addCChain(int conf_id) {
    vec<Lit>& lits = clauses[c2c[conf_id]];
    P.beginChain(c2c[conf_id]);
    for (int i=0; i<lits.size();i++) {
      // pick up unit clause id corresponding to this lit
      map<Lit,ClauseId>::iterator iter = units.find(~lits[i]);
      assert(iter!=units.end());
      P.resolve(c2c[iter->second], var(lits[i]));
    }
    P.endChain();
  }

  void addRoot(int ci) {
    c2c[ci] = ci;
    pclauses[ci].first=DONE;
  }

  void build_clause(int ci) {
    pair<enum_ty,vector<int> >& clause_info = pclauses[ci];
    vector<int>& resolvents = clause_info.second;
    int rsz = resolvents.size();
    for (int ii=0;ii<rsz;ii++)
      build(resolvents[ii]);
    c2c[ci] = addChain(resolvents,ci); // learnt
    pclauses[ci].first=DONE;
  }

  void build_var(int ci) {
    pair<enum_ty,vector<int> >& clause_info = pclauses[ci];
    int lit = clause_info.second[0];
    int ante = clause_info.second[1];
    build(ante);
    if (clauses[c2c[ante]].size()==1) {
      pclauses[ci].first=DONE;
      return;
    };
    vec<Lit> cc;
    clauses[c2c[ante]].copyTo(cc);
    vector<pair<int,int> > levels;
    for (int ii=0;ii<cc.size();ii++) {
      if (lit==index(cc[ii])) continue; // skip lit of the var itself
      int ci = vars[var(cc[ii])];
      levels.push_back(make_pair(pclauses[ci].second[2],ci));
    }
    sort(levels.begin(),levels.end());
    for (int ii=0;ii<cc.size()-1;ii++)
      build(levels[ii].second);
    c2c[ci] = addVChain(lit>>1, (bool)(lit&1), ante, ci);
    pclauses[ci].first=DONE;
  }

  // ci is index in pclauses
  void build(int ci) {
    switch (pclauses[ci].first) {
    case ROOT: addRoot(ci); break;
    case CL: build_clause(ci); break;
    case VAR: build_var(ci); break;
    case DONE: break;
    default: cerr << "build default\n"; exit(1);
    }
  }

public:

  Z2M(Proof& P_,vec<vec<Lit> >& clauses_,map<Lit,ClauseId>& units_, vector<int>& vars_, int numclauses_,
      int numvars_, parsed_clauses& pclauses_) :
    P(P_),
    clauses(clauses_),
    units(units_),
    vars(vars_),numclauses(numclauses_),numvars(numvars_),
    pclauses(pclauses_),
    vartmp(numvars_,-1),
    c2c(pclauses_.size(),-1) {}

  void build_clauses() {
    pair<enum_ty,vector<int> >& clause_info = pclauses.back();
    int conf_id = clause_info.second[0];
    build(conf_id);
    vec<Lit> cc;
    clauses[c2c[conf_id]].copyTo(cc);
    vector<pair<int,int> > levels;
    for (int ii=0;ii<cc.size();ii++) {
      int ci = vars[var(cc[ii])];
      levels.push_back(make_pair(pclauses[ci].second[2],ci));
    }
    sort(levels.begin(),levels.end());
    for (int ii=0;ii<cc.size();ii++)
      build(levels[ii].second);
    addCChain(conf_id);
  }

};

//==========================================================================================

int main(int argc, char** argv) {
  char*       input  = NULL; // the name of the input CNF problem file
  char*       proof  = NULL; // the name of the output minisat proof trace file
  char*       zchaff  = NULL; // the name of the input zChaff proof trace file
  bool        check  = false; // verify the proof if true

  for (int i = 1; i < argc; i++) {
    if (argv[i][0] != '-') {
      if (input != NULL)
        fprintf(stderr, "ERROR! Only one input file may be specified.\n"), exit(1);
      input = argv[i];
    } else {
      switch (argv[i][1]){
      case 'c':
        check = true;
        break;
      case 'm':
        i++; if (i >= argc) fprintf(stderr, "ERROR! Missing filename after '-m' option.\n");
        proof = argv[i];
        break;
      case 'z':
        i++; if (i >= argc) fprintf(stderr, "ERROR! Missing filename after '-z' option.\n");
        zchaff = argv[i];
        break;
      }
    }
  }

  Proof P;  // minisat proof ADT
  vec<vec<Lit> > clauses; // clause database
  map<Lit,ClauseId> units; // map literal to corresponding unit clause id, if any
  int numvars = 0, numclauses = 0, conf_id;
  parsed_clauses* pclauses = new parsed_clauses();
  // first read CNF from original file and add to proof
  gzFile in = (input == NULL) ? gzdopen(0, "rb") : gzopen(input, "rb");
  parse_DIMACS(P, clauses, in, pclauses, units, numvars, numclauses);
  gzclose(in);

  // then read resolvents from zchaff trace
  vector<int> vars(numvars);   // vars[i] is pclauses idx for variable i
  parse_zChaff(zchaff, numclauses, pclauses, vars);

  // finally translate to minisat format
  Z2M translator(P,clauses,units,vars,numclauses,numvars,*pclauses);
  translator.build_clauses();

  // (check) and save proof
  delete pclauses;
  Proof* current = &P;
  if (check) { // quick check
    reportf("Checking proof...\n");
    checkProof(current);
  }
  if (proof != NULL) current->save(proof); // save it
  printProofStats();
  return 0;
}