#include <stdio.h>
#include <stdlib.h>

int main (int argc, char** argv) {
  int i, nVar, nCls, opt = 0;

  FILE* cnf = fopen (argv[1], "r");
  if (cnf == NULL) {
    printf ("c ERROR parsing CNF formula %s\n", argv[1]);
    exit (0); }

  char comment[1024];

  int tmp = fscanf (cnf, " p cnf %i %i ", &nVar, &nCls);
  while (tmp < 2) {
    tmp = fscanf (cnf, " %s ", comment);
    tmp = fscanf (cnf, " p cnf %i %i ", &nVar, &nCls);
  }

  // parse cnf
  int lit, nLit = 0, *formula;
  formula = (int*) malloc (sizeof (int) * nVar * nCls); // should become something dynamic
  while (1) {
    tmp = fscanf (cnf, " %i ", &lit);
    if (tmp == EOF) break;
    formula[nLit++] = lit; }

  fclose (cnf);

  if (argv[3] != NULL)
    if (argv[3][0] == '-' && argv[3][1] == 'O') opt = 1;

  FILE *pr  = fopen (argv[2], "r");
  if (pr == NULL) {
    printf ("c ERROR parsing PR proof %s\n", argv[2]);
    exit (0); }

  int *assignment;
  assignment  = (int*) malloc (sizeof (int) * (2*nVar + 1));
  assignment += nVar;
  int def = nVar + 1;
  int *lemma, lemma_size, *witness, witness_size;

  lemma   = (int*) malloc (sizeof (int) * nVar);
  witness = (int*) malloc (sizeof (int) * nVar);

  while (1) {
    tmp = fscanf (pr, " d %i ", &lit);
    if (tmp == EOF) break;

    // assignment reset... should become redundant
    for (i = 1; i <= nVar; i++) assignment[i] = assignment[-i] = 0;

    // if deletion step, then output step to stdout
    // and remove the clause from the formula.
    if (tmp > 0) {
      if (abs(lit) > nVar) {
        printf ("c introduction of new variables in not supported\n");
        exit (0); }
      assignment[lit] = 1;
      printf ("d %i ", lit);
      while (lit) {
        tmp = fscanf (pr, " %i ", &lit);
        if (abs(lit) > nVar) {
          printf ("c introduction of new variables in not supported\n");
          exit (0); }
        if (lit != 0) printf ("%i ", lit), assignment[lit] = 1;
        else          printf ("0\n"); }

      int first = 0;
      for (i = 0; i < nLit; i++) {
        if (formula[i] == 0) {
          int k;
          for (k = first; k < i; k++) formula[k] = 0;
          first = i + 1; }
        if (assignment[formula[i]] != 1) {
          while (formula[i] != 0) i++;
          first = i + 1; } }
      goto next_lemma; }
    else { // parse lemma and potential witness
      int wflag    = 0;
      lemma_size   = 0;
      witness_size = 0;
      tmp = fscanf (pr, " %i ", &lit);
      if (abs(lit) > nVar) {
        printf ("c introduction of new variables in not supported\n");
        exit (0); }
      int pivot    = lit;
      lemma[lemma_size++] = lit;
      while (lit) {
        tmp = fscanf (pr, " %i ", &lit);
        if (abs(lit) > nVar) {
          printf ("c introduction of new variables in not supported\n");
          exit (0); }
        if (lit == pivot) {
          wflag = 1;
          lemma[lemma_size++] = 0; }
        if (wflag) witness[witness_size++] = lit;
        else       lemma  [  lemma_size++] = lit; }

      int *p;
      // if no witness is provided, then the lemma should be DRAT already
      if (witness_size == 0) {
        p = lemma;
        while (*p) printf ("%i ", *p++);
        printf ("0\n");
        p = lemma;
        while (*p) formula[nLit++] = *p++;
        formula[nLit++] = 0;
        goto next_lemma; }

      // set the assignment to the witness
      p = witness;
      while (*p) {
        lit = *p++;
        assignment[ lit] =  2;
        assignment[-lit] = -2; }

      int forced = 0, count = 0;

      if (opt) {
        for (i = 0; i < nLit; i++) {
          if (formula[i] == 0) { // end of clause
            if ((count == 1) && (assignment[forced] == 2)) {
              assignment[ forced] =  1;
              assignment[-forced] = -1; }
            forced = 0; count = 0; }
          else if (assignment[formula[i]] != -2) { count++; forced = formula[i];  } } }

      int mflag = 1;
      p = lemma;
      while (*p) if (assignment[*p++] == 2) mflag = 0;

      count = 0;
      p = lemma;
      while (*p++) count++;
      if (count == 1) mflag = 0;

//      printf("c mflag = %i\n", mflag);

      // phase I: add shortened copies of clauses reduced, but not satisfied by omega
      int piv = 0, sat = 0, red = 0;
      if (mflag == 0) {
        for (i = 0; i < nLit; i++) {
          if (formula[i] == 0) {
            if ((sat == 0) && (red >  0)) {
              int k;
              printf ("%i ", -def);
              for (k = piv; k < i; k++)
                if (assignment[formula[k]] == 0)
                  printf ("%i ", formula[k]);
                printf("0\n"); }
            piv = i + 1; sat = 0; red = 0; }
          else if (assignment[formula[i]] >  0) sat++;
          else if (assignment[formula[i]] < -1) red++; } }
      else {
        p = lemma;
        while (*p) printf ("%i %i 0\n", -def, -(*p++));
      }

      // phase II (a): add the implication x -> omega
      if (opt == 0 && mflag == 0) {
        p = witness;
        while (*p) printf ("%i %i 0\n", *p++, -def); }

      // phase II (b): weaken the involved clauses
      piv = 0, sat = 0, red = 0;
      for (i = 0; i < nLit; i++) {
        if (formula[i] == 0) {
          if ((sat > 0) && (red >  0)) {
            int k;
            printf ("%i ", def);
            for (k = piv; k < i; k++) printf ("%i ", formula[k]);
            printf("0\n");
            printf ("d ");
            for (k = piv; k < i; k++) printf ("%i ", formula[k]);
            printf("0\n"); }
          piv = i + 1; sat = 0; red = 0; }
        else if (assignment[formula[i]] >  0) sat++;
        else if (assignment[formula[i]] < -1) red++; }

      // phase II (c): remove the implication x -> omega
      if (opt == 0 && mflag == 0) {
        p = witness;
        while (*p) printf ("d %i %i 0\n",  *p++, -def); }

      // phase III: print the weakened PR clause
      p = lemma;
      printf ("%i ", def);
      while (*p) printf ("%i ", *p++);
      printf ("0\n");

      // phase IV (a): add the implication x -> omega
      p = witness;
      while (*p) {
        int lit = *p++;
        if (assignment[lit] == 2) printf ("%i %i 0\n", lit, -def); }
      if (mflag == 0) {
        p = witness;
        while (*p) {
          int lit = *p++;
          if (assignment[lit] == 1) printf ("%i %i 0\n", lit, -def); } }
      else {
        p = lemma;
        while (*p) printf ("d %i %i 0\n", -def, -(*p++));
      }

      // phase IV (b): strengthen the involved clauses
      piv = 0, sat = 0, red = 0;
      for (i = 0; i < nLit; i++) {
        if (formula[i] == 0) {
          if ((sat > 0) && (red >  0)) {
            int k;
            for (k = piv; k < i; k++) if (assignment[formula[k]] == 1) printf ("%i ", formula[k]);
            for (k = piv; k < i; k++) if (assignment[formula[k]] != 1) printf ("%i ", formula[k]);
            printf("0\n");
            printf ("d %i ", def);
            for (k = piv; k < i; k++) printf ("%i ", formula[k]);
            printf("0\n"); }
          piv = i + 1; sat = 0; red = 0; }
        else if (assignment[formula[i]] >  0) sat++;
        else if (assignment[formula[i]] < -1) red++; }

      // strengthen the weakened PR clause and add it to the formula
      p = lemma;
      while (*p) printf ("%i ", *p++);
      printf ("0\n");
      p = lemma;
      printf ("d %i ", def);
      while (*p) printf ("%i ", *p++);
      printf ("0\n");
      p = lemma;
      while (*p) formula[nLit++] = *p++;
      formula[nLit++] = 0;

      // phase IV (c): remove the implication x -> omega
      p = witness;
      while (*p) {
        int lit = *p++;
        if (assignment[lit] == 2) printf ("d %i %i 0\n", lit, -def); }
      if (mflag == 0) {
        p = witness;
        while (*p) {
          int lit = *p++;
          if (assignment[lit] == 1) printf ("d %i %i 0\n", lit, -def); } }

      // phase IV: remove the clauses that contain the literal -x (which are blocked)
      if (mflag == 0) {
        piv = 0, sat = 0, red = 0;
        for (i = 0; i < nLit; i++) {
          if (formula[i] == 0) {
            if ((sat == 0) && (red >  0)) {
              int k;
              printf ("d %i ", -def);
              for (k = piv; k < i; k++)
                if (assignment[formula[k]] == 0)
                  printf ("%i ", formula[k]);
                printf("0\n"); }
            piv = i + 1; sat = 0; red = 0; }
          else if (assignment[formula[i]] >  0) sat++;
          else if (assignment[formula[i]] < -1) red++; } }

    next_lemma:; }
  }
}