/* Translate a SAT format file (which contains a boolean formula in cnf 
   formulation */
/* Compile: gcc -o sat2cnf sat2cnf.c */

/* Written by Tamas Badics (badics@rutcor.rutgers.edu)
   Last modification: Fri Apr 23 16:37:46 EDT 1993

Usage: ./sat2cnf [-in in_file] [-out out_file]
Description: 
        Translates from SAT format to CNF format.
        By default it uses the stdin and stdout.
*/

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

#define MAXFILE_LENGTH 4000000
#define LINE_LENGTH 78

void cnfsat2cnf(FILE * input, FILE * output);
void writestring(char * s, FILE * f);
void myputc(char c);
char mygetc(void);
void myungetc(char c);
int look_up(char * s);

void main(int argc, char * argv[])
{
	int i;
	FILE * output, * input;
	
	output = stdout;
	input = stdin;
	
	for (i = 1; i < argc; i++){
		switch (look_up(argv[i])){
		  case 0:   /* -out */
			output = fopen(argv[++i],"w");
			if (output == NULL) {
				fprintf(stderr
                    ,"%s: Output file %s can't be opened\n",argv[0],argv[i]);
				exit(-1);
			}	
			break;
		  case 1:  /* -in */ 
			input = fopen(argv[++i],"r");
			if (input == NULL) {
				fprintf(stderr
                    ,"%s: Input file %s can't be opened\n",argv[0],argv[i]);
				exit(-1);
			}	
			break;
		  default:
			goto USAGE;
			break;
		} 
	}

	cnfsat2cnf(input, output);

	if (output != stdout)  fclose(output);
	if (input != stdin)	  fclose(input);
	exit(0);
	
  USAGE:
	if (output != stdout)  fclose(output);
	if (input != stdin)  fclose(input);

	printf("Usage: %s [-in in_file] [-out out_file]\n",argv[0]);
	printf("Description: \n\tTranslates from SAT format to CNF format.\n");
	printf("\tBy default it uses the stdin and stdout.\n");
	
	exit(0);
}
/*=================================================================*/
#define OPS_NUM 2

int look_up(char * s)
{
	char * ops[OPS_NUM]  = { "-out", "-in"};
	int i;
	
	for (i = 0; i < OPS_NUM; i++)
	  if (strcmp(ops[i], s) == 0)
		return i;

	return -1;
} 
/*=================================================================*/
void print_err(char * s, int stop)
{
	fprintf(stderr, "%s\n", s);
	if (stop)
	  exit(-1);
}

/*=================================================================*/
char * Ws; /* work string */
char * Acr; /* Actual character in reading*/
char * Acw; /* Actual character in writing*/
int C;

void readfile(FILE * f);
  
/*=================================================================*/
void cnfsat2cnf(FILE * input, FILE * output)
{
	int bracket = 0, d;
	char c;
	char * tmp;
	
	tmp = (char *)calloc(100, sizeof(char));
	Ws = (char *)calloc(MAXFILE_LENGTH, sizeof(char));
	if (Ws == NULL) 
	  print_err("Not enough memory", 1);

	Acr = Acw = Ws;
	readfile(input);
	Acw = Ws;
	
	while ((c = mygetc()) != '\0'){
		switch (c)
		  {
			case 'c':
			  myputc(c);
			  while ((c = mygetc()) != '\n' && c != '\0') myputc(c);
			  myputc('\n');
			  break;

			case 'p':
			  for (; *(Acw-1) != '\n'; Acw--);
			  myputc(c);
			  sscanf(Acr, "%s %d\n", tmp, &d);
			  while ((c = mygetc()) != '\n' && c != '\0');
			  Acw += strlen(sprintf(Acw, " cnf %d %d\n", d, C));
			  break;
			  
			case '-':
			  if (*(Acw - 1) != ' ') myputc(' ');
			  myputc(c);
			  while ((c = mygetc()) == '(' || c == ' ' || c == '\n')
				if (c == '(') bracket++;
			  myungetc(c);
			  break;

			case '\n':
			case ' ':
			case '+':
			case '*':
			  myputc(' ');
			  break;

			case '(':
			  bracket++;
			  myputc(' ');
			  break;
	
			case ')':
			  bracket--;
			  myputc(' ');
			  if (bracket == 2){ 
				  myputc('0');
				  myputc('\n');
			  }
			  break;
			  
			default:
			  myputc(c);
			  break;
		  }
	}		

	myputc('\n');
	myputc('\0');
	
	writestring(Ws, output);
	
	free(Ws);
	free(tmp);
}

/*=================================================================*/
void myputc(char c)
{
	if (Acw - Ws == MAXFILE_LENGTH)
	  print_err("File is longer than allocated space", 1);
	
	if (c == ' ' && (*(Acw-1) == ' ' || *(Acw-1) == '\n'))
	  return;
	
	*Acw = c;
	Acw++;
}
/*=================================================================*/
char mygetc(void)
{
	char c = *Acr;
	
	Acr++;
	return(c);
}

/*=================================================================*/
void myungetc(char c)
{
	Acr--;
	*Acr = c;
}

/*=================================================================*/
void readfile(FILE * f) /* reads f into Ws cleaning the whitechars */
{
	char c;
	int nl, i, bracket = 0;
	
	C = 0;
	while ((c = fgetc(f)) != EOF){
		switch (c)
		  {
			case '\n':
			  nl = 1;
			case ' ':
			case '\t':

			  while ((c = fgetc(f)) == ' ' || c == '\t'|| c == '\n')
				if (c == '\n') nl = 1;
			  
			  (nl == 1) ? myputc('\n') : myputc(' ');
			  nl = 0;
			  ungetc(c, f);
			  break;

			case 'c':
			  myputc('c');
			  for (i = 0; 
				   (c = fgetc(f)) != '\n' && i < LINE_LENGTH - 1 && c != EOF
				   ; i++) 
				myputc(c);

			  myputc('\n');
			  if ((i == LINE_LENGTH - 1 && c != '\n') || c == EOF){
				  ungetc(c, f);
				  ungetc(' ', f);
				  ungetc('c', f);
			  }
			  break;
			  
			case 'p':
			  myputc(c);
			  while ((c = fgetc(f)) != '\n' && c != EOF) myputc(c);
			  for (i=0; i < 20; i++, *Acw = ' ', Acw++);
			  myputc('\n');
			  break;

			case '(':
			  bracket++;
			  myputc(c);
			  break;

			case ')':
			  bracket--;
			  if (bracket == 2) C++;
			  myputc(c);
			  break;
			  
			default:
			  myputc(c);
			  break;
		  }
	}
	myputc('\0');
	if (bracket != 0) 
	  print_err("Error in input: Mismatching brackets.",1);
	
}

/*=================================================================*/
void writestring(char * s, FILE * f) /* writes a string to f cutting after
										LINE_LENGTH characters */
{
	int i, nl;
	char * t, *p;
	int len = strlen(s);
	char * ls = (char *)calloc(LINE_LENGTH + 1, sizeof(char));
	
	if (ls == NULL)
	  print_err("Not enough memory" , 1);

	for (i = 0; i < len;){
		nl = (t = strchr(s, '\n')) ? t - s + 1: len -i;
		  
		if (nl <= LINE_LENGTH ){ 
			strncpy(ls, s, nl);
			*(ls + nl) = '\0';
			s += nl;
			i += nl;
			fputs(ls, f);
		}else{
			nl = LINE_LENGTH;
			for (p = s + nl; *p != ' ' && p != s ; p--, nl--); 
			if (p == s)
			  print_err("Too short LINE_LENGTH.", 1);

			strncpy(ls, s, nl);
			*(ls + nl) = '\0';
			s += nl;
			i += nl;
			fputs(ls, f);
			fputc('\n', f);
		}
	} 

	free(ls);
}