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

void printStringArray(array_t * array)
{
  
  int i;
  char * data;
  arrayForEachItem(char *, array, i, data)
  {
    printf("%s\n",data);
  }
} 
void printIntArray(array_t * array)
{
  
  int i;
  int data;
  arrayForEachItem(int, array, i, data)
  {
    printf("%d\n",data);
  }
} 
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);
    }
  }
}
/**Function********************************************************************
 
  Synopsis    [Test if a node is in a given submodule]

  Description [Return true if the node is in one of the submdule, 
  else return false. The comparison is made by the name of the node
  compare to the name of the submodule. Node name n that belongs to a 
  subsystem named sub as in the following form : sub.n]

  SideEffects []

  SeeAlso     []

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

boolean Dbg_TestNodeInSubs(char* nodeName,array_t * subsName)
{
  assert(nodeName != NIL(char));
  if(subsName == NIL(array_t))
    return 0;
  if(array_n(subsName) == 0)
    return 0;
  int i;
  char * subName;
  arrayForEachItem(char*, subsName, i, subName){
      if(strstr(nodeName,subName) != NULL) 
        return 1;
  }
  return 0;
}