/* Translate a CNF format file to SAT format */
/* Compile: gcc -o cnf2sat cnf2sat.c */

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

Usage: ./cnf2sat [-in in_file] [-out out_file]
Description: 
        Translates from CNF format to SAT 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 cnf2sat(FILE * input, FILE * output);
void writestring(char * s, FILE * f);
void myputc(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;
		} 
	}

	cnf2sat(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 CNF format to SAT 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 * Acw; /* Actual character in writing*/

/*=================================================================*/
void cnf2sat(FILE * f, FILE * output)
{
	char c;
	char * tmp;
	int i, d1, d2;
	
	tmp = (char *)calloc(100, sizeof(char));
	Ws = (char *)calloc(MAXFILE_LENGTH, sizeof(char));
	if (Ws == NULL) 
	  print_err("Not enough memory", 1);

	Acw = Ws;

	while ((c = fgetc(f)) != EOF){
		switch (c)
		  {
			case '\n':
			case ' ':
			case '\t':
			  myputc(' ');
			  while ((c = fgetc(f)) == ' ' || c == '\t'|| c == '\n');
			  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':
			  for (; *(Acw-1) != '\n'; Acw--);
			  myputc(c);
			  fscanf(f, "%s %d %d\n", tmp, &d1, &d2);
			  Acw += strlen(sprintf(Acw, " sat %d\n(*(+( ", d1));
			  break;

			case '0':
			  if (*(Acw-1) == ' '){ 
				  myputc(')');
				  myputc('\n');
				  myputc('+');
				  myputc('(');
				  myputc(' ');
			  }else
				myputc(c);
			  break;
			  
			default:
			  myputc(c);
			  break;
		  }
	}
	Acw -= 3;
	myputc(')');
	myputc(')');
	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++;
}

/*=================================================================*/
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);
}