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

  FileName    [satCore.c]

  PackageName [sat]

  Synopsis    [Routines for UNSAT core generation,both CNF-based and Aig-based
	      UNSAT core generetions are available]

  Author      [Bing Li]

  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 "satInt.h"
#include "puresatInt.h"

static char rcsid[] UNUSED = "$Id: satCore.c,v 1.20 2009/04/12 00:14:11 fabio Exp $";

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

#define CONFLICT 1
#define NO_CONFLICT 2
/**AutomaticStart*************************************************************/

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

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

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

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

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


/*---------------------------------------------------------------------------*/

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


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

  Synopsis    [Print literals of given clauses]

  Description [Print literals of given clauses]

  SideEffects [ ]

  SeeAlso     [ ]

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

void
sat_PrintClauseLits(satManager_t * cm,
		       long concl)
{
  long i, node, var_idx,*lit;

  for(i=0, lit = (long*)SATfirstLit(concl); i<SATnumLits(concl);i++, lit++){
    node = SATgetNode(*lit);
    var_idx = SATnodeID(node);
    if(SATisInverted(node))
      fprintf(vis_stdout,"%ld ", -var_idx);
    else
      fprintf(vis_stdout,"%ld ",var_idx);
  }
  fprintf(vis_stdout,"0\n");
}


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

  Synopsis    [Print literals of given clauses to a certain file for UNSAT
	       core generation]

  Description [Print literals of given clauses to a certain file for UNSAT
	       core generation]

  SideEffects [ ]

  SeeAlso     [ ]

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

void
sat_PrintClauseLitsForCore(satManager_t * cm,
		       long concl,
		       FILE *fp)
{
  long i, node, var_idx,*lit, cls_idx;

  lit = (long*)SATfirstLit(concl);
  cls_idx = -(*(lit-1));

  if(fp) {
    /** cls_idx -= cm->numOfVar * satNodeSize; **/
    cls_idx -= cm->initNumVariables * satNodeSize;
    /**cls idx starts from 0 **/
    cls_idx = cls_idx/satNodeSize - 1;
    fprintf(fp,"#clause index:%ld\n",cls_idx);
    for(i=0, lit = (long*)SATfirstLit(concl); i<SATnumLits(concl);i++, lit++){
      node = SATgetNode(*lit);
      var_idx = SATnodeID(node);
      if(SATisInverted(node))
	fprintf(fp, "%ld ", -var_idx);
      else
	fprintf(fp, "%ld ",var_idx);
    }
    fprintf(fp, "0\n");
  }
  else {
    if(cm->clauseIndexInCore == 0)
      cm->clauseIndexInCore = sat_ArrayAlloc(1024);
    sat_ArrayInsert(cm->clauseIndexInCore, cls_idx);
  }

}


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

  Synopsis    [Recursively generate the UNSAT core]

  Description [Recursively generate the UNSAT core]

  SideEffects [ ]

  SeeAlso     [ ]

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

void
sat_GenerateCoreRecur(satManager_t * cm,
		 long concl,
		 FILE *fp,
		 int * count)
{
  int j;
  long tmp;
  satArray_t * dep;

  if(!(SATflags(concl)&NewMask)){
    SATflags(concl)|=NewMask;
    /** Not Conflict **/
    if(!(SATflags(concl)& IsConflictMask)){
      (*count)++;
      sat_PrintClauseLitsForCore(cm,concl,fp);
    }
    /** is CONFLICT **/
    else{
      if(!st_lookup(cm->dependenceTable,(char *)concl, &dep)){
	fprintf(cm->stdOut,"%ld is not in depe table\n",concl);
	exit(0);
      }
      else{
	for(j=0;j<dep->num; j++){
	  tmp = dep->space[j];
	  sat_GenerateCoreRecur(cm, tmp, fp, count);
	}
      }
    }
  }/**  if(!(SATflags(concl)&NewMask)){ **/
}



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

  Synopsis    [Generate dependence clauses for the conflict]

  Description [Generate dependence clauses for the conflict]

  SideEffects [ ]

  SeeAlso     [ ]

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

void
sat_GetDependence(satManager_t * cm, long concl, satArray_t* dep)
{
long node, *lit, ante;
int i;

  for(i=0, lit = (long*)SATfirstLit(concl); i<SATnumLits(concl);i++, lit++){
    node = SATgetNode(*lit);
    node = SATnormalNode(node);
    ante = SATante(node);
    if(ante==0){
      if(!st_lookup(cm->anteTable, (char *)node, &ante)){
	fprintf(vis_stdout,"ante = 0 and is not in anteTable %ld\n",node);
	exit(0);
      }
    }
    if(!(SATflags(ante)&NewMask)){
      SATflags(ante)|=NewMask;
      sat_ArrayInsert(dep,ante);
      sat_GetDependence(cm,ante,dep);
    }
  }
}

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

  Synopsis    [Conflict Core Generation]

  Description [Conflict Core Generation]

  SideEffects [ ]

  SeeAlso     [ ]

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

void
sat_GenerateCore(satManager_t * cm)
{
  int j, tmp,value;
  long *lit, node, concl, i;
  satArray_t * dep;
  FILE *fp = cm->fp;
  int  count, inverted;
  st_generator *stGen;
  satArray_t* tmpdep = sat_ArrayAlloc(1);
  satLevel_t * d;

  cm->status = 0;
  count = 0;
  d = SATgetDecision(0);
  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize){
    node = i;
    if((SATflags(node)&IsCNFMask)&&(SATnumLits(node)==1)){
      lit = (long*)SATfirstLit(node);
      tmp = SATgetNode(*lit);
      inverted = SATisInverted(tmp);
      tmp = SATnormalNode(tmp);


      value = !inverted;
      if(SATvalue(tmp) < 2)	{
	if(SATvalue(tmp) == value)	continue;
	else {
	  cm->status = SAT_UNSAT;
	  d->conflict = node;
	  break;
	}
      }

      SATvalue(tmp) = !inverted;
      SATmakeImplied(tmp, d);
      SATante(tmp) = node;
      if((SATflags(tmp) & InQueueMask) == 0) {
	sat_Enqueue(cm->queue, tmp);
	SATflags(tmp) |= InQueueMask;
      }
      /** sat_ArrayInsert(unitArray, tmp); **/
    }
  }

  sat_ImplicationMain(cm, d);
  if(d->conflict == 0) {
    fprintf(vis_stderr,"There should be a conflict\n");
    exit(0);
  }
  /** Last Conflict Cls **/
  concl = d->conflict;
  sat_ArrayInsert(tmpdep,concl);
  SATflags(concl)|=NewMask;
  /** sat_ArrayInsert(arr,cl); **/
  if(!(SATflags(concl)&IsConflictMask)){
    count++;
    sat_PrintClauseLitsForCore(cm,concl,fp);
  }

  sat_GetDependence(cm, concl, tmpdep);
  for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
    SATflags(i)&=ResetNewMask;
  }

  for(i=0;i<tmpdep->num;i++){
    concl = tmpdep->space[i];
    if(!(SATflags(concl)&NewMask)){
      SATflags(concl)|=NewMask;
      /** is CONFLICT **/
      if((SATflags(concl)&IsConflictMask)){
	if(!st_lookup(cm->dependenceTable,(char *)concl,&dep)){
	  fprintf(cm->stdOut,"%ld is conflict but not in depe table\n",concl);
	  exit(0);
	}
	else{
	  for(j=0;j<dep->num; j++){
	    tmp = dep->space[j];
	    sat_GenerateCoreRecur(cm, tmp, fp, &count);
	  }
	}
      }
      /**not CONFLICT **/
      else{
	count++;
	sat_PrintClauseLitsForCore(cm,concl,fp);
      }
    }
  }
  /**fclose(fp); **/
  cm->numOfClsInCore = count;

  for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
    SATflags(i)&=ResetNewMask;
  }
  st_foreach_item(cm->dependenceTable, stGen,&node, &dep)
    sat_ArrayFree(dep);
  sat_ArrayFree(tmpdep);
  sat_Undo(cm,d);
  st_free_table(cm->dependenceTable);
  st_free_table(cm->anteTable);
  cm->status = SAT_UNSAT;
}

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

  Synopsis    [Implication propogation from assertations in an array ]

  Description [This funct is only for AIG assertation]

  SideEffects []

  SeeAlso     []

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

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

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

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

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

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


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

  Synopsis    [Force implication to pure and unit literals and set antecedence
	      of them]

  Description [Force implication to pure and unit literals and set antecedence
	      of them]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_ImplyUnitPureLitsWithAnte(satManager_t * cm, satLevel_t *d)
{
  int tmp, inverted;
  long node, *lit, i;

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize){
    node = i;
    if((SATflags(node)&IsCNFMask)&&(SATnumLits(node)==1)){
      int value;
      lit = (long*)SATfirstLit(node);
      tmp = SATgetNode(*lit);
      inverted = SATisInverted(tmp);
      tmp = SATnormalNode(tmp);

      value = !inverted;
      if(SATvalue(tmp) < 2)	{
	if(SATvalue(tmp) == value)	continue;
	else {
	  cm->status = SAT_UNSAT;
	  d->conflict = node;
	  break;
	}
      }

      SATvalue(tmp) = !inverted;
      SATmakeImplied(tmp, d);
      SATante(tmp) = node;
      if((SATflags(tmp) & InQueueMask) == 0) {
	sat_Enqueue(cm->queue, tmp);
	SATflags(tmp) |= InQueueMask;
      }
    }
  }

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

  sat_ImplyArray(cm, d, cm->pureLits);
}


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

  Synopsis    [Build an node for resolution tree]

  Description [tmpIP, lp,size must be prepared
	       Get formula for leaf nodes]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_BuildRT(
  satManager_t * cm,
  RTnode_t root,
  long *lp,
  long *tmpIP,
  int size,
  boolean NotCNF)
{
  int i;
  long tmpnode;
  RTManager_t *rm = cm->rm;

  RT_formula(root) = rm->cpos;

  RT_fSize(root) = size;


  if(rm->maxpos<=rm->cpos+size+1){
    rm->fArray = REALLOC(long,rm->fArray,rm->maxpos+FORMULA_BLOCK);
    rm->maxpos = rm->maxpos+FORMULA_BLOCK;
  }

  for(i=0;i<size;i++,lp++){
    if(NotCNF)
      tmpnode = *lp;
    else
      tmpnode = SATgetNode(*lp);
    rm->fArray[rm->cpos] = tmpnode;
    rm->cpos++;
  }
}

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

  Synopsis    [Generate interpolation forwardly]

  Description []

  SideEffects []

  SeeAlso     []

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

bAigEdge_t sat_GenerateFwdIP(bAig_Manager_t* manager,
			     satManager_t *cm,
			     RTnode_t  RTnode,
			     int cut)
{
  int i;
  long node, node1, left, right, result, *lp, *lp1;
  int IPTrue=0, local=1, first=0, second=0, allDummy=1;
  RTManager_t * rm = cm->rm;

  manager->class_ = cut;
  if(RT_flag(RTnode)&RT_VisitedMask){
#if DBG
    assert(RT_IPnode(RTnode)!=-1);
#endif

    return RT_IPnode(RTnode);
  }
#if DBG
  assert(RT_IPnode(RTnode)==-1);
#endif
  RT_flag(RTnode) |= RT_VisitedMask;

  if(RT_pivot(RTnode)==0){ /*leaf*/

#if DBG
    assert(RT_left(RTnode)==RT_NULL&&RT_right(RTnode)==RT_NULL);
#endif

#if DBG
    assert(RT_oriClsIdx(RTnode)==0);
#endif
    if(RT_oriClsIdx(RTnode))
      lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
    else

      lp = RT_formula(RTnode) + cm->rm->fArray;
    lp1 = lp;
    for(i=0;i<RT_fSize(RTnode);i++,lp++){
      if(*lp == DUMMY)
	continue;
      else{
	allDummy = 0;
#if DBG
	assert(*lp>0);
#endif
      }
      if(RT_oriClsIdx(RTnode))/*is CNF*/
	node = SATgetNode(*lp);
      else /*is AIG*/
	node = *lp;

      node = SATnormalNode(node);
      if(SATflags(node)&IsGlobalVarMask)
	continue;

      if(SATclass(node)>cut){
	IPTrue = 1;
#if DBG
	second = 1;
#else
	break;
#endif
      }
#if DBG
      else{
	first = 1;
      }
#endif
    }

#if DBG
    assert(!allDummy);
    assert(!(first&&second));
#endif


    if(IPTrue){
      RT_IPnode(RTnode) = bAig_One;
      return bAig_One;
    }

    lp = lp1;
    result = bAig_Zero;
    for(i=0;i<RT_fSize(RTnode);i++,lp++){
      if(RT_oriClsIdx(RTnode))/*is CNF*/
	node = SATgetNode(*lp);
      else /*is AIG*/
	node = *lp;
      node1 = SATnormalNode(node);
      if(flags(node1)&IsGlobalVarMask){
	result = PureSat_Or(manager,result,node);
	cm->nodesArray = manager->NodesArray;
      }
    }

    RT_IPnode(RTnode) = result;
    return result;
  } /*leaf*/

  /*not leaf*/
  else{

#if DBG
    assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL);
#endif
    left = sat_GenerateFwdIP(manager,cm,RT_left(RTnode),cut);
    right = sat_GenerateFwdIP(manager,cm,RT_right(RTnode),cut);
    if(RT_pivot(RTnode)<0){
      int class_;
      class_ = RT_pivot(RTnode)-DUMMY;
#if DBG
      assert(class_>0);
#endif
      if(class_>cut)
	local=0;
    }
    else{
      node = SATnormalNode(RT_pivot(RTnode));
      if((SATflags(node)&IsGlobalVarMask)||
	 (SATclass(node)>cut))
	local = 0;
    }
    if(local==0){
      result = PureSat_And(manager,left,right);

    }
    else{
      result = PureSat_Or(manager,left,right);

    }
  }/* else{ not leaf*/

  cm->nodesArray = manager->NodesArray;
  RT_IPnode(RTnode) = result;
  return result;

}


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

  Synopsis    [Generate interpolation backwardly]

  Description []

  SideEffects []

  SeeAlso     []

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


bAigEdge_t sat_GenerateBwdIP(bAig_Manager_t* manager,
			     satManager_t *cm,
			     RTnode_t RTnode,
			     int cut)
{
  int i;
  long node,node1, left, right, result, *lp, *lp1;
  int IPTrue=0, local=1, allGV=1;
  RTManager_t * rm = cm->rm;

  manager->class_ = cut;

  if(RT_flag(RTnode)&RT_VisitedMask){
#if DBG
    assert(RT_IPnode(RTnode)!=-1);
#endif

    return RT_IPnode(RTnode);
  }
#if DBG
  assert(RT_IPnode(RTnode)==-1);
#endif
  RT_flag(RTnode) |= RT_VisitedMask;

  if(RT_pivot(RTnode)==0){ /*leaf*/

#if DBG
    assert(RT_left(RTnode)==RT_NULL&&RT_right(RTnode)==RT_NULL);
    assert(RT_oriClsIdx(RTnode)==0);
#endif
    result = bAig_Zero;
    if(RT_oriClsIdx(RTnode))
      lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
    else

      lp = RT_formula(RTnode) + cm->rm->fArray;
    lp1 = lp;
    for(i=0;i<RT_fSize(RTnode);i++,lp++){
      if(*lp == DUMMY)
	continue;
      else{
	assert(*lp>0);
      }
      if(RT_oriClsIdx(RTnode))/*is CNF*/
	node = SATgetNode(*lp);
      else /*is AIG*/
	node = *lp;
      node = SATnormalNode(node);
      if(SATflags(node)&IsGlobalVarMask)
	continue;
      else
	allGV = 0;

      if(SATclass(node)<=cut){
	  IPTrue = 1;
	  break;
      }
    }

    if(IPTrue||allGV){
      RT_IPnode(RTnode) = bAig_One;
      return bAig_One;
    }

    lp = lp1;
    for(i=0;i<RT_fSize(RTnode);i++,lp++){
      if(RT_oriClsIdx(RTnode))/*is CNF*/
	node = SATgetNode(*lp);
      else /*is AIG*/
	node = *lp;
      node1 = SATnormalNode(node);
      if(SATflags(node1)&IsGlobalVarMask){
	result = PureSat_Or(manager,result,node);
	cm->nodesArray = manager->NodesArray;
      }
    }
    RT_IPnode(RTnode)  = result;
    return result;
  } /*leaf*/

  /*not leaf*/
  else{

#if DBG
    assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL);
#endif
    left = sat_GenerateBwdIP(manager,cm,RT_left(RTnode),cut);
    right = sat_GenerateBwdIP(manager,cm,RT_right(RTnode),cut);
    if(RT_pivot(RTnode)<0){
      int class_;
      class_ = RT_pivot(RTnode)-DUMMY;
#if DBG
      assert(class_>0);
#endif
      if(class_<=cut)
	local=0;
    }
    else{
      node = SATnormalNode(RT_pivot(RTnode));

      if((SATflags(node)&IsGlobalVarMask)||
	 (SATclass(node)<=cut))
	local = 0;
    }
    if(local==0){
      result = PureSat_And(manager,left,right);

    }
    else{
      result = PureSat_Or(manager,left,right);

    }
  }/* else{ not leaf*/

  cm->nodesArray = manager->NodesArray;
  RT_IPnode(RTnode) = result;
  return result;

}

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

  Synopsis    [ Reset resolution tree]

  Description []

  SideEffects []

  SeeAlso     []

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

void ResetRTree(RTManager_t *rm)
{
  int i;
  for(i=RTnodeSize;i<=rm->aSize;i+=RTnodeSize){
    RT_IPnode(i) = -1;
    RT_flag(i) &= RT_ResetVisitedMask;
  }

  return;
}

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

  Synopsis    [Free a resolution tree]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
RT_Free(RTManager_t *rm)
{
  FREE(rm->nArray);
  FREE(rm->fArray);
  FREE(rm);
}

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

  Synopsis    [Mark nodes in layer associated with property]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MarkLayerProperty(satManager_t *cm,
		      long v,
		      int layer)
{
  satVariable_t *var = SATgetVariable(v);

  if((v==bAig_NULL))
    return;

  if(!(SATflags(v)&CoiMask)){

    return;
  }

  /*already assigned score*/
  if(SATflags(v)&Visited2Mask){

    return;
  }

  var->scores[0] = SCOREUNIT*layer;
  var->scores[1] = SCOREUNIT*layer;
  SATflags(v) |= Visited2Mask;


  if((SATflags(v)&StateBitMask)&&
     (SATclass(v)<=cm->Length)){

    return;
  }

  sat_MarkLayerProperty(cm,SATleftChild(v),layer);
  sat_MarkLayerProperty(cm,SATrightChild(v),layer);

}

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

  Synopsis    [Mark nodes in layers associated normal visible latches]

  Description []

  SideEffects []

  SeeAlso     []

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

void sat_MarkLayer(satManager_t *cm,
		   long v,
		   int layer)
{
  satVariable_t *var = SATgetVariable(v);

  if((v==bAig_NULL))
    return;

  if(!(SATflags(v)&CoiMask)){

    return;
  }

  /*already assigned score*/
  if(SATflags(v)&Visited2Mask){

    return;
  }

  var->scores[0] = SCOREUNIT*layer;
  var->scores[1] = SCOREUNIT*layer;
  SATflags(v) |= Visited2Mask;


  if((SATflags(v)&StateBitMask)){

    return;
  }

  sat_MarkLayer(cm,SATleftChild(v),layer);
  sat_MarkLayer(cm,SATrightChild(v),layer);

}

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

  Synopsis    [Mark nodes in layers associated with initial states]

  Description []

  SideEffects []

  SeeAlso     []

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


void sat_MarkLayerInitState(satManager_t *cm,
			    long v,
			    int layer)
{
  satVariable_t *var = SATgetVariable(v);

  if((v==bAig_NULL))
    return;

  if(!(SATflags(v)&CoiMask)){

    return;
  }

  /*already assigned score*/
  if(SATflags(v)&Visited2Mask){

    return;
  }

  var->scores[0] = SCOREUNIT*layer;
  var->scores[1] = SCOREUNIT*layer;
  SATflags(v) |= Visited2Mask;


  /*if((SATflags(v)&StateBitMask)){
    fprintf(vis_stderr,"%d ISV return\n",SATnormalNode(v));
    return;
    }*/

  sat_MarkLayerInitState(cm,SATleftChild(v),layer);
  sat_MarkLayerInitState(cm,SATrightChild(v),layer);

}

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

  Synopsis    [Mark nodes in layers of a certain latch aig nodes]

  Description []

  SideEffects []

  SeeAlso     []

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

void sat_MarkLayerLatch(satManager_t *cm,
			long v,
			int layer)
{
  satVariable_t *var = SATgetVariable(v);

  if((v==bAig_NULL))
    return;

  if(!(SATflags(v)&CoiMask)){

    return;
  }

  /*not assigned score yet*/
  if(!(SATflags(v)&Visited2Mask)){
    var->scores[0] = SCOREUNIT*layer;
    var->scores[1] = SCOREUNIT*layer;
    SATflags(v) |= Visited2Mask;

  }
  sat_MarkLayer(cm,SATleftChild(v),layer);
  sat_MarkLayer(cm,SATrightChild(v),layer);

}

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

  Synopsis    [layer score initialization]

  Description []

  SideEffects []

  SeeAlso     []

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

void sat_InitLayerScore(satManager_t * cm){
  int i,j,k,layer;
  long v;
  st_table *table;
  st_generator * stgen, *stgen1;
  satVariable_t *var;

  int objExist;
  int inverted;
  long *plit, nv;
  int size;
  int count0, count1;
  satArray_t *ordered, *newOrdered;
  array_t * layerArray = array_alloc(st_table *,cm->LatchLevel+1);

  for(k=1;k<=cm->LatchLevel;k++){
      cm->assignedArray[k]=0;
      cm->numArray[k]=0;
  }

  cm->currentLevel = cm->LatchLevel;

  for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
    SATflags(i)&=ResetVisited2Mask;
  }


  sat_MarkLayerInitState(cm,cm->InitState,cm->LatchLevel);

  sat_MarkLayerProperty(cm,cm->property,cm->LatchLevel);


  st_foreach_item(cm->layerTable,stgen,&table,&layer)
    array_insert(st_table *,layerArray,layer,table);

  for(i=cm->LatchLevel;i>=1;i--){
    table = array_fetch(st_table*,layerArray,i);
    st_foreach_item(table,stgen1,&v,NIL(char*)){
      sat_MarkLayerLatch(cm,v,i);

    }
  }

  array_free(layerArray);

  for(i=bAigNodeSize;i<cm->nodesArraySize;i+=bAigNodeSize){
    if(SATflags(i)&Visited2Mask){
      int layer;
      SATflags(i)&=ResetVisited2Mask;
      var = SATgetVariable(i);
#if DBG
      assert(var->scores[0]%SCOREUNIT==0);
#endif
      layer = var->scores[0]/SCOREUNIT;
      cm->numArray[layer]++;
    }
  }

  if(cm->option->verbose >= 2){
    for(i=1;i<=cm->LatchLevel;i++){
      fprintf(vis_stdout,"Level %d:%d\n",i,cm->numArray[i]);
    }
  }


  ordered = cm->orderedVariableArray;
  if(ordered == 0)
    ordered = sat_ArrayAlloc(cm->initNumVariables);
  else
    ordered->num = 0;
  cm->orderedVariableArray = ordered;

  objExist = 0;


  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;
    if((SATflags(v) & IsBDDMask)) {
      continue;
    }
    if((SATflags(v) & IsCNFMask)) {
      size = SATnumLits(v);
      plit = (long*)SATfirstLit(v);
      for(j=0; j<size; j++, plit++) {
	nv = SATgetNode(*plit);
	inverted = !(SATisInverted(nv));
	nv = SATnormalNode(nv);
	var = SATgetVariable(nv);
	var->litsCount[inverted]++;
      }
      continue;
    }
    if(!(SATflags(v) & CoiMask))	continue;
    if(!(SATflags(v) & VisitedMask) && objExist)	continue;

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

    count0 = count1 = SATnFanout(v);
    if(count0 == 0 && SATleftChild(v) == 2 && SATrightChild(v) == 2) {
      count0 = 0;
      count1 = 0;
    }
    else if(SATleftChild(v) != 2) {
      count0 += 2;
      count1++;
    }
    else {
      count0 += 3;
      count1 += 3;
    }

    var = SATgetVariable(v);
    var->litsCount[0] += count0;
    var->litsCount[1] += count1;

    sat_ArrayInsert(ordered, v);
  }

  for(i=0; i<cm->unitLits->num; i++) {
    v = cm->unitLits->space[i];
    v = SATnormalNode(v);
    SATflags(v) |= NewMask;
  }
  if(cm->assertion) {
    for(i=0; i<cm->assertion->num; i++) {
      v = cm->assertion->space[i];
      v = SATnormalNode(v);
      SATflags(v) |= NewMask;
    }
  }

  newOrdered = sat_ArrayAlloc((ordered->num) * 2);
  size = ordered->num;
  for(i=0; i<size; i++) {
    v = ordered->space[i];
    var = SATgetVariable(v);
    var->lastLitsCount[0] = var->litsCount[0];
    var->lastLitsCount[1] = var->litsCount[1];
    var->scores[0] += var->lastLitsCount[0];
    var->scores[1] += var->lastLitsCount[1];

    if(SATflags(v) & NewMask);
    else if(var->scores[0] == 0 && var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
      sat_ArrayInsert(cm->pureLits, (v));
    }
    else if(var->scores[0] == 0 && !(SATflags(v) & NewMask)) {
      sat_ArrayInsert(cm->pureLits, (v));
    }
    else if(var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
      sat_ArrayInsert(cm->pureLits, SATnot(v));
    }
    else {
      sat_ArrayInsert(newOrdered, v);
      sat_ArrayInsert(newOrdered, (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1]);
    }
  }

  for(i=0; i<cm->unitLits->num; i++) {
    v = cm->unitLits->space[i];
    v = SATnormalNode(v);
    SATflags(v) &= ResetNewMask;
  }
  if(cm->assertion) {
    for(i=0; i<cm->assertion->num; i++) {
      v = cm->assertion->space[i];
      v = SATnormalNode(v);
      SATflags(v) &= ResetNewMask;
    }
  }

  cm->orderedVariableArray = ordered;
  size = newOrdered->num;
  qsort(newOrdered->space, size>>1, sizeof(long)*2, ScoreCompare);

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

  sat_ArrayFree(newOrdered);

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

}

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

  Synopsis    [Generate unsat proof in the form of resolution graph]

  Description []

  SideEffects []

  SeeAlso     []

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

void
sat_GenerateCore_All(satManager_t * cm)
{
  int i,j,value;
  long *lit, ante, node, tmp1;
  int  count, inverted;
  satLevel_t * d;
  satArray_t *clauseArray = sat_ArrayAlloc(1);
  int objectFlag;

  long conflicting, ante2;
  int nMarked,first;
  long v,left,right,result,*lp,*tmpIP;
  long *space,*tmp;
  satArray_t *implied;
  RTnode_t  tmprt;
  int size = 0, *bLevel;
  long *fdaLit=ALLOC(long,1);
  boolean endnow;
  RTManager_t * rm = cm->rm;

  cm->status = 0;
  count = 0;
  d = SATgetDecision(0);
  sat_ImplyArrayWithAnte(cm,d,cm->obj);
  sat_ImplyArrayWithAnte(cm,d,cm->auxObj);
  sat_ImplyArrayWithAnte(cm,d,cm->assertArray);



  if(cm->status==0){
  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize){
    node = i;
    if((SATflags(node)&IsCNFMask)&&(SATnumLits(node)==1)){
      lit = (long*)SATfirstLit(node);
      tmp1 = SATgetNode(*lit);
      inverted = SATisInverted(tmp1);
      tmp1 = SATnormalNode(tmp1);


      value = !inverted;
      if(SATvalue(tmp1) < 2)	{
	if(SATvalue(tmp1) == value)	continue;
	else {
	  cm->status = SAT_UNSAT;
	  d->conflict = node;
	  break;
	}
      }

      SATvalue(tmp1) = !inverted;
      SATmakeImplied(tmp1, d);
      SATante(tmp1) = node;
      if((SATflags(tmp1) & InQueueMask) == 0) {
	sat_Enqueue(cm->queue, tmp1);
	SATflags(tmp1) |= InQueueMask;
      }

    }
  }
  }


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

  if(d->conflict == 0) {
    fprintf(vis_stderr,"There should be a conflict\n");
    exit(0);
  }

  conflicting = d->conflict;
  nMarked = 0;

  sat_MarkNodeInConflict(
	  cm, d, &nMarked, &objectFlag, bLevel, clauseArray);
  /* Traverse implication graph backward*/
  first = 1;
  implied = d->implied;
  space = implied->space+implied->num-1;



  if(cm->option->coreGeneration){
    /*if last conflict is CNF*/
    if(SATflags(conflicting)&IsCNFMask){
      /*is conflict CNF*/
      if(SATflags(conflicting)&IsConflictMask){
	 if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){
	    fprintf(vis_stderr,"RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
	    exit(0);
	  }
	  else{
	    rm->root = tmprt;
#if PR
	    fprintf(vis_stdout,"Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
	  }
      }
      /*CNF but not conflict*/
      else{
	rm->root = RTCreateNode(rm);

	size = SATnumLits(conflicting);
	RT_fSize(rm->root) = size;
	lp = (long*)SATfirstLit(conflicting);
	sat_BuildRT(cm,rm->root, lp, tmpIP,size,0);
      }
    }
    /*if last conflict is AIG*/
    else{
      rm->root = RTCreateNode(rm);
      node = SATnormalNode(conflicting);
      left = SATleftChild(node);
      right = SATrightChild(node);
      result = PureSat_IdentifyConflict(cm,left,right,conflicting);
      inverted = SATisInverted(left);
      left = SATnormalNode(left);
      left = inverted ? SATnot(left) : left;

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

      j = node;

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

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


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

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


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

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

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

	    size = 1;
	    if(ante != SATnormalNode(v)){
	      value = SATvalue(ante);
	      node = SATnormalNode(ante);
	      node = value==1?SATnot(node):node;
	      tmp[1] = node;
	      size++;
	      ante2 = SATante2(v);
	      if(ante2){
		value = SATvalue(ante2);
		node = SATnormalNode(ante2);
		node = value==1?SATnot(node):node;
		tmp[2] = node;
		size++;
	      }
	    }

	    lp = tmp;
	    sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
	    FREE(tmp);
	  }
	  /* left is CNF*/
	  else{

	    lp = (long*)SATfirstLit(ante);
	    size = SATnumLits(ante);
	    RT_fSize(tmprt) = size;
	    sat_BuildRT(cm,tmprt, lp, tmpIP,size,0);
	  }
	} /*else{ // if not conflict CNF*/

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

      sat_MarkNodeInImpliedNode(
	cm, d, v, &nMarked, &objectFlag, bLevel, clauseArray);
    }/*if(SATflags(v) & VisitedMask) {*/
    first = 0;
  }/*for(i=implied->num-1; i>=*/


  if(cm->option->verbose >= 2)
    fprintf(vis_stdout,"total # of RTree node:%ld\n",rm->aSize/RTnodeSize);

  sat_ArrayFree(clauseArray);
  FREE(fdaLit);
  if(cm->option->arosat)
    AS_Undo(cm,d);
  else
    sat_Undo(cm,d);
  cm->status = SAT_UNSAT;
}


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

  Synopsis    [Merge level for Arosat]

  Description []

  SideEffects []

  SeeAlso     []

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


void sat_ASmergeLevel(satManager_t *cm)
{
  int base;
  long v;
  satVariable_t *var;
  int *assignedArray = cm->assignedArray;
  int * numArray = cm->numArray,level=0;

  if(cm->option->verbose >= 2)
    fprintf(vis_stdout,"MERGE LEVEL\n");
  while(cm->LatchLevel>0){
  if(cm->option->verbose >= 2)
    fprintf(vis_stdout,"Merge level %d and %d\n",cm->LatchLevel, cm->LatchLevel-1);
    level++;
    cm->LatchLevel--;
    if(cm->numArray[cm->LatchLevel]>0)
      break;
  }
  if(cm->option->verbose >= 2)
    fprintf(vis_stdout,"After Merge,Latch level:%d\n",cm->LatchLevel);
#if DBG
  assert(cm->LatchLevel>0);
#endif

  for(v=satNodeSize;v<cm->initNodesArraySize;v+=satNodeSize){
    if(!SATflags(v)&CoiMask)
      continue;
    var = SATgetVariable(v);
    base = var->scores[0]/SCOREUNIT;
    if(base==cm->LatchLevel+level){
      var->scores[0] = cm->LatchLevel*SCOREUNIT + var->scores[0]%SCOREUNIT;
      var->scores[1] = cm->LatchLevel*SCOREUNIT + var->scores[1]%SCOREUNIT;
    }
  }
  assignedArray[cm->LatchLevel]+=assignedArray[cm->LatchLevel+level];
  numArray[cm->LatchLevel]+=numArray[cm->LatchLevel+level];

}

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

  Synopsis    [CNF based conflict enforcing]

  Description []

  SideEffects []

  SeeAlso     []

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

int sat_CE_CNF(
	satManager_t *cm,
	satLevel_t *d,
	int v,
	satArray_t *wl)
{
  long size, i, *space;
  long lit, *plit, dir;
  long nv, tv, *oplit, *wlit;
  int isInverted, value;
  long inverted, clit;
  satStatistics_t *stats;
  satOption_t *option;
  satQueue_t *Q;

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

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

    if(plit == 0 || *plit == 0) {

      continue;
    }

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

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

	tv = SATgetNode(*wlit);
	isInverted = SATisInverted(tv);
	tv = SATnormalNode(tv);
	value = SATvalue(tv) ^ isInverted;
	if(value == 0) {  /* conflict happens*/

	  return CONFLICT;
	}
	else if(value > 1) { /* implication*/
	  /*implication can only be made on the other wl*/

	  break;
	}

	break;
      }

      clit = *oplit;

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

      if(SATisWL(clit)) { /* found other watched literal*/
	wlit = oplit;
	/*a little diff from zchaff, if otherwl==1, break*/
	if(value == 1)	{
	  break;
	}
	/*since it is otherwl, it can't be zero. Here it is unknow*/
	continue;
      }

      if(value == 0)
	continue;

      /*now it is 1 or unknow*/
      break;
    }/*while(1)*/
  }/*for*/
  return NO_CONFLICT;
}

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

  Synopsis    [Conflict enforcing]

  Description []

  SideEffects []

  SeeAlso     []

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

  long enforce=0;

  v = SATnormalNode(v);

  var = SATgetVariable(v);

  wlArray = var->wl[value^1];

  /*need recovery*/
  SATvalue(v) = value;

  /* implcation on CNF*/
  if(wlArray && wlArray->size) {
    if(sat_CE_CNF(cm, d, v, wlArray)==CONFLICT){
      enforce = 1;
    }
  }

  /*need recovery*/
  SATvalue(v) = value;

  if(enforce==0){
    /* implication on AIG*/
    fan = SATfanout(v);
    size = SATnFanout(v);
    for(i=0; i<size; i++, fan++) {
      cur = *fan;
      cur = cur >> 1;
      cur = SATnormalNode(cur);
      left = SATleftChild(cur);
      right = SATrightChild(cur);
      value1 = SATgetValue(left, right, cur);
      if(value1==1||value1==5||value1==9||value1==13||value1==17
	 ||value1==20||value1==33||value1==49){
	/*fprintf(vis_stdout,"AIG Output enforce\n");*/
	enforce=1;
	break;
      }
    }
  }

  if(enforce==0){
    left = SATleftChild(v);
    right = SATrightChild(v);
    if(left!=2&&right!=2){
      value1 = SATgetValue(left, right, v);
      if(value1==1||value1==5||value1==9||value1==13||value1==17
	 ||value1==20||value1==33||value1==49){
	/*fprintf(vis_stdout,"AIG Children enforce\n");*/
	enforce=1;
      }
    }
  }


  SATvalue(v)=2;

  return enforce;

}

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

  Synopsis    [Decision procedure for Arosat]

  Description []

  SideEffects []

  SeeAlso     []

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


int sat_ASDec(satManager_t *cm,
	      satLevel_t *d,
	      long v)
{
  int dfs;
  int *numArray,*assignedArray;
  satVariable_t *var=SATgetVariable(v);

  assignedArray = cm->assignedArray;
  numArray = cm->numArray;

  v = SATnormalNode(v);
  dfs = var->scores[0]/SCOREUNIT;

#if DBG

  assert(dfs==cm->LatchLevel);
  assert(!(SATflags(SATnormalNode(v)) & InQueueMask));
  assert(SATvalue(SATnormalNode(v))==2);
#endif
  if(!(SATflags(SATnormalNode(v))&AssignedMask)){
    SATflags(SATnormalNode(v))|=AssignedMask;
    assignedArray[dfs]++;
    /* if(dfs==cm->OriLevel)
    //  fprintf(vis_stdout,"Assign Level %d: %d dfs=%d assArray[%d]=%d\n",
    //     d->level,v,dfs,dfs,cm->assignedArray[dfs]);*/

    if(cm->assignedArray[dfs]==cm->numArray[dfs])
      sat_ASmergeLevel(cm);
    /*fprintf(vis_stdout,"Decisionlevel:%d: %d dfs=%d,assArray[%d]=%d, numArray[%d]=%d\n",
      //      d->level,v,dfs,dfs,assignedArray[dfs],dfs,numArray[dfs]);*/
  }
  return 0;
}

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

  Synopsis    [Implication procedure for Arosat]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_ASImp(satManager_t *cm,
	  satLevel_t *d,
	  long v,
	  int value)
{
  int dfs;
  long tmpv;
  int *numArray,*assignedArray;
  satVariable_t *var=SATgetVariable(v);

  assignedArray = cm->assignedArray;
  numArray = cm->numArray;

  v = SATnormalNode(v);

#if DBG
  assert(SATvalue(v)==2);
#endif
  dfs = var->scores[0]/SCOREUNIT;


  if(dfs==cm->LatchLevel){
    if(!(SATflags(SATnormalNode(v))&AssignedMask)){

      SATflags(SATnormalNode(v))|=AssignedMask;
      assignedArray[dfs]++;

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

    }

    return 0;
  }
  else{
    /*if conflict enforcing*/
    if(sat_CE(cm,d,v,dfs,value)){

      if(!(SATflags(SATnormalNode(v))&AssignedMask)){
	SATflags(SATnormalNode(v))|=AssignedMask;
	assignedArray[dfs]++;

#if DBG
	assert(assignedArray[dfs]<=numArray[dfs]);
#endif

      }

      return 0;
    }
    /*else implication is prohibited*/
    else{

#if DBG
      assert(value==0||value==1);
#endif
      if(value==0)
	tmpv = -1;
      else
	tmpv = 1;
      SATgetVariable(v)->RecVal = tmpv;

      return 1;
    }
  }
  return 0;
}