#include "debugInt.h"
/**Function********************************************************************
 
  Synopsis    [create New node]

  Description [Create new primary input in the current network at a given
  output node.  Return the variable created]

  SideEffects [Modify the network]

  SeeAlso     []

******************************************************************************/
Ntk_Node_t * Dbg_CreateNewNode(Ntk_Network_t * ntk,Ntk_Node_t*
node, char * varName  )
{
	array_t * fanin = array_dup(Ntk_NodeReadFanins(node));
	array_t * fanout = array_alloc(Ntk_Node_t*,0);
	char * nodeName = util_strsav(Ntk_NodeReadName(node));
	//Create var Name
	char * newVarName = (char *) malloc(strlen(nodeName) + strlen(varName) +1);
	sprintf(newVarName,"%s_%s",nodeName,varName);
	Var_Variable_t * var = Var_VariableAlloc(NIL(Hrc_Node_t),newVarName);
	//Create new Node
	Ntk_Node_t * newNode = Ntk_NodeCreateInNetwork(ntk, newVarName,var);
	Ntk_NodeDeclareAsPrimaryInput(newNode);
	//Add in the fanin of the node
    array_insert_last(Ntk_Node_t*,fanin,newNode);
	Ntk_NodeSetFanins(node,fanin);
	//Add Fanout to the newNode
    array_insert_last(Ntk_Node_t*,fanout,node);
	Ntk_NodeSetFanouts(newNode,fanout);
	free(newVarName);

	return newNode;

}
/**Function********************************************************************
 
  Synopsis    [Add abnormal predicates to the network]

  Description [Given a network after flatten the hierarchy,
  change the table of each combinatorial node
  with a new table including the abnormal predicate.
  For a combinatorial node n is tranformed into (abn_n)?i_n:n 
  If the abnormal predicate is active then n is replaced by a free input.
  We assume that the combinatorial gate at on one bit only.]

  SideEffects [fill the abnormal structure]

  SeeAlso     []

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

void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal ) /*abnormal struct*/
{

  Ntk_Network_t * ntk = abnormal->network;
  lsGen gen;
  Ntk_Node_t* node;
  Ntk_NetworkForEachNode(ntk,gen,node){
  //For each combinatorial node
  if(Ntk_NodeTestIsCombinational(node)){
	if(Ntk_NodeReadNumFanins(node) > 1 && Ntk_NodeReadNumFanouts(node)> 0)
	{
		char * nodeName = util_strsav(Ntk_NodeReadName(node));
        printf("%s \n",  nodeName); 

		Tbl_Table_t    *table =  Ntk_NodeReadTable(node);
        if(abnormal->verbose){
		  (void) fprintf(vis_stdout, "** old table\n");
		  Tbl_TableWriteBlifMvToFile(table,2,vis_stdout);
        }
		// Build new variables abnormal  and  input
		Ntk_Node_t * abnNode = Dbg_CreateNewNode(ntk,node,"abn");
		Ntk_Node_t * iNode   = Dbg_CreateNewNode(ntk,node,"i");
		Dbg_AddFreeInput(abnormal,iNode);
		Dbg_AddAbnormalPredicate(abnormal,abnNode);
		Var_Variable_t * abn = Ntk_NodeReadVariable(abnNode);
		Var_Variable_t * i   = Ntk_NodeReadVariable(iNode);
		//Add in the table
		Tbl_TableAddColumn(table,abn,0);
		int abnIndex = Tbl_TableReadVarIndex(table, abn, 0);
		Tbl_TableAddColumn(table,i,0);
		int iIndex = Tbl_TableReadVarIndex(table, i, 0);
        
		int rowNum;
		for(rowNum = 0; rowNum <  Tbl_TableReadNumRows(table);rowNum++){
			Tbl_Entry_t *abnEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
			Tbl_EntrySetValue(abnEntry,0,0);
			Tbl_TableSetEntry(table, abnEntry, rowNum, abnIndex, 0);
			Tbl_Entry_t *iEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
			Tbl_EntrySetValue(iEntry,0,1);
			Tbl_TableSetEntry(table, iEntry, rowNum, iIndex, 0);
		}
		//the new row
		int r = Tbl_TableAddRow(table);
        
		int colNum;
	    for (colNum = 0; colNum < Tbl_TableReadNumInputs(table); colNum++) {
			Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
			if(colNum == abnIndex || colNum == iIndex)
				Tbl_EntrySetValue(entry,1,1);
			else
				Tbl_EntrySetValue(entry,0,1);
		    Tbl_TableSetEntry(table, entry, r, colNum, 0);
		}
        int defaultVal = Dbg_GetDefaultValue(table);
        if(defaultVal == -1)
        {
          	(void) fprintf(vis_stdout, "Error default value of the table \
            of node %s\n", nodeName);
            return;
        }
        int outVal = (defaultVal +1 )% 2;
        if(abnormal->verbose)
          	(void) fprintf(vis_stdout, "Default value : %d\n",defaultVal);
		for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){
			Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
			Tbl_EntrySetValue(entry,outVal,outVal);
		    Tbl_TableSetEntry(table, entry, r, colNum, 1);
		}
        if(abnormal->verbose){
		 printf("---------------\n");
		 Tbl_TableWriteBlifMvToFile(table,0,vis_stdout);
        }
	  }
	}
}
 Ntk_NetworkAddApplInfo(ntk, DBG_NETWORK_APPL_KEY,
 (Ntk_ApplInfoFreeFn) Dbg_AbnormalFreeCallback,
 (void *) abnormal);
}
/**Function********************************************************************
 
  Synopsis    [Allocate a new abnormal structure]

  Description [The structure contains the network with abnormal predicate,
  and two sets of Ntk_Node_t for the abnormal and the free inputs]

  SideEffects [Allocate the abnormal structure]

  SeeAlso     []

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

Dbg_Abnormal_t * Dbg_DebugAbnormalAlloc(Ntk_Network_t * network)
{
	 Dbg_Abnormal_t * abn = ALLOC(Dbg_Abnormal_t, 1);

	 abn->network = network;
	 abn->abnormal = array_alloc(Ntk_Node_t*,0);
	 abn->freeInputs = array_alloc(Ntk_Node_t*,0);
     abn->abnAigArray = NIL(array_t);
     abn->abnCnfIndexArray = NIL(array_t);
	 abn->verbose = 0;
	 return abn;
}	

/**Function********************************************************************
 
  Synopsis    [Deallocate a new abnormal structure]

  Description [Free the arrays not the network]

  SideEffects [free the abnormal structure]

  SeeAlso     []

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

void  Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn)
{
	 array_free(abn->abnormal);
	 array_free(abn->freeInputs);
     array_free(abn->abnCnfIndexArray);
     array_free(abn->abnAigArray);
	 FREE(abn);
}	
/**Function********************************************************************

  Synopsis    [Call-back function to free an abnormal structure.]

  Description [This function will be stored in the network together with the
  pointer to the structure. Whenever the network deletes the partitioning
  information, this function is called and it will deallocate the abnormal and
  the information attached to it.]

  SideEffects []

  SeeAlso     [Ntk_NetworkAddApplInfo]

******************************************************************************/
void
Dbg_AbnormalFreeCallback(
   void *data)
{
  Dbg_DebugAbnormalFree((Dbg_Abnormal_t *) data);
} /* End of Part_PartitionFreeCallback */


/**Function********************************************************************
 
  Synopsis    [Add abnormal predicate]

  Description [add a node to the predicates array, it should not be already
  present by construction of abnormal predicate]

  SideEffects []

  SeeAlso     []

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

void  Dbg_AddAbnormalPredicate(Dbg_Abnormal_t * abn, Ntk_Node_t* abnNode)
{
	assert(abnNode != NIL(Ntk_Node_t*));
	array_insert_last(Ntk_Node_t*,abn->abnormal, abnNode);
}
/**Function********************************************************************
 
  Synopsis    [Add free inputs]

  Description [add a node to the free inputs, it should not be already
  present by construction of abnormal predicate]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void  Dbg_AddFreeInput(Dbg_Abnormal_t * abn, Ntk_Node_t* fNode)
{
	assert(fNode != NIL(Ntk_Node_t*));
	array_insert_last(Ntk_Node_t*,abn->freeInputs, fNode);
}

/**Function********************************************************************
 
  Synopsis    [returns a free inputs]

  Description [returns the array of freeinputs]

  SideEffects []

  SeeAlso     [Dbg_ReadAbn]

******************************************************************************/
array_t* Dbg_ReadFreeInputs(Dbg_Abnormal_t *abnormal)
{
	assert(abnormal != NIL(Dbg_Abnormal_t));
	return abnormal->freeInputs;
}
/**Function********************************************************************
 
  Synopsis    [returns a abnormal predicates]

  Description [returns the array of abnormal predicates]

  SideEffects []

  SeeAlso     [Dbg_ReadFreeInputs]

******************************************************************************/
array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal)
{
	assert(abnormal != NIL(Dbg_Abnormal_t));
	return abnormal->abnormal;
}
/**Function********************************************************************
 
  Synopsis    [returns the abnormal structure]

  Description [returns the abnormal structure associated to the network]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network)
{
	Dbg_Abnormal_t * abn = (Dbg_Abnormal_t *) Ntk_NetworkReadApplInfo(network, DBG_NETWORK_APPL_KEY);

	return abn;
}
/**Function********************************************************************
 
  Synopsis    [Initialize the abnormal predicate in the clauses array abni =0]

  Description [Fill the Dbg data structure, abnAigArray conains the set of Aig 
  for the set of abnormal perdicate. Each abnormal are set to zero in the clause
  array.predicabnCnfIndexArray is the cnf index. The   correspondance is made by
  the index in the table, the index of a node in   abnArray is the same in
  abnAigArray and in abnIndexArray. If this array were  alredy computed nothing
  is done, if the aig or index information either.]

  SideEffects [Fill abnAigArray and abnCnfIndexArray]

  SeeAlso     []

******************************************************************************/
void Dbg_InitAbn(Dbg_Abnormal_t * abn,
bAig_Manager_t   * manager,
st_table * nodeToMvfAigTable,
BmcCnfClauses_t *cnfClauses)
{
  if(abn->abnAigArray != NIL(array_t))
    (void) fprintf(vis_stdout, "Abnormal aig alredy filled\n");
  if(abn->abnCnfIndexArray != NIL(array_t)){
    (void) fprintf(vis_stdout, "Abnormal index alredy filled\n"); 
     return;
  }
  //Fill
   int size = array_n(abn->abnormal);
   array_t * abnAigArray = array_alloc(bAigEdge_t *,size);
   array_t * abnIndexArray = array_alloc(int,size);
   int aIndex;
   Ntk_Node_t * abnNode;
   Dbg_ForEachAbnormal(abn, aIndex,abnNode){
   MvfAig_Function_t * abnMvfAig = Bmc_ReadMvfAig(abnNode, nodeToMvfAigTable);
    if (abnMvfAig ==  NIL(MvfAig_Function_t)){
     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \
     create abnormal predicate firs \n", Ntk_NodeReadName(abnNode));
     return ;
    }
    int mvfSize   = array_n(abnMvfAig);
    int i;
    bAigEdge_t         * abnBAig  = ALLOC(bAigEdge_t, mvfSize);

    for(i=0; i< mvfSize; i++)
    {
      abnBAig[i] = bAig_GetCanonical(manager,
      MvfAig_FunctionReadComponent(abnMvfAig,  i));
    }
    array_insert(bAigEdge_t*,abnAigArray,aIndex,abnBAig);
    int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[0],0,cnfClauses);
    array_insert(int,abnIndexArray,aIndex,cnfClauses->nextIndex);
    // Create clause
     array_t           *abnClause = NIL(array_t);
	 abnClause = array_alloc(int, 0);   
	 array_insert_last(int, abnClause, abnIndex);
	 BmcCnfInsertClause(cnfClauses, abnClause);
     array_free(abnClause);
   }
   abn->abnAigArray = abnAigArray;
   abn->abnCnfIndexArray = abnIndexArray;
}