src/sat/satDebug.c

Go to the documentation of this file.

#include "satInt.h"

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

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

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
static int numCompareInt(const void *x, const void *y);


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


void
sat_PrintNode(
        satManager_t *cm,
        long v)
{
int inverted, i, size;
long ante, cur, *fan, *plit;
satVariable_t *var;
satArray_t *wl;

  inverted = SATisInverted(v);
  v = SATnormalNode(v);
  if(SATflags(v) & IsCNFMask) {
    size = SATnumLits(v);
    fprintf(cm->stdOut, "CNF %6ld (%4ld) U(%ld)", v, SATnumConflict(v), SATconflictUsage(v));
    sat_PrintFlag(cm, v);
    fprintf(cm->stdOut, "    ");
    for(i=0, plit = (long*)SATfirstLit(v); i<size; i++, plit++) {
      if(i!=0 && i%5 == 0)
        fprintf(cm->stdOut, "\n    ");
      sat_PrintLiteral(cm, *plit);
    }
    fprintf(cm->stdOut, "\n");
  }
  else if(SATflags(v) & IsBDDMask) {
  }
  else {
    fprintf(cm->stdOut, "AIG ");
    sat_PrintFlag(cm, SATnormalNode(v));
    fprintf(cm->stdOut, "    ");
    sat_PrintNodeAlone(cm, v);
    sat_PrintNodeAlone(cm, SATleftChild(v));
    sat_PrintNodeAlone(cm, SATrightChild(v));
    fprintf(cm->stdOut, "\n");
    size = SATnFanout(v);
    fprintf(cm->stdOut, "%4d ", size);
    for(i=0, fan=SATfanout(v); i<size; i++, fan++) {
      cur = (*fan) >>1;
      fprintf(cm->stdOut, "%6ld ", cur);
    }
    fprintf(cm->stdOut, "\n");

    fprintf(cm->stdOut, "  canonocal : %ld\n", sat_GetCanonical(cm, v));
    if(cm->variableArray && SATvalue(v) < 2) {
      ante = SATante(v);
      if(SATflags(ante) & IsCNFMask) {
        fprintf(cm->stdOut, "  ante CNF  : %ld\n", SATante(v));
      }
      else{
        fprintf(cm->stdOut, "  ante      : %ld\n", SATante(v));
        fprintf(cm->stdOut, "  ante2     : %ld\n", SATante2(v));
      }
    }

    if(cm->variableArray) {
    var = SATgetVariable(v);
    wl = var->wl[0];
    if(wl && wl->num) {
      fprintf(cm->stdOut, "  0 wl : ");
      for(i=0; i<wl->num; i++) {
        plit = (long *)(wl->space[i]);
        if(plit == 0)   continue;
        fprintf(cm->stdOut, "%ld", (*plit)>>2);
        while(1) {
          plit++;
          if(*plit < 0) break;
        }
        fprintf(cm->stdOut, "(%ld) ", -(*plit));
      }
      fprintf(cm->stdOut, "\n");
    }
    wl = var->wl[1];
    if(wl && wl->num) {
      fprintf(cm->stdOut, "  1 wl : ");
      for(i=0; i<wl->num; i++) {
        plit = (long *)(wl->space[i]);
        if(plit == 0)   continue;
        fprintf(cm->stdOut, "%ld", (*plit)>>2);
        while(1) {
          plit++;
          if(*plit < 0) break;
        }
        fprintf(cm->stdOut, "(%ld) ", -(*plit));
      }
      fprintf(cm->stdOut, "\n");
    }
    }
  }
  fflush(cm->stdOut);
}

void
sat_PrintFlag(satManager_t *cm, long v)
{
int flag;

  flag = SATflags(SATnormalNode(v));
  fprintf(cm->stdOut, "%c%c%c%c%c%c%c%c%c%c%c%c%c%c\n",
          (flag & CoiMask)           ? 'C' : ' ',
          (flag & VisitedMask)       ? 'V' : ' ',
          (flag & NewMask)           ? 'N' : ' ',
          (flag & InQueueMask)       ? 'Q' : ' ',
          (flag & ObjMask)           ? 'o' : ' ',
          (flag & NonobjMask)        ? 'n' : ' ',
          (flag & IsSystemMask)      ? 'S' : ' ',
          (flag & IsConflictMask)    ? 'c' : ' ',
          (flag & InUseMask)         ? 'U' : ' ',
          (flag & StaticLearnMask)   ? 's' : ' ',
          (flag & StateBitMask)      ? 'T' : ' ',
          (flag & IsBlockingMask)    ? 'B' : ' ',
          (flag & IsFrontierMask)    ? 'F' : ' ',
          (flag & LeafNodeMask)      ? 'L' : ' ');

}

void
sat_PrintNodeAlone(satManager_t *cm, long v)
{
int value, level, inverted;

  inverted = SATisInverted(v);
  v = SATnormalNode(v);
  value = SATvalue(v);
  level = value>1 ? -1 : (cm->variableArray ? SATlevel(v) : -1);
  fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
          v, inverted ? '\'' : ' ', level,
          SATgetValueChar(value),
          (SATflags(v)&ObjMask) ? '*' : ' ');
}

void
sat_PrintLiteral(satManager_t *cm, long lit)
{
int value, level, inverted;
long v;

  v = SATgetNode(lit);
  inverted = SATisInverted(v);
  v = SATnormalNode(v);
  value = SATvalue(v);
  level = value>1 ? -1 : SATlevel(v);
  fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
          v, inverted ? '\'' : ' ', level, SATgetValueChar(value),
          SATisWL(lit) ? '*' : ' ');
}

void
sat_PrintImplicationGraph(
        satManager_t *cm,
        satLevel_t *d)
{
long ante, ante2, v;
int i;
satArray_t *implied;

  fprintf(cm->stdOut, "++++++++++++++++++++++++++++++++\n");
  fprintf(cm->stdOut, "* Level %d %ld->%ld\n",
                d->level, d->decisionNode, SATvalue(d->decisionNode));
  fprintf(cm->stdOut, "++++++++++++++++++++++++++++++++\n");

  implied = d->implied;
  for(i=0; i<implied->num; i++) {
    v = implied->space[i];
    ante = SATante(v);
    if(SATflags(ante) & IsCNFMask) {
      sat_PrintNodeAlone(cm, v);
      fprintf(cm->stdOut, "<= %6ld %c(%cCNF)\n",
              ante, (SATflags(ante) & ObjMask) ? '*' : ' ',
              (SATflags(ante) & IsConflictMask) ? 'c' : ' ');
      sat_PrintNode(cm, ante);
    }
    else if(SATflags(ante) & IsBDDMask) {
    }
    else {
      sat_PrintNodeAlone(cm, v);
      fprintf(cm->stdOut, "<= ");
      sat_PrintNodeAlone(cm, ante);
      ante2 = SATante2(v);
      if(ante2)
        sat_PrintNodeAlone(cm, ante2);
      fprintf(cm->stdOut, "\n");
    }
  }
  fflush(cm->stdOut);
}

void
sat_CheckFlagsOnConflict(satManager_t *cm)
{
long i;

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    if(!(SATflags(i) & CoiMask))
      continue;

    if(SATflags(i) & VisitedMask || SATflags(i) & NewMask) {
      fprintf(cm->stdOut, "%s ERROR : %ld has flag\n",
              cm->comment, i);
      sat_PrintNode(cm, i);
    }
  }
}

void
sat_PrintScore(satManager_t *cm)
{
int i;
long v;
satArray_t *ordered;
satVariable_t *var;

  fprintf(cm->stdOut, "------------Print Score-----------\n");
  ordered = cm->orderedVariableArray;
  for(i=0; i<ordered->num; i++) {
    v = ordered->space[i];
    var = SATgetVariable(v);
    fprintf(cm->stdOut, "%5ld : %3d %3d\n", v, var->scores[0], var->scores[1]);
  }
  fflush(cm->stdOut);
}


void
sat_PrintDotForConflict(
        satManager_t *cm,
        satLevel_t *d,
        long conflict,
        int includePreviousLevel)
{
satArray_t *root;
long left, right, nv;
int inverted, size, value, i;
long *plit;
satOption_t *option;

  root = sat_ArrayAlloc(8);

  conflict = d->conflict;
  inverted = SATisInverted(conflict);
  conflict = SATnormalNode(conflict);

  option = cm->option;
  if(SATflags(conflict) & IsCNFMask) {
    size = SATnumLits(conflict);
    for(i=0, plit=(long*)SATfirstLit(conflict); i<size; i++, plit++) {
      nv = SATgetNode(*plit);
      if(d->level == SATlevel(nv))
        sat_ArrayInsert(root, nv);
    }
  }
  else {
    value = SATvalue(conflict);
    if(value == 1) {
      if(d->level == SATlevel(conflict))
        sat_ArrayInsert(root, conflict);

      left = SATleftChild(conflict);
      inverted = SATisInverted(left);
      left = SATnormalNode(left);
      value = SATvalue(left) ^ inverted;
      if(value == 0) {
        if(d->level == SATlevel(left))
          sat_ArrayInsert(root, left);
      }
      else {
        right = SATrightChild(conflict);
        inverted = SATisInverted(right);
        right = SATnormalNode(right);
        value = SATvalue(right) ^ inverted;
        if(value == 0) {
          if(d->level == SATlevel(right))
            sat_ArrayInsert(root, right);
        }
      }
    }
    else if(value == 0) {
      left = SATleftChild(conflict);
      right = SATrightChild(conflict);
      if(d->level == SATlevel(conflict))
        sat_ArrayInsert(root, conflict);
      if(d->level == SATlevel(left))
        sat_ArrayInsert(root, left);
      if(d->level == SATlevel(right))
        sat_ArrayInsert(root, right);
    }
  }

  sat_PrintDotForImplicationGraph(cm, d, root, includePreviousLevel);
  sat_ArrayFree(root);
}

void
sat_PrintDotForWholeGraph(
        satManager_t *cm,
        satLevel_t *d,
        int includePreviousLevel)
{
satArray_t *root, *implied;
int v, i;

  root = sat_ArrayAlloc(8);
  implied = d->implied;
  for(i=implied->num-1; i>=0; i--) {
    v = implied->space[i];
    sat_ArrayInsert(root, v);
  }
  sat_PrintDotForImplicationGraph(cm, d, root, includePreviousLevel);
  sat_ArrayFree(root);
}
void
sat_PrintDotForImplicationGraph(
        satManager_t *cm,
        satLevel_t *d,
        satArray_t *root,
        int includePreviousLevel)
{
char name[1024];
long v, nv, *plit, lit;
int i, j, size;
int inverted;
long ante, ante2;
st_table *table;
FILE *fp;
satArray_t *implied;


  for(i=0; i<root->num; i++) {
    v = root->space[i];
    v  = SATnormalNode(v);
    SATflags(v) |= VisitedMask;
  }

  sprintf(name, "%d_%ld_%d_%d.dot",
          d->level, d->decisionNode, cm->each->nDecisions, includePreviousLevel);
  fp = fopen(name, "w");

  fprintf(fp, "digraph \"AndInv\" {\n  rotate=90;\n");
  fprintf(fp, "  margin=0.5;\n  label=\"AndInv\";\n");
  fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");

  table = st_init_table(st_numcmp, st_numhash);
  implied = d->implied;
  for(i=implied->num-1; i>=0; i--) {
    v = implied->space[i];
    if(!(SATflags(v) & VisitedMask)) continue;
    if((SATflags(v) & NewMask)) continue;

    st_insert(table, (char *)(long)v, (char *)(long)v);

    ante = SATante(v);
    if(SATflags(ante) & IsCNFMask) {
      size = SATnumLits(ante);
      for(j=0, plit=(long *)SATfirstLit(ante); j<size; j++) {
        lit = plit[j];
        nv = SATgetNode(lit);
        inverted = SATisInverted(nv);
        nv = SATnormalNode(nv);
        if(nv == v)     continue;

        st_insert(table, (char *)nv, (char *)nv);
        if(SATlevel(nv) == d->level) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n",
                  nv, SATlevel(nv), v, SATlevel(v));
          SATflags(nv) |= VisitedMask;
        }
        else if(includePreviousLevel) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n",
                  nv, SATlevel(nv), v, SATlevel(v));
        }
      }
    }
    else {
      fprintf(fp,"%ld.%d  [label=\"%ld.%d \"];\n", v, SATlevel(v), v, SATlevel(v));
      ante2 = SATnormalNode(SATante2(v));
      if(ante2) {
        st_insert(table, (char *)ante2, (char *)ante2);
        if(SATlevel(ante2) == d->level) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n", ante2, SATlevel(ante2), v, SATlevel(v));
          SATflags(ante2) |= VisitedMask;
        }
        else if(includePreviousLevel && SATlevel(ante2)>=0) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n", ante2, SATlevel(ante2), v, SATlevel(v));
        }
      }

      if(ante) {
        st_insert(table, (char *)ante, (char *)ante);
        if(SATlevel(ante) == d->level) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n", ante, SATlevel(ante), v, SATlevel(v));
          SATflags(ante) |= VisitedMask;
        }
        else if(includePreviousLevel && SATlevel(ante)>=0) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n", ante, SATlevel(ante), v, SATlevel(v));
        }
      }
    }
    SATflags(v) |= NewMask;
  }
  fprintf(fp, "}\n");
  fclose(fp);

  for(i=implied->num-1; i>=0; i--) {
    v = implied->space[i];
    SATflags(v) &= ResetNewVisitedMask;
  }
  for(i=0; i<root->num; i++) {
    v = root->space[i];
    SATflags(v) &= ResetVisitedMask;
  }

  st_free_table(table);

}

void
sat_CheckNonobjConflictClause(
        satManager_t *cm,
        long v)
{
int i, size, inverted;
long *plit, nv;
satLevel_t *d;

  d = 0;
  size = SATnumLits(v);
  for(i=0, plit = (long*)SATfirstLit(v); i<size; i++, plit++) {
    nv = SATgetNode(*plit);
    inverted = SATisInverted(nv);
    nv = SATnormalNode(nv);

    d = sat_AllocLevel(cm);
    d->decisionNode = nv;

    SATvalue(nv) = inverted;
    SATmakeImplied(nv, d);

    sat_Enqueue(cm->queue, nv);
    SATflags(nv) |= InQueueMask;

    sat_ImplicationMain(cm, d);
    if(d->conflict)     break;
  }

  if(d->conflict == 0) {
    fprintf(cm->stdOut, "%s ERROR : %ld does not result in conflict\n",
            cm->comment, v);
    sat_PrintNode(cm, v);
  }
  sat_Backtrack(cm, -1);
}

void
sat_CheckNonobjUnitClause(
        satManager_t *cm)
{
int v, i;
int inverted;
satLevel_t *d;
satArray_t *arr;

  arr = cm->nonobjUnitLitArray;

  for(i=0; i<arr->num; i++) {
    v = arr->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

    d = sat_AllocLevel(cm);
    d->decisionNode = v;

    SATvalue(v) = inverted;
    SATmakeImplied(v, d);

    sat_Enqueue(cm->queue, v);
    SATflags(v) |= InQueueMask;

    sat_ImplicationMain(cm, d);
    if(d->conflict == 0) {
      fprintf(cm->stdOut, "%s ERROR : %d unit literal does not result in conflict\n",
            cm->comment, v);
    }
    sat_Backtrack(cm, -1);

  }
}

void
sat_CheckInitialCondition(
        satManager_t *cm)
{
long i;

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    if(!(SATflags(i) & CoiMask))
      continue;

    if(SATvalue(i) != 2) {
      fprintf(cm->stdOut, "%s ERROR : %ld has value %ld\n",
              cm->comment, i, SATvalue(i));
    }
    if(SATflags(i) & VisitedMask || SATflags(i) & NewMask) {
      fprintf(cm->stdOut, "%s ERROR : %ld has flag\n",
              cm->comment, i);
      sat_PrintNode(cm, i);
    }
  }
}

void
sat_CheckConflictClause(
        satManager_t *cm,
        satArray_t *clauseArray)
{
satArray_t *decisionArray;
satLevel_t *d;
int i, value, inverted;
long v;
int conflictFlag, tvalue;

  decisionArray = sat_ArrayAlloc(cm->currentDecision);
  for(i=1; i<=cm->currentDecision; i++) {
    v = cm->decisionHead[i].decisionNode;
    value = SATvalue(v);
    sat_ArrayInsert(decisionArray, v^(!value));
  }

  sat_Backtrack(cm, 0);

  conflictFlag = 0;
  for(i=0; i<clauseArray->num; i++) {
    v = clauseArray->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

    d = sat_AllocLevel(cm);
    d->decisionNode = v;

    value = !inverted;
    tvalue = SATvalue(v);
    if(tvalue < 2 && tvalue !=  value) {
      fprintf(cm->stdOut, "ERROR : Early conflict condition detect\n");
      break;
    }
    SATvalue(v) = value;
    SATmakeImplied(v, d);

    sat_Enqueue(cm->queue, v);
    SATflags(v) |= InQueueMask;

    sat_ImplicationMain(cm, d);

    if(d->conflict) {
      conflictFlag = 1;
      break;
    }
  }

  if(conflictFlag == 0) {
    fprintf(cm->stdOut, "ERROR : Wrong conflict clause\n");
    sat_PrintClauseArray(cm, clauseArray);
  }

  sat_Backtrack(cm, 0);

  conflictFlag = 0;
  for(i=0; i<decisionArray->num; i++) {
    v = decisionArray->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

    d = sat_AllocLevel(cm);
    d->decisionNode = v;

    value = !inverted;
    SATvalue(v) = value;
    SATmakeImplied(v, d);

    sat_Enqueue(cm->queue, v);
    SATflags(v) |= InQueueMask;

    sat_ImplicationMain(cm, d);
    if(d->conflict) {
      conflictFlag = 1;
    }
  }
  if(conflictFlag == 0) {
    fprintf(cm->stdOut, "ERROR : Can't produce conflict\n");
    exit(0);
  }
}

void
sat_PrintClauseArray(
        satManager_t *cm,
        satArray_t *clauseArray)
{
int i, inverted;
long v;

  fprintf(cm->stdOut, "    ");
  for(i=0; i<clauseArray->num; i++) {
    v = clauseArray->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    if(i!=0 && i%5 == 0)
      fprintf(cm->stdOut, "\n    ");
    sat_PrintNodeAlone(cm, v);
  }
  fprintf(cm->stdOut, "\n");
  fflush(cm->stdOut);
}

void
sat_PrintProfileForNumConflict(satManager_t *cm)
{
char filename[1024];
FILE *fout;
int i, index;
satArray_t *arr;
long count;
long total, part;
long v;
long maxValue;


  sprintf(filename, "nConflict.dat");
  fout = fopen(filename, "w");
  index = 1;
  maxValue = 0;
  arr = sat_ArrayAlloc(1024);
  for(v=satNodeSize; v<cm->nodesArraySize; v+=satNodeSize) {
    if(!(SATflags(v) & IsCNFMask))      continue;
    if(SATnumConflict(v) == 0)  continue;
    if(SATnumConflict(v) > maxValue)
      maxValue = SATnumConflict(v);
    sat_ArrayInsert(arr, SATnumConflict(v));
  }

  qsort(arr->space, arr->num, sizeof(int), numCompareInt);
  total = 0;
  part = 0;
  for(i=0; i<arr->num; i++) {
    count = arr->space[i];
    if(count == 0)      continue;
    total += count;
    if(count > 1) {
      part += count;
    }
    fprintf(fout, "%d %ld\n", i, count);
  }
  index = i;
  sat_ArrayFree(arr);
  fclose(fout);


  sprintf(filename, "nConflict.gp");
  fout = fopen(filename, "w");
  fprintf(fout, "set xlabel \"Conflict Index\"\n");
  fprintf(fout, "set ylabel \"Number of Conflicting %ld/%ld\"\n", part, total);
  fprintf(fout, "set nokey\n");
  fprintf(fout, "set size square 0.8,1\n");
  fprintf(fout, "set xrange [0:%d]\n", index+1);
  fprintf(fout, "set yrange [0:%ld]\n", maxValue+1);
  fprintf(fout, "set grid\n");
  fprintf(fout, "set border 3 linewidth 0.5\n");
  fprintf(fout, "set xtics nomirror\n");
  fprintf(fout, "set ytics nomirror\n");
  fprintf(fout, "set mxtics 2\n");
  fprintf(fout, "set mytics 2\n");
  fprintf(fout, "set pointsize 2\n");
  fprintf(fout, "set terminal postscript eps enhanced color solid \"Times-Roman\" 24\n");
  fprintf(fout, "set output \"nConflict.eps\"\n");
  fprintf(fout, "plot \"nConflict.dat\" using 1:2 with line linetype 3\n");
  fclose(fout);
}

static int
numCompareInt(const void *x, const void *y)
{
long n1, n2;

  n1 = *(int *)x;
  n2 = *(int *)y;
  return(n1 > n2);
}