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

  FileName    [satInc.c]

  PackageName [sat]

  Synopsis    [Routines for sat incremental function.]

  Author      [HoonSang Jin]

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


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

#include "satInt.h"

static char rcsid[] UNUSED = "$Id: satInc.c,v 1.16 2009/04/11 18:26:37 fabio Exp $";
static satManager_t *SatCm;

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

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

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

static int ScoreDistillCompare(const void *x, const void *y);

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


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


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

  Synopsis    [ Apply distillation method to find
		the clauses that can be forwarded]

  Description [ Apply distillation method to find
		the clauses that can be forwarded]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_IncrementalUsingDistill(satManager_t *cm)
{
  sat_TrieBasedImplication(cm, cm->trieArray, 1);
  sat_FreeTrie(cm, cm->trieArray);
  cm->trieArray = 0;
  fprintf(cm->stdOut, "%s %d conflicts are forwarded from distillation,\n",
	  cm->comment,
	  cm->each->nDistillObjConflictCl + cm->each->nDistillNonobjConflictCl);
}

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

  Synopsis    [ Make decision based on trie when applying distillation ]

  Description [ Make decision based on trie when applying distillation ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satLevel_t *
sat_DecisionBasedOnTrie(
	satManager_t *cm,
	long v,
	int value)
{
satLevel_t *d;

  d = sat_AllocLevel(cm);
  d->decisionNode = v;

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

  sat_Enqueue(cm->queue, v);
  SATflags(v) |= InQueueMask;

  return(d);
}

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

  Synopsis    [ Apply implication based on trie]

  Description [ Apply implication based on trie]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_TrieBasedImplication(
	satManager_t *cm,
	satArray_t *trieArray,
	int depth)
{
int i;
satTrie_t *t;
satLevel_t *d;
satArray_t *tArray;

  if(trieArray == 0)	return;

  for(i=0; i<trieArray->num; i++) {
    t = (satTrie_t *)(trieArray->space[i]);
    if(SATvalue(t->id) < 2)	continue;

    tArray = t->child[0];
    if(tArray) {
      d = sat_DecisionBasedOnTrie(cm, t->id, 0);
      sat_ImplicationMain(cm, d);
      if(d->conflict) {
	sat_ConflictAnalysisOnTrie(cm, d);
      }
      else if(cm->status == 0) {
	sat_TrieBasedImplication(cm, tArray, depth+1);
      }
      sat_Backtrack(cm, depth-1);
    }

    tArray = t->child[1];
    if(tArray && cm->status == 0) {
      d = sat_DecisionBasedOnTrie(cm, t->id, 1);
      sat_ImplicationMain(cm, d);
      if(d->conflict) {
	sat_ConflictAnalysisOnTrie(cm, d);
      }
      else if(cm->status == 0) {
	sat_TrieBasedImplication(cm, tArray, depth+1);
      }
      sat_Backtrack(cm, depth-1);
    }

    if(cm->status == SAT_BACKTRACK && depth == 1) {
      cm->status = 0;
      d = SATgetDecision(0);
      sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
      sat_ImplyArray(cm, d, cm->objUnitLitArray);
      sat_MarkObjectiveFlagToArray(cm, cm->objUnitLitArray);
      sat_ImplicationMain(cm, d);
      if(d->conflict) {
	cm->status = SAT_UNSAT;
	return;
      }
      i--;
    }
  }
}

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

  Synopsis    [ Conflict analysis based on trie]

  Description [  Conflict analysis based on trie]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_ConflictAnalysisOnTrie(
	satManager_t *cm,
	satLevel_t *d)
{
int bLevel;
long v, learned, unitLit;
int objectFlag;
satArray_t *clauseArray;
satStatistics_t *stats;

  bLevel = 0;
  unitLit = -1;
  clauseArray = cm->auxArray;
  sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &unitLit);

  if(clauseArray->num > (int)(cm->currentDecision*2)) {
    sat_GetConflictAsConflictClause(cm, clauseArray);
  }

  if(clauseArray->num == 1) {
    cm->status = SAT_BACKTRACK;
    v = clauseArray->space[0];
    if(objectFlag)
      sat_ArrayInsert(cm->objUnitLitArray, SATnot(v));
    else
      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(v));
  }
  else {
    learned = sat_AddClauseIncremental(cm, clauseArray, objectFlag, 1);
  }

  stats = cm->each;
  if(objectFlag) {
    stats->nInitObjConflictCl++;
    stats->nInitObjConflictLit += clauseArray->num;
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
    stats->nDistillObjConflictCl++;
    stats->nDistillObjConflictLit += clauseArray->num;
  }
  else {
    stats->nInitNonobjConflictCl++;
    stats->nInitNonobjConflictLit += clauseArray->num;
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
    stats->nDistillNonobjConflictCl++;
    stats->nDistillNonobjConflictLit += clauseArray->num;
  }
  stats->nConflictCl++;
  stats->nConflictLit += clauseArray->num;
}

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

  Synopsis    [ Get conflict clauses from the decision variables]

  Description [ When applying distillation,
		get conflict clauses from the decision variables
		to create conflict clause ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_GetConflictAsConflictClause(
	satManager_t *cm,
	satArray_t *clauseArray)
{
int i;
satLevel_t *d;

  clauseArray->num = 0;
  for(i=1; i<=cm->currentDecision; i++) {
    d = SATgetDecision(i);
    sat_ArrayInsert(clauseArray,
	    (d->decisionNode)^(!(SATvalue(d->decisionNode))));
  }
}

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

  Synopsis    [ Restore conflict clauses to use them for current run]

  Description [ Restore conflict clauses to use them for current run]

  SideEffects [ ]

  SeeAlso     [ sat_SaveNonobjClauses sat_SaveAllClauses ]

******************************************************************************/
void
sat_RestoreForwardedClauses(satManager_t *cm, int objectFlag)
{
int i, size;
int total;
long *space, c, *start;
satArray_t *saved;
satArray_t *clause;
//Bing
 int NotCoi = 0, ct=0;


  if(cm->option->checkNonobjForwarding) {
    sat_CheckForwardedClauses(cm);
  }

  saved = cm->savedConflictClauses;
  if(saved == 0)
    return;

  clause = sat_ArrayAlloc(50);

  total = 0;
  for(i=0, space=saved->space; i<saved->num; i++, space++){
    if(*space < 0) {
      space++;
      i++;
      start = space;
      size = 0;
      clause->num = 0;
      //Bing:
      NotCoi = 0;
      while(*space > 0) {
	sat_ArrayInsert(clause, SATnot((*space)));
	//Bing:
	if(!(SATflags(*space)&CoiMask)){
	  NotCoi = 1;
	}
	size++;
	i++;
	space++;
      }


      //Bing:
      if(cm->option->AbRf){
	if(!NotCoi){
	  c = sat_AddClauseIncremental(cm, clause, objectFlag, 0);
	  total++;
	}
	else
	  ct++;
      }
      else{
	c = sat_AddClauseIncremental(cm, clause, objectFlag, 0);
	total++;
      }
    }
  }
  sat_ArrayFree(clause);
  sat_ArrayFree(saved);
  cm->savedConflictClauses = 0;

/**  fprintf(cm->stdOut, "%s %d clauses are forwarded by reststoring
     non-objective\n", cm->comment, total) ; **/
}

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

  Synopsis    [ Check whether the given conflict clauses can be forwared ]

  Description [ Check whether the given conflict clauses can be forwared ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_CheckForwardedClauses(satManager_t *cm)
{
long *space, *start;
long nv;
int size, i;
int total;
int conflictFlag, inverted;
int j, value, level;
satLevel_t *d;
satArray_t *saved;
satArray_t *clause;

  d = 0;
  saved = cm->savedConflictClauses;
  if(saved == 0)
    return;

  clause = sat_ArrayAlloc(50);

  total = 0;
  for(i=0, space=saved->space; i<saved->num; i++, space++){
    if(*space < 0) {
      start = space;
      space++;
      i++;
      size = 0;
      clause->num = 0;
      conflictFlag = 0;
      while(*space > 0) {
	sat_ArrayInsert(clause, SATnot((*space)));
	if(conflictFlag == 0) {
	  nv = *space;
	  inverted = (SATisInverted(nv));
	  nv = SATnormalNode(nv);

	  d = sat_AllocLevel(cm);
	  d->decisionNode = nv;
	  SATvalue(nv) = inverted;
	  SATmakeImplied(nv, d);

	  sat_Enqueue(cm->queue, nv);
	  SATflags(nv) |= InQueueMask;

	  sat_ImplicationMain(cm, d);
	  if(d->conflict)	conflictFlag = 1;
	}
	size++;
	i++;
	space++;
      }

      if(d->conflict == 0) {
	fprintf(cm->stdOut, "%s ERROR : %ld does not result in conflict\n",
	    cm->comment, *start);
	for(j=0; j<clause->num; j++) {
	  nv = clause->space[j];
	  inverted = SATisInverted(nv);
	  nv = SATnormalNode(nv);
	  value = SATvalue(nv);
	  level = value>1 ? -1 : SATlevel(nv);
	  fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
		  nv, inverted ? '\'' : ' ', level, SATgetValueChar(value),
		  ' ');
	}
	fprintf(cm->stdOut, "\n");
      }
      sat_Backtrack(cm, -1);

      total++;
    }
  }
  sat_ArrayFree(clause);
}

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

  Synopsis    [ Save objective independent conflict clauses]

  Description [ When applying incremental SAT, one has to save objective
		independent conflict clause  They are restored by
		sat_RestoreForwardedClauses ]

  SideEffects [ ]

  SeeAlso     [ sat_RestoreForwardedClauses ]

******************************************************************************/
void
sat_SaveNonobjClauses(satManager_t *cm)
{
int limit, total, passed;
int size, j;
long *plit, nv, v, i;
satArray_t *savedArray;

  savedArray = sat_ArrayAlloc(1024);

  total = passed = 0;
  limit = cm->option->incNumNonobjLitsLimit;
  for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
    if(SATreadInUse(i) == 0)		continue;
    if(!(SATflags(i) & NonobjMask))	{
      continue;
    }
    size = SATnumLits(i);
    if(size > limit) {
      total++;
    }
    else {
      total++;
      passed++;
      plit = (long*)SATfirstLit(i);
      nv = (*(plit-1));
      sat_ArrayInsert(savedArray, nv);
      for(j=0; j<size; j++, plit++) {
	v = SATgetNode(*plit);
	sat_ArrayInsert(savedArray, v);
      }
      sat_ArrayInsert(savedArray, nv);
    }
  }
  if(cm->option->verbose > 1) {
    fprintf(cm->stdOut, "%s %d NonObjective Clauses forwarded out of %d\n",
	    cm->comment, passed, total);
  }
  cm->savedConflictClauses = savedArray;
}

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

  Synopsis    [ Save all conflict clauses]

  Description [ When applying incremental SAT for BMC,
		one can forward all the clauses
		They are restored by sat_RestoreForwardedClauses ]

  SideEffects [ ]

  SeeAlso     [ sat_RestoreForwardedClauses ]

******************************************************************************/
void
sat_SaveAllClauses(satManager_t *cm)
{
int limit, total, passed;
int size, j;
long *plit, nv, v, i;
satArray_t *savedArray;

  savedArray = sat_ArrayAlloc(1024);

  total = passed = 0;
  limit = cm->option->incNumNonobjLitsLimit;
  for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
    if(SATreadInUse(i) == 0)		continue;
    size = SATnumLits(i);
    total++;
    plit = (long*)SATfirstLit(i);
    nv = (*(plit-1));
    sat_ArrayInsert(savedArray, nv);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      sat_ArrayInsert(savedArray, v);
    }
    sat_ArrayInsert(savedArray, nv);
  }
  /**
  if(cm->option->verbose > 1) {
    fprintf(cm->stdOut, "%s %d clauses are forwarded\n",
	    cm->comment, total);
  }
  **/
  cm->savedConflictClauses = savedArray;
}

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

  Synopsis    [ Build Trie with objective dependent conflict clauses]

  Description [ When applying incremental SAT based on distillation
		build Trie with objective dependent conflict clauses.]

  SideEffects [ ]

  SeeAlso     [ sat_BuildTrie ]

******************************************************************************/
void
sat_BuildTrieForDistill(satManager_t *cm)
{
int limit, nCl, nLit;
int j, n;
int size, inverted;
long v, *plit, i;
int findFlag;
satVariable_t *var;
satArray_t *trieArray;
satArray_t *unitArray;
satTrie_t *t;

  size = cm->initNumVariables * satNodeSize;
  for(i=satNodeSize; i<size; i+= satNodeSize) {
    var = SATgetVariable(i);
    var->scores[0] = 0;
    var->scores[1] = 0;
  }

  nCl = nLit = 0;
  limit = cm->option->incNumObjLitsLimit;
  for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
    if(SATreadInUse(i) == 0)		continue;
    if(SATflags(i) & NonobjMask)	continue;

    size = SATnumLits(i);
    if(size > limit)	continue;
    n = 0;
    for(j=0, plit = (long*)SATfirstLit(i); j<size; j++, plit++) {
      v = SATgetNode(*plit);
      inverted = SATisInverted(v);
      v = SATnormalNode(v);
      var = SATgetVariable(v);
      var->scores[inverted] += 1;
      if(SATvalue(v) < 2)	continue;
      n++;
    }
    if(n > 0) {
      nCl++;
      nLit += n;
    }
  }
  if(cm->option->verbose > 1) {
    fprintf(cm->stdOut, "%s Candidates for Distill %d clauses %d literals\n",
	    cm->comment, nCl, nLit);
  }

  trieArray = sat_ArrayAlloc(64);
  cm->trieArray = trieArray;
  unitArray = cm->objUnitLitArray;
  if(unitArray) {
    for(i=0; i<unitArray->num; i++) {
      v = unitArray->space[i];
      inverted = SATisInverted(v);
      v = SATnormalNode(v);

      findFlag = 0;
      for(j=0;  j<trieArray->num; j++) {
	t = (satTrie_t *)(trieArray->space[j]);
	if(t->id == v) {
	  if(t->child[inverted] == 0)
	    t->child[inverted] = sat_ArrayAlloc(2);
	  findFlag = 1;
	}
      }

      if(findFlag == 0) {
	t = ALLOC(satTrie_t, 1);
	memset(t, 0, sizeof(satTrie_t));
	t->id = v;
	if(t->child[inverted] == 0)
	  t->child[inverted] = sat_ArrayAlloc(2);
	sat_ArrayInsert(trieArray, (long)t);
      }
    }
  }

  for(i=cm->beginConflict; i<cm->nodesArraySize; i+=satNodeSize) {
    if(SATreadInUse(i) == 0)		continue;
    if(SATflags(i) & NonobjMask)	continue;

    size = SATnumLits(i);
    if(size > limit)	continue;

    plit = (long*)SATfirstLit(i);
    SatCm = cm;
    qsort(plit, size, sizeof(long), ScoreDistillCompare);
    sat_BuildTrie(cm, trieArray, plit, 1);
  }
}

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

  Synopsis    [ Build Trie with objective dependent conflict clauses]

  Description [ When applying incremental SAT based on distillation
		build Trie with objective dependent conflict clauses.]

  SideEffects [ ]

  SeeAlso     [ sat_BuildTrieForDistill ]

******************************************************************************/
void
sat_BuildTrie(
	satManager_t *cm,
	satArray_t *trieArray,
	long *plit,
	int depth)
{
int i, inverted;
long v;
satTrie_t *t;

  while(1) {
    if(*plit <= 0)	return;
    v = SATgetNode(*plit);
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    if(SATvalue(v) < 2)plit++;
    else		break;
  }

  for(i=0; i<trieArray->num; i++) {
    t = (satTrie_t *)(trieArray->space[i]);
    if(t->id == v) {
      if(t->child[inverted] == 0)
	t->child[inverted] = sat_ArrayAlloc(2);
      plit++;
      sat_BuildTrie(cm, t->child[inverted], plit, depth+1);
      return;
    }
  }

  t = ALLOC(satTrie_t, 1);
  memset(t, 0, sizeof(satTrie_t));
  t->id = v;
  t->depth = depth;
  sat_ArrayInsert(trieArray, (long)t);

  if(t->child[inverted] == 0)
    t->child[inverted] = sat_ArrayAlloc(2);
  plit++;
  sat_BuildTrie(cm, t->child[inverted], plit, depth+1);
}



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

  Synopsis    [ Free trie structure ]

  Description [ Free trie structure ]

  SideEffects [ ]

  SeeAlso     [ sat_BuildTrieForDistill ]

******************************************************************************/
void
sat_FreeTrie(satManager_t *cm, satArray_t *arr)
{
int i;
satTrie_t *t;

  if(arr == 0)	return;

  for(i=0; i<arr->num; i++) {
    t = (satTrie_t *)(arr->space[i]);
    if(t->child[0]) {
      sat_FreeTrie(cm, t->child[0]);
      sat_ArrayFree(t->child[0]);
    }
    if(t->child[1]) {
      sat_FreeTrie(cm, t->child[1]);
      sat_ArrayFree(t->child[1]);
    }
    free(t);
  }

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

  Synopsis    [ sort variable order based on occurrence to build Trie ]

  Description [ sort variable order based on occurrence to build Trie ]

  SideEffects [ ]

  SeeAlso     [ sat_BuildTrieForDistill ]

******************************************************************************/
static int
ScoreDistillCompare(const void *x, const void *y)
{
int n1, n2;
int i1, i2;
satVariable_t  v1, v2;

  n1 = *(int *)x;
  n2 = *(int *)y;
  n1 >>= 2;
  n2 >>= 2;
  i1 = SATisInverted(n1);
  n1 = SATnormalNode(n1);
  i2 = SATisInverted(n2);
  n2 = SATnormalNode(n2);
  v1 = SatCm->variableArray[SATnodeID(n1)];
  v2 = SatCm->variableArray[SATnodeID(n2)];

  if(v1.scores[i1] == v2.scores[i2]) {
    return(n1 > n2);
  }
  return(v1.scores[i1] < v2.scores[i2]);
}