source: vis_dev/vis-2.3/src/sat/satInterface.c @ 99

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