src/baig/baigAllSat.c

Go to the documentation of this file.

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

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

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


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


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;

}

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

  objective = bAig_Not(objective);
  t->objective = objective;
  returnFlag = 0;

  while(1) {
    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; 
        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; 
    }

    if(t->frontier->num <= 1) {
      returnFlag = 1; 
    }


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

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

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

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

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

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

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

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

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


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

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

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


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

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


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;

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

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

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

  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; 
      tvalue = SATvalue(v);
  
      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) { 
    sat_Backtrack(cm, 0);
    cm->currentDecision--;

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


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

  if(clauseArray->num == 0) { 
    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--;

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

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

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

    return;
  }

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

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

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;
  cm->option->includeLevelZeroLiteral = 1;
  lastLit = cm->literals->last-cm->literals->begin;
  lastNode = cm->nodesArraySize;

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

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

    tv = orderArray->space[i];
    v = SATnormalNode(tv);
    value = SATvalue(v);
    if(value < 2) { 
      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);
  }

  notLiftableArray = sat_ArrayAlloc(orderArray->num);
  for(i=orderArray->num-1; i>=0; i--) {
    while(1) {
      if(i<0) break;
      tv = orderArray->space[i];
      v = SATnormalNode(tv);
      value = SATvalue(v);
      ante = SATante(v);
      if(ante) { 
        tvalue = !SATisInverted(tv);
        if(tvalue == value)
          sat_ArrayInsert(notLiftableArray, tv);
        i--;
        continue;
      }
      else { 
        sat_Backtrack(cm, SATlevel(v)-1);
        break;
      }
    }
    if(i<0)     break;

    bLevel = cm->currentDecision;

    tv = orderArray->space[i];
    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);

    if(d->conflict) { 
      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) {
        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) { 
        break;
      }
    }

    if(d->conflict) { 
      sat_Backtrack(cm, bLevel);
      continue;
    }

    bAigSolverForLifting(cm, cm->currentDecision); 
    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;


  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;
      if(value > 0)
        inserted = 1;
      sat_ArrayInsert(tmpArray, v^(!inverted));
    }
    if(inserted)
      sat_AddConflictClause(allsat, tmpArray, 0);
  }
  sat_ArrayFree(tmpArray);

  return;
}

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;
  cm->option->includeLevelZeroLiteral = 1;
  lastLit = cm->literals->last-cm->literals->begin;
  lastNode = cm->nodesArraySize;

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

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

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

  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;
      if(value > 0)
        inserted = 1;
      sat_ArrayInsert(tmpArray, SATnot(tv));
    }
    if(inserted)
      sat_AddConflictClause(allsat, tmpArray, 0);
  }
  sat_ArrayFree(tmpArray);
#endif

  return;
}

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

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

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

}

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;

  cm = allsat;
  lastLit = 0;
  
  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);

  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;

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

  lifting->currentDecision = -1;

}

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;

  cm = allsat;
  lastLit = 0;
  
  if(t->constrain) {
    if(allsat->nodesArraySize != allsat->frontierNodesEnd){
      v = allsat->nodesArraySize-satNodeSize;
      lastLit = (bAigEdge_t *) SATfirstLit(v);
      lastLit += SATnumLits(v);
      lastLit++;
    }
    lifting->nodesArraySize = allsat->nodesArraySize;
  
  }
  else {
    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);

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

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

  if(size > 1) { 
    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 { 
    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;

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

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

  lifting->currentDecision = -1;

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


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

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

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

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

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

  sat_InitScoreForMixed(cm);

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

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

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

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

  d = sat_AllocLevel(cm);

  sat_ApplyForcedAssignmentMain(cm, d);

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

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

}

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

  t->objective = 0; 
}

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

}

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;

  cm->reached = t->reached;
  cm->frontier = t->frontier;
  t->reached = 0;
  t->frontier = 0;

  return(cm);

}

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) { 
      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) {  
        }
        else if(v == 1)  
          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) {  
          andArr->space[j] = 0;
        }
        else if(v == 1)  
          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); 
        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) { 
      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) {  
          andArr->space[j] = 0;
        }
        else if(v == 1)  
          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); 
        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) { 
      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); 
        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);
}

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;

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

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

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

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);
} 
static int
indexCompare(
  const void * node1,
  const void * node2)
{
  bAigEdge_t v1, v2;

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