#include "utilities.h"
/*---------------------------------------------------------------------------*/
/* Read_blif_mv                                                              */
/*---------------------------------------------------------------------------*/
Hrc_Manager_t * rlmv(FILE * file)
{
		return  Io_BlifMvRead( file, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE);

}
/*---------------------------------------------------------------------------*/
/* flatten_hierarchy                                                         */
/*---------------------------------------------------------------------------*/
Ntk_Network_t * flatten_hier(Hrc_Manager_t * hmgr)
{
	assert(hmgr != NULL);
	int            sweep       = 1;
	int            verbose     = 0;
	lsList         varNameList = (lsList) NULL;
	Ntk_Network_t *ntk;
	// flatten
	Hrc_Node_t    *currentNode = Hrc_ManagerReadCurrentNode(hmgr);
	ntk = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, NULL);

	Hrc_NodeAddApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY,
                      (Hrc_ApplInfoFreeFn) Ntk_NetworkFreeCallback,
                      (Hrc_ApplInfoChangeFn) NULL,  // not currently used by hrc 
                      (void *) ntk);
	Ntk_NetworkSweep(ntk, verbose);
	return ntk;

}
/*---------------------------------------------------------------------------*/
/* Build_partition_maigs                                                     */
/*---------------------------------------------------------------------------*/

st_table * build_partition_maigs(Ntk_Network_t * ntk)
{
	Ntk_Node_t    *node, *latch;
    lsGen          gen;
	int i;
	array_t       *result;
	array_t		  *inputs;
	array_t       *roots;
	st_table      *leaves;
	st_table      *nodeToMvfAigTable;  /* mapes each node with its mvfAig */
	MvfAig_Function_t  *mvfAig;
	mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(ntk);
	if (manager == NIL(mAig_Manager_t)) {
		manager = mAig_initAig();
		Ntk_NetworkSetMAigManager(ntk, manager);
	}
	  roots = array_alloc(Ntk_Node_t *, 0);
  Ntk_NetworkForEachCombOutput(ntk, gen, node) {
    array_insert_last(Ntk_Node_t *, roots, node);
  }
  Ntk_NetworkForEachNode(ntk, gen, node) {
    if(Ntk_NodeTestIsShadow(node))	continue;
    if(Ntk_NodeTestIsCombInput(node))	continue;
    if(Ntk_NodeTestIsCombOutput(node))continue;

    if(Ntk_NodeReadNumFanouts(node) == 0 && Ntk_NodeReadNumFanins(node)) {
	/**
      fprintf(vis_stdout, "WARNING : dangling node %s\n", Ntk_NodeReadName(node));
      **/
      array_insert_last(Ntk_Node_t *, roots, node);
    }
  }

  leaves = st_init_table(st_ptrcmp, st_ptrhash);

  inputs = array_alloc(Ntk_Node_t *, 16);
  Ntk_NetworkForEachCombInput(ntk, gen, node) {
    array_insert_last(Ntk_Node_t *, inputs, node);
  }
  array_sort(inputs, nodenameCompare);
  for(i=0; i<array_n(inputs); i++) {
    node = array_fetch(Ntk_Node_t *, inputs, i);
    st_insert(leaves,  node, (char *) ntmaig_UNUSED);
    Ntk_NodeSetMAigId(node, 
                       mAig_CreateVar(manager,
		                      Ntk_NodeReadName(node),
                                      Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
  }
  result = ntmaig_NetworkBuildMvfAigs(ntk, roots, leaves);

  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(ntk, 
						  MVFAIG_NETWORK_APPL_KEY);
  Ntk_NetworkForEachLatch(ntk, gen, latch) {
		node  = Ntk_LatchReadDataInput(latch);
		st_lookup(nodeToMvfAigTable, node,  &mvfAig);
		Ntk_NodeSetMAigId(node, mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig));
		node  = Ntk_LatchReadInitialInput(latch);
		st_lookup(nodeToMvfAigTable, node,  &mvfAig);
		Ntk_NodeSetMAigId(node,   mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig));
	}

	roots->num = 0;
	Ntk_NetworkForEachLatch(ntk, gen, latch) {
		if(!st_lookup(nodeToMvfAigTable, latch,  &mvfAig))
			array_insert_last(Ntk_Node_t *, roots, latch);
		}
  result = ntmaig_NetworkBuildMvfAigs(ntk, roots, leaves);
  array_free(roots);
  array_free(inputs);
  st_free_table(leaves);
  MvfAig_FunctionArrayFree(result);
  return nodeToMvfAigTable;
}
/*---------------------------------------------------------------------------*/
/* Create unroll circuit k steps                                             */
/*---------------------------------------------------------------------------*/
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, (char *) 0);
		}
	}
	return CoiTable;

}
void build_unroll_circuit(Ntk_Network_t * ntk, int bound,BmcOption_t * options,BmcCnfClauses_t* cnfClauses)
{
    st_table        *CoiTable =  generateAllLatches(ntk);
	lsGen           gen ;
	Ntk_Node_t		*node;


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

	 options->verbosityLevel = BmcVerbosityMax_c;
	 options->satSolver = CirCUs;
	 options->timeOutPeriod = 0;
	 options->printInputs = TRUE;
	 options->minK = bound;
	 options->maxK = bound;
	 options->step = bound;
	 options->dbgLevel = 1;

     //nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph 
     st_table* nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(ntk, MVFAIG_NETWORK_APPL_KEY);
     assert(nodeToMvfAigTable != NIL(st_table));

     // Create clauses database 
	 int initState = BMC_INITIAL_STATES;
	 BmcCnfGenerateClausesForPath(ntk, 0, bound, initState, cnfClauses, nodeToMvfAigTable, CoiTable);

}

void printSATAssig( array_t* result)
{
	int k;
	printf("RESULT : \n");
	for(k=0; k< array_n(result); k++){
		printf("%d\n",array_fetch(int, result, k));
	}
}
void printNodeToMvFaigTable(st_table* nodeToMvfAigTable)
{
	// nodeToMvFaigTable contents
	st_generator    *stGen;
	Ntk_Node_t * latch;
	printf("*** NODETOMV ***\n");
	st_foreach_item(nodeToMvfAigTable, stGen, &latch, NULL) {
		printf("%s , %d\n",Ntk_NodeReadName(latch),Ntk_NodeReadMAigId(latch)); 
   	}
	printf("***************\n");
}
void printCNFIndex(BmcCnfClauses_t* cnfClauses)
{
	// Cnf index Table content
	st_generator    *stGen;
	nameType_t      *nodeName;
	int index,i,k;
	printf("*** cnfIndextable ***\n");
	st_foreach_item(cnfClauses->cnfIndexTable, stGen,&nodeName,&index){
		printf("(%s,%d)\n",nodeName, index);
	}
}
void printCNFClauses(BmcCnfClauses_t* cnfClauses)
{
	int i,k;
	printf("*** clause table ***\n");
	for (i = 0; i < cnfClauses->nextIndex; i++) {
		k = array_fetch(int, cnfClauses->clauseArray, i);
		printf("%d%c", k, (k == 0) ? '\n' : ' ');
    }
}
void
printClauseLits(satManager_t *cm,long concl,FILE * file)
{
  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(file,"%ld ", -var_idx);
    else
      fprintf(file,"%ld ",var_idx);
  }
  fprintf(file,"0\n");
}

int getClsIndex(long concl,int numVarInCnf)
{
	int clsIndex;
	clsIndex = concl -  numVarInCnf * satNodeSize;
    clsIndex = (clsIndex/satNodeSize)-1;
	return clsIndex;

}

void printSatArrayCore(satManager_t *cm,satArray_t *clauseIndexInCore)
{
	int i,v,clsIndex;
     for(i=0; i<clauseIndexInCore->num; i++) {
	 	v = clauseIndexInCore->space[i];
	 	clsIndex = getClsIndex(v,cm->initNumVariables);
		printf("\nclause idx = %d\n",clsIndex);
		printClauseLits(cm,v,vis_stdout);
	 }		
}
void printSatArrayCoreToCnf(satManager_t *cm,satArray_t *clauseIndexInCore, char *filename)
{
	FILE * file = fopen(filename,"w");
	fprintf(file,"p cnf %d %d\n",clauseIndexInCore->num,cm->initNumVariables);
	int i,v,clsIndex;
     for(i=0; i<clauseIndexInCore->num; i++) {
	 	v = clauseIndexInCore->space[i];
	 	clsIndex = getClsIndex(v,cm->initNumVariables);
		//printf("\nclause idx = %d\n",clsIndex);
		printClauseLits(cm,v,file);
	 }		
	 fclose(file);
}

array_t * checkSATCircus( satManager_t *cm,BmcOption_t * options, boolean unsatcore,	satArray_t *clauseIndexInCore)
{

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

  satOption = sat_InitOption();
  satOption->verbose = options->verbosityLevel;
  //satOption->unsatCoreFileName = "Ucore.txt";
  satOption->clauseDeletionHeuristic = 0;
  satOption->coreGeneration = unsatcore;
  satOption->minimizeConflictClause = 1;

  cm->comment = ALLOC(char, 2);
  cm->comment[0] = ' ';
  cm->comment[1] = '\0';
  cm->stdOut = stdout;
  cm->stdErr = stderr;

  cm->option = satOption;
  cm->each = sat_InitStatistics();

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

  maxSize = 10000 << (bAigNodeSize-4);
  cm->nodesArray = ALLOC(bAigEdge_t, maxSize);
  cm->maxNodesArraySize = maxSize;
  cm->nodesArraySize = bAigNodeSize;

  sat_AllocLiteralsDB(cm);
	
  sat_ReadCNF(cm, options->satInFile);
  sat_Main(cm);
   if(cm->status == SAT_UNSAT) {
    if (options->verbosityLevel != BmcVerbosityNone_c){
      (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
	  }
	  if(unsatcore)
	  {
		clauseIndexInCore =  cm->clauseIndexInCore;
	  }
    fflush(cm->stdOut);

	}else if(cm->status == SAT_SAT) {
    if (options->verbosityLevel != BmcVerbosityNone_c){
      (void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
    }
    fflush(cm->stdOut);
    result = array_alloc(int, 0);
    {
      int i, size, value;
      
      size = cm->initNumVariables * bAigNodeSize;
      for(i=bAigNodeSize; i<=size; i+=bAigNodeSize) {
		value = SATvalue(i);
		if(value == 1) {
			array_insert_last(int, result, SATnodeID(i));
		}
		else if(value == 0) {
			array_insert_last(int, result, -(SATnodeID(i)));
		}
      }
    }
  }
  return result;

}
int findIndex(BmcCnfClauses_t* cnfClauses , char * nodeName)
{	
	int index;
	st_lookup(cnfClauses->cnfIndexTable,nodeName,&index);
	return index;

}

mdd_t * buildBdd4StateVal(array_t* stateName, int max, array_t * val,
mdd_manager * mddManager)
{
	array_t * mvar_val= array_alloc(int,0);
	array_t * mvar_name= array_alloc(char*,0);
	array_t * mvar_strides= NIL(array_t);

    if(array_n(stateName) == 1)
	{
		array_insert_last(int, mvar_val,max);
		array_insert_last(char*, mvar_name,array_fetch(char*, stateName,0));
	}
	else
	{
		int i;
		for( i = 0;i<max;i++)  array_insert_last(int, mvar_val,1);
		mvar_name = array_dup(stateName);

		printf(" Num of var , %d %d \n",array_n(stateName),array_n(mvar_val));
		
	}
	
	mdd_create_variables(mddManager, mvar_val,mvar_name, mvar_strides);

	array_t *mvar_list = mdd_ret_mvar_list(mddManager);
	array_t *bvar_list = mdd_ret_bvar_list(mddManager);

	bvar_type bv = array_fetch(bvar_type, bvar_list, 0);

	mvar_type mv;
	bdd_node* f,*f2, * left, *right;
	int i,v, value,mask;

	f =  bdd_read_one(mddManager);
	bdd_ref(f);
	mv = array_fetch(mvar_type, mvar_list, 0);
	printf("mvar name: %s;%d\n", mv.name,array_n(bvar_list)); 
//	for(v=0;v<array_n(val); v++)
//	{	
		value = array_fetch(int,val,0);
		mask = 1;
		for(i= array_n(bvar_list)-1;i>=0; i--)
		{
		  printf("---->value %d , %d, %d \n",value,(value & mask),i);
			left =  bdd_bdd_ith_var(mddManager,i);
			if((value&mask) > 0)
				right =  bdd_bdd_and(mddManager,left,f);
			else
				right =  bdd_bdd_and(mddManager,bdd_not_bdd_node(left),f);
			bdd_ref(right);
			bdd_recursive_deref(mddManager,f);
			f = right;
			mask = mask *2;
		}

	for(v=1;v<array_n(val); v++)
	{	
		value = array_fetch(int,val,v);
		mask = 1;
		printf("----val_value : %d\n",value);
		f2 =  bdd_read_one(mddManager);
		bdd_ref(f2);

		for(i= array_n(bvar_list)-1;i>=0; i--)
		{
		  printf("---->value %d , %d, %d \n",value,(value & mask),i);
			left =  bdd_bdd_ith_var(mddManager,i);
			if((value&mask) > 0)
				right =  bdd_bdd_and(mddManager,left,f2);
			else
				right =  bdd_bdd_and(mddManager,bdd_not_bdd_node(left),f2);
			bdd_ref(right);
			bdd_recursive_deref(mddManager,f2);
			f2 = right;
			mask = mask *2;
		}
		right =  bdd_bdd_or(mddManager,f2,f);
		bdd_ref(right);
		bdd_recursive_deref(mddManager,f2);
		bdd_recursive_deref(mddManager,f);
		f = right;
	}
		
	mdd_t * mdd = bdd_construct_bdd_t(mddManager, f);
	mdd_print_support(mdd); 
	//FILE * file = fopen("bdd.dot","w");
	//bdd_dump_dot(mddManager, 1, &f, NULL, NULL,file);

	//fclose(file);
	array_free(mvar_val);
	array_free(mvar_name);

	return mdd;
	
}


void addObjState(array_t* stateName, int max, array_t * val, int steps,BmcCnfClauses_t *cnfClauses)
{
		
	mdd_manager * mddManager = mdd_init_empty();
	mdd_t * mdd =  buildBdd4StateVal(stateName, max,val,mddManager);
	int index;
	index = BmcGenerateCnfFormulaForBdd(mdd,steps, cnfClauses);
	printf("number of clause : %d index %d \n", cnfClauses-> noOfClauses,index);

	array_t * newClause;
	newClause = array_alloc(int,1);
	array_insert(int,newClause,0,index);
	BmcCnfInsertClause(cnfClauses, newClause);




	array_free(newClause);
	mdd_quit(mddManager);

	
}