src/sat/satImplication.c

Go to the documentation of this file.

#include "satInt.h"
#include "baig.h"

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

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

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


typedef int (*IMPLY_FN)
    (satManager_t *cm, satLevel_t *d, long v, long left, long right);


IMPLY_FN satImplicationFN[64]= {
  sat_ImplyStop,                 /* 0    */
  sat_ImplyConflict,             /* 1  */
  sat_ImplyLeftForward,          /* 2  */
  sat_ImplyLeftForward,          /* 3  */
  sat_ImplyStop,                 /* 4  */
  sat_ImplyConflict,             /* 5  */
  sat_ImplyLeftForward,          /* 6  */
  sat_ImplyLeftForward,          /* 7  */
  sat_ImplySplit,                /* 8  */
  sat_ImplyConflict,             /* 9  */
  sat_ImplyLeftForward,          /* 10  */
  sat_ImplyLeftForward,          /* 11  */
  sat_ImplySplit,                /* 12  */
  sat_ImplyConflict,             /* 13  */
  sat_ImplyLeftForward,          /* 14  */
  sat_ImplyLeftForward,          /* 15  */
  sat_ImplyStop,                 /* 16  */
  sat_ImplyConflict,             /* 17  */
  sat_ImplyRightForward,         /* 18  */
  sat_ImplyRightForward,         /* 19  */
  sat_ImplyConflict,             /* 20  */
  sat_ImplyStop,                 /* 21  */
  sat_ImplyForwardOne,           /* 22  */
  sat_ImplyForwardOne,           /* 23  */
  sat_ImplyPropRight,            /* 24  */
  sat_ImplyPropRightOne,         /* 25  */
  sat_ImplyStop,                 /* 26  */
  sat_ImplyStop,                 /* 27  */
  sat_ImplyPropRight,            /* 28  */
  sat_ImplyPropRightOne,         /* 29  */
  sat_ImplyStop,                 /* 30  */
  sat_ImplyStop,                 /* 31  */
  sat_ImplySplit,                /* 32  */
  sat_ImplyConflict,             /* 33  */
  sat_ImplyRightForward,         /* 34  */
  sat_ImplyRightForward,         /* 35  */
  sat_ImplyPropLeft,             /* 36  */
  sat_ImplyPropLeftOne,          /* 37  */
  sat_ImplyStop,                 /* 38  */
  sat_ImplyStop,                 /* 39  */
  sat_ImplySplit,                /* 40  */
  sat_ImplyPropLeftRight,        /* 41  */
  sat_ImplyStop,                 /* 42  */
  sat_ImplyStop,                 /* 43  */
  sat_ImplySplit,                /* 44  */
  sat_ImplyPropLeftRight,        /* 45  */
  sat_ImplyStop,                 /* 46  */
  sat_ImplyStop,                 /* 47  */
  sat_ImplySplit,                /* 48  */
  sat_ImplyConflict,             /* 49  */
  sat_ImplyRightForward,         /* 50  */
  sat_ImplyRightForward,         /* 51  */
  sat_ImplyPropLeft,             /* 52  */
  sat_ImplyPropLeftOne,          /* 53  */
  sat_ImplyStop,                 /* 54  */
  sat_ImplyStop,                 /* 55  */
  sat_ImplySplit,                /* 56  */
  sat_ImplyPropLeftRight,        /* 57  */
  sat_ImplyStop,                 /* 58  */
  sat_ImplyStop,                 /* 59  */
  sat_ImplySplit,                /* 60  */
  sat_ImplyPropLeftRight,        /* 61  */
  sat_ImplyStop,                 /* 62  */
  sat_ImplyStop,                 /* 63  */
};



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


int
sat_ImplyStop(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  return(0);
}

int
sat_ImplySplit(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  return(0);
}

int
sat_ImplyConflict(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  if(left != 2)  {
    d->conflict = SATnormalNode(v);
  }
  return(0);
}


int
sat_ImplyLeftForward(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{

  v = SATnormalNode(v);
  left = SATnormalNode(left);

  SATvalue(v) = 0;
  SATmakeImplied(v, d);
  SATante(v) = left;

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

  SATflags(v) |= (SATflags(left) & ObjMask);

  cm->each->nAigImplications++;
  return(0);
}

int
sat_ImplyRightForward(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  v = SATnormalNode(v);
  right = SATnormalNode(right);

  SATvalue(v) = 0;
  SATmakeImplied(v, d);
  SATante(v) = right;

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

  SATflags(v) |= (SATflags(right) & ObjMask);
  cm->each->nAigImplications++;

  return(0);
}


int
sat_ImplyForwardOne(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  v = SATnormalNode(v);
  left = SATnormalNode(left);
  right = SATnormalNode(right);

  SATvalue(v) = 1;
  SATmakeImplied(v, d);
  SATante(v) = right;
  SATante2(v) = left;

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

  SATflags(v) |= (SATflags(right) & ObjMask);
  SATflags(v) |= (SATflags(left) & ObjMask);
  cm->each->nAigImplications++;

  return(0);
}

int
sat_ImplyPropRight(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  int isInverted;

  isInverted = SATisInverted(right);
  v = SATnormalNode(v);
  left = SATnormalNode(left);
  right = SATnormalNode(right);

  SATmakeImplied(right, d);
  SATvalue(right) = isInverted;

  SATante(right) = left;
  SATante2(right) = v;

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

  SATflags(right) |= (SATflags(left) & ObjMask);
  SATflags(right) |= (SATflags(v) & ObjMask);
  cm->each->nAigImplications++;
  return(0);
}

int
sat_ImplyPropRightOne(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  int isInverted;

  isInverted = SATisInverted(right);
  v = SATnormalNode(v);
  left = SATnormalNode(left);
  right = SATnormalNode(right);

  SATmakeImplied(right, d);

  SATante(right) = v;

  SATvalue(right) = !isInverted;

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

  SATflags(right) |= (SATflags(v) & ObjMask);
  cm->each->nAigImplications++;
  return(0);
}


int
sat_ImplyPropLeft(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  int isInverted;

  isInverted = SATisInverted(left);
  v = SATnormalNode(v);
  left = SATnormalNode(left);
  right = SATnormalNode(right);

  SATmakeImplied(left, d);

  SATante(left) = v;
  SATante2(left) = right;

  SATvalue(left) = isInverted;

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

  SATflags(left) |= (SATflags(v) & ObjMask);
  SATflags(left) |= (SATflags(right) & ObjMask);
  cm->each->nAigImplications++;
  return(0);
}



int
sat_ImplyPropLeftOne(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  int isInverted;

  isInverted = SATisInverted(left);
  v = SATnormalNode(v);
  left = SATnormalNode(left);
  right = SATnormalNode(right);

  SATmakeImplied(left, d);

  SATante(left) = v;

  SATvalue(left) = !isInverted;

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

  SATflags(left) |= (SATflags(v) & ObjMask);
  cm->each->nAigImplications++;
  return(0);
}



int
sat_ImplyPropLeftRight(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  int isLeftInverted;
  int isRightInverted;

  if(left == right)     return 1;

  isLeftInverted = SATisInverted(left);
  isRightInverted = SATisInverted(right);

  v = SATnormalNode(v);
  left = SATnormalNode(left);
  right = SATnormalNode(right);

  SATmakeImplied(left, d);
  SATmakeImplied(right, d);

  SATante(left) = v;
  SATante(right) = v;

  SATvalue(left) = !isLeftInverted;
  SATvalue(right) = !isRightInverted;

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

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

  SATflags(left) |= (SATflags(v) & ObjMask);
  SATflags(right) |= (SATflags(v) & ObjMask);
  cm->each->nAigImplications += 2;
  return(0);
}


void
sat_ImplyCNF(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        satArray_t *wl)
{
int size, i, j;
long *space;
long lit, *plit, *tplit;
int dir;
long nv, tv, *oplit, *wlit;
int isInverted, value;
int tsize, inverted;
long cur, clit;
satStatistics_t *stats;
satOption_t *option;
satQueue_t *Q;
satVariable_t *var;

  size = wl->num;
  space = wl->space;
  Q = cm->queue;
  stats = cm->each;
  option = cm->option;
  nv = 0;
  wlit = 0;

  for(i=0; i<size; i++) {
    plit = (long*)space[i];

    if(plit == 0 || *plit == 0) {
      size--;
      space[i] = space[size];
      i--;
      continue;
    }

    lit = *plit;
    dir = SATgetDir(lit);
    oplit = plit;

    while(1) {
      oplit += dir;
      if(*oplit <=0) {
        if(dir == 1) nv =- (*oplit);
        if(dir == SATgetDir(lit)) {
          oplit = plit;
          dir = -dir;
          continue;
        }

        tv = SATgetNode(*wlit);
        isInverted = SATisInverted(tv);
        tv = SATnormalNode(tv);
        value = SATvalue(tv) ^ isInverted;
        if(value == 0) {  
          d->conflict = nv;
          wl->num = size;
          return;
        }
        else if(value > 1) { 
          SATvalue(tv) = !isInverted;
          SATmakeImplied(tv, d);
          SATante(tv) = nv;

          if((SATflags(tv) & InQueueMask) == 0) {
            sat_Enqueue(Q, tv);
            SATflags(tv) |= InQueueMask;
          }

          stats->nCNFImplications++;

          if(option->incTraceObjective == 1) {
            tsize = SATnumLits(nv);
            for(j=0, tplit=(long*)SATfirstLit(nv); j<tsize; j++, tplit++) {
              cur = SATgetNode(*tplit);
              cur = SATnormalNode(cur);
              if(SATflags(cur) & ObjMask) {
                SATflags(tv) |= ObjMask;
                break;
              }
            }
          }
        }

        break;
      }

      clit = *oplit;

      tv = SATgetNode(clit);
      inverted = SATisInverted(tv);
      tv = SATnormalNode(tv);
      value = SATvalue(tv) ^ inverted;

      if(SATisWL(clit)) { /* found other watched literal */
        wlit = oplit;
        if(value == 1)  {
          break;
        }
        continue;
      }

      if(value == 0)
        continue;

      SATunsetWL(plit);

      size--;
      space[i] = space[size];
      i--;

      var = SATgetVariable(tv);
      SATsetWL(oplit, dir);

      inverted = !inverted;
      if(var->wl[inverted]) {
        sat_ArrayInsert(var->wl[inverted], (long)oplit);
      }
      else {
        var->wl[inverted] = sat_ArrayAlloc(4);
        sat_ArrayInsert(var->wl[inverted], (long)oplit);
      }

      break;
    }
  }
  wl->num = size;
}


int
sat_ImplyNode(
        satManager_t *cm,
        satLevel_t *d,
        long v)
{
long *fan, cur;
int value;
int i, size;
long left, right;
satVariable_t *var;
satArray_t *wlArray;

  value = SATvalue(v) ^ 1;
  var = SATgetVariable(v);
  wlArray = var->wl[value];

  if(wlArray && wlArray->size) {
    sat_ImplyCNF(cm, d, v, wlArray);
  }

  if(d->conflict)
    return(0);

  fan = (long *)SATfanout(v);
  size = SATnFanout(v);
  for(i=0; i<size; i++, fan++) {
    cur = *fan;
    cur = cur >> 1;
    cur = SATnormalNode(cur);
    left = SATleftChild(cur);
    right = SATrightChild(cur);
    value = SATgetValue(left, right, cur);

    (satImplicationFN[value])(cm, d, cur, left, right);

    if(d->conflict)
      return(0);
  }

  left = SATleftChild(v);
  right = SATrightChild(v);
  value = SATgetValue(left, right, v);

  (satImplicationFN[value])(cm, d, v, left, right);

  if(d->conflict)
    return(0);


  return(1);
}


void
sat_ImplicationMain(
        satManager_t *cm,
        satLevel_t *d)
{
satQueue_t *Q, *BDDQ;
long v;

  Q = cm->queue;
  BDDQ = cm->BDDQueue;

  while(1) {
    v = sat_Dequeue(Q);
    while(v && d->conflict == 0) {
      sat_ImplyNode(cm, d, v);
      SATflags(v) &= ResetInQueueMask;

      v = sat_Dequeue(Q);
    }

    if(d->conflict)
      break;

    if(cm->option->BDDImplication) {
      v = sat_Dequeue(Q);
      while(v && d->conflict == 0) {
        sat_ImplyBDD(cm, d, v);
        SATflags(v) &= ResetInQueueMask;

        v = sat_Dequeue(Q);
      }
    }

    if(Q->size == 0 && BDDQ->size == 0)
      break;
  }

  sat_CleanImplicationQueue(cm);
  cm->implicatedSoFar += d->implied->num;
}



void
sat_CleanImplicationQueue(
        satManager_t *cm)
{
satQueue_t *Q;
 int i;
 bAigEdge_t v;

  Q = cm->queue;

  if(Q->size <=0)       return;

  //Bing: important, can't be zero, since some var's value,which are now in
  //implication queue will be erased. This may lead to not being able to
  //identify conflict
  if(cm->option->AbRf || cm->option->IP || cm->option->arosat){
    if(Q->front <= Q->rear) {
      for(i=Q->front; i<=Q->rear; i++) {
        v = Q->array[i];
        SATflags(v) &= ResetInQueueMask;
      }
    }
    else {
      for(i=Q->front; i<Q->max; i++) {
        v = Q->array[i];
        SATflags(v) &= ResetInQueueMask;
      }
      for(i=0; i<Q->rear; i++) {
        v = Q->array[i];
        SATflags(v) &= ResetInQueueMask;
      }
    }
  }
#if 0
  if(Q->front <= Q->rear) {
    for(i=Q->front; i<=Q->rear; i++) {
      v = Q->array[i];
      SATflags(v) &= ResetInQueueMask;
      SATante(v) = 0;
      SATante2(v) = 0;
      SATvalue(v) = 2;
    }
  }
  else {
    for(i=Q->front; i<Q->max; i++) {
      v = Q->array[i];
      SATflags(v) &= ResetInQueueMask;
      SATante(v) = 0;
      SATante2(v) = 0;
      SATvalue(v) = 2;
    }
    for(i=0; i<Q->rear; i++) {
      v = Q->array[i];
      SATflags(v) &= ResetInQueueMask;
      SATante(v) = 0;
      SATante2(v) = 0;
      SATvalue(v) = 2;
    }
  }
#endif

  Q->size = 0;
  Q->front = 1;
  Q->rear = 0;
}


void
sat_ImplyArray(
        satManager_t *cm,
        satLevel_t *d,
        satArray_t *arr)
{
int i, size;
long v;
int inverted, value;
satQueue_t *Q;

  if(arr == 0)  return;
  if(cm->status)return;

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

    value = !inverted;
    if(SATvalue(v) < 2) {
      if(SATvalue(v) == value)  continue;
      else {
        cm->status = SAT_UNSAT;
        d->conflict = v;
        //Bing:
        return;
      }
    }

    SATvalue(v) = value;
    SATmakeImplied(v, d);
    //Bing:
    cm->each->nCNFImplications++;
    if(cm->option->coreGeneration && cm->option->IP){
      st_insert(cm->anteTable,(char *)SATnormalNode(v),(char *)SATnormalNode(v));
    }

    if((SATflags(v) & InQueueMask) == 0) {
      sat_Enqueue(Q, v);
      SATflags(v) |= InQueueMask;
    }
  }
}

void
sat_ImplyBDD(
        satManager_t *cm,
        satLevel_t *d,
        long v)
{
}

void
sat_BuildLevelZeroHyperImplicationGraph(
        satManager_t *cm)
{
}