/* Anderson MacKay, Elec422 GSAT project
 *
 * GSAT demonstration code
 *
 * version 0.1: non-functional, but compilable ... and descriptive of 
 *              how the chip should work.
 */

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

/* useful utility functions */
void init_clause(void);
void toggle_variable_bit(int);
int check_variable(int, int);

/* Define some global variables (ugliness!) */

int variable_bitarray[4]; /* assuming int == 32 bits here, unfortunately */
int current_clause_count_9bits = 0;
int last_clause_count_9bits = 0;

/* the following variables would need to be initialized, presumably
   by an exterior program writing to off-chip memory */

char clause_bytearray[1536]; /* again, assuming char == 8 bits, although
			       it really doesn't matter here. */
int num_clauses_9bits;

int
main ()
{
  int t; /* scratch variable */
  int clause_marker_9bits; /* this is our index through the clauses */
  int variable_marker_7bits; /* our marker of which variable we flipped. */
  /* offsets into the clause array for the three pieces of our current
     clause. */
  int clause_offset;
  unsigned char clause_piece;
  int variable_num;
  /* these next three are storage as we examine a single clause: if a
     particular part of the clause is satisfied, then we set the value to
     1, otherwise it is set to 0. */
  int clause_part1_1bit, clause_part2_1bit, clause_part3_1bit;

  /* initialize clause_bytearray from the output of the python
    program.  Currently, this will create an expression using at most
    the first 26 variable in variable_bitarray */
  
  /* the whole program is one huge while loop terminating if we
     find a satisfiable assignment set for this problem. */
  init_clause();
  
  while(current_clause_count_9bits < num_clauses_9bits)
    {
      /* reset our counters before looping over the clauses */
      last_clause_count_9bits = current_clause_count_9bits;
      current_clause_count_9bits = 0;
      
      /* now, we randomly twiddle 1 bit in the variable array. */
      variable_marker_7bits = (int)random();
      toggle_variable_bit(variable_marker_7bits);

      /* here we iterate over the clauses (which are in external memory) */
      for(clause_marker_9bits = 0; clause_marker_9bits < num_clauses_9bits; clause_marker_9bits++)
	{
	  clause_offset = clause_marker_9bits * 3; /* start with the first variable */
	  clause_piece = clause_bytearray[clause_offset];
	  variable_num = (int)(clause_piece & 0x7F); /* mask off the inversion bit */
	  if (clause_piece & 0x80) /* the negation bit is set */
	    clause_part1_1bit = check_variable(variable_num, 1);
	  else
	    clause_part1_1bit = check_variable(variable_num, 0);
	  
	  /* now we're done with the first clause, we move to the next. */
	  clause_offset += 1;
	  clause_piece = clause_bytearray[clause_offset];
	  variable_num = (int)(clause_piece & 0x7F);
	  if (clause_piece & 0x80)
	    clause_part2_1bit = check_variable(variable_num, 1);
	  else
	    clause_part2_1bit = check_variable(variable_num, 0);
	      
	  /* and then on to the third clause */
	  clause_offset += 1;
	  clause_piece = clause_bytearray[clause_offset];
	  variable_num = (int)(clause_piece & 0x7F);
	  if (clause_piece & 0x80)
	    clause_part3_1bit = check_variable(variable_num, 1);
	  else
	    clause_part3_1bit = check_variable(variable_num, 0);

	  /* now we have all the clauses checked, we OR them together, and
	     optionally increment the current clause count if this clause
	     is satisfied. */
	  if(clause_part1_1bit || clause_part2_1bit || clause_part3_1bit)
	    current_clause_count_9bits++;
	}

      /* now, if this was a less than optimal change :), then we change
	 it back and reset the appropriate variables. */
      
      if (current_clause_count_9bits < last_clause_count_9bits)
	{
	  current_clause_count_9bits = last_clause_count_9bits;
	  toggle_variable_bit(variable_marker_7bits);
	}
    }

  /* now we do have to print out something in the way of results. */
  for(t = 0; t < 4; t++)
    printf("%d: %x\n", t, variable_bitarray[t]);
  
  return 0;
}

void
init_clause(void)
{
  char current[3], var;
  int index = 0;
  
  fgets (current, 3, stdin);
  do {
     if (*current != '\0') {
       var = current[0];
       var |= (0x80 * (current[1] == '\''));

       clause_bytearray[index] = var;

       ++index;
     }

    fgets (current, 3, stdin);
  }  while (feof (stdin) == 0 && index < 1536);
}



/* variable is the 7 bit (0-127) index of the 1 bit register to flip */
void
toggle_variable_bit(int variable)
{
  int big_index;
  int mask;

  big_index = (variable & 0x0060) >> 4; /* mask out all but bits 6 and 7,
					   then rotate them to least 
					   significant positions */
  mask = 1 << (variable & 0x001F); /* the rest of the bits choose which bit 
				      in that register */
  variable_bitarray[big_index] ^= mask; /* use C's XOR-in-place operator to 
					   do the flip */
}

/* this function selects a bit from the array, and returns it (allowing
   for an optional negation if specified.  See the comments in 
   toggle_variable_bit(int) above for a rundown on how this works. */

int
check_variable(int variable, int isneg)
{
  int big_index;
  int masking_index;
  int variable_value;

  big_index = (variable & 0x0060) >> 4;
  masking_index = (variable & 0x001F);
  variable_value = (variable_bitarray[big_index] >> masking_index) & 0x0001;
  
  if (isneg == 1)
    {
      if(variable_value == 0)
	return 1;
      else
	return 0;
    }
  else
    return variable_value;
}