source: vis_dev/vis-2.3/src/baig/baigAllSat.c @ 80

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

  FileName    [baigAllSat.c]

  PackageName [baig]

  Synopsis    [Routines to check sat-based invariant checking.]

  Author      [HoonSang Jin]

  Copyright [ This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]


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

#include "baig.h"
#include "baigInt.h"
#include "ntk.h"
#include "bmc.h"
#include "sat.h"

static char rcsid[] UNUSED = "$Id: baigAllSat.c,v 1.4 2009/04/11 02:40:01 fabio Exp $";
static satManager_t *SATcm;

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

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

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
static int nodenameCompare( const void * node1, const void * node2);
static int levelCompare( const void * node1, const void * node2);
static int indexCompare( const void * node1, const void * node2);
static int StringCheckIsInteger(char *string, int *value);

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


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


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

  Synopsis    [Create data structure for transition relation.]

  Description [Create data structure for transition relation.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
bAigTransition_t *
bAigCreateTransitionRelation(
        Ntk_Network_t *network,
        mAig_Manager_t *manager)
{
bAigTransition_t *t;
array_t   *bVarList, *mVarList;
array_t *latcharr;
Ntk_Node_t *node, *dataInput;
mAigMvar_t mVar;
mAigBvar_t bVar;
st_table *node2MvfAigTable;
lsGen gen;
int nLatches, nInputs;
int i, j, index, index1;
int mAigId, maxCS;
bAigEdge_t v;
bAigEdge_t *cstates, *nstates, *inputs;

  t = ALLOC(bAigTransition_t, 1);
  memset(t, 0, sizeof(bAigTransition_t));
  t->network = network;
  t->manager = manager;

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

  latcharr = array_alloc(Ntk_Node_t *, 16);
  nLatches = 0;
  Ntk_NetworkForEachLatch(network, gen, node) {
    mAigId = Ntk_NodeReadMAigId(node);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    nLatches += mVar.encodeLength;
    array_insert_last(Ntk_Node_t *, latcharr, node);
  }
  t->nLatches = nLatches;

  node2MvfAigTable = 
        (st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);

  array_sort(latcharr, nodenameCompare);

  cstates = ALLOC(bAigEdge_t, nLatches);
  nstates = ALLOC(bAigEdge_t, nLatches);
  t->tstates = ALLOC(bAigEdge_t, nLatches);
  t->initials = ALLOC(bAigEdge_t, nLatches);

  nLatches = 0;
  maxCS = 0;
  for(j=0; j<array_n(latcharr); j++) {
    node = array_fetch(Ntk_Node_t *, latcharr, j);
    mAigId = Ntk_NodeReadMAigId(node);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    index = nLatches;
    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
      bVar = array_fetch(mAigBvar_t, bVarList, index1++);
      v = bVar.node;
      cstates[index++] = v;
      if(maxCS < v)
        maxCS = v;
    }

    dataInput = Ntk_LatchReadDataInput(node);
    mAigId = Ntk_NodeReadMAigId(dataInput);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    index = nLatches;
    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
      bVar = array_fetch(mAigBvar_t, bVarList, index1++);
      v = bVar.node;
      v = bAig_GetCanonical(manager, v);
      nstates[index++] = v;
    }

    dataInput = Ntk_LatchReadInitialInput(node);
    mAigId = Ntk_NodeReadMAigId(dataInput);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    index = nLatches;
    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
      bVar = array_fetch(mAigBvar_t, bVarList, index1++);
      v = bVar.node;
      v = bAig_GetCanonical(manager, v);
      t->initials[index++] = v;
    }
    nLatches = index;
  }

  nInputs = 0;
  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
    mAigId = Ntk_NodeReadMAigId(node);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    nInputs += mVar.encodeLength;
  }
  Ntk_NetworkForEachPseudoInput(network, gen, node) {
    mAigId = Ntk_NodeReadMAigId(node);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    nInputs += mVar.encodeLength;
  }
  t->nInputs = nInputs;

  inputs = ALLOC(bAigEdge_t, nInputs);
  nInputs = 0;
  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
    mAigId = Ntk_NodeReadMAigId(node);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
      bVar = array_fetch(mAigBvar_t, bVarList, index1++);
      v = bVar.node;
      inputs[nInputs++] = v;
    }
  }
  Ntk_NetworkForEachPseudoInput(network, gen, node) {
    mAigId = Ntk_NodeReadMAigId(node);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
      bVar = array_fetch(mAigBvar_t, bVarList, index1++);
      v = bVar.node;
      inputs[nInputs++] = v;
    }
  }

  t->cstates = cstates;
  t->nstates = nstates;
  t->inputs = inputs;

  maxCS /= bAigNodeSize;
  maxCS++;
  t->csize = maxCS;
  t->cobj = ALLOC(bAigEdge_t, maxCS);
  memset(t->cobj, 0, sizeof(bAigEdge_t)*maxCS);
  t->c2n = ALLOC(bAigEdge_t, maxCS);
  memset(t->c2n, 0, sizeof(bAigEdge_t)*maxCS);
  nLatches = t->nLatches;
  for(i=0; i<nLatches; i++) {
    v = t->cstates[i];
    t->c2n[SATnodeID(v)] = t->nstates[i];
  }
  memcpy(t->tstates, cstates, sizeof(bAigEdge_t)*t->nLatches);

  t->vinputs = ALLOC(int, t->nInputs);
  memset(t->vinputs, 0, sizeof(int)*t->nInputs);
  t->vtstates = ALLOC(int, t->nLatches);
  memset(t->vtstates, 0, sizeof(int)*t->nLatches);
  
  t->avgLits = 0;
  t->sum = 0;
  t->interval = 10;
  t->period = 100;
  array_free(latcharr);

  return(t);
}


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

  Synopsis    [Create AIG for invariant property.]

  Description [Create AIG for invariant property.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
bAigEdge_t
bAig_CreatebAigForInvariant(
        Ntk_Network_t *network,
        bAig_Manager_t *manager,
        Ctlsp_Formula_t *inv)
{
bAigEdge_t result, left, right;
st_table *nodeToMvfAigTable;
int nodeValue;
int check;    
char *nodeNameString;
char *nodeValueString;
Ntk_Node_t *node;
Var_Variable_t *nodeVar;
MvfAig_Function_t  *tmpMvfAig;


  if (inv == NIL(Ctlsp_Formula_t))      return mAig_NULL; 
  if (inv->type == Ctlsp_TRUE_c)        return mAig_One; 
  if (inv->type == Ctlsp_FALSE_c)       return mAig_Zero;

  assert(Ctlsp_isPropositionalFormula(inv));

  if (inv->type == Ctlsp_ID_c){
    nodeNameString  = Ctlsp_FormulaReadVariableName(inv);
    nodeValueString = Ctlsp_FormulaReadValueName(inv);
    node = Ntk_NetworkFindNodeByName(network, nodeNameString);
      
    if (node == NIL(Ntk_Node_t)) {
      fprintf(vis_stderr, "sat_inv error: Could not find node corresponding to the name\t %s\n", nodeNameString);
      return mAig_NULL;
    }

    nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
    if (nodeToMvfAigTable == NIL(st_table)){
      fprintf(vis_stderr, 
              "sat_inv error: please run build_partiton_maigs first");
      return mAig_NULL;
    }
    tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
    if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
      array_free(tmpMvfAig);
      tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
    }
      
    nodeVar = Ntk_NodeReadVariable(node);
    if (Var_VariableTestIsSymbolic(nodeVar)) {
      nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
      if ( nodeValue == -1 ) {
        fprintf(vis_stderr, 
                "Value specified in RHS is not in domain of variable\n");
        fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
        return mAig_NULL;
      }
    }
    else { 
      check = StringCheckIsInteger(nodeValueString, &nodeValue);
      if( check == 0 ) {
        fprintf(vis_stderr,"Illegal value in the RHS\n");
        fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
        return mAig_NULL;
      }
      if( check == 1 ) {
        fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
        fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
        return mAig_NULL;
      }
      if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
        fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
        fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
        return mAig_NULL;
      }
    }
    result = bAig_GetCanonical(manager,
              MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue));
    return result;
  }

  left = bAig_CreatebAigForInvariant(network, manager, inv->left);
  if (left == mAig_NULL){
    return mAig_NULL;
  }  
  right = bAig_CreatebAigForInvariant(network, manager, inv->right);

  if (right == mAig_NULL && inv->type ==Ctlsp_NOT_c ){
    return mAig_Not(left);
  }  
  else if(right == mAig_NULL) {
    return mAig_NULL;
  }

  switch(inv->type) {
    case Ctlsp_OR_c:
      result = mAig_Or(manager, left, right);
      break;
    case Ctlsp_AND_c:
      result = mAig_And(manager, left, right);
      break;
    case Ctlsp_THEN_c:
      result = mAig_Then(manager, left, right); 
      break;
    case Ctlsp_EQ_c:
      result = mAig_Eq(manager, left, right);
      break;
    case Ctlsp_XOR_c:
      result = mAig_Xor(manager, left, right);
      break;
    default:
      fail("Unexpected LTL type");
  }
  return result;

}

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

  Synopsis    [Compute AG.]

  Description [Compute AG.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
bAigCheckInvariantWithAG(
        bAigTransition_t *t,
        bAigEdge_t objective)
{
int included, returnFlag;
bAig_Manager_t *manager;
satManager_t *cm;
long frontierNodesBegin;

  manager = t->manager;
  bAigCleanUpDataFromPreviousExecution(t);

  /** This is for applying SAT-based AX operation **/
  objective = bAig_Not(objective);
  t->objective = objective;
  returnFlag = 0;

  while(1) {
    /** 
     * This function do nothing in the first iteration, 
     * since no frontier is provided at first.
     * Instead of frontier, we have complemented objective at first
     **/

    if(t->verbose > 1) 
      fprintf(vis_stdout, "** SAT_INV : %d'th pre-image is being computed\n", t->iteration+1);

    frontierNodesBegin = manager->nodesArraySize;
    if(t->iteration > 0) {
      bAigBuildObjectiveFromFrontierSet(t);
      if(t->frontier->num <= 1) {
        returnFlag = 1; /** property passed **/
        break;
      }
    }
    
    cm = bAigCirCUsInterfaceForAX(t);
    cm->frontierNodesBegin = frontierNodesBegin;

    t->allsat = cm;
  

    sat_CleanDatabase(cm);

    bAigMarkConeOfInfluenceForAX(t, cm);

    fflush(vis_stdout);

    bAig_ComputeAX(t);

    if(t->verbose > 1) {
      sat_ReportStatistics(cm, cm->each);
    }

    included = bAigInclusionTestOnInitialStates(t);
    if(included == 0) {
      returnFlag = 2; /** propoerty failed **/
    }

    /** reched to convergenece **/
    if(t->frontier->num <= 1) {
      returnFlag = 1; /** property passed **/
    }


    bAig_PostProcessForAX(t, cm);
    t->manager->nodesArraySize = frontierNodesBegin;
    t->allsat = 0;

    if(t->lifting) {
      sat_FreeManager(t->lifting);
      t->lifting = 0;
    }

    if(t->originalFrontier) {
      sat_ArrayFree(t->originalFrontier);
      t->originalFrontier = 0;
    }

    if(returnFlag) {
      break;
    }
    t->iteration++;
  } 

  if(t->verbose > 0) {
    fprintf(vis_stdout, "** SAT_INV : Total %d pre-image is computed\n", t->iteration+1);
  }

  sat_ArrayFree(t->frontier);
  t->frontier = 0;
  sat_ArrayFree(t->reached);
  t->reached = 0;

  fflush(vis_stdout);

  return(returnFlag);
}

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

  Synopsis    [Reduce the number of blocking clauses based on UNSAT core generation.]

  Description [Reduce the number of blocking clauses based on UNSAT core generation.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigReduceBlockingClauseWithUnsatCore(bAigTransition_t *t)
{
satArray_t *cnfArray;
satArray_t *coreArray;
satArray_t *rootArray;
satOption_t *option;
satManager_t *cm;
st_table *mappedTable;
char filename[1024];
int flag, i, size;
bAigEdge_t v, nv, *plit;

  cnfArray = sat_ArrayAlloc(1024);
  mappedTable = st_init_table(st_numcmp, st_numhash);

  sat_ArrayInsert(cnfArray, 0);
  cm = t->allsat;
  /** Collect CNF from frontier of previous run **/
  for(v = cm->frontierNodesBegin; v<cm->frontierNodesEnd; v+= satNodeSize) {
    if(!(SATflags(v) & IsCNFMask))      continue;
    size = SATnumLits(v);
    plit = (long*)SATfirstLit(v);
    for(i=0; i<size; i++, plit++) {
      nv = SATgetNode(*plit);
      sat_ArrayInsert(cnfArray, nv);
      nv = SATnormalNode(nv);
      SATflags(nv) |= VisitedMask;
    }
    sat_ArrayInsert(cnfArray, 0);
  }

  /** Collect transition function(AIG) for CNF translation **/
  rootArray = sat_ArrayAlloc(t->nLatches);
  for(i=0; i<t->nLatches; i++) {
    v = t->nstates[i];
    v = SATnormalNode(v);
    if(v>1 && (SATflags(v) & VisitedMask))
      sat_ArrayInsert(rootArray, v);
  }
  for(i=0; i<rootArray->num; i++) {
    v = rootArray->space[i];
    SATflags(v) &= ResetVisitedMask;
  }

  if(cm->maxNodesArraySize > t->manager->maxNodesArraySize) {
    t->manager->maxNodesArraySize = cm->maxNodesArraySize;
    t->manager->nameList   = REALLOC(char *, t->manager->nameList  , t->manager->maxNodesArraySize/bAigNodeSize);
    t->manager->bddIdArray = REALLOC(int ,   t->manager->bddIdArray  , t->manager->maxNodesArraySize/bAigNodeSize);
    t->manager->bddArray   = REALLOC(bdd_t *, t->manager->bddArray  , t->manager->maxNodesArraySize/bAigNodeSize);
  }
  t->manager->maxNodesArraySize = cm->maxNodesArraySize;
  t->manager->NodesArray = cm->nodesArray;
  bAig_CreateCNFFromAIG(t->manager, rootArray, cnfArray);
  sat_ArrayFree(rootArray);

  /** Collect all previous blocking clauses **/
  for(v = cm->frontierNodesEnd; v<cm->nodesArraySize; v+= satNodeSize) {
    if(!(SATflags(v) & IsCNFMask))      continue;
    if(!(SATflags(v) & IsBlockingMask)) continue;
    size = SATnumLits(v);
    plit = (long*)SATfirstLit(v);
    for(i=0; i<size; i++, plit++) {
      nv = SATgetNode(*plit);
      sat_ArrayInsert(cnfArray, nv);
    }
    sat_ArrayInsert(cnfArray, -v);
  }

  /** add objecitve into CNF instance **/
  sat_ArrayInsert(cnfArray, t->objective);
  sat_ArrayInsert(cnfArray, 0);

  option = sat_InitOption();

  if(t->verbose > 2) {
    sprintf(filename, "core%d.cnf", t->iteration);
    sat_WriteCNFFromArray(cnfArray, filename);
  }
  coreArray = sat_ArrayAlloc(1024);
  flag = sat_CNFMainWithArray(option, cnfArray, 1, coreArray, mappedTable);

  if(flag == SAT_SAT)   {
    sprintf(filename, "core%d.cnf", t->iteration);
    fprintf(stdout, "ERROR : this instance %s should be UNSAT\n", filename);
    sat_WriteCNFFromArray(cnfArray, filename);
  }

  for(i=0; i<coreArray->num; i++) {
    v = coreArray->space[i];
    if(st_lookup(mappedTable, (char *)v, &nv)) {
      /* If a clause is blocking clause then it is in the table **/
      SATflags(nv) |= InCoreMask;    
    }
    /**
    else {
      fprintf(stdout, "ERROR : the clause %ld should be in the mapping table\n", v);
    }
    **/
  }
  for(v=satNodeSize; v<cm->nodesArraySize; v+=satNodeSize) {
    if(!(SATflags(v) & IsCNFMask))
      continue;
    if(!(SATflags(v) & IsBlockingMask))
      continue;
    if(!(SATflags(v) & IsFrontierMask))
      continue;
    if((SATflags(v) & InCoreMask))
      continue;

    SATresetInUse(v);
    if(t->verbose > 4) {
      fprintf(vis_stdout, "NOTICE : deleted blocking clause\n");
      sat_PrintNode(cm, v);
    }
  }


  st_free_table(mappedTable);
  sat_ArrayFree(cnfArray);
  sat_ArrayFree(coreArray);
}

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

  Synopsis    [Check if the initial states are included in conjunction of block clauses.]

  Description [Check if the initial states are included in conjunction of block clauses. It is done by checking satisfiability of formula (I \wedge \neg B).
 If it is unsatisfiable then all the initial states are included in B.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
bAigInclusionTestOnInitialStates(bAigTransition_t *t)
{
satArray_t *cnfArray;
satOption_t *option;
char filename[1024];
int flag;

  if(t->inclusionInitial == 0)  return(1);

  cnfArray = bAigCreateCNFInstanceForInclusionTestOnInitialStates(t);
  option = sat_InitOption();

  if(t->verbose > 2) {
    sprintf(filename, "init%d.cnf", t->iteration);
    sat_WriteCNFFromArray(cnfArray, filename);
  }
  flag = sat_CNFMainWithArray(option, cnfArray, 0, 0, 0);
  sat_ArrayFree(cnfArray);

  if(flag == SAT_UNSAT) return(1);
  else                  return(0);

  return(1);
}

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

  Synopsis    [Create instance for initial states inclusion test]

  Description [Create instance for initial states inclusion test]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satArray_t *
bAigCreateCNFInstanceForInclusionTestOnInitialStates(bAigTransition_t *t)
{
satArray_t *cnfArray, *frontier;
satArray_t *andArr, *orArr, *fandArr, *clause;
satArray_t *rootArray;
bAigEdge_t v, cv, out, objective;
bAigEdge_t maxIndex;
long *space;
int i, j;
int nCls;

  maxIndex = 0;
  for(i=0; i<t->nLatches; i++) {
    v = t->cstates[i];
    if(maxIndex < v)    maxIndex = v;
  }
  maxIndex += bAigNodeSize;
 
  cnfArray = sat_ArrayAlloc(2048);
  andArr = sat_ArrayAlloc(1024);
  orArr = sat_ArrayAlloc(1024);
  fandArr = sat_ArrayAlloc(1024);
  clause = sat_ArrayAlloc(1024);
 
  nCls = 0;
  frontier = t->frontier; 
  sat_ArrayInsert(cnfArray, 0);
  for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
    if(*space <= 0) { /** 0 or -1 is seperator between clauses **/
      space++;
      i++;

      if(i >= frontier->num) {
        break;
      }

      fandArr->num = 0;
      andArr->num = 0;
      while(*space > 0) {
        sat_ArrayInsert(fandArr, *space);
        i++;
        space++;
      }
      i--;
      space--;


      for(j=0; j<fandArr->num; j++) {
        v = fandArr->space[j];
        sat_ArrayInsert(andArr, v);
      }

      out = maxIndex;
      maxIndex += bAigNodeSize;
      sat_ArrayInsert(orArr, out);

      for(j=0; j<andArr->num; j++) {
        v = andArr->space[j];
        sat_ArrayInsert(cnfArray, SATnot(v));
        sat_ArrayInsert(cnfArray, SATnot(out));
        sat_ArrayInsert(cnfArray, -1); /** seperator **/
        nCls++;
      }

      for(j=0; j<andArr->num; j++) {
        v = andArr->space[j];
        sat_ArrayInsert(cnfArray, v);
      }
      sat_ArrayInsert(cnfArray, out);
      sat_ArrayInsert(cnfArray, -1);
      nCls++;
    }
  }

  objective = maxIndex;
  maxIndex += bAigNodeSize;
  for(i=0; i<orArr->num; i++) {
    v = orArr->space[i];
    sat_ArrayInsert(cnfArray, SATnot(v));
    sat_ArrayInsert(cnfArray, objective);
    sat_ArrayInsert(cnfArray, -1);
    nCls++;
  }
  for(i=0; i<orArr->num; i++) {
    v = orArr->space[i];
    sat_ArrayInsert(cnfArray, v);
  }

  sat_ArrayInsert(cnfArray, SATnot(objective));

  sat_ArrayInsert(cnfArray, -1);
  nCls++;

  /** assert objective **/
  sat_ArrayInsert(cnfArray, objective);
  sat_ArrayInsert(cnfArray, -1);
  nCls++;

  sat_ArrayFree(andArr);
  sat_ArrayFree(orArr);
  sat_ArrayFree(fandArr);
  sat_ArrayFree(clause);


  /** Collect AIG for CNF translation **/
  rootArray = sat_ArrayAlloc(t->nLatches);
  for(i=0; i<t->nLatches; i++) {
    v = t->initials[i];
    if(v>1)
      sat_ArrayInsert(rootArray, v);
  }

  if(t->allsat->maxNodesArraySize > t->manager->maxNodesArraySize) {
    t->manager->maxNodesArraySize = t->allsat->maxNodesArraySize;
    t->manager->nameList   = REALLOC(char *, t->manager->nameList  , t->manager->maxNodesArraySize/bAigNodeSize);
    t->manager->bddIdArray = REALLOC(int ,   t->manager->bddIdArray  , t->manager->maxNodesArraySize/bAigNodeSize);
    t->manager->bddArray   = REALLOC(bdd_t *, t->manager->bddArray  , t->manager->maxNodesArraySize/bAigNodeSize);
  }
  t->manager->maxNodesArraySize = t->allsat->maxNodesArraySize;
  t->manager->NodesArray = t->allsat->nodesArray;
  bAig_CreateCNFFromAIG(t->manager, rootArray, cnfArray);
  sat_ArrayFree(rootArray);

  /** 
   * connect AIG root and current state variable with equivalence
   * relation 
   * **/
  for(i=0; i<t->nLatches; i++) {
    v = t->initials[i];
    cv = t->cstates[i];
    if(v == 0) {
      sat_ArrayInsert(cnfArray, SATnot(cv));
      sat_ArrayInsert(cnfArray, -1);
    }
    else if(v == 1) {
      sat_ArrayInsert(cnfArray, cv);
      sat_ArrayInsert(cnfArray, -1);
    }
    else {
      sat_ArrayInsert(cnfArray, SATnot(v));
      sat_ArrayInsert(cnfArray, (cv));
      sat_ArrayInsert(cnfArray, -1);
      sat_ArrayInsert(cnfArray, (v));
      sat_ArrayInsert(cnfArray, SATnot(cv));
      sat_ArrayInsert(cnfArray, -1);
    }
  }

  return(cnfArray);
}

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

  Synopsis    [Create instance for AIG]

  Description [Create instance for AIG]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_CreateCNFFromAIG(
        bAig_Manager_t *manager,
        satArray_t *rootArray,
        satArray_t *cnfArray)
{
int i;
bAigEdge_t v, left, right;

  for(i=0; i<rootArray->num; i++) {
    v = rootArray->space[i];
    bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
  }

  for(v=bAigFirstNodeIndex ; v<manager->nodesArraySize; v+=bAigNodeSize){
    if(flags(v) & IsCNFMask) 
      continue;
    if(flags(v) & VisitedMask) {
      /** create CNF for this AIG **/
      left = leftChild(v);
      if(left == 2)
        continue;
      right = rightChild(v);

      sat_ArrayInsert(cnfArray, SATnot(left));
      sat_ArrayInsert(cnfArray, SATnot(right));
      sat_ArrayInsert(cnfArray, (v));
      sat_ArrayInsert(cnfArray, -1);
      sat_ArrayInsert(cnfArray, (left));
      sat_ArrayInsert(cnfArray, SATnot(v));
      sat_ArrayInsert(cnfArray, -1);
      sat_ArrayInsert(cnfArray, (right));
      sat_ArrayInsert(cnfArray, SATnot(v));
      sat_ArrayInsert(cnfArray, -1);
    }
  }

  for(i=0; i<rootArray->num; i++) {
    v = rootArray->space[i];
    bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
  }
  return;
}
                      


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

  Synopsis    [Compute AX based on SAT.]

  Description [Compute AX based on SAT.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_ComputeAX(bAigTransition_t *t)
{
satManager_t *cm;
long btime, etime;

  btime = util_cpu_time();

  cm = t->allsat;
  sat_PreProcessingForMixed(cm);

  if(cm->status == 0) {
    if(t->constrain)
      bAigCreateSatManagerForLifting(t);
    else 
      bAigCreateSatManagerForLiftingUnconstrained(t);
  /**
    **/
    bAigSolveAllSatWithLifting(t);
    if(t->iteration > 0 && t->reductionUsingUnsat)
      bAigReduceBlockingClauseWithUnsatCore(t);
  }

  sat_PostProcessing(cm);

  /** Copy to transition so that they can be used for next iteration **/
  t->reached = cm->reached;
  t->frontier = cm->frontier;
  cm->reached = 0;
  cm->frontier = 0;

  etime = util_cpu_time();
  cm->each->satTime = (double)(etime - btime) / 1000.0 ;
  fflush(vis_stdout);
  return;
  
}


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

  Synopsis    [Enumerate solution with lifting.]

  Description [Enumerate solution with lifting.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigSolveAllSatWithLifting(bAigTransition_t *t)
{
satManager_t *cm;
satLevel_t *d;
satOption_t *option;
int level;

  cm = t->allsat;

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

  option = cm->option;

  /**
  option->decisionHeuristic = 0;
  option->decisionHeuristic |= DVH_DECISION;
  **/

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

  while(1) {
    sat_PeriodicFunctions(cm);

    d = sat_MakeDecision(cm);

    if(d == 0)  {
      bAigBlockingClauseAnalysisBasedOnLifting(t, cm);

      if(cm->currentDecision == -1) {
        sat_Undo(cm, SATgetDecision(0));
        cm->status = SAT_UNSAT;
        return;
      }
      d = SATgetDecision(cm->currentDecision);
    }

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

      if(d->conflict == 0)      
        break;

      level = sat_ConflictAnalysis(cm, d);

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

      d = SATgetDecision(cm->currentDecision);
    }
  }

  return;
}

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

  Synopsis    [Apply minimization based on lifting and create blocking clause.]

  Description [Apply minimization based on lifting and create blocking clause.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigBlockingClauseAnalysisBasedOnLifting(bAigTransition_t *t, satManager_t *allsat)
{
satManager_t *cm;
satLevel_t *d;
satArray_t *clauseArray;
bAigEdge_t v, obj, blocked, fdaLit;
int objInverted, inverted;
int i, satisfied;
int value, tvalue;
int mLevel, bLevel;

  cm = allsat;
  for(i=0; i<t->nInputs; i++) {
    v = t->inputs[i];
    t->vinputs[i] = SATvalue(v);
  }

  SATcm = allsat;
  qsort(t->tstates, t->nLatches, sizeof(bAigEdge_t), levelCompare);

  for(i=0; i<t->nLatches; i++) {
    v = t->tstates[i];
    t->vtstates[i] = SATvalue(v);
  }

  /** cm is lifting instance from now on **/
  cm = t->lifting;

  obj = (bAigEdge_t )cm->obj->space[0];
  objInverted = SATisInverted(obj);
  obj = SATnormalNode(obj);

  d = sat_AllocLevel(cm);
  satisfied = 0;

  clauseArray = sat_ArrayAlloc(256);
  clauseArray->num = 0;

  /** 
   * Propagate primary input variable first, 
   * since  they can be freely qunatified
   **/
  for(i=0; i<t->nInputs; i++) {
    if(satisfied)       break;
    v = t->inputs[i];
    if(!(SATflags(v) & CoiMask))        continue;

    value = t->vinputs[i];
    if(value > 1)       continue;
    tvalue = SATvalue(v);
    if(tvalue < 2)      continue;

    SATvalue(v) = value;
    SATmakeImplied(v, d);
    sat_Enqueue(cm->queue, v);
    SATflags(v) |= InQueueMask;

    sat_ImplicationMain(cm, d);

    value = SATvalue(obj);
    if(value < 2)       satisfied = 1;  
  }

  /** 
   * Propagate current state variable to apply greedy minization.
   * Save candidates variable for lifting to clauseArray 
   **/
  if(satisfied == 0) {
    d = sat_AllocLevel(cm);
    for(i=0; i<t->nLatches; i++) {
      if(satisfied)     break;
      v = t->tstates[i];
      if(!(SATflags(v) & CoiMask))      continue;

      value = t->vtstates[i];
      if(value > 1)     continue; /** exceptional case **/
      tvalue = SATvalue(v);
  
      /** 
       * If a current state variable is implied by other state variable
       * sasignments then it is part of candidate variable
       **/
      sat_ArrayInsert(clauseArray, v^(!value));
  
      if(tvalue > 1) {
        SATvalue(v) = value;
        SATmakeImplied(v, d);
        sat_Enqueue(cm->queue, v);
        SATflags(v) |= InQueueMask;
    
        sat_ImplicationMain(cm, d);
        value = SATvalue(obj);
        if(value < 2)   satisfied = 1;  
      }
    }
  }

  value = SATvalue(obj);
  if(value > 1) {
    fprintf(stdout, "ERROR : Can't justify objective %ld\n", t->objective);
    exit(0);
  }

  if(clauseArray->num == 0) { 
    /** the objective is satified with primary input only **/
    sat_Backtrack(cm, 0);
    cm->currentDecision--;

    sat_Backtrack(allsat, 0);
    allsat->currentDecision--;
    return;
  }


  bAigCollectAntecdentOfObjective(t, cm, t->objective, clauseArray);

  if(clauseArray->num == 0) { 
    /** the objective is satified with primary input only **/
    fprintf(stdout, "ERROR : This might be the bug after greedy heuristic\n");
    sat_Backtrack(cm, 0);
    cm->currentDecision--;

    return;
  }

  sat_Backtrack(cm, 0);
  d = SATgetDecision(cm->currentDecision);
  sat_Undo(cm, d);
  cm->currentDecision--;

  /**
  bAigMinimizationBasedOnLifting(t, t->objective, clauseArray);
  **/
  if(t->disableLifting == 0)
    bAigMinimizationBasedOnLiftingAllAtOnce(t, t->objective, clauseArray);

  if(clauseArray->num == 0) { 
    /** the objective is satified with primary input only **/
    /**
    fprintf(stdout, "ERROR : This might be the bug after lifting\n");
    **/

    if(cm->currentDecision >= 0) {
      sat_Backtrack(cm, 0);
      cm->currentDecision--;
    }

    sat_Backtrack(allsat, 0);
    allsat->currentDecision--;

    return;
  }

  /** operation on all sat instance **/
  cm = t->allsat;

  mLevel = 0;
  for(i=0; i<clauseArray->num; i++) {
    v = clauseArray->space[i];
    v = SATnormalNode(v);
    if(mLevel < SATlevel(v))
      mLevel = SATlevel(v);
  }

  blocked = sat_AddBlockingClause(cm, clauseArray);
  SATflags(blocked) |= IsFrontierMask;

  if(t->verbose > 3)
    sat_PrintNode(cm, blocked);

  sat_Backtrack(cm, mLevel);
  d = SATgetDecision(cm->currentDecision);

  if(t->verbose > 3) {
    qsort(clauseArray->space, clauseArray->num, sizeof(long), indexCompare);
    for(i=0; i<clauseArray->num; i++) {
      fprintf(stdout, "%ld ", clauseArray->space[i]);
    }
    fprintf(stdout, "\n");
  }

  if(bAigCheckExistenceOfUIP(cm, clauseArray, mLevel, &fdaLit, &bLevel)) {
    sat_Backtrack(cm, bLevel);

    if(SATlevel(fdaLit) == 0) {
      sat_Backtrack(cm, 0);
      cm->currentDecision = -1;
      sat_ArrayFree(clauseArray);
      return;
    }

    d = SATgetDecision(cm->currentDecision);
    inverted = SATisInverted(fdaLit);
    fdaLit = SATnormalNode(fdaLit);
    SATante(fdaLit) = blocked;
    SATvalue(fdaLit) = inverted;
    SATmakeImplied(fdaLit, d);
    
    if((SATflags(fdaLit) & InQueueMask)  == 0) {
      sat_Enqueue(cm->queue, fdaLit);
      SATflags(fdaLit) |= InQueueMask;
    }
  }
  else {
    d->conflict = blocked;
    sat_ConflictAnalysisWithBlockingClause(cm, d);
  }

  sat_ArrayFree(clauseArray);
  return;
}

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

  Synopsis    [Apply minization based on checking antecedent of objective.]

  Description [Apply minization based on checking antecedent of objective.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
bAigCheckExistenceOfUIP(
        satManager_t *cm, 
        satArray_t *clauseArray, 
        int mLevel, 
        bAigEdge_t *fdaLit, 
        int *bLevel)
{
int i, nLit, level;
int uipFlag;
bAigEdge_t v, ante;

  nLit = 0;
  *bLevel = 0;
  *fdaLit = 0;
  uipFlag = 0;
  for(i=0; i<clauseArray->num; i++) {
    v = clauseArray->space[i];
    v = SATnormalNode(v);
    level = SATlevel(v);
    if(level == mLevel) {
      nLit++;
      if(nLit > 1)
        break;

      ante = SATante(v);
      if(ante == 0) {
        uipFlag = 1;
        *fdaLit = clauseArray->space[i];
      }
    }
    else if(*bLevel < level)
      *bLevel = level;
  }

  if(nLit > 1)
    uipFlag = 0;

  if(uipFlag)   return(1);
  else          return(0);
}

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

  Synopsis    [Apply minization based on checking antecedent of objective.]

  Description [Apply minization based on checking antecedent of objective.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigMinimizationBasedOnLifting(
        bAigTransition_t *t, 
        bAigEdge_t obj,
        satArray_t *orderArray)
{
satManager_t *allsat, *cm;
satLevel_t *d;
satArray_t *tmpArray;
satArray_t *notLiftableArray;
bAigEdge_t v, tv, *plit;
bAigEdge_t lastNode, lastLit, ante;
int inverted, inserted;
int tvalue, value, bLevel;
int i, j, size;

  cm = t->lifting;
  allsat = t->allsat;
  /** 
   * This is for incremental SAT to identified objective dependent conflict
   * clauses
   **/
  cm->option->includeLevelZeroLiteral = 1;
  lastLit = cm->literals->last-cm->literals->begin;
  lastNode = cm->nodesArraySize;

  /** 
   * Make level 0 implication  
   * 1. Primary input since they are not the target of lifting
   * 2. Unit and pure literals..
   * 3. Complemented objective
   **/
  d = sat_AllocLevel(cm);
  for(i=0; i<t->nInputs; i++) {
    v = t->inputs[i];
    if(!(SATflags(v) & CoiMask))        continue;
    value = t->vinputs[i];

    SATvalue(v) = value;
    SATmakeImplied(v, d);
    sat_Enqueue(cm->queue, v);
    SATflags(v) |= InQueueMask;

  }
  sat_ImplyArray(cm, d, cm->assertion);
  sat_ImplyArray(cm, d, cm->unitLits);
  sat_ImplyArray(cm, d, cm->pureLits);
  sat_ImplyArray(cm, d, cm->auxObj);
  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);

  value = SATisInverted(obj);
  v = SATnormalNode(obj);
  SATvalue(v) = value;
  SATmakeImplied(v, d);
  if((SATflags(v) & InQueueMask) == 0) {
    sat_Enqueue(cm->queue, v);
    SATflags(v) |= InQueueMask;
  }
  sat_ImplicationMain(cm, d);

  /** Apply lifting **/
  for(i=0; i<orderArray->num; i++) {
    cm->status = 0;

    /** check liftability of i'th variable on order array */

    tv = orderArray->space[i];
    v = SATnormalNode(tv);
    value = SATvalue(v);
    if(value < 2) { /** implied by other decisions */
      continue;
    }
    value = !SATisInverted(tv);
    SATvalue(v) = value;

    d = sat_AllocLevel(cm);

    SATmakeImplied(v, d);
    if((SATflags(v) & InQueueMask) == 0) {
      sat_Enqueue(cm->queue, v);
      SATflags(v) |= InQueueMask;
    }
    sat_ImplicationMain(cm, d);
  }

  /** check liftability of i'th variable on order array */
  notLiftableArray = sat_ArrayAlloc(orderArray->num);
  for(i=orderArray->num-1; i>=0; i--) {
      /** to identify previous decision **/
    while(1) {
      if(i<0) break;
      tv = orderArray->space[i];
      v = SATnormalNode(tv);
      value = SATvalue(v);
      ante = SATante(v);
      if(ante) { /** implied by other decisions */
        tvalue = !SATisInverted(tv);
        if(tvalue == value)
          sat_ArrayInsert(notLiftableArray, tv);
        i--;
        continue;
      }
      else { /** decision variable **/
        sat_Backtrack(cm, SATlevel(v)-1);
        break;
      }
    }
    if(i<0)     break;

    bLevel = cm->currentDecision;

    tv = orderArray->space[i];
    value = SATisInverted(tv); /** assign complemented value **/
    SATvalue(v) = value;

    d = sat_AllocLevel(cm);
    SATmakeImplied(v, d);
    if((SATflags(v) & InQueueMask) == 0) {
      sat_Enqueue(cm->queue, v);
      SATflags(v) |= InQueueMask;
    }
    sat_ImplicationMain(cm, d);

    if(d->conflict) { /** the variable can be lifted **/
      sat_Backtrack(cm, bLevel);
      continue;
    }

    for(j=0; j<notLiftableArray->num; j++) {
      v = notLiftableArray->space[j];
      value = !SATisInverted(v);
      v = SATnormalNode(v);
      tvalue = SATvalue(v);
      if(tvalue < 2 && tvalue != value) {
        /** the variable can be lifted **/
        sat_Backtrack(cm, bLevel);
        d->conflict = v;
        continue;
      }
      SATvalue(v) = value;
      SATmakeImplied(v, d);
      if((SATflags(v) & InQueueMask) == 0) {
        sat_Enqueue(cm->queue, v);
        SATflags(v) |= InQueueMask;
      }
      sat_ImplicationMain(cm, d);
      if(d->conflict) { /** the variable can be lifted **/
        break;
      }
    }

    if(d->conflict) { /** the variable can be lifted **/
      sat_Backtrack(cm, bLevel);
      continue;
    }

    bAigSolverForLifting(cm, cm->currentDecision); /** Need further decision **/
    /** There is a case that the implication queue is not empty **/
    sat_CleanImplicationQueue(cm);
    if(cm->status == SAT_SAT) {
      sat_ArrayInsert(notLiftableArray, tv); 
    }
    sat_Backtrack(cm, bLevel);
  }

  memcpy(orderArray->space, notLiftableArray->space, sizeof(long)*notLiftableArray->num);
  orderArray->num = notLiftableArray->num;
  sat_ArrayFree(notLiftableArray);

  sat_Backtrack(cm, 0);
  d = SATgetDecision(cm->currentDecision);
  sat_Undo(cm, d);
  cm->currentDecision--;
  cm->status = 0;


  /** Forward clauses from lifting process to allsat process **/
  /** Need to review this code **/
  tmpArray = sat_ArrayAlloc(64);
  for(i=lastNode; i<cm->nodesArraySize; i+=satNodeSize) {
    size = SATnumLits(i);
    plit = (long*)SATfirstLit(i);
    inserted = 0;
    tmpArray->num = 0;
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      inverted = SATisInverted(v);
      v = SATnormalNode(v);
      value = (allsat->nodesArray[v+satValue]) ;
      value = value ^ inverted;
      /** To check if the clause is safe to add allsat instance **/
      if(value > 0)
        inserted = 1;
      sat_ArrayInsert(tmpArray, v^(!inverted));
    }
    if(inserted)
      sat_AddConflictClause(allsat, tmpArray, 0);
  }
  sat_ArrayFree(tmpArray);

  return;
}

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

  Synopsis    [Apply minization based on checking antecedent of objective.]

  Description [Apply minization based on checking antecedent of objective.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigMinimizationBasedOnLiftingAllAtOnce(
        bAigTransition_t *t, 
        bAigEdge_t obj,
        satArray_t *orderArray)
{
satManager_t *allsat, *cm;
satLevel_t *d;
satArray_t *implied;
satArray_t *notLiftableArray;
bAigEdge_t v, tv;
bAigEdge_t lastNode, lastLit;
long *space;
int value;
int i, j, size, num;

  cm = t->lifting;
  allsat = t->allsat;
  /** 
   * This is for incremental SAT to identified objective dependent conflict
   * clauses
   **/
  cm->option->includeLevelZeroLiteral = 1;
  lastLit = cm->literals->last-cm->literals->begin;
  lastNode = cm->nodesArraySize;

  /** 
   * Make level 0 implication  
   * 1. Primary input since they are not the target of lifting
   * 2. Unit and pure literals..
   * 3. Complemented objective
   **/
  d = sat_AllocLevel(cm);
  for(i=0; i<t->nInputs; i++) {
    v = t->inputs[i];
    if(!(SATflags(v) & CoiMask))        continue;
    value = t->vinputs[i];

    SATvalue(v) = value;
    SATmakeImplied(v, d);
    sat_Enqueue(cm->queue, v);
    SATflags(v) |= InQueueMask;

  }
  sat_ImplyArray(cm, d, cm->assertion);
  sat_ImplyArray(cm, d, cm->unitLits);
  sat_ImplyArray(cm, d, cm->pureLits);
  sat_ImplyArray(cm, d, cm->auxObj);
  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);

  value = SATisInverted(obj);
  v = SATnormalNode(obj);
  SATvalue(v) = value;
  SATmakeImplied(v, d);
  if((SATflags(v) & InQueueMask) == 0) {
    sat_Enqueue(cm->queue, v);
    SATflags(v) |= InQueueMask;
  }
  sat_ImplicationMain(cm, d);

  /** Apply lifting **/
  num = d->implied->num;
  notLiftableArray = sat_ArrayAlloc(orderArray->num);
  for(i=0; i<orderArray->num; i++) {
    cm->status = 0;
    d->conflict = 0;

    /** check liftability of i'th variable on order array */

    tv = orderArray->space[i];
    v = SATnormalNode(tv);
    value = SATisInverted(tv);
    SATvalue(v) = value;

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

    for(j=i+1; j<orderArray->num; j++) {
      v = orderArray->space[j];
      value = !SATisInverted(v);
      v = SATnormalNode(v);
      SATvalue(v) = value;
      SATmakeImplied(v, d);
      if((SATflags(v) & InQueueMask) == 0) {
        sat_Enqueue(cm->queue, v);
        SATflags(v) |= InQueueMask;
      }
    }

    for(j=0; j<notLiftableArray->num; j++) {
      v = notLiftableArray->space[j];
      value = !SATisInverted(v);
      v = SATnormalNode(v);
      SATvalue(v) = value;
      SATmakeImplied(v, d);
      if((SATflags(v) & InQueueMask) == 0) {
        sat_Enqueue(cm->queue, v);
        SATflags(v) |= InQueueMask;
      }
    }
    sat_ImplicationMain(cm, d);


    if(d->conflict == 0) {
      bAigSolverForLifting(cm, 0); /** Need further decision **/
    /** There is a case that the implication queue is not empty **/
      sat_CleanImplicationQueue(cm);
    }
    else  {
      cm->status = SAT_UNSAT;
    }

    if(cm->status == SAT_SAT) {
      sat_ArrayInsert(notLiftableArray, tv); 
      sat_Backtrack(cm, 0);
    }

    d = SATgetDecision(0);
    implied = d->implied;
    space = implied->space;
    size = implied->num;
    for(j=num; j<size; j++) {
      v = space[j];
  
      SATvalue(v) = 2;
      SATflags(v) &= ResetNewVisitedObjInQueueMask;
      SATante(v) = 0;
      SATante2(v) = 0;
      SATlevel(v) = -1;
    }
    implied->num = num;
    cm->currentDecision = 0;

  }

  memcpy(orderArray->space, notLiftableArray->space, sizeof(long)*notLiftableArray->num);
  orderArray->num = notLiftableArray->num;
  sat_ArrayFree(notLiftableArray);


  d = SATgetDecision(0);
  sat_Undo(cm, d);
  cm->status = 0;
  cm->currentDecision = -1;

#if 0
  /** Forward clauses from lifting process to allsat process **/
  /** Need to review this code **/
  tmpArray = sat_ArrayAlloc(64);
  for(i=lastNode; i<cm->nodesArraySize; i+=satNodeSize) {
    size = SATnumLits(i);
    plit = (long*)SATfirstLit(i);
    inserted = 0;
    tmpArray->num = 0;
    for(j=0; j<size; j++, plit++) {
      tv = SATgetNode(*plit);
      inverted = SATisInverted(tv);
      v = SATnormalNode(tv);
      value = (allsat->nodesArray[v+satValue]) ;
      value = value ^ inverted;
      /** To check if the clause is safe to add allsat instance **/
      if(value > 0)
        inserted = 1;
      sat_ArrayInsert(tmpArray, SATnot(tv));
    }
    if(inserted)
      sat_AddConflictClause(allsat, tmpArray, 0);
  }
  sat_ArrayFree(tmpArray);
#endif

  return;
}

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

  Synopsis    [SAT solver for lifting .]

  Description [SAT solver for lifting. ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigSolverForLifting(satManager_t *cm, int tLevel)
{
satLevel_t *d;
int level;

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

  while(1) {
    d = sat_MakeDecision(cm);

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

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

      if(d->conflict == 0)      
        break;

      level = sat_ConflictAnalysisForLifting(cm, d);

      if(cm->currentDecision <= -1) {
        cm->status = SAT_UNSAT;
        return;
      }

      d = SATgetDecision(cm->currentDecision);
    }
  }
  return;
}

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

  Synopsis    [Apply minization based on checking antecedent of objective.]

  Description [Apply minization based on checking antecedent of objective.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigCollectAntecdentOfObjective(
        bAigTransition_t *t, 
        satManager_t *cm, 
        bAigEdge_t obj, 
        satArray_t *clauseArray)
{
int i, value;
bAigEdge_t v;

  bAigCollectAntecdentOfObjectiveAux(cm, obj);

  clauseArray->num = 0;
  for(i=0; i<t->nLatches; i++) {
    v = t->tstates[i];
    if(SATflags(v) & VisitedMask) {
      value = t->vtstates[i];
      sat_ArrayInsert(clauseArray, v^(!value));
    }
  }
  /** 
   * We don't need to reset visited flags, since they will be reset by
   * backtracking 
   **/
}

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

  Synopsis    [Apply minization based on checking antecedent of objective.]

  Description [Apply minization based on checking antecedent of objective.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigCollectAntecdentOfObjectiveAux(satManager_t *cm, bAigEdge_t v)
{
int i, size, completeness;
int value, inverted;
bAigEdge_t ante, nv, *plit;

  if(v == 2)    
    return;

  v = SATnormalNode(v);
  if(SATflags(v) & VisitedMask)
    return;

  SATflags(v) |= VisitedMask;
  ante = SATante(v);
  if(ante == 0) 
    return;

  if(SATflags(ante) & IsCNFMask) {

    size = SATnumLits(ante);

    completeness = 1;
    for(i=0, plit=(bAigEdge_t*)SATfirstLit(ante); i<size; i++, plit++) {
      nv = SATgetNode(*plit);
      inverted = SATisInverted(nv);
      nv = SATnormalNode(nv);
      value = SATvalue(nv) ^ inverted;
      if(v == nv) {
        if(value == 0)  completeness = 0;
      }
      else {
        if(value == 1)  completeness = 0;
      }
    }
    if(completeness == 0) {
      fprintf(stdout, "ERROR : incomplete implication graph\n");
    }

    for(i=0, plit=(bAigEdge_t*)SATfirstLit(ante); i<size; i++, plit++) {
      nv = SATgetNode(*plit);
      nv = SATnormalNode(nv);
      if(SATflags(nv) & VisitedMask)
        continue;
      bAigCollectAntecdentOfObjectiveAux(cm, nv);
    }
  }
  else {
    bAigCollectAntecdentOfObjectiveAux(cm, ante);
    ante = SATante2(v);
    if(ante)
      bAigCollectAntecdentOfObjectiveAux(cm, ante);
  }

}

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

  Synopsis    [Create SAT manager for lifting.]

  Description [Create SAT manager for lifting.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigCreateSatManagerForLiftingUnconstrained(bAigTransition_t *t)
{
satManager_t *lifting, *allsat, *cm;
bAigEdge_t *lastLit;
satOption_t *option;
satLiteralDB_t *literals;
long objective;

  allsat = t->allsat;
  lifting = sat_InitManager(0);
  t->lifting = lifting;

  /** to add blocking clause to lifting instance, modify lastLit **/
  cm = allsat;
  lastLit = 0;
  
  /**  To copy circuit structure **/
  lifting->nodesArraySize = allsat->frontierNodesBegin;

  lifting->initNodesArraySize = lifting->nodesArraySize;
  lifting->maxNodesArraySize = lifting->nodesArraySize * 2;

  lifting->nodesArray = ALLOC(long, lifting->maxNodesArraySize);
  memcpy(lifting->nodesArray, allsat->nodesArray, sizeof(long) * lifting->nodesArraySize);

  lifting->HashTable = ALLOC(long, bAig_HashTableSize);
  memcpy(lifting->HashTable, allsat->HashTable, sizeof(long)*bAig_HashTableSize);

  /** allocate literal pool **/
  sat_AllocLiteralsDB(lifting);
  literals = lifting->literals;

  lifting->comment = ALLOC(char, 2);
  lifting->comment[0] = ' ';
  lifting->comment[1] = '\0';
  lifting->stdErr = allsat->stdErr;
  lifting->stdOut = allsat->stdOut;
  lifting->status = 0;
  lifting->orderedVariableArray = 0;
  lifting->unitLits = sat_ArrayAlloc(16);
  lifting->pureLits = sat_ArrayAlloc(16);
  lifting->option = 0;
  lifting->each = 0;
  lifting->decisionHead = 0;
  lifting->variableArray = 0;
  lifting->queue = 0;
  lifting->BDDQueue = 0;
  lifting->unusedAigQueue = 0;

  option = sat_InitOption();
  lifting->option = option;
  option->verbose = 0;

  /** this is important because of incrementality **/
  option->decisionHeuristic = 0;
  option->decisionHeuristic |= DVH_DECISION;

  lifting->each = sat_InitStatistics();

  if(t->originalFrontier || t->allsat->reached) {
    objective = bAigBuildComplementedObjectiveWithCNF(
          t, lifting, t->originalFrontier, t->allsat->reached);
    objective = SATnot(objective);
  }
  else {
    lifting->initNumVariables = lifting->nodesArraySize;
    if(lifting->variableArray == 0) {
      lifting->variableArray = ALLOC(satVariable_t, lifting->initNumVariables+1);
      memset(lifting->variableArray, 0, 
              sizeof(satVariable_t) * (lifting->initNumVariables+1));
    }
    sat_CleanDatabase(lifting);

    if(t->allsat->assertion) t->lifting->assertion = sat_ArrayDuplicate(t->allsat->assertion);
    if(t->allsat->auxObj)    t->lifting->auxObj = sat_ArrayDuplicate(t->allsat->auxObj);
    objective = allsat->obj->space[0];
    sat_MarkTransitiveFaninForNode(lifting, objective, CoiMask);
  }


  sat_PreProcessingForMixedNoCompact(lifting);

  if(lifting->obj)      sat_ArrayFree(lifting->obj);    
  lifting->obj = sat_ArrayAlloc(1);
  sat_ArrayInsert(lifting->obj, (objective));

  /* 
   * reset score of PI 
   * Since the scores of PI and current state variables are high than 
   * other variables because of blocking clauses that forwarded from
   * prevous image step.
  for(i=0; i<t->nInputs; i++) {
    v = t->inputs[i];
    var = lifting->variableArray[SATnodeID(v)];
    var.scores[0] = 0;
    var.scores[1] = 0;
  }
  for(i=0; i<t->nLatches; i++) {
    v = t->cstates[i];
    var = lifting->variableArray[SATnodeID(v)];
    var.scores[0] = 0;
    var.scores[1] = 0;
  }
   **/

  /** 
   * To apply greedy minimization, the objective is not asserted 
   * The complemented objective will be asserted during lifting
   * process
   **/


  lifting->currentDecision = -1;

}

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

  Synopsis    [Create SAT manager for lifting.]

  Description [Create SAT manager for lifting.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigCreateSatManagerForLifting(bAigTransition_t *t)
{
satManager_t *lifting, *allsat, *cm;
bAigEdge_t *lastLit, v;
satOption_t *option;
satLiteralDB_t *literals;
int size, dir;
int nCls, nLits, index;
long *space;

  allsat = t->allsat;
  lifting = sat_InitManager(0);
  t->lifting = lifting;

  /** to add blocking clause to lifting instance, modify lastLit **/
  cm = allsat;
  lastLit = 0;
  
  if(t->constrain) {
    /**
    if(allsat->nodesArraySize != allsat->frontierNodesEnd){
      v = allsat->frontierNodesEnd-satNodeSize;
      lastLit = SATfirstLit(v);
      lastLit += SATnumLits(v);
      lastLit++;
    }
    lifting->nodesArraySize = allsat->frontierNodesEnd;
    **/
    if(allsat->nodesArraySize != allsat->frontierNodesEnd){
      v = allsat->nodesArraySize-satNodeSize;
      lastLit = (bAigEdge_t *) SATfirstLit(v);
      lastLit += SATnumLits(v);
      lastLit++;
    }
    lifting->nodesArraySize = allsat->nodesArraySize;
  
  }
  else {
/**    
 *  To copy circuit, frontier, and all blocking clauses
 *    lifting->nodesArraySize = allsat->nodesArraySize; 
 **/
    /**  To copy circuit structure **/
    lifting->nodesArraySize = allsat->frontierNodesBegin;
  }

  /** 
   * We save the frontier SAT first in allsat instance and
   * blocking clauses geenrated from previous runs.
   **/
  lifting->initNodesArraySize = lifting->nodesArraySize;
  lifting->maxNodesArraySize = lifting->nodesArraySize * 2;

  lifting->nodesArray = ALLOC(long, lifting->maxNodesArraySize);
  memcpy(lifting->nodesArray, allsat->nodesArray, sizeof(long) * lifting->nodesArraySize);

  lifting->HashTable = ALLOC(long, bAig_HashTableSize);
  memcpy(lifting->HashTable, allsat->HashTable, sizeof(long)*bAig_HashTableSize);

  literals = ALLOC(satLiteralDB_t, 1);
  lifting->literals = literals;

  if(lastLit > 0) {
    size = lastLit - allsat->literals->begin;
  }
  else {
    size = 0;
  }

  if(size > 1) { /** there are clauses for objective **/
    literals->begin = ALLOC(long, size*4);
    literals->end = literals->begin + size*4;
    memcpy(literals->begin, allsat->literals->begin, sizeof(long)*size);
    literals->last = literals->begin + size;
    literals->initialSize = literals->begin+size-1;
  }
  else { /** there is no extra logic for objective **/
    size = 1024 * 1024;
    literals->begin = ALLOC(long, size);
    *(literals->begin) = 0;
    literals->last = literals->begin + 1;
    literals->end = literals->begin + size;
    literals->initialSize = literals->last;
  }

  lifting->initNumVariables = allsat->initNumVariables;
  lifting->initNumClauses = allsat->initNumClauses;
  lifting->initNumLiterals = allsat->initNumLiterals;
  lifting->comment = ALLOC(char, 2);
  lifting->comment[0] = ' ';
  lifting->comment[1] = '\0';
  lifting->stdErr = allsat->stdErr;
  lifting->stdOut = allsat->stdOut;
  lifting->status = 0;
  lifting->orderedVariableArray = 0;
  lifting->unitLits = sat_ArrayAlloc(16);
  lifting->pureLits = sat_ArrayAlloc(16);
  lifting->option = 0;
  lifting->each = 0;
  lifting->decisionHead = 0;
  lifting->variableArray = 0;
  lifting->queue = 0;
  lifting->BDDQueue = 0;
  lifting->unusedAigQueue = 0;

  option = sat_InitOption();
  lifting->option = option;
  option->verbose = 0;

  /** this is important because of incrementality **/
  option->decisionHeuristic = 0;
  option->decisionHeuristic |= DVH_DECISION;

  lifting->each = sat_InitStatistics();

  sat_CleanDatabase(lifting);

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

  cm = lifting;
  nCls = nLits = 0;
  for(space = literals->begin; space < literals->last; space++) {
    if(*space < 0) {
      v = -(*space);
      space++;
      SATfirstLit(v) = (long) space;
      index = 0;
      while(1) {
        if(*space < 0)  break;
        dir = SATgetDir(*space);
        nLits++;
        if(dir == -2){
          space++;
          index++;
          continue;
        }
        SATunsetWL(space);
        sat_AddWL(cm, v, index, dir);
        space++;
        index++;
      }
      nCls++;
    }
  }
  lifting->initNumClauses = nCls;
  lifting->initNumLiterals = nLits;

  if(allsat->assertion) lifting->assertion = sat_ArrayDuplicate(allsat->assertion);
  if(allsat->auxObj)    lifting->auxObj = sat_ArrayDuplicate(allsat->auxObj);

  bAigMarkConeOfInfluenceForAX(t, lifting);


  bAigPreProcessingForLiftingInstance(t, lifting) ;

  /* 
   * reset score of PI 
   * Since the scores of PI and current state variables are high than 
   * other variables because of blocking clauses that forwarded from
   * prevous image step.
  for(i=0; i<t->nInputs; i++) {
    v = t->inputs[i];
    var = lifting->variableArray[SATnodeID(v)];
    var.scores[0] = 0;
    var.scores[1] = 0;
  }
  for(i=0; i<t->nLatches; i++) {
    v = t->cstates[i];
    var = lifting->variableArray[SATnodeID(v)];
    var.scores[0] = 0;
    var.scores[1] = 0;
  }
   **/

  /** 
   * To apply greedy minimization, the objective is not asserted 
   * The complemented objective will be asserted during lifting
   * process
   **/

  if(lifting->obj)      sat_ArrayFree(lifting->obj);    
  lifting->obj = sat_ArrayDuplicate(allsat->obj);

  lifting->currentDecision = -1;

}
/**Function********************************************************************

  Synopsis    [ Pre-processing to run CirCUs with AIG and CNF]

  Description [ Pre-processing to run CirCUs with AIG and CNF]

  SideEffects [ One has to run sat_PostProcessing for AllSat enumeration after running CirCUs]

  SeeAlso     [ sat_PostProcessing ]

******************************************************************************/
void
bAigPreProcessingForLiftingInstance(bAigTransition_t *t, satManager_t *cm) 
{
satLevel_t *d;
int i;
long v;


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

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

  /** compact fanout of AIG node 
  sat_CompactFanout(cm);
  **/

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

  if(cm->option->allSatMode) {
    sat_RestoreFrontierClauses(cm);
    sat_RestoreBlockingClauses(cm);
  }

  /** Initial score **/
  sat_InitScoreForMixed(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;

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

  /** 
   * There is a case that circuit consists of single objective node 
   **/
  for(i=0; i<cm->pureLits->num; i++) {
    v = cm->pureLits->space[i];
    if(v == t->objective) {
      for(;i<cm->pureLits->num; i++) {
        cm->pureLits->space[i] = cm->pureLits->space[i+1];
      }
      cm->pureLits->num--;
      break;
    }
  }

  sat_ImplyArray(cm, d, cm->assertion);
  sat_ImplyArray(cm, d, cm->unitLits);
  sat_ImplyArray(cm, d, cm->pureLits);
  sat_ImplyArray(cm, d, cm->auxObj);
  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
  sat_ImplyArray(cm, d, cm->obj);

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

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

}

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

  Synopsis    [Post processing after computing AX.]

  Description [Free sat manager...]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_PostProcessForAX(bAigTransition_t *t, satManager_t *cm)
{
bAig_Manager_t *manager;

  manager = t->manager;
  if(cm->maxNodesArraySize > manager->maxNodesArraySize) {
    manager->maxNodesArraySize = cm->maxNodesArraySize;
    manager->nameList   = REALLOC(char *, manager->nameList  , manager->maxNodesArraySize/bAigNodeSize);
    manager->bddIdArray = REALLOC(int ,   manager->bddIdArray  , manager->maxNodesArraySize/bAigNodeSize);
    manager->bddArray   = REALLOC(bdd_t *, manager->bddArray  , manager->maxNodesArraySize/bAigNodeSize);
  }

  manager->maxNodesArraySize = cm->maxNodesArraySize;
  manager->NodesArray = cm->nodesArray;
  manager->literals = cm->literals;
  cm->literals->last = cm->literals->initialSize;

  cm->nodesArray = 0;
  cm->literals = 0;
  cm->HashTable = 0;

  sat_FreeManager(cm);

  /** reset objective for next iteration **/
  t->objective = 0; 
}

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

  Synopsis    [Mark cone of influence for AX.]

  Description [Mark cone of influence for objective and intermediate variable that are created for complement frontier.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigMarkConeOfInfluenceForAX(bAigTransition_t *t, satManager_t *cm)
{
satArray_t *arr;
int i;
bAigEdge_t v;

  sat_MarkTransitiveFaninForNode(cm, t->objective, CoiMask);

  if(t->tVariables) {
    arr = t->tVariables;
    for(i=0; i<arr->num; i++) {
      v = arr->space[i];
      SATflags(v) |= CoiMask;
    }
  }

  if(t->auxObj) {
    arr = t->auxObj;
    for(i=0; i<arr->num; i++) {
      v = arr->space[i];
      sat_MarkTransitiveFaninForNode(cm, v, CoiMask);
    }
  }

  if(t->objArr) {
    arr = t->objArr;
    for(i=0; i<arr->num; i++) {
      v = arr->space[i];
      sat_MarkTransitiveFaninForNode(cm, v, CoiMask);
    }
  }

}

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

  Synopsis    [Make interface for CirCUs to compute AX.]

  Description [Make interface for CirCUs to compute AX.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satManager_t *
bAigCirCUsInterfaceForAX(bAigTransition_t *t)
{
satManager_t *cm;
bAig_Manager_t *manager;
satOption_t *option;
int i;
bAigEdge_t v;

  manager = t->manager;
  cm = sat_InitManager(0);
  memset(cm, 0, sizeof(satManager_t));

  cm->nodesArraySize = manager->nodesArraySize;
  cm->initNodesArraySize = manager->nodesArraySize;
  cm->maxNodesArraySize = manager->maxNodesArraySize;
  cm->nodesArray = manager->NodesArray;
  cm->HashTable = manager->HashTable;
  cm->literals = manager->literals;
  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
  cm->initNumClauses = 0;
  cm->initNumLiterals = 0;
  cm->comment = ALLOC(char, 2);
  cm->comment[0] = ' ';
  cm->comment[1] = '\0';
  cm->stdErr = vis_stderr;
  cm->stdOut = vis_stdout;
  cm->status = 0;
  cm->orderedVariableArray = 0;
  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);
  cm->option = 0;
  cm->each = 0;
  cm->decisionHead = 0;
  cm->variableArray = 0;
  cm->queue = 0;
  cm->BDDQueue = 0;
  cm->unusedAigQueue = 0;

  option = sat_InitOption();
  cm->option = option;
  option->verbose = 0;

  cm->each = sat_InitStatistics();
  sat_AllocLiteralsDB(cm);

  cm->obj = sat_ArrayAlloc(1);
  sat_ArrayInsert(cm->obj, t->objective);

  if(t->auxObj && t->auxObj->num) {
    cm->auxObj = sat_ArrayAlloc(t->auxObj->num);
    for(i=0; i<t->auxObj->num; i++) {
      v = t->auxObj->space[i];
      sat_ArrayInsert(cm->auxObj, v);
    }
  }
  cm->option->allSatMode = 1;

  /** 
   * Copy to reachable states and frontier to satManager  
   * so that they can be used to build current instance. 
   **/
  cm->reached = t->reached;
  cm->frontier = t->frontier;
  t->reached = 0;
  t->frontier = 0;

  return(cm);

}

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

  Synopsis    [Build new objective from frontier set by complementing blocking cluases] 

  Description [Build new objective from frontier set by complementing blocking cluases, the frontier array of bAigTransition_t save the blocking clause as clause form. The structure of frontier array is as follows.
      clause seperator, literals in clause, clause seperator, ..., clause seperator ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
bAigEdge_t
bAigBuildObjectiveFromFrontierSet(bAigTransition_t *t)
{
mAig_Manager_t *manager;
satArray_t *frontier;
satArray_t *clause;
satArray_t *andArr, *orArr;
satArray_t *fandArr;
satArray_t *fArr;
int i, j, nCls, removeFlag;
int inverted;
long *space, index;
bAigEdge_t v, tv, out, objective;
  
  manager = t->manager;

  andArr = sat_ArrayAlloc(1024);
  fandArr = sat_ArrayAlloc(1024);
  clause = sat_ArrayAlloc(1024);

  if(t->coiStates == 0) 
    t->coiStates = ALLOC(bAigEdge_t, sizeof(bAigEdge_t) * t->csize);
  memset(t->coiStates, 0, sizeof(bAigEdge_t)*t->csize);

  if(t->tVariables) t->tVariables->num = 0;
  else              t->tVariables = sat_ArrayAlloc(1024);
  fArr = sat_ArrayAlloc(1024);
  orArr = t->tVariables;

  nCls = 0;
  frontier = t->frontier; 
  sat_ArrayInsert(fArr, 0);
  for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
    if(*space <= 0) { /** 0 or -1 is seperator between clauses **/
      space++;
      i++;

      if(i >= frontier->num) {
        break;
      }

      removeFlag = 0;
      fandArr->num = 0;
      andArr->num = 0;
      while(*space > 0) {
#if 0
        v = *space;
        inverted = SATisInverted(v);
        tv = SATnormalNode(v);
        index = SATnodeID(tv);
        if(index > t->csize) {
          fprintf(stdout, "ERROR : %ld is not current state variable\n", tv);
          exit(0);
        }
        v = t->c2n[index];
        v = v ^ (inverted);
        if(v == 0) {  /** skip **/
        }
        else if(v == 1)  /** trivially satisfied **/
          removeFlag = 1;
        else if(removeFlag == 0) {
          sat_ArrayInsert(andArr, v);
          t->coiStates[index] = 1;
        }
#endif

        sat_ArrayInsert(fandArr, *space);
        i++;
        space++;
      }
      i--;
      space--;


      removeFlag = 0;
      for(j=0; j<fandArr->num; j++) {
        v = fandArr->space[j];
        inverted = SATisInverted(v);
        tv = SATnormalNode(v);
        index = SATnodeID(tv);
        if(index > t->csize) {
          fprintf(stdout, "ERROR : %ld is not current state variable\n", tv);
          exit(0);
        }
        v = t->c2n[index];
        v = v ^ (inverted);

        if(t->verbose > 4)
          fprintf(stdout, "%ld(%ld) ",fandArr->space[j], v); 
        if(v == 0) {  /** skip **/
          andArr->space[j] = 0;
        }
        else if(v == 1)  /** trivially satisfied **/
          removeFlag = 1;
        else  {
          sat_ArrayInsert(andArr, v);
          t->coiStates[index] = 1;
        }
      }
      if(t->verbose > 4)
        fprintf(stdout, "\n");

      if(removeFlag)
        continue;

     
      if(t->verbose > 4) {
        fprintf(stdout, "%ld-> ", andArr->num);
        for(j=0; j<andArr->num; j++) {
          v = andArr->space[j];
          fprintf(stdout, "%ld ", v);
        }
        fprintf(stdout, "\n");
      }

      out = bAig_CreateNode(manager, 2, 2);
      sat_ArrayInsert(orArr, out);

      for(j=0; j<andArr->num; j++) {
        v = andArr->space[j];
        sat_ArrayInsert(fArr, SATnot(v));
        sat_ArrayInsert(fArr, SATnot(out));
        sat_ArrayInsert(fArr, -1); /** seperator **/
        nCls++;
      }

      for(j=0; j<andArr->num; j++) {
        v = andArr->space[j];
        sat_ArrayInsert(fArr, v);
      }
      sat_ArrayInsert(fArr, out);
      sat_ArrayInsert(fArr, -1);
      nCls++;
    }
  }

  objective = bAig_CreateNode(manager, 2, 2);
  for(i=0; i<orArr->num; i++) {
    v = orArr->space[i];
    sat_ArrayInsert(fArr, SATnot(v));
    sat_ArrayInsert(fArr, objective);
    sat_ArrayInsert(fArr, -1);
    nCls++;
  }
  for(i=0; i<orArr->num; i++) {
    v = orArr->space[i];
    sat_ArrayInsert(fArr, v);
  }

  sat_ArrayInsert(fArr, SATnot(objective));

  sat_ArrayInsert(fArr, -1);
  nCls++;

  if(orArr->num == 0) {
    fArr->num = 0;
  }

  if(t->verbose > 0) {
    fprintf(vis_stdout, "** SAT_INV : %ld number of frontier blocking clauses are processed\n", orArr->num);
    fprintf(vis_stdout, "** SAT_INV : %d number of clauses are added to build objective\n", nCls);
  }

  sat_ArrayFree(andArr);
  sat_ArrayFree(fandArr);
  sat_ArrayFree(clause);

  t->originalFrontier = frontier;
  t->frontier = fArr;
  t->objective = objective;

  if(t->objArr == 0) 
    t->objArr = sat_ArrayAlloc(t->nLatches);
  t->objArr->num = 0;
  for(i=0; i<t->csize; i++) {
    if(t->coiStates[i]) {
      sat_ArrayInsert(t->objArr, SATnormalNode(t->c2n[i]));
    }
  }


  return(objective);
}

bAigEdge_t
bAigBuildComplementedObjectiveWithCNF(
        bAigTransition_t *t, 
        satManager_t *cm,
        satArray_t *narr,
        satArray_t *carr)
{
satArray_t *clause;
satArray_t *andArr, *orArr;
satArray_t *fandArr;
satArray_t *fArr, *arr;
satArray_t *frontier;
int i, j, nCls, removeFlag;
int inverted;
long *space, index;
bAigEdge_t v, tv, out, objective;
bAigEdge_t obj1, obj2;
  
  andArr = sat_ArrayAlloc(1024);
  fandArr = sat_ArrayAlloc(1024);
  clause = sat_ArrayAlloc(1024);

  if(t->coiStates == 0) 
    t->coiStates = ALLOC(bAigEdge_t, sizeof(bAigEdge_t) * t->csize);
  memset(t->coiStates, 0, sizeof(bAigEdge_t)*t->csize);

  if(t->tVariables) t->tVariables->num = 0;
  else              t->tVariables = sat_ArrayAlloc(1024);
  fArr = sat_ArrayAlloc(1024);

  orArr =sat_ArrayAlloc(1024);

  sat_ArrayInsert(fArr, 0);
  nCls = 0;
  frontier = narr;


  if(frontier) {
  for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
    if(*space <= 0) { /** 0 or -1 is seperator between clauses **/
      space++;
      i++;

      if(i >= frontier->num) {
        break;
      }

      removeFlag = 0;
      fandArr->num = 0;
      andArr->num = 0;
      while(*space > 0) {
        sat_ArrayInsert(fandArr, *space);
        i++;
        space++;
      }
      i--;
      space--;


      removeFlag = 0;
      for(j=0; j<fandArr->num; j++) {
        v = fandArr->space[j];
        inverted = SATisInverted(v);
        tv = SATnormalNode(v);
        index = SATnodeID(tv);
        if(index > t->csize) {
          fprintf(stdout, "ERROR : %ld is not current state variable\n", tv);
          exit(0);
        }
        v = t->c2n[index];
        v = v ^ (inverted);

        if(t->verbose > 4)
          fprintf(stdout, "%ld(%ld) ",fandArr->space[j], v); 
        if(v == 0) {  /** skip **/
          andArr->space[j] = 0;
        }
        else if(v == 1)  /** trivially satisfied **/
          removeFlag = 1;
        else  {
          sat_ArrayInsert(andArr, v);
          t->coiStates[index] = 1;
        }
      }
      if(t->verbose > 4)
        fprintf(stdout, "\n");

      if(removeFlag)
        continue;

     
      if(t->verbose > 4) {
        fprintf(stdout, "%ld-> ", andArr->num);
        for(j=0; j<andArr->num; j++) {
          v = andArr->space[j];
          fprintf(stdout, "%ld ", v);
        }
        fprintf(stdout, "\n");
      }

      out = sat_CreateNode(cm, 2, 2);
      sat_ArrayInsert(orArr, out);
      sat_ArrayInsert(t->tVariables, out);

      for(j=0; j<andArr->num; j++) {
        v = andArr->space[j];
        sat_ArrayInsert(fArr, SATnot(v));
        sat_ArrayInsert(fArr, SATnot(out));
        sat_ArrayInsert(fArr, -1); /** seperator **/
        nCls++;
      }

      for(j=0; j<andArr->num; j++) {
        v = andArr->space[j];
        sat_ArrayInsert(fArr, v);
      }
      sat_ArrayInsert(fArr, out);
      sat_ArrayInsert(fArr, -1);
      nCls++;
    }
  }
  }

  obj1 = sat_CreateNode(cm, 2, 2);
  for(i=0; i<orArr->num; i++) {
    v = orArr->space[i];
    sat_ArrayInsert(fArr, SATnot(v));
    sat_ArrayInsert(fArr, obj1);
    sat_ArrayInsert(fArr, -1);
    nCls++;
  }
  for(i=0; i<orArr->num; i++) {
    v = orArr->space[i];
    sat_ArrayInsert(fArr, v);
  }

  sat_ArrayInsert(fArr, SATnot(obj1));

  sat_ArrayInsert(fArr, -1);
  nCls++;

#if 1
  frontier = carr;
  if(frontier) {
  for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
    if(*space <= 0) { /** 0 or -1 is seperator between clauses **/
      space++;
      i++;

      if(i >= frontier->num) {
        break;
      }

      fandArr->num = 0;
      andArr->num = 0;
      while(*space > 0) {
        sat_ArrayInsert(fandArr, *space);
        i++;
        space++;
      }
      i--;
      space--;


      if(t->verbose > 4) {
        fprintf(stdout, "%ld-> ", andArr->num);
        for(j=0; j<andArr->num; j++) {
          v = andArr->space[j];
          fprintf(stdout, "%ld ", v);
        }
        fprintf(stdout, "\n");
      }

      out = sat_CreateNode(cm, 2, 2);
      sat_ArrayInsert(orArr, out);
      sat_ArrayInsert(t->tVariables, out);

      for(j=0; j<andArr->num; j++) {
        v = andArr->space[j];
        sat_ArrayInsert(fArr, SATnot(v));
        sat_ArrayInsert(fArr, SATnot(out));
        sat_ArrayInsert(fArr, -1); /** seperator **/
        nCls++;
      }

      for(j=0; j<andArr->num; j++) {
        v = andArr->space[j];
        sat_ArrayInsert(fArr, v);
      }
      sat_ArrayInsert(fArr, out);
      sat_ArrayInsert(fArr, -1);
      nCls++;
    }
  }
  }

  obj2 = sat_CreateNode(cm, 2, 2);
  for(i=0; i<orArr->num; i++) {
    v = orArr->space[i];
    sat_ArrayInsert(fArr, SATnot(v));
    sat_ArrayInsert(fArr, obj2);
    sat_ArrayInsert(fArr, -1);
    nCls++;
  }
  for(i=0; i<orArr->num; i++) {
    v = orArr->space[i];
    sat_ArrayInsert(fArr, v);
  }

  sat_ArrayInsert(fArr, SATnot(obj2));

  sat_ArrayInsert(fArr, -1);
  nCls++;
  #endif

  sat_ArrayInsert(t->tVariables, obj1);
  sat_ArrayInsert(t->tVariables, obj2);
  objective = sat_CreateNode(cm, 2, 2);
  sat_ArrayInsert(fArr, SATnot(obj1));
  sat_ArrayInsert(fArr, SATnot(obj2));
  sat_ArrayInsert(fArr, objective);
  sat_ArrayInsert(fArr, -1);
  sat_ArrayInsert(fArr, (obj1));
  sat_ArrayInsert(fArr, SATnot(objective));
  sat_ArrayInsert(fArr, -1);
  sat_ArrayInsert(fArr, (obj2));
  sat_ArrayInsert(fArr, SATnot(objective));
  sat_ArrayInsert(fArr, -1);

  if(orArr->num == 0) {
    fArr->num = 0;
  }

  if(t->verbose > 0) {
    fprintf(vis_stdout, "** SAT_INV : %ld number of frontier blocking clauses are processed\n", orArr->num);
    fprintf(vis_stdout, "** SAT_INV : %d number of clauses are added to build objective\n", nCls);
  }

  sat_ArrayFree(andArr);
  sat_ArrayFree(fandArr);
  sat_ArrayFree(clause);

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


  if(t->allsat->assertion) t->lifting->assertion = sat_ArrayDuplicate(t->allsat->assertion);
  if(t->allsat->auxObj)    t->lifting->auxObj = sat_ArrayDuplicate(t->allsat->auxObj);

  sat_MarkTransitiveFaninForNode(cm, objective, CoiMask);

  for(i=0; i<t->csize; i++) {
    if(t->coiStates[i]) {
      sat_MarkTransitiveFaninForNode(cm, SATnormalNode(t->c2n[i]), CoiMask);
    }
  }

  if(t->tVariables) {
    arr = t->tVariables;
    for(i=0; i<arr->num; i++) {
      v = arr->space[i];
      SATflags(v) |= CoiMask;
    }
  }

  if(t->auxObj) {
    arr = t->auxObj;
    for(i=0; i<arr->num; i++) {
      v = arr->space[i];
      sat_MarkTransitiveFaninForNode(cm, v, CoiMask);
    }
  }
  return(objective);
}

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

  Synopsis    [Function to clean data of bAigTransition_t generated from previous execution]

  Description [Function to clean data of bAigTransition_t generated from previous execution]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigCleanUpDataFromPreviousExecution(bAigTransition_t *t)
{
  if(t->frontier) {
    sat_ArrayFree(t->frontier);
    t->frontier = 0;
  }
  if(t->reached) {
    sat_ArrayFree(t->reached);
    t->reached = 0;
  }

  t->objective = 0;
  t->iteration = 0;
  t->nBlocked = 0;
  t->sum = 0;
  t->avgLits = 0;

}
/**Function********************************************************************

  Synopsis    [Function to print information of bAigTransition_t]

  Description [Function to print information of bAigTransition_t]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAigPrintTransitionInfo(bAigTransition_t *t)
{
int i;

  fprintf(vis_stdout, "Transition relation information in terms of AIG\n");
  fprintf(vis_stdout, "objective : %ld\n", t->objective);
  fprintf(vis_stdout, "number of primary inputs : %d\n", t->nInputs);
  fprintf(vis_stdout, "number of states variables : %d\n", t->nLatches);

  fprintf(vis_stdout, "primary inputs :");
  for(i=0; i<t->nInputs; i++) {
    fprintf(vis_stdout, "%5ld ", t->inputs[i]);
    if((i+1)%10 == 0 && i > 0) 
      fprintf(vis_stdout, "\n                ");
  }
  fprintf(vis_stdout, "\n");

  fprintf(vis_stdout, "state variables :");
  for(i=0; i<t->nLatches; i++) {
    fprintf(vis_stdout, "%5ld(%5ld):%5ld ", 
            t->cstates[i], t->initials[i], t->nstates[i]);
    if((i+1)%3 == 0 && i > 0) 
      fprintf(vis_stdout, "\n                 ");
  }
  fprintf(vis_stdout, "\n");
}

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

  Synopsis    [Function to arrange node to the alphabetic order ]

  Description [Function to arrange node to the alphabetic order ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
nodenameCompare(
  const void * node1,
  const void * node2)
{
Ntk_Node_t *v1, *v2;
char *name1, *name2;

  v1 = *(Ntk_Node_t **)(node1);
  v2 = *(Ntk_Node_t **)(node2);
  name1 = Ntk_NodeReadName(v1);
  name2 = Ntk_NodeReadName(v2);
  
  return (strcmp(name1, name2));
} 

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

  Synopsis    [Function to check if given string is integer]

  Description [Function to check if given string is integer]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
StringCheckIsInteger(
  char *string,
  int *value)
{
  char *ptr;
  long l;
  
  l = strtol (string, &ptr, 0) ;
  if(*ptr != '\0')
    return 0;
  if ((l > MAXINT) || (l < -1 - MAXINT))
    return 1 ;
  *value = (int) l;
  return 2 ;
}

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

  Synopsis    [Function to check the deicison level of variable ]

  Description [Function to check the deicison level of variable ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
levelCompare(
  const void * node1,
  const void * node2)
{
  bAigEdge_t v1, v2;
  int l1, l2;

  v1 = *(bAigEdge_t *)(node1);
  v2 = *(bAigEdge_t *)(node2);
  l1 = SATcm->variableArray[SATnodeID(v1)].level;
  l2 = SATcm->variableArray[SATnodeID(v2)].level;
  
  if(l1 == l2)  return(v1 > v2);
  return (l1 > l2);
} 
/**Function********************************************************************

  Synopsis    [Function to check the index ]

  Description [Function to check the index ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
indexCompare(
  const void * node1,
  const void * node2)
{
  bAigEdge_t v1, v2;

  v1 = *(bAigEdge_t *)(node1);
  v2 = *(bAigEdge_t *)(node2);
  
  return(v1 > v2);
}