source: vis_dev/vis-2.3/src/puresat/puresatArosat.c @ 86

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

  FileName    [puresatArosat.c]

  PackageName [puresat]

  Synopsis    [Abstraction refinement for large scale invariant checking.]

  Description [This file contains the functions to check invariant properties
  by the PureSAT abstraction refinement algorithm, which is entirely based on
  SAT solver, the input of which could be either CNF or AIG. It has several
  parts:

  * Localization-reduction base Abstraction
  * K-induction or interpolation to prove the truth of a property
  * Bounded Model Checking to find bugs
  * Incremental concretization based methods to verify abstract bugs
  * Incremental SAT solver to improve efficiency
  * UNSAT proof based method to obtain refinement
  * AROSAT to bring in only necessary latches into unsat proofs
  * Bridge abstraction to get compact coarse refinement
  * Refinement minization to guarrantee minimal refinements
  * Unsat proof-based refinement minimization to eliminate multiple candidate
    by on SAT test
  * Refinement prediction to decrease the number of refinement iterations
  * Dynamic switching to redistribute computional resources to improve
    efficiency

  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure", "Efficient computation
  of small abstraction refinements", and "Efficient abstraction refinement in
  interpolation-based unbounded model checking"]

  Author      [Bing Li]

  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
  All rights reserved.

  Permission is hereby granted, without written agreement and without
  license or royalty fees, to use, copy, modify, and distribute this
  software and its documentation for any purpose, provided that the
  above copyright notice and the following two paragraphs appear in
  all copies of this software.]

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

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

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


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


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

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

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

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


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

  Synopsis    [comparing score for sorting]

  Description []

  SideEffects []

  SeeAlso     []

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

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

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

/*---------------------------------------------------------------------------*/
/* 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                                          */
/*---------------------------------------------------------------------------*/


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

  Synopsis    [No further implcation when this function is called.]

  Description [No further implcation when this function is called.
                      0       0       0       1
                      |       |       |       |
                     ---     ---     ---     ---
                     / \     / \     / \     / \
                    0   X   X   0   0   0   1   1
              ]

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [No further implcation when this function is called.]

  Description [No further implcation when this function is called.
               and need split on output.
                      0
                      |
                     ---
                     / \
                    X   X
              ]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [The conflict happens.]

  Description [The conflict happens when
                      0       1       1       1       1
                      |       |       |       |       |
                     ---     ---     ---     ---     ---
                     / \     / \     / \     / \     / \
                    1   1   X   0   0   X   1   0   0   1
              ]

  SideEffects []

  SeeAlso     []

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


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

  Synopsis    [A value implied to output due to left child.]

  Description [A value implied to output due to left child
                      X       X
                      |       |
                     ---     ---
                     / \     / \
                    0   1   0   X
              ]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [A value implied to output due to right child.]

  Description [A value implied to output due to right child
                      X       X
                      |       |
                     ---     ---
                     / \     / \
                    1   0   X   0
              ]

  SideEffects []

  SeeAlso     []

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


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

  Synopsis    [A value implied to output due to both child.]

  Description [A value implied to output due to both child
                      X
                      |
                     ---
                     / \
                    1   1
              ]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [A value implied to right child due to both output and left.]

  Description [A value implied to right child due to both output and left
                      0
                      |
                     ---
                     / \
                    1   X
              ]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [A value implied to right child due to both output and left.]

  Description [A value implied to right child due to both output and left
                      1
                      |
                     ---
                     / \
                    1   X
              ]

  SideEffects []

  SeeAlso     []

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


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

  Synopsis    [A value implied to left child due to both output and right.]

  Description [A value implied to left child due to both output and right
                      0
                      |
                     ---
                     / \
                    X   1
              ]

  SideEffects []

  SeeAlso     []

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



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

  Synopsis    [A value implied to left child due to both output and right.]

  Description [A value implied to left child due to both output and right
                      1
                      |
                     ---
                     / \
                    X   1
              ]

  SideEffects []

  SeeAlso     []

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



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

  Synopsis    [A value implied to left and right child due to output.]

  Description [A value implied to left and right child due to output
                      1
                      |
                     ---
                     / \
                    X   X
              ]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [erase previous assignments by arosat]

  Description []

  SideEffects []

  SeeAlso     []

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

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;



}


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

  Synopsis    [implication for cnf]

  Description []

  SideEffects []

  SeeAlso     []

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

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) {  /** conflict happens **/
          d->conflict = nv;
          wl->num = size;
          return;
        }
        else if(value > 1) { /** implication **/

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

          /** to identify the objective dependent clause for incremental
          * SAT
          **/
          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--;

      /** move watched literal */
      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;
}


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

  Synopsis    [implication for aig node and cnf ]

  Description []

  SideEffects []

  SeeAlso     []

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

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

  /** implcation on CNF **/
  if(wlArray && wlArray->size) {
    AS_ImplyCNF(cm, d, v, wlArray);
  }

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

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


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

  Synopsis    [The main procedure of implication propogation]

  Description []

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Implication for assertation in one array]

  Description []

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Preprocessing step for AROSAT]

  Description []

  SideEffects []

  SeeAlso     []

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

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


  /** create implication queue **/
  cm->queue = sat_CreateQueue(1024);
  cm->BDDQueue = sat_CreateQueue(1024);
  cm->unusedAigQueue = sat_CreateQueue(1024);

  /**
  create variable array : one can reduce size of variable array using
  mapping. for fanout free internal node....
  **/

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

  /** create decision stack **/
  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;

  /** to avoid purify warning **/
  SATvalue(2) = 2;
  SATflags(0) = 0;

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

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


  /** Level 0 decision.... **/
  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);
    }
  }

}


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

  Synopsis    [backtrack procedure for arosat]

  Description []

  SideEffects []

  SeeAlso     []

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


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


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

  Synopsis    [procedure for updating score]

  Description []

  SideEffects []

  SeeAlso     []

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


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

}


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

  Synopsis    [Periodically executed operations]

  Description []

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Decision procedure]

  Description []

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Find UIP for generating conflict clauses]

  Description []

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Conflict analysis procedure]

  Description []

  SideEffects []

  SeeAlso     []

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

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) {
      /** Bing : UNSAT core generation */
    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);
}


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

  Synopsis    [Main solving procedure]

  Description []

  SideEffects []

  SeeAlso     []

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

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

  }
}


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

  Synopsis    [The main procedure of AROSAT solver]

  Description []

  SideEffects []

  SeeAlso     []

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

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

  btime = util_cpu_time();
  AS_PreProcessing(cm);

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

  /** Bing: UNSAT core generation **/
  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 ;

}


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

  Synopsis    [Create one layer for AROSAT]

  Description []

  SideEffects []

  SeeAlso     []

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


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

}



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

  Synopsis    [Create all the layers]

  Description []

  SideEffects []

  SeeAlso     []

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


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

}