src/puresat/puresatArosat.c

Go to the documentation of this file.

#include "puresatInt.h"
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

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


static int
ScoreCompare(
  const void * node1,
  const void * node2)
{
int v1;
int v2;
int s1, s2;

  v1 = *(int *)(node1);
  v2 = *(int *)(node2);
  s1 = *((int *)(node1) + 1);
  s2 = *((int *)(node2) + 1);

  if(s1 == s2) {
    return(v1 > v2);
  }
  return(s1 < s2);
}

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


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


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


ASIMPLY_FN ASImplicationFN[64]= {
  AS_ImplyStop,                 /* 0    */
  AS_ImplyConflict,             /* 1  */
  AS_ImplyLeftForward,          /* 2  */
  AS_ImplyLeftForward,          /* 3  */
  AS_ImplyStop,                 /* 4  */
  AS_ImplyConflict,             /* 5  */
  AS_ImplyLeftForward,          /* 6  */
  AS_ImplyLeftForward,          /* 7  */
  AS_ImplySplit,                /* 8  */
  AS_ImplyConflict,             /* 9  */
  AS_ImplyLeftForward,          /* 10  */
  AS_ImplyLeftForward,          /* 11  */
  AS_ImplySplit,                /* 12  */
  AS_ImplyConflict,             /* 13  */
  AS_ImplyLeftForward,          /* 14  */
  AS_ImplyLeftForward,          /* 15  */
  AS_ImplyStop,                 /* 16  */
  AS_ImplyConflict,             /* 17  */
  AS_ImplyRightForward,         /* 18  */
  AS_ImplyRightForward,         /* 19  */
  AS_ImplyConflict,             /* 20  */
  AS_ImplyStop,                 /* 21  */
  AS_ImplyForwardOne,           /* 22  */
  AS_ImplyForwardOne,           /* 23  */
  AS_ImplyPropRight,            /* 24  */
  AS_ImplyPropRightOne,         /* 25  */
  AS_ImplyStop,                 /* 26  */
  AS_ImplyStop,                 /* 27  */
  AS_ImplyPropRight,            /* 28  */
  AS_ImplyPropRightOne,         /* 29  */
  AS_ImplyStop,                 /* 30  */
  AS_ImplyStop,                 /* 31  */
  AS_ImplySplit,                /* 32  */
  AS_ImplyConflict,             /* 33  */
  AS_ImplyRightForward,         /* 34  */
  AS_ImplyRightForward,         /* 35  */
  AS_ImplyPropLeft,             /* 36  */
  AS_ImplyPropLeftOne,          /* 37  */
  AS_ImplyStop,                 /* 38  */
  AS_ImplyStop,                 /* 39  */
  AS_ImplySplit,                /* 40  */
  AS_ImplyPropLeftRight,        /* 41  */
  AS_ImplyStop,                 /* 42  */
  AS_ImplyStop,                 /* 43  */
  AS_ImplySplit,                /* 44  */
  AS_ImplyPropLeftRight,        /* 45  */
  AS_ImplyStop,                 /* 46  */
  AS_ImplyStop,                 /* 47  */
  AS_ImplySplit,                /* 48  */
  AS_ImplyConflict,             /* 49  */
  AS_ImplyRightForward,         /* 50  */
  AS_ImplyRightForward,         /* 51  */
  AS_ImplyPropLeft,             /* 52  */
  AS_ImplyPropLeftOne,          /* 53  */
  AS_ImplyStop,                 /* 54  */
  AS_ImplyStop,                 /* 55  */
  AS_ImplySplit,                /* 56  */
  AS_ImplyPropLeftRight,        /* 57  */
  AS_ImplyStop,                 /* 58  */
  AS_ImplyStop,                 /* 59  */
  AS_ImplySplit,                /* 60  */
  AS_ImplyPropLeftRight,        /* 61  */
  AS_ImplyStop,                 /* 62  */
  AS_ImplyStop,                 /* 63  */
};



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


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

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

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


int
AS_ImplyLeftForward(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  if(sat_ASImp(cm,d,v,0))
    return(0);

  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
AS_ImplyRightForward(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{

  if(sat_ASImp(cm,d,v,0))
    return(0);

  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
AS_ImplyForwardOne(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{

  if(sat_ASImp(cm,d,v,1))
    return(0);

  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
AS_ImplyPropRight(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  int isInverted;

  isInverted = SATisInverted(right);


  if(sat_ASImp(cm,d,right, isInverted))
    return(0);

  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
AS_ImplyPropRightOne(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  int isInverted;


  if(sat_ASImp(cm,d,right,!SATisInverted(right)))
    return(0);

  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
AS_ImplyPropLeft(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  int isInverted;


  if(sat_ASImp(cm,d,left,SATisInverted(left)))
    return(0);

  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
AS_ImplyPropLeftOne(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  int isInverted;


  if(sat_ASImp(cm,d,left,!SATisInverted(left)))
    return(0);

  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
AS_ImplyPropLeftRight(
        satManager_t *cm,
        satLevel_t *d,
        long v,
        long left,
        long right)
{
  int isLeftInverted;
  int isRightInverted;

  int lImp=1,rImp=1;

  if(left == right)     return 1;


  if(sat_ASImp(cm,d,left,!SATisInverted(left)))
    lImp = 0;
  if(sat_ASImp(cm,d,right,!SATisInverted(right)))
    rImp = 0;


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

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

  if(lImp){
    SATmakeImplied(left, d);
    SATante(left) = v;
    SATvalue(left) = !isLeftInverted;
    sat_Enqueue(cm->queue, left);
    SATflags(left) |= InQueueMask;
    SATflags(left) |= (SATflags(v) & ObjMask);
    cm->each->nAigImplications ++;
  }

  if(rImp){
    SATmakeImplied(right, d);
    SATante(right) = v;
    SATvalue(right) = !isRightInverted;
    sat_Enqueue(cm->queue, right);
    SATflags(right) |= InQueueMask;
    SATflags(right) |= (SATflags(v) & ObjMask);
    cm->each->nAigImplications ++;
  }

  return(0);
}

void
AS_Undo(
        satManager_t *cm,
        satLevel_t *d)
{
satArray_t *implied, *satisfied;
int size, i;
long *space, v;
 satVariable_t *var;
 int dfs;

  implied = d->implied;
  space = implied->space;
  size = implied->num;
  for(i=0; i<size; i++, space++) {
    v = *space;

    SATvalue(v) = 2;
    SATflags(v) &= ResetNewVisitedObjInQueueMask;
    SATante(v) = 0;
    SATante2(v) = 0;
    SATlevel(v) = -1;


    if(SATflags(SATnormalNode(v))&AssignedMask){
      SATflags(SATnormalNode(v))&=ResetAssignedMask;
      var=SATgetVariable(v);
      dfs = var->scores[0]/SCOREUNIT;
      cm->assignedArray[dfs]--;

#if DBG
      assert(cm->assignedArray[dfs]>=0);
#endif
    }

  }

  cm->implicatedSoFar -= size;

  if(d->satisfied) {
    satisfied = d->implied;
    space = satisfied->space;
    size = satisfied->num;
    for(i=0; i<size; i++, space++) {
      v = *space;

      SATflags(v) &= ResetBDDSatisfiedMask;
    }
    d->satisfied->num = 0;
  }
  if(d->level > 0) {
    if((cm->decisionHead[d->level-1]).currentVarPos < cm->currentVarPos)
      cm->currentVarPos = (cm->decisionHead[d->level-1]).currentVarPos;
  }
  else
    cm->currentVarPos = d->currentVarPos;

  d->implied->num = 0;
  d->currentVarPos = 0;

  d->conflict = 0;



}


void
AS_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;

 long tmpv;

  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);

        tmpv = tv;
        isInverted = SATisInverted(tv);
        tv = SATnormalNode(tv);
        value = SATvalue(tv) ^ isInverted;
        if(value == 0) {  
          d->conflict = nv;
          wl->num = size;
          return;
        }
        else if(value > 1) { 
          if(sat_ASImp(cm,d,tmpv,!isInverted))
            break;

          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
AS_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) {
    AS_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);
#if DBG

    assert(SATflags(SATnormalNode(left))&CoiMask);
    assert(SATflags(SATnormalNode(right))&CoiMask);
#endif
    (ASImplicationFN[value])(cm, d, cur, left, right);

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

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

  assert(left==bAig_NULL||SATflags(SATnormalNode(left))&CoiMask);
  assert(right==bAig_NULL||SATflags(SATnormalNode(right))&CoiMask);
#endif


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

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


  return(1);
}


void
AS_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) {
      AS_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
AS_ImplyArray(
        satManager_t *cm,
        satLevel_t *d,
        satArray_t *arr)
{
int i, size;
long v;
int inverted, value;
satQueue_t *Q;
 satVariable_t *var;

 int dfs;

  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;

        return;
      }
    }


    var = SATgetVariable(v);
    dfs = var->scores[0]/SCOREUNIT;
    if(dfs==cm->LatchLevel){
      if(!(SATflags(SATnormalNode(v))&AssignedMask)){
        SATflags(SATnormalNode(v))|=AssignedMask;
        cm->assignedArray[dfs]++;

#if DBG
        assert(cm->assignedArray[dfs]<=cm->numArray[dfs]);
#endif
        if(cm->assignedArray[dfs]==cm->numArray[dfs])
          sat_ASmergeLevel(cm);
      }
    }


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

    if(cm->option->coreGeneration){
      st_insert(cm->anteTable,(char *)SATnormalNode(v),(char *)SATnormalNode(v));
    }

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

void
AS_PreProcessing(satManager_t *cm)
{
satLevel_t *d;


  cm->queue = sat_CreateQueue(1024);
  cm->BDDQueue = sat_CreateQueue(1024);
  cm->unusedAigQueue = sat_CreateQueue(1024);

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

  cm->auxArray = sat_ArrayAlloc(1024);
  cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
  cm->objUnitLitArray = sat_ArrayAlloc(128);



  if(cm->option->AbRf == 0)
    sat_CompactFanout(cm);


  /*assign initial layer score to variables*/
   sat_InitLayerScore(cm);

  if(cm->decisionHeadSize == 0) {
    cm->decisionHeadSize = 32;
    cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);
    memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
  }
  cm->currentDecision = -1;

  SATvalue(2) = 2;
  SATflags(0) = 0;

  cm->initNodesArraySize = cm->nodesArraySize;
  cm->beginConflict = cm->nodesArraySize;

  if(cm->option->incTraceObjective) {
    sat_RestoreForwardedClauses(cm, 0);
  }
  else if(cm->option->incAll) {
    sat_RestoreForwardedClauses(cm, 1);
  }

  if(cm->option->incTraceObjective) {
    sat_MarkObjectiveFlagToArray(cm, cm->obj);
    sat_MarkObjectiveFlagToArray(cm, cm->objCNF);
  }


  d = sat_AllocLevel(cm);

  sat_ApplyForcedAssignmentMain(cm, d);

  if(cm->status == SAT_UNSAT)
    return;


  if(cm->option->coreGeneration){
    cm->rm = ALLOC(RTManager_t, 1);
    memset(cm->rm,0,sizeof(RTManager_t));
  }


  AS_ImplyArray(cm, d, cm->auxObj);
  AS_ImplyArray(cm, d, cm->obj);
  AS_ImplyArray(cm,d,cm->assertArray);


  AS_ImplicationMain(cm, d);
  if(d->conflict) {
    cm->status = SAT_UNSAT;
  }

  if(cm->status == 0) {
    if(cm->option->incDistill) {
      sat_IncrementalUsingDistill(cm);
    }
  }

}


void
AS_Backtrack(
        satManager_t *cm,
        int level)
{
satLevel_t *d;


  d = SATgetDecision(cm->currentDecision);
  while(1) {
    if(d->level <= level)
      break;

    AS_Undo(cm, d);
    cm->currentDecision--;
    if(cm->currentDecision == -1)
      break;
    d = SATgetDecision(cm->currentDecision);
  }
  return;
}


void
AS_UpdateScore(
        satManager_t *cm)
{
satArray_t *one, *tmp;
satArray_t *ordered;
satVariable_t *var;
int size, i;
long v;
int value;

 int baseScore,realScore,newNum;

  ordered = cm->orderedVariableArray;

  one = sat_ArrayAlloc(ordered->num);
  tmp = sat_ArrayAlloc(ordered->num);

  size = ordered->num;
  for(i=0; i<size; i++) {
    v = ordered->space[i];

    if(SATvalue(v) < 2 && SATlevel(v) == 0)
      continue;

    var = SATgetVariable(v);

    baseScore =(var->scores[0]/SCOREUNIT)*SCOREUNIT;
    realScore = var->scores[0]%SCOREUNIT;
    newNum = var->litsCount[0] - var->lastLitsCount[0];
    var->scores[0] =  baseScore + (realScore>>1) + newNum;
    baseScore =(var->scores[1]/SCOREUNIT)*SCOREUNIT;
    realScore = var->scores[1]%SCOREUNIT;
    newNum = var->litsCount[1] - var->lastLitsCount[1];
    var->scores[1] =  baseScore + (realScore>>1) + newNum;

    var->lastLitsCount[0] = var->litsCount[0];
    var->lastLitsCount[1] = var->litsCount[1];


    if((var->scores[0] + var->scores[1]) < 1) {
      sat_ArrayInsert(one, v);
    }
    else {
      value = (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1];
      sat_ArrayInsert(tmp, v);
      sat_ArrayInsert(tmp, value);
    }
  }

  qsort(tmp->space, (tmp->num)>>1, sizeof(long)*2, ScoreCompare);

  ordered->num = 0;
  size = tmp->num;
  for(i=0; i<size; i++) {
    v = tmp->space[i];
    sat_ArrayInsert(ordered, v);
    var = SATgetVariable(v);
    var->pos = (i>>1);
    i++;
  }

  size = one->num;
  for(i=0; i<size; i++) {
    v = one->space[i];
    var = SATgetVariable(v);
    var->pos = ordered->num;
    sat_ArrayInsert(ordered, v);
  }

  sat_ArrayFree(one);
  sat_ArrayFree(tmp);

  cm->orderedVariableArray = ordered;
  cm->currentVarPos = 0;

  for(i=1; i<cm->currentDecision; i++) {
    cm->decisionHead[i].currentVarPos = 0;
  }

  if(cm->option->verbose > 3)
    sat_PrintScore(cm);

}


void
AS_PeriodicFunctions(satManager_t *cm)
{
satStatistics_t *stats;
satOption_t *option;
int nDecisions;
int gap;

  stats = cm->each;
  option = cm->option;
  nDecisions = stats->nDecisions-stats->nShrinkDecisions;
  if(nDecisions && !(nDecisions % option->decisionAgeInterval)) {
    if(option->decisionAgeRestart) {
      gap = stats->nConflictCl-stats->nOldConflictCl;
      if(gap > option->decisionAgeInterval>>2)  {

        AS_UpdateScore(cm);

        AS_Backtrack(cm, cm->lowestBacktrackLevel);
        cm->currentTopConflict = cm->literals->last-1;
        cm->currentTopConflictCount = 0;
        cm->lowestBacktrackLevel = MAXINT;
      }
      stats->nOldConflictCl = stats->nConflictCl;
    }
    else {

      AS_UpdateScore(cm);
    }

  }

  if(stats->nBacktracks > option->nextClauseDeletion) {
    option->nextClauseDeletion += option->clauseDeletionInterval;
    sat_ClauseDeletion(cm);
  }
}

satLevel_t *
AS_MakeDecision(satManager_t *cm)
{
satLevel_t *d;
int value;
long v;
satStatistics_t *stats;

  d = SATgetDecision(cm->currentDecision);

  if(cm->queue->size)
    return(d);

  d = sat_AllocLevel(cm);

  v = 0;
  v = sat_DecisionBasedOnBDD(cm, d);

  if(v == 0)
    v = sat_DecisionBasedOnScore(cm, d);

  if(v == 0)
    return(0);


  sat_ASDec(cm,d,v);

  stats = cm->each;

  stats->nDecisions++;

  value = !(SATisInverted(v));
  v = SATnormalNode(v);
  d->decisionNode = v;


    if((SATgetVariable(v)->RecVal)!=0){
      if(SATgetVariable(v)->RecVal==-1)
        value=0;
      else{
#if DBG
        assert(SATgetVariable(v)->RecVal==1);
#endif
        value=1;
      }

    }


  SATvalue(v) = value;

  SATmakeImplied(v, d);
#if DBG

  assert(SATflags(v)&CoiMask);
#endif

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

  return(d);
}

void
AS_FindUIP(
        satManager_t *cm,
        satArray_t *clauseArray,
        satLevel_t *d,
        int *objectFlag,
        int *bLevel,
        long *fdaLit)
{
long conflicting;
int nMarked, value;
int first, i,j;
long *space, v,left,right,inverted,result,*tmp;
satArray_t *implied;
satOption_t *option;
RTnode_t  tmprt;
int size = 0;
long *lp, *tmpIP,ante,ante2,node;
 RTManager_t * rm = cm->rm;

  conflicting = d->conflict;
  nMarked = 0;
  option = cm->option;
  if(option->incTraceObjective) *objectFlag = 0;
  else                          *objectFlag = ObjMask;

  (*objectFlag) |= (SATflags(conflicting) & ObjMask);

  /* find seed from conflicting clause to find unique implication point.
   * */
  clauseArray->num = 0;
  sat_MarkNodeInConflict(
          cm, d, &nMarked, objectFlag, bLevel, clauseArray);

  /* Traverse implication graph backward */
  first = 1;
  implied = d->implied;
  space = implied->space+implied->num-1;


  if(cm->option->coreGeneration){
    /*if last conflict is CNF*/
    if(SATflags(conflicting)&IsCNFMask){
      /*is conflict CNF*/
      if(SATflags(conflicting)&IsConflictMask){
         if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){
            fprintf(vis_stderr,"RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
            exit(0);
          }
          else{
            rm->root = tmprt;
          }
      }
      /*CNF but not conflict*/
      else{
        rm->root = RTCreateNode(rm);
        RT_oriClsIdx(rm->root) = conflicting;
        size = SATnumLits(conflicting);
        RT_fSize(rm->root) = size;
      }
    }
    /*if last conflict is AIG*/
    else{
      rm->root = RTCreateNode(rm);
      node = SATnormalNode(conflicting);
      left = SATleftChild(node);
      right = SATrightChild(node);
      result = PureSat_IdentifyConflict(cm,left,right,conflicting);
      inverted = SATisInverted(left);
      left = SATnormalNode(left);
      left = inverted ? SATnot(left) : left;

      inverted = SATisInverted(right);
      right = SATnormalNode(right);
      right = inverted ? SATnot(right) : right;

      j = node;

      if(result == 1){
        tmp = ALLOC(long,3);
        tmp[0] = left;
        tmp[1] = SATnot(j);
        size = 2;
      }
      else if(result == 2){
        tmp = ALLOC(long,3);
        tmp[0] = right;
        tmp[1] = SATnot(j);
        size = 2;
      }
      else if(result == 3){
        tmp = ALLOC(long,4);
        tmp[0] = SATnot(left);
        tmp[1] = SATnot(right);
        tmp[2] = j;
        size = 3;
      }
      else{
        fprintf(vis_stderr,"wrong returned result value, exit\n");
        exit(0);
      }

      lp = tmp;
      sat_BuildRT(cm,rm->root, lp, tmpIP,size,1);
      FREE(tmp);
    }
  }


  for(i=implied->num-1; i>=0; i--, space--) {
    v = *space;
    if(SATflags(v) & VisitedMask) {
      SATflags(v) &= ResetVisitedMask;
      --nMarked;

      if(nMarked == 0 && (!first || i==0))  {
        value = SATvalue(v);
        *fdaLit = v^(!value);
        sat_ArrayInsert(clauseArray, *fdaLit);
        break;
      }



      if(cm->option->coreGeneration){
        ante = SATante(v);
        if(ante==0){
          if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v),&ante))){
            fprintf(vis_stderr,"ante = 0 and is not in anteTable %ld\n",v);
            exit(0);
          }
        }

        /*build non-leaf node*/
        tmprt = RTCreateNode(rm);
        RT_pivot(tmprt) = SATnormalNode(v);
        RT_right(tmprt) = rm->root;
        rm->root = tmprt;

        if((SATflags(ante)&IsConflictMask)&&(SATflags(ante)&IsCNFMask)){
          if(!st_lookup(cm->RTreeTable,(char*)ante,&tmprt)){
            fprintf(vis_stderr,"RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
            exit(0);
          }
          else{
            RT_left(rm->root) = tmprt;
          }
        }
        else{ /* if not conflict CNF*/
          /*left */
          tmprt = RTCreateNode(rm);
          RT_left(rm->root) = tmprt;
          /*left is AIG*/
          if(!(SATflags(ante) & IsCNFMask)){
            /*generate formula for left*/
            tmp = ALLOC(long,3);
            value = SATvalue(v);
            node = SATnormalNode(v);
            node = value==1?node:SATnot(node);
            tmp[0] = node;

            size = 1;
            if(ante != SATnormalNode(v)){
              value = SATvalue(ante);
              node = SATnormalNode(ante);
              node = value==1?SATnot(node):node;
              tmp[1] = node;
              size++;
              ante2 = SATante2(v);
              if(ante2){
                value = SATvalue(ante2);
                node = SATnormalNode(ante2);
                node = value==1?SATnot(node):node;
                tmp[2] = node;
                size++;
              }
            }
            /*generate p1 and p2*/
            lp = tmp;
            sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
            FREE(tmp);
          }
          /* left is CNF*/
          else{
            RT_oriClsIdx(tmprt) = ante;
            //generate p1 and p2 for left
            lp = (long*)SATfirstLit(ante);
            size = SATnumLits(ante);
            RT_fSize(tmprt) = size;
          }
        } /*else{  if not conflict CNF*/

      }/*if(cm->option->coreGeneration){*/


      sat_MarkNodeInImpliedNode(
              cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
      /*Bing:Important for EffIP*/
      first = 0;
    }
    /* first = 0;*/
  }


  /* Minimize conflict clause */
  if(option->minimizeConflictClause)
    sat_MinimizeConflictClause(cm, clauseArray);
  else
    sat_ResetFlagForClauseArray(cm, clauseArray);

  return;
}


int
AS_ConflictAnalysis(
        satManager_t *cm,
        satLevel_t *d)
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, learned, conflicting;
int inverted;
RTManager_t * rm = cm->rm;


  conflicting = d->conflict;

  if(d->level == 0) {
    if(cm->option->coreGeneration)
      sat_ConflictAnalysisForCoreGen(cm, d);
    cm->currentDecision--;
    return (-1);
  }

  stats = cm->each;
  option = cm->option;


  stats->nBacktracks++;

  clauseArray = cm->auxArray;

  bLevel = 0;
  fdaLit = -1;
  clauseArray->num = 0;

  /*  Find Unique Implication Point */
  AS_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
  stats->nNonchonologicalBacktracks += (d->level - bLevel);


  if(clauseArray->num == 0) {
    sat_PrintImplicationGraph(cm, d);
    sat_PrintNode(cm, conflicting);
  }

  /* If we could find UIP then it is critical error...
  * at lease the decision node has to be detected as UIP.
  */
  if(fdaLit == -1) {
    fprintf(vis_stdout, "%s ERROR : Illegal unit literal\n", cm->comment);
    fflush(vis_stdout);
    sat_PrintNode(cm, conflicting);
    sat_PrintImplicationGraph(cm, d);
    sat_PrintDotForConflict(cm, d, conflicting, 0);
    exit(0);
  }

  if(bLevel && cm->lowestBacktrackLevel > bLevel)
    cm->lowestBacktrackLevel = bLevel;


  inverted = SATisInverted(fdaLit);
  fdaLit = SATnormalNode(fdaLit);

  if(option->verbose > 2) {
    if(option->verbose > 4)
      sat_PrintNode(cm, conflicting);
    fprintf(vis_stdout, "conflict at %3d on %6ld  bLevel %d UnitLit ",
            d->level, conflicting, bLevel);
    sat_PrintNodeAlone(cm, fdaLit);
    fprintf(vis_stdout, "\n");
  }

  d->conflict = 0;

  /* unit literal conflict clause */
  if(clauseArray->num == 1) {
    learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);

    stats->nUnitConflictCl++;
    cm->currentTopConflict = cm->literals->last-1;
    cm->currentTopConflictCount = 0;

    AS_Backtrack(cm, 0);

    d = SATgetDecision(cm->currentDecision);
    cm->implicatedSoFar -= d->implied->num;
    SATante(fdaLit) = 0;


    if(!(SATflags(SATnormalNode(fdaLit))&AssignedMask)){
      satVariable_t *var = SATgetVariable(fdaLit);
      int dfs = var->scores[0]/SCOREUNIT;
#if DBG
      assert(dfs==cm->LatchLevel);
#endif
      SATflags(SATnormalNode(fdaLit))|=AssignedMask;
      cm->assignedArray[dfs]++;
      if(cm->assignedArray[dfs]==cm->numArray[dfs])
        sat_ASmergeLevel(cm);
    }


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

    if((SATflags(fdaLit) & InQueueMask)  == 0) {
      sat_Enqueue(cm->queue, fdaLit);
      SATflags(fdaLit) |= InQueueMask;
    }

    clauseArray->num = 0;

    if(option->incTraceObjective && objectFlag == 0)
      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));

    if(option->incDistill && objectFlag)
      sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));

    if(objectFlag)
      SATflags(fdaLit) |= ObjMask;

    /* Bing: UNSAT core generation */
    if(cm->option->coreGeneration){

      st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
      st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
      RT_oriClsIdx(rm->root) = learned;
    }

    return(bLevel);
  }

  /* add conflict learned clause */
  learned = sat_AddConflictClause(cm, clauseArray, objectFlag);

  cm->currentTopConflict = cm->literals->last-1;
  cm->currentTopConflictCount = 0;

   /* Bing: UNSAT core generation */
  if(cm->option->coreGeneration){
   st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
   RT_oriClsIdx(rm->root) = learned;
  }

  if(option->verbose > 2) {
    sat_PrintNode(cm, learned);
    fflush(vis_stdout);
  }


  /* apply Deepest Variable Hike decision heuristic */
  if(option->decisionHeuristic & DVH_DECISION)
   sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);


  /* Backtrack and failure driven assertion */
  AS_Backtrack(cm, bLevel);

  d = SATgetDecision(bLevel);
  cm->implicatedSoFar -= d->implied->num;


    if(!(SATflags(SATnormalNode(fdaLit))&AssignedMask)){
      satVariable_t *var = SATgetVariable(fdaLit);
      int dfs = var->scores[0]/SCOREUNIT;
#if DBG
      assert(dfs==cm->LatchLevel);
#endif
      SATflags(SATnormalNode(fdaLit))|=AssignedMask;
      cm->assignedArray[dfs]++;
      if(cm->assignedArray[dfs]==cm->numArray[dfs])
        sat_ASmergeLevel(cm);
    }


  SATante(fdaLit) = learned;
  SATvalue(fdaLit) = inverted;
  SATmakeImplied(fdaLit, d);

  if((SATflags(fdaLit) & InQueueMask)  == 0) {
    sat_Enqueue(cm->queue, fdaLit);
    SATflags(fdaLit) |= InQueueMask;
  }

  clauseArray->num = 0;
  if(objectFlag)
    SATflags(fdaLit) |= ObjMask;

  return(bLevel);
}


void
AS_Solve(satManager_t *cm)
{
satLevel_t *d;
satOption_t *option;
satVariable_t *var;
int level;

  d = SATgetDecision(0);
  cm->implicatedSoFar = d->implied->num;
  cm->currentTopConflict = 0;

  option = cm->option;
  if(option->BDDMonolithic) {
    sat_TryToBuildMonolithicBDD(cm);
  }

  if(cm->status == SAT_UNSAT) {
    AS_Undo(cm, SATgetDecision(0));
    return;
  }

  while(1) {
    AS_PeriodicFunctions(cm);

    if(cm->currentDecision == 0)
      sat_BuildLevelZeroHyperImplicationGraph(cm);

    d = AS_MakeDecision(cm);

    if(d == 0)  {
      cm->status = SAT_SAT;
      return;
    }

    while(1) {
      AS_ImplicationMain(cm, d);

      if(d->conflict == 0)      {
        if(cm->option->verbose > 2) {
          var = SATgetVariable(d->decisionNode);
          fprintf(vis_stdout, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied %.3f %%\n",
            d->level, d->decisionNode, SATvalue(d->decisionNode),
            var->scores[0], var->scores[1],
            cm->each->nDecisions, d->implied->num,
            (double)cm->implicatedSoFar/(double)cm->initNumVariables * 100);
          fflush(vis_stdout);
        }

        break;
      }
        if(cm->option->verbose > 2) {
          var = SATgetVariable(d->decisionNode);
          fprintf(vis_stdout, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied  %.3f %% Conflict\n",
            d->level, d->decisionNode, SATvalue(d->decisionNode),
            var->scores[0], var->scores[1],
            cm->each->nDecisions, d->implied->num,
            (double)cm->implicatedSoFar/(double)cm->initNumVariables * 100);
          fflush(vis_stdout);
        }

      level = AS_ConflictAnalysis(cm, d);

      if(cm->currentDecision == -1) {
        if(cm->option->incDistill) {
          sat_BuildTrieForDistill(cm);
        }
        AS_Undo(cm, SATgetDecision(0));
        cm->status = SAT_UNSAT;
        return;
      }

      d = SATgetDecision(cm->currentDecision);
    }

  }
}


void AS_Main(satManager_t *cm)
{
long btime, etime;

  btime = util_cpu_time();
  AS_PreProcessing(cm);

  if(cm->status == 0)
    AS_Solve(cm);

  if(cm->option->coreGeneration && cm->status == SAT_UNSAT){

    sat_GenerateCore_All(cm);
  }

  sat_PostProcessing(cm);

  etime = util_cpu_time();
  cm->each->satTime = (double)(etime - btime) / 1000.0 ;

}


void PureSatCreateOneLayer(Ntk_Network_t *network,
                           PureSat_Manager_t *pm,
                           satManager_t *cm,
                           array_t * latchArray,
                           int layer)
{
  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                                         MVFAIG_NETWORK_APPL_KEY);
  MvfAig_Function_t *mvfAig;
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  mAigMvar_t lmVar;
  mAigBvar_t bVar;
  array_t *bVarList,*mVarList;
  int i,j,k,lmAigId,index,index1;
  char * name;
  Ntk_Node_t * latch;
  bAigEdge_t node,v, *li, *bli;
  st_table *table = st_init_table(st_numcmp,st_numhash);

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);

  arrayForEachItem(char*,latchArray,i,name){

    latch = Ntk_NetworkFindNodeByName(network,name);
    st_lookup(node2MvfAigTable,latch,&mvfAig);
    for(j=0;j<mvfAig->num;j++){
      int retVal;
      v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
      if(v==bAig_Zero||v==bAig_One)
        continue;
      retVal = st_lookup(tf->li2index,(char *)v,&index);
      assert(retVal);
      for(k=1;k<=pm->Length;k++){
        li = tf->latchInputs[k];
        if(li[index]==bAig_Zero||li[index]==bAig_One)
          continue;
        node = bAig_NonInvertedEdge(li[index]);
        st_insert(table,(char*)node,(char*)(long)layer);

      }
    }

    lmAigId = Ntk_NodeReadMAigId(latch);
    lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
    for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
      int retVal;
      bVar = array_fetch(mAigBvar_t,bVarList,index1);
      if(bVar.node==bAig_Zero||bVar.node==bAig_One)
        continue;
      retVal = st_lookup(tf->bli2index,(char *)bVar.node,&index);
      assert(retVal);
      for(k=1;k<=pm->Length;k++){
        bli = tf->blatchInputs[k];
        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
          continue;
        node = bAig_NonInvertedEdge(bli[index]);
        st_insert(table,(char*)node,(char*)(long)layer);

      }
    }
  }

  st_insert(cm->layerTable,table,(char*)(long)layer);

}



void PureSatCreateLayer(Ntk_Network_t *network,
                        PureSat_Manager_t *pm,
                        satManager_t *cm,
                        array_t *absModel,
                        array_t *sufArray)
{
  int layer;
  char* name;
  int i,j,threshold;
  array_t *tmpArray;

  if(sufArray->num<4)
    layer = 1;
  else if(sufArray->num<6)
    layer = 2;
  else if(sufArray->num<10)
    layer = 3;
  else if(sufArray->num<20)
    layer = 5;
  else if(sufArray->num<50)
    layer = 8;
  else
    layer = 10;

  threshold = sufArray->num/layer;
  layer = array_n(sufArray)/threshold;
  layer = sufArray->num%threshold?layer+1:layer;

  cm->LatchLevel = layer;
  cm->OriLevel = layer;
  cm->layerTable = st_init_table(st_ptrcmp,st_ptrhash);

  layer = layer+1;
  for(i=0;i<array_n(sufArray);i=i+threshold){
    if(i==0)
      tmpArray = array_dup(absModel);
    else
      tmpArray = array_alloc(char*,0);
    layer = layer-1;
    for(j=0;j<threshold;j++){
      if(i+j>=array_n(sufArray))
        break;
      name = array_fetch(char*,sufArray,i+j);
      array_insert_last(char*,tmpArray,name);

    }
    PureSatCreateOneLayer(network,pm,cm,tmpArray,layer);
    array_free(tmpArray);
  }
  assert(layer==1);
  cm->assignedArray = ALLOC(int,cm->LatchLevel+1);
  cm->numArray = ALLOC(int,cm->LatchLevel+1);

}