/*
SAT competition input compliance checker and size counter.
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.
*/

#include <stdio.h>
#include <stdlib.h>
#include <time.h>
#include <unistd.h>
#include <string.h>

#define MAXLEN 65000 //Lines should be shorter than this

typedef long long int *CLAUSE;

void err(int status, char*message) //prints the message on stderr and 
                                   //terminates with the given status
{
  fprintf(stderr,"\nerror %d: %s",status, message);
  fflush(stderr);
  exit(status);
}

int sign(long long int lit) //just sign (-1,0,1)
{
  if (lit>0) return 1; else if (lit<0) return -1; else return 0;
}


inline int llicomp(const void *a, const void *b)
{
  return ((*((long long int *)a))-(*(long long int *)b));
}

int main(int argc, char** argv)
{   
  FILE *fi, *fo; //input and output streams
  char buffer[MAXLEN]; //input file buffer
  char *cbuffer; //current position in the current string
  long long int clause[MAXLEN]; //current clause buffer
  int pgiven=0; //did we read the "p" line
  long long int nvar, ncla; //...given in the "p" line
  long long int lit; //current literal
  long long int nlit; //current length of current clause
  long long int cla=0; //current clause number (1..ncla)
  long long int L=0;
  
  if (argc<2) err(1,"\nUsage: counter file.cnf\n\n");

  //read the formula...
  fi=fopen(argv[1],"rt");
  if (!fi) err(2,"\nCannot open input file.\n\n");
  
  while (!feof(fi))
  {
    fgets(buffer,MAXLEN,fi);
    if (buffer[strlen(buffer)-1]!='\n') if (!feof(fi)) 
    {
      fprintf(stderr,"%s\n",buffer);
      err(4,"\nLine too long.\n\n");
    }
    switch (buffer[0])
    {
      case 'c': if (pgiven) err(5,"\nComment after the \"p\" line.\n\n");
		break; //drop comments
      case 'p': if (pgiven) err(6,"\nTwo \"p\" lines.\n\n");
		pgiven=1;
		if (2!=sscanf(buffer,"p cnf %lld %lld\n",&nvar,&ncla))
		  err(7,"\nFailed to process the \"p\" line.\n\n");
		break;
      default:  if (!pgiven) //we don't know the number of vars yet! 
		  err(8, "\nEither \"c\" or \"p\" line was expected.\n\n");
//DEBUG		fprintf(stderr,"[%s]",buffer);
//fprintf(stderr,"\n%lld: ",cla);
		if (++cla>ncla) //check that the rest of file is empty
		{
		  while (!feof(fi))
		  {
		    char c;
		    if (sscanf(buffer,"%c",&c)>=1) //found a character here!
		      err(9, "\nToo many clauses or garbage before EOF.\n\n");
		    if (!fgets(buffer,MAXLEN,fi)) break;
		  }
		  break;
		}
		cbuffer=buffer;
		while (1)
		{
//DEBUG		  fprintf(stderr,"<%s>",cbuffer);
		  if (sscanf(cbuffer,"%lld",&lit)!=1) 
		  {
		    fprintf(stderr,"%s",buffer);
		    err(10, "\n0-terminated clause line was expected.\n\n");
		  }
		  if (!lit) //end of clause
		  {
    long long int clen;
    L+=nlit;
		    clause[nlit++]=0;
    qsort(clause,nlit-1,sizeof(long long int),llicomp);
    for (clen=0; clause[clen]!=0; clen++)
      if (clause[clen+1]==clause[clen]) 
      {
	fprintf(stderr, "Clause %lld, variable %lld:", cla, clause[clen]); 
	fflush(stderr);
	err(5001, "\nA variable occurs twice in a clause\n\n");
      }
    //  else fprintf(stderr,"%lld ",clause[clen]);
		    nlit=0;
		    break;
		  }
		  else 
		  {
		    clause[nlit++]=abs(lit); //don't need sign
		    cbuffer=strpbrk(cbuffer," \t"); //strchr(cbuffer,' ');
		    if (!cbuffer)
		    {
		      fprintf(stderr,"%s",buffer);
		      err(110, "\n0-terminated clause line was expected.\n\n");
		    }
		    else cbuffer++;
		  }
		} 
    }
  }
  fclose(fi);
  if (cla<ncla) err(12, "\nToo few clauses.\n\n");

  printf("%lld\n",L);
 
  exit(0);
}