#include "debug.h"
void printNodeArray(array_t * nodeArray)
{
  int i;
  Ntk_Node_t* node;
  arrayForEachItem(Ntk_Node_t *, nodeArray, i, node){
    printf("%s\n",Ntk_NodeReadName(node)); 
  }


}

void printLatch(st_table* CoiTable)
{
// COI contents
   printf("*** COI ***\n");
   st_generator    *stGen;
   Ntk_Node_t * latch;
   st_foreach_item(CoiTable, stGen, &latch, NULL) {
	printf("%s\n",Ntk_NodeReadName(latch)); 
  }
}


st_table * generateAllLatches(Ntk_Network_t * ntk)
{
    st_table        *CoiTable = st_init_table(st_ptrcmp, st_ptrhash);
	lsGen           gen ;
	Ntk_Node_t		*node;

	Ntk_NetworkForEachNode(ntk,gen, node){
		if (Ntk_NodeTestIsLatch(node)){
			st_insert(CoiTable, (char *) node, Ntk_NodeReadName(node));
		}
	}
	return CoiTable;

}


void mdd_GetState_Values(
mdd_manager *mgr ,
mdd_t *  top, 
FILE  * f) 
{
  mdd_t * T;
  mdd_t * E;
  int    id;
  array_t * val = array_alloc(int, 4); 
  static int level;
  char c = ' ' ;

  level++;

  id = bdd_top_var_id(top);

  mvar_type mv =  
array_fetch(mvar_type, mdd_ret_mvar_list((mgr)),(id));
 // fprintf(f,"(");

  // Pour le Then
  T=bdd_then(top);
 
 //variable belongs to what we are looking for
// if(strstr(mv.name,var_name) !=NULL)
  if(bdd_is_tautology(T,1)){
    //array_insert(type, array, position, object)
    fprintf(f,"%s = 1 ",mv.name);
    //c = '+';
  } else
    if(!bdd_is_tautology(T,0)){
      fprintf(f,"%s = 1 * ",mv.name);
      //mdd_FunctionPrint(mgr, T,f);
     // c = '+';
    }

  mdd_free(T);
  
  //pour le Else
  E=bdd_else(top);
  if(bdd_is_tautology(E,0)){
    goto fin;
  }
  
  if(bdd_is_tautology(E,1)){
    fprintf(f,"%c %s = 0",c, mv.name);
    goto fin;
  }
  
  fprintf(f,"%c %s = 0 * ",c, mv.name);
  /*
  mdd_FunctionPrint(mgr, E,f);
  mdd_free(E);
*/
 fin:
  fprintf(f,")");
  level--;
  return;
}
/**Function********************************************************************
 
  Synopsis    [Performs the sat call]

  Description [Retrun the result of SAT call, avec positionnement des options]
  SideEffects []

  SeeAlso     []

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

int Dbg_SatCheck(char * forceAssigName, char * cnfFileName,int verbose
)
{
 satManager_t *cm;
 cm = sat_InitManager(0);
 cm->comment = ALLOC(char, 2);
 cm->comment[0] = ' ';
 cm->comment[1] = '\0';
 cm->stdOut = stdout;
 cm->stdErr = stderr;

 
  satOption_t  *satOption;
  array_t      *result = NIL(array_t);
  int          maxSize;

  satOption = sat_InitOption();
  satOption->verbose = 2;
  //satOption->unsatCoreFileName = "Ucore.txt";
  satOption->clauseDeletionHeuristic = 0;
  //satOption->coreGeneration = 1 ;
  //satOption->minimizeConflictClause = 1;
  if(forceAssigName != NULL)
    satOption->forcedAssignArr = sat_ReadForcedAssignment(forceAssigName);
   cm->option = satOption;
   cm->each = sat_InitStatistics();

  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);

  maxSize = 1024 << 8;
  cm->nodesArray = ALLOC(long, maxSize);
  cm->maxNodesArraySize = maxSize;
  cm->nodesArraySize = satNodeSize;

  sat_AllocLiteralsDB(cm);

   sat_ReadCNF(cm,cnfFileName);
   sat_Main(cm);

if(verbose){
   if(cm->status == SAT_UNSAT) {
    if(cm->option->forcedAssignArr)
      fprintf(cm->stdOut, "%s UNSAT under given assignment\n",
	      cm->comment);
    fprintf(cm->stdOut, "%s UNSATISFIABLE\n", cm->comment);
    fflush(cm->stdOut);
    sat_ReportStatistics(cm, cm->each);
    sat_FreeManager(cm);
  }
  else if(cm->status == SAT_SAT) {
    fprintf(cm->stdOut, "%s SATISFIABLE\n", cm->comment);
    fflush(cm->stdOut);
    sat_PrintSatisfyingAssignment(cm);
    sat_ReportStatistics(cm, cm->each);
    sat_FreeManager(cm);
  }
}
return cm->status;
}
/**Function********************************************************************
 
  Synopsis    [Generate a CNF of the network]

  Description [Generate the set of clauses of the unroll network for a given 
  length and for a given cone of influence]
  SideEffects []

  SeeAlso     []

******************************************************************************/
BmcCnfClauses_t*
Dbg_GenerateCNF(Ntk_Network_t * network, 
BmcOption_t * options,
st_table  *CoiTable
){
st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
/*
 *nodeToMvfAigTable maps each node to its multi-function And/Inv graph
 */
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
/*
 * Create a clause database
 */
cnfClauses = BmcCnfClausesAlloc();
/*
 * Generate clauses for an initialized path of length k
 */
BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
			 cnfClauses, nodeToMvfAigTable, CoiTable);
return cnfClauses;

}
/**Function********************************************************************
 
  Synopsis    [Return the default value of a Node]

  Description [Given a table of a node , return its default value if it exists 
  else -1   This function only work for binary gate with only one default
  value.]
  SideEffects []

  SeeAlso     []

******************************************************************************/
int Dbg_GetDefaultValue(Tbl_Table_t * table)
{
  Tbl_Entry_t * defEntry;
  int defIndex;
  lsList * rangeList;
  Tbl_TableForEachDefaultEntry(table,defEntry,defIndex)
  { 
    rangeList = Tbl_EntryReadList(defEntry);
    int length = lsLength(rangeList);
    if ( length  != 1)
      return -1;
    Tbl_Range_t * range;
    int valDefault;
    lsGen gen;
    Tbl_EntryForEachValue(defEntry,valDefault,gen,range){
      return Tbl_RangeEnd(range);
    }
  }
}