/*
SAT competition output compliance verifier
Copyright (C) 2002 Laurent Simon and Edward Hirsch

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
*/


/* usage: verifier file.cnf < output
   the output is readed form stdin, the output format is checked and 
   the model is checked wrt file.cnf */

#include <stdio.h>
#include <malloc.h>
#include <stdlib.h>
#include <sys/time.h> 
#include <time.h> 
#include <string.h>

typedef long *CLAUSE; //starts with its length
typedef long *SUBST;  //2 = UNKNOWN; 0th element: number of variables

struct CNF
{
  long nvars;
  long nclauses;
  CLAUSE *clauses;
  long *clauses_lengths;
  long *sclauses_lengths;
};

//#define HS_DEBUG
char st[256];

struct CNF NewCNF(char *fn)
{
  FILE *f=fopen(fn,"rt");
  struct CNF c;
  long i;
  long *d;
  if (!f) { fprintf(stderr,"c~~ verifier: Failed to open %s\n",fn); exit(100); }
  while (fgetc(f)!='p') fgets(&(st[0]),250,f); 
  if (2!=fscanf(f," cnf %ld %ld",&(c.nvars),&(c.nclauses)))
  {
    fprintf(stderr,"c~~ verifier: ERROR: wrong .cnf file\n");
    exit(1);
  }
  d=(long*)malloc((c.nvars+2)*sizeof(long)); 
  c.clauses=(CLAUSE*)(malloc(c.nclauses*sizeof(CLAUSE)));
  c.clauses_lengths=(long*)(malloc(c.nclauses*sizeof(long)));
  c.sclauses_lengths=(long*)(malloc(c.nclauses*sizeof(long)));
  for (i=0; i<c.nclauses; i++) // read the formula clause by clause
  {
    long j;
    d[0]=1;
    for (j=1; d[j-1]!=0; j++) fscanf(f,"%ld",&(d[j])); // read first to d[]
    c.clauses[i]=(CLAUSE)(malloc((j-2)*sizeof(long)));
    c.clauses_lengths[i]=(c.sclauses_lengths[i]=j-2); // write down its length
    for (j=0; j<c.clauses_lengths[i]; j++) 
      c.clauses[i][j]=d[j+1]; // copy now d to c[i][]
  }
  fclose(f);
  return c;
}


int main(int argc, char *argv[])
{
  struct CNF F;
  SUBST s;
  long lit,i;
  int hasV0 = 0;
  int hasVLine = 0;
  int haslineS = 0;
  char c;
  int *varmodel;
  char sol[40]="";

  if (argc<2) { fprintf(stderr,"c~~ verifier: Required argument missing.\n"); exit(100); }

  F=NewCNF(argv[1]);
  s=(SUBST)(malloc((F.nvars+1)*sizeof(long)));
  s[0]=F.nvars;
  for (i=1; i<=F.nvars; i++) s[i]=2;
  varmodel=(int*)malloc((F.nvars+1)*sizeof(int));
  for (i=1; i<=F.nvars; i++) varmodel[i]=0;

  while (!feof(stdin))
  {
    if (scanf("%128s",&(st[0]))==1)
      //    fprintf(stderr,"c~~ verifier: <%s>\n",st);
      switch (st[0])
	{
	case 'c': scanf("%c",&c);
	  while (c!='\n') scanf("%c",&c); 
	  break;
	case 's':
	  if (haslineS) {
	    fprintf(stderr, "c~~ verifier: ERROR: Two lines 's' defined\n'");
	    exit(1);
	  }
	  i = scanf("%20s\n",&(sol[0]));
	  if (i >= 19) {
	    fprintf(stderr,"c~~ verifier: ERROR: Non-valid line 's'\n");
	    exit(1);
	  }
	  haslineS = 1; 
	  break;
	case 'v':
	  hasVLine = 1;
	  while (scanf("%ld",&lit)==1)
	    if (lit == 0) {
	      hasV0 = 1;
	      // Noter que plus de v... Et qu'on en a un...
	    } else if (abs(lit)<=F.nvars)
	      {
		//		long cl,j;
		if (hasV0) {
		  fprintf(stderr,"c~~ verifier: ERROR: litteral %ld after 0\n",lit);
		  exit(1);
		}
		if (varmodel[abs(lit)]) {// already defined 
		  if  ( ( (lit < 0) && (varmodel[abs(lit)] == 1) ) ||
			( (lit > 0) && (varmodel[abs(lit)] == -1) ) ) {
		      fprintf(stderr,"c~~ verifier: ERROR: literal %ld contradictory in model\n",lit);
		      exit(1);
		  } else
		    fprintf(stderr,"c~~ verifier: WARNING: literal %ld defined twice in model\n", lit);
		}
		varmodel[abs(lit)] = lit<0?-1:1;
		// To costly for huge formulae... Let's move it to the end!
/*  		for (cl=0; cl<F.nclauses; cl++) */
/*  		  for (j=0; j<F.clauses_lengths[cl]; j++) */
/*  		    if (F.clauses[cl][j]==lit)  */
/*  		      F.clauses_lengths[cl]=-1; */
	      }
	    else { fprintf(stderr,"c~~ verifier: ERROR: illegal literal  %ld\n",lit); exit(1); }
	  break;
	default: fprintf(stderr,"c~~ verifier: WARNING: illegal line somewhere\n");
	  scanf("%c",&c);
	  while (c!='\n') scanf("%c",&c); 
	  break;
	}
  }
  if (strcmp(sol,"SATISFIABLE")==0)
    {
      long cl,j,clauseok;
      if (hasV0 == 0) {
	fprintf(stderr,"c~~ verifier: WARNING: Model line doesn't end with 0\n");
      }
      for (cl=0; cl<F.nclauses; cl++) {
	clauseok=0;
	for (j=0; j<F.clauses_lengths[cl]; j++) {
	  lit = F.clauses[cl][j];
	  if ( ( (lit < 0) && (varmodel[abs(lit)] == -1) ) ||
	       ( (lit > 0) && (varmodel[abs(lit)] == 1) ) ) {
	    clauseok=1;
	    break;
	  }
	}
	if (clauseok==0) 
	  { fprintf(stderr,"c~~ verifier: ERROR some clauses left%c (v lines don't define an implicant)\n",7); 
	  fprintf(stderr,"c~~ verifier: ERROR: Original clause left: ");
	  fprintf(stderr,"c~~ verifier: ");
	  for (j=0; j<F.clauses_lengths[cl]; j++)
	    fprintf(stderr,"%d ",F.clauses[cl][j]);
	  fprintf(stderr,"0\n");
	  exit(1); }
      }
      fprintf(stderr,"c~~ verifier: OK: SATISFIABLE claimed, and implicant is correct\n");
      exit(10);
    }
  else if (strcmp(sol,"UNSATISFIABLE") == 0) {
    if (hasVLine) {
      fprintf(stderr,"c~~ verifier: ERROR: v line defined, and UNSAT claimed\n");
      exit(1);}
    fprintf(stderr,"c~~ verifier: OK: UNSATISFIABLE claimed, no model provided by solver\n");
    exit(20);
  } else if (strcmp(sol,"UNKNOWN") == 0) {
    if (hasVLine) {
      fprintf(stderr,"c~~ verifier: ERROR: v line defined, and UNKNOWN claimed\n");
      exit(1);}
    fprintf(stderr,"c~~ verifier: OK: UNKNOWN claimed, no model provided by solver\n");
    exit(0);
  } else if (strcmp(sol,"") == 0)  {
    if (hasVLine) {
      fprintf(stderr,"c~~ verifier: ERROR: v line defined, and no results given (no line 's XXXXX')\n");
      exit(1);}
    fprintf(stderr,"c~~ verifier: OK: no results given, no model provided by solver\n");
    exit(0);
  } else {
    fprintf(stderr,"c~~ verifier: ERROR: wrong answer <%s>\n",sol); 
    exit(1);
  }
 exit(0);
}