src/sat/satCore.c

Go to the documentation of this file.

#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

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

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

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

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

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

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


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


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

}


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;
    if(!(SATflags(concl)& IsConflictMask)){
      (*count)++;
      sat_PrintClauseLitsForCore(cm,concl,fp);
    }
    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);
        }
      }
    }
  }
}



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

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_ImplicationMain(cm, d);
  if(d->conflict == 0) {
    fprintf(vis_stderr,"There should be a conflict\n");
    exit(0);
  }
  concl = d->conflict;
  sat_ArrayInsert(tmpdep,concl);
  SATflags(concl)|=NewMask;
  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;
      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);
          }
        }
      }
      else{
        count++;
        sat_PrintClauseLitsForCore(cm,concl,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;
}

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


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


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

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;

}


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;

}

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

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

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

}

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

}

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

}

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

}

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

}

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


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

}

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

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;

}

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

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