/**CFile***********************************************************************

  FileName    [satInterface.c]

  PackageName [sat]

  Synopsis    [Routines for various decision heuristics.]

  Author      [HoonSang Jin]

  Copyright [ This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]


******************************************************************************/

#include "satInt.h"

static char rcsid[] UNUSED = "$Id: satInterface.c,v 1.20 2009/04/11 18:26:37 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************

  Synopsis    [Set option for unsat core generation]

  Description [Set option for unsat core generation]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void sat_SetOptionForUP(satManager_t * cm)
{
  cm->option->includeLevelZeroLiteral = 1;
  cm->option->minimizeConflictClause = 0;
  cm->option->clauseDeletionHeuristic = 0;
  cm->dependenceTable = st_init_table(st_ptrcmp, st_ptrhash);
  cm->anteTable = st_init_table(st_numcmp, st_numhash);
  cm->fp = fopen(cm->option->unsatCoreFileName, "w");
}

/**Function********************************************************************

  Synopsis    [Read CNF]

  Description [Read CNF]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_ReadCNF(satManager_t *cm, char *filename)
{
FILE *fin;
satArray_t *clauseArray;
char line[16384], word[1024], *lp;
int nVar, nCl, nArg;
int i, id, sign;
long v;
int begin;
 long cls_idx;

  if(!(fin = fopen(filename, "r"))) {
    fprintf(cm->stdOut, "%s ERROR : Can't open CNF file %s\n",
	    cm->comment, filename);
    return(0);
  }

  //Bing: for unsat core
  if(cm->option->coreGeneration)
    sat_SetOptionForUP(cm);

  begin = 0;
  clauseArray = sat_ArrayAlloc(1024);
  while(fgets(line, 16384, fin)) {
    lp = sat_RemoveSpace(line);
    if(lp[0] == '\n')	continue;
    if(lp[0] == '#')	continue;
    if(lp[0] == 'c')	continue;
    if(lp[0] == 'p') {
      nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl);
      if(nArg < 2) {
	fprintf(cm->stdErr, "ERROR : Unable to read the number of variables and clauses from CNF file %s\n", filename);
	fclose(fin);
	sat_ArrayFree(clauseArray);
	return(0);
      }
      begin = 1;

      for(i=1; i<=nVar; i++) {
	v = sat_CreateNode(cm, 2, 2);
	SATflags(v) |= CoiMask;
	SATvalue(v) = 2;
      }

      cm->initNumVariables = nVar;
      cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
      memset(cm->variableArray, 0, sizeof(satVariable_t) * (cm->initNumVariables+1));
      continue;
    }
    else if(begin == 0)	continue;

    clauseArray->num = 0;
    while(1) {
      lp = sat_RemoveSpace(lp);
      lp = sat_CopyWord(lp, word);

      if(strlen(word)) {
	id = atoi(word);
	sign = 1;

	if(id != 0) {
	  if(id < 0) {
	    id = -id;
	    sign = 0;
	  }
	  sat_ArrayInsert(clauseArray, (id*satNodeSize + sign));
	}
	else {
	  if(clauseArray->num == 1) {
	    v = clauseArray->space[0];
	    sat_ArrayInsert(cm->unitLits, SATnot(v));
	    cm->initNumClauses++;
	    cm->initNumLiterals += clauseArray->num;
	    //Bing: for unsat core
	    if(cm->option->coreGeneration){
	      cls_idx = sat_AddUnitClause(cm, clauseArray);
	      if(cm->option->coreGeneration){
		v = SATnormalNode(v);
		st_insert(cm->anteTable,(char *)v,(char *)cls_idx);
	      }
	    }
	  }
	  else {
	    sat_AddClause(cm, clauseArray);
	    cm->initNumClauses++;
	    cm->initNumLiterals += clauseArray->num;
	  }
	  break;
	}
      }
    }
  }
  if(cm->initNumClauses == 0) {
    fprintf(cm->stdOut, "%s ERROR : CNF is not valid\n", cm->comment);
    return(0);
  }

  if(cm->initNumClauses != nCl) {
    fprintf(cm->stdOut, "%s WARNING : wrong number of clauses\n", cm->comment);
  }

  fclose(fin);
  sat_ArrayFree(clauseArray);

  return(1);
}

/**Function********************************************************************

  Synopsis    [Read CNF from Array]

  Description [Read CNF from Array]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_ReadCNFFromArray(
	satManager_t *cm,
	satArray_t *cnfArray,
	st_table *mappedTable)
{
satArray_t *clauseArray;
int nVar, nCl;
int i;
long tv, v, c, *space;

  if(cnfArray == 0) {
    fprintf(cm->stdOut, "%s ERROR : Can't find CNF array \n", cm->comment);
    return(0);
  }

  nVar = 0;
  nCl = 0;
  for(i=1; i<cnfArray->num; i++) {
    v = cnfArray->space[i];
    if(v <= 0)	nCl++;
    else {
      v = SATnormalNode(v);
      if(v > nVar)	nVar = v;
    }
  }
  nVar = nVar / satNodeSize;
  for(i=1; i<=nVar; i++) {
    v = sat_CreateNode(cm, 2, 2);
    SATflags(v) |= CoiMask;
    SATvalue(v) = 2;
  }

  cm->initNumVariables = nVar;
  cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
  memset(cm->variableArray, 0, sizeof(satVariable_t) * (cm->initNumVariables+1));

  clauseArray = sat_ArrayAlloc(1024);
  for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){
    if(*space <= 0) {
      space++;
      i++;
      if(i>=cnfArray->num)
	break;
      clauseArray->num = 0;
      while(*space > 0) {
	v = (*space);
	sat_ArrayInsert(clauseArray, SATnot(v));
	i++;
	space++;
      }

      /**
       * If clause is blocking clause then it has clause index in it.
       **/
      tv = *space;

      if(clauseArray->num > 1)
	c = sat_AddClause(cm, clauseArray);
      else {
	c = sat_AddUnitClause(cm, clauseArray);
	if(cm->option->coreGeneration) {
	  st_insert(cm->anteTable,(char *)(long)(SATnormalNode(v)),(char *)(long)c);
	}
      }
      if(clauseArray->num == 1)
	sat_ArrayInsert(cm->unitLits, (v));

      if(tv < -1) { /* this is blocking clause */
	st_insert(mappedTable, (char *)c, (char *)(-tv));
      }

      cm->initNumClauses++;
      cm->initNumLiterals += clauseArray->num;
      i--;
      space--;
    }
  }
  sat_ArrayFree(clauseArray);


  return(1);
}

/**Function********************************************************************

  Synopsis    [Write CNF from Array]

  Description [Write CNF from Array]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_WriteCNFFromArray(satArray_t *cnfArray, char *filename)
{
FILE *fin;
int nVar, nCl;
int i ;
long v, *space;

  if(cnfArray == 0) {
    fprintf(stdout, "ERROR : Can't find CNF array \n");
    return(0);
  }

  if(!(fin=fopen(filename, "w"))) {
    fprintf(stdout, "ERROR : Can't find file %s\n", filename);
    return(0);
  }

  nVar = 0;
  nCl = 0;
  for(i=1; i<cnfArray->num; i++) {
    v = cnfArray->space[i];
    if(v <= 0)	nCl++;
    else {
      v = SATnormalNode(v);
      if(v > nVar)	nVar = v;
    }
  }
  nVar = nVar / satNodeSize;

  fprintf(fin, "p cnf %d %d\n", nVar, nCl);

  for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){
    if(*space <= 0) {
      space++;
      i++;
      if(i>=cnfArray->num)
	break;

      while(*space > 0) {
	v = (*space);
	if(SATisInverted(v))	v = -(SATnodeID(v));
	else			v = SATnodeID(v);
	fprintf(fin, "%ld ", v);
	i++;
	space++;
      }
      fprintf(fin, "0\n");

      i--;
      space--;
    }
  }
  fclose(fin);

  return(1);
}
/**Function********************************************************************

  Synopsis    [Copy word from lp to word]

  Description [Copy word from lp to word and lp moved to next word.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
char *
sat_CopyWord(char *lp, char *word)
{
char *wp;

  for(wp = word; ; lp++, wp++) {
    if((*lp == ' ') || (*lp == '\t') || (*lp == '\n'))	break;
    *wp = *lp;
  }
  *wp = '\0';
  return(lp);
}

/**Function********************************************************************

  Synopsis    [skip space and return the beginning of word ]

  Description [skip space and return the beginning of word ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
char *
sat_RemoveSpace(char *line)
{
int i;

  for(i=0; ; i++) {
    if(line[i] == ' ')		continue;
    else if(line[i] == '\t')	continue;
    return(&(line[i]));
  }
}


/**Function********************************************************************

  Synopsis    [Write CNF file under partial assignment]

  Description [Write CNF file under partial assignment.
		If a literal in a clause is satisfied then the clause is
		ignored. If a literal in a clause is unsatisfied then the
		literal is ignored.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_WriteCNFWithPartialAssignment(satManager_t *cm, char *filename)
{
int nVars, nCls, j;
int size, satisfied;
int inverted, value;
long *plit, v, tv, tsize, i;
FILE *fout;

  nVars = 0;
  nCls = 0;
  tsize = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
  for(i=satNodeSize; i<tsize; i+=satNodeSize) {
    if(SATleftChild(i) == 2 && SATrightChild(i) == 2)	continue;
    if(!(SATflags(i) & IsCNFMask))	{
      if(!(SATflags(i) & CoiMask))	continue;
      fprintf(cm->stdOut, "Warning : current implementation can't take care of AIG node\n");
      continue;
    }
    if(SATreadInUse(i) == 0)	continue;

    size = SATnumLits(i);
    satisfied = 0;
    plit = (long *)SATfirstLit(i);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      inverted = SATisInverted(v);
      v = SATnormalNode(v);
      value = SATvalue(v) ^ inverted;
      if(value == 1) {
	satisfied = 1;
	break;
      }
      if(v > nVars)	nVars = v;
    }
    if(satisfied)	continue;

    nCls++;
  }
  nVars /= satNodeSize;

  if(!(fout = fopen(filename, "w"))) {
    fprintf(cm->stdOut, "%s ERROR : Can't open file %s\n",
	    cm->comment, filename);
    exit(0);
  }

  fprintf(fout, "p cnf %d %d\n", nVars, nCls);
  tsize = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
  for(i=satNodeSize; i<tsize; i+=satNodeSize) {
    if(SATleftChild(i) == 2 && SATrightChild(i) == 2)	continue;
    if(!(SATflags(i) & IsCNFMask))	{
      if(!(SATflags(i) & CoiMask))	continue;
      continue;
    }
    if(SATreadInUse(i) == 0)	continue;

    satisfied = 0;
    size = SATnumLits(i);
    plit = (long *)SATfirstLit(i);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      inverted = SATisInverted(v);
      v = SATnormalNode(v);
      value = SATvalue(v) ^ inverted;
      if(value == 1) {
	satisfied = 1;
	break;
      }
    }
    if(satisfied)	continue;

    plit = (long *)SATfirstLit(i);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      inverted = SATisInverted(v);
      v = SATnormalNode(v);
      value = SATvalue(v) ^ inverted;
      if(value < 2) {
	continue;
      }
      tv = SATnodeID(v);
      fprintf(fout, "%ld ", inverted ? -tv : tv);
    }
    fprintf(fout, "0\n");
  }
  fclose(fout);
}
/**Function********************************************************************

  Synopsis    [ Write CNF ]

  Description [ Write CNF ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_WriteCNF(satManager_t *cm, char *filename)
{
FILE *fout;
long i, tv, *plit, size, j;
int csize, inverted;
int nVar, nCl;
long left, right;

  if(!(fout = fopen(filename, "w"))) {
    fprintf(cm->stdOut, "%s ERROR : Can't open file %s\n",
	    cm->comment, filename);
    exit(0);
  }

  nVar = cm->initNumVariables;
  nCl = 0;
  size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
  for(i=satNodeSize; i<size; i+=satNodeSize) {
    if(SATleftChild(i) == 2 && SATrightChild(i) == 2)	continue;
    if(SATflags(i) & IsCNFMask) {
      if(SATreadInUse(i) == 0)	continue;
      nCl++;
      continue;
    }
    if(!(SATflags(i) & CoiMask))	continue;
    nCl += 3;
  }
  sat_CountUnitLiteralClauses(cm, cm->assertion, &nCl);
  sat_CountUnitLiteralClauses(cm, cm->unitLits, &nCl);
  sat_CountUnitLiteralClauses(cm, cm->auxObj, &nCl);
  sat_CountUnitLiteralClauses(cm, cm->obj, &nCl);

  fprintf(fout, "p cnf %d %d\n", nVar, nCl);

  sat_PrintUnitLiteralClauses(cm, cm->assertion, fout);
  sat_PrintUnitLiteralClauses(cm, cm->unitLits, fout);
  sat_PrintUnitLiteralClauses(cm, cm->auxObj, fout);
  sat_PrintUnitLiteralClauses(cm, cm->obj, fout);

  size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
  for(i=satNodeSize; i<size; i+=satNodeSize) {
    if(SATleftChild(i) == 2 && SATrightChild(i) == 2)	continue;
    if(SATflags(i) & IsCNFMask) {
      csize = SATnumLits(i);
      plit = (long*)SATfirstLit(i);
      for(j=0; j<csize; j++, plit++) {
	 tv = SATgetNode(*plit);
	 inverted = SATisInverted(tv);
	 tv = SATnormalNode(tv);
	 tv = SATnodeID(tv);
	 fprintf(fout, "%ld ", inverted ? -tv : tv);
      }
      fprintf(fout, "0\n");
      continue;
    }
    if(!(SATflags(i) & CoiMask))	continue;


    left = SATleftChild(i);
    inverted = SATisInverted(left);
    left = SATnormalNode(left);
    left = SATnodeID(left);
    left = inverted ? -left : left;

    right = SATrightChild(i);
    inverted = SATisInverted(right);
    right = SATnormalNode(right);
    right = SATnodeID(right);
    right = inverted ? -right : right;

    j = SATnodeID(i);

    fprintf(fout, "%ld %ld %ld 0\n", -left, -right, j);
    fprintf(fout, "%ld %ld 0\n", left, -j);
    fprintf(fout, "%ld %ld 0\n", right, -j);
  }

  fclose(fout);
}

/**Function********************************************************************

  Synopsis    [ Write CNF ]

  Description [ Write CNF ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_WriteCNFWithPointer(satManager_t *cm, FILE *fout)
{
long i, j, size, tv, *plit;
int csize, inverted;
int nVar, nCl;
long left, right;

  nVar = cm->initNumVariables;
  nCl = 0;
  size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
  for(i=satNodeSize; i<size; i+=satNodeSize) {
    if(SATleftChild(i) == 2 && SATrightChild(i) == 2)	continue;
    if(SATflags(i) & IsCNFMask) {
      if(SATreadInUse(i) == 0)	continue;
      nCl++;
      continue;
    }
    if(!(SATflags(i) & CoiMask))	continue;
    nCl += 3;
  }
  sat_CountUnitLiteralClauses(cm, cm->assertion, &nCl);
  sat_CountUnitLiteralClauses(cm, cm->unitLits, &nCl);
  sat_CountUnitLiteralClauses(cm, cm->auxObj, &nCl);
  sat_CountUnitLiteralClauses(cm, cm->obj, &nCl);

  fprintf(fout, "p cnf %d %d\n", nVar, nCl);

  sat_PrintUnitLiteralClauses(cm, cm->assertion, fout);
  sat_PrintUnitLiteralClauses(cm, cm->unitLits, fout);
  sat_PrintUnitLiteralClauses(cm, cm->auxObj, fout);
  sat_PrintUnitLiteralClauses(cm, cm->obj, fout);

  size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
  for(i=satNodeSize; i<size; i+=satNodeSize) {
    if(SATleftChild(i) == 2 && SATrightChild(i) == 2)	continue;
    if(SATflags(i) & IsCNFMask) {
      csize = SATnumLits(i);
      plit = (long*)SATfirstLit(i);
      for(j=0; j<csize; j++, plit++) {
	 tv = SATgetNode(*plit);
	 inverted = SATisInverted(tv);
	 tv = SATnormalNode(tv);
	 tv = SATnodeID(tv);
	 fprintf(fout, "%ld ", inverted ? -tv : tv);
      }
      fprintf(fout, "0\n");
      continue;
    }
    if(!(SATflags(i) & CoiMask))	continue;


    left = SATleftChild(i);
    inverted = SATisInverted(left);
    left = SATnormalNode(left);
    left = SATnodeID(left);
    left = inverted ? -left : left;

    right = SATrightChild(i);
    inverted = SATisInverted(right);
    right = SATnormalNode(right);
    right = SATnodeID(right);
    right = inverted ? -right : right;

    j = SATnodeID(i);

    fprintf(fout, "%ld %ld %ld 0\n", -left, -right, j);
    fprintf(fout, "%ld %ld 0\n", left, -j);
    fprintf(fout, "%ld %ld 0\n", right, -j);
  }

}
/**Function********************************************************************

  Synopsis    [ Count the number of unit literal clauses ]

  Description [ Count the number of unit literal clauses ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CountUnitLiteralClauses(
	satManager_t *cm,
	satArray_t *arr,
	int *nCl)
{
int i, count;
long v;

  if(arr == 0)	return;
  count = 0;
  for(i=0; i<arr->num; i++) {
    v = arr->space[i];
    if(v == 1)	count++;
  }

  *nCl += arr->num - count;
}

/**Function********************************************************************

  Synopsis    [ Print unit literal clauses ]

  Description [ Print unit literal clauses ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintUnitLiteralClauses(
	satManager_t *cm,
	satArray_t *arr,
	FILE *fout)
{
int i, inverted;
long v;

  if(arr == 0)	return;
  for(i=0; i<arr->num; i++) {
    v = arr->space[i];
    if(v == 1)	continue;
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    v = SATnodeID(v);
    fprintf(fout, "%ld 0\n", inverted ? -v : v);
  }
}