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

  FileName    [debug.c]

  PackageName [debug]

  Synopsis    [Debug package initialization, ending, and the command debug]

  Author      [Cecile B.]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

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

#include "debugInt.h"
#include "imgInt.h"
#include "partInt.h"
static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12  braun Exp $";

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

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

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

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

static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);


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


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

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

  Synopsis    [Initializes the test package.]

  SideEffects []

  SeeAlso     [Debug_End]

******************************************************************************/
void
Debug_Init(void)
{
  /*
   * Add a command to the global command table.  By using the leading
   * underscore, the command will be listed under "help -a" but not "help".
   */
  Cmd_CommandAdd("_debug_test",  CommandDebug, /* doesn't changes_network */ 0);
  Cmd_CommandAdd("_transition",  CommandTransition, 1);
  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);

}


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

  Synopsis    [Ends the test package.]

  SideEffects []

  SeeAlso     [Debug_Init]

******************************************************************************/
void
Debug_End(void)
{
  /*
   * For example, free any global memory (if any) which the test package is
   * responsible for.
   */
}


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
{
  Ntk_Network_t * ntk;
  int c,verbose;
  Dbg_Abnormal_t * abnormal;
  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (ntk == NIL(Ntk_Network_t)) {
	(void) fprintf(vis_stdout, "** abn error: No network\n");
	return 1;
  }
  while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
	switch(c) {
		case 'v':
			verbose = 1;
			break;
		}
 }
  abnormal = Dbg_DebugAbnormalAlloc(ntk);
  abnormal->verbose = verbose;
  Dbg_AddAbnormalPredicatetoNetwork(abnormal);
}
/**Function********************************************************************

  Synopsis    [Implements the _sat_debug command.]

  CommandName [_sat_debug]

  CommandSynopsis [locate faulty candidates]

  CommandArguments [\[-h\] \[-v\]]
  
  CommandDescription [This command compute the fault candidates of a given
  properties.<p>

  Command options:<p>  

  <dl>
  <dt> -h
  <dd> Print the command usage.
  </dl>

  <dt> -v
  <dd> Verbose mode.
  </dl>
  ]

  SideEffects []

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


static int 
CommandSatDebug(
Hrc_Manager_t ** hmgr, 
int argc, 
char ** argv){
int            c,i;
int            verbose = 0;              /* default value */
BmcOption_t  *options = BmcOptionAlloc();
Ntk_Network_t * network;
bAig_Manager_t    *manager;


/*
 * Parse command line options.
 */
util_getopt_reset();
while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
  switch(c) {
    case 'v':
      verbose = 1;
	  options->verbosityLevel =  verbose;
      break;
    case 'h':
      goto usage;
	case 'm':
      for (i = 0; i < strlen(util_optarg); i++) {
		if (!isdigit((int)util_optarg[i])) {
			goto usage;
		}
      }
      options->minK = atoi(util_optarg);
      break;
    case 'k':
      for (i = 0; i < strlen(util_optarg); i++) {
		if (!isdigit((int)util_optarg[i])) {
			goto usage;
		}
      }
	  options->maxK = atoi(util_optarg);
	  break;
	case 'o':
      options->cnfFileName = util_strsav(util_optarg);
      break;	

    default:
      goto usage;
  }
}
 if (options->minK > options->maxK){
    (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");    
    goto usage;
  }

if (verbose) {
  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
}
 /* create SAT Solver input file */
 if (options->cnfFileName == NIL(char)) {
    options->satInFile = BmcCreateTmpFile(); 
}
 else {
    options->satInFile = options->cnfFileName;
 }

/* create SAT Solver output file */
options->satOutFile = BmcCreateTmpFile();
if (options->satOutFile == NIL(char)){
  BmcOptionFree(options);
 (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
  return 1;
}

options->verbosityLevel =  1;
//options->satSolver
//options->clauses 

 /*
   * Read the network
   */
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    (void) fprintf(vis_stdout, "** bmc error: No network\n");
    BmcOptionFree(options);
    return 1;
  }
  manager = Ntk_NetworkReadMAigManager(network);
  if (manager == NIL(mAig_Manager_t)) {
    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
    BmcOptionFree(options);
    return 1;
  }
  /*
    We need the bdd when building the transition relation of the automaton
  */
  if(options->inductiveStep !=0){
    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
 
    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
    if (designFsm == NIL(Fsm_Fsm_t)) {
	 (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
      return 1;
    }
  }

 /*
    Compute the cone of influence 
	here a list of state variables (latches)
  */
	st_table        *CoiTable =  generateAllLatches(network);
  /*
      Generate clauses for each time frame.  This is the old way of generating
      clauses in BMC.
    */
    st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
	BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
    FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
	/*
    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));

	if(verbose)
	{	
		(void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
		printLatch(nodeToMvfAigTable);
		(void) fprintf(vis_stdout, "------      COI       ----\n");
		printLatch(CoiTable);
		(void) fprintf(vis_stdout, "--------------------------\n");
    }
    /*
      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);
	 if(verbose)
		(void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
		latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
   	
    
	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
fclose(cnfFile);
BmcCnfClausesFree(cnfClauses);
BmcOptionFree(options);
return 0;
  usage:
  (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
  minimum length] [-o cnf_file]\n");
  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
  (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n");  
  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the counterexample\n");  
  return 1;		/* error exit */

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

  Synopsis    [Implements the _Debug_test command.]

  CommandName [_Debug_test]

  CommandSynopsis [template for implementing commands]

  CommandArguments [\[-h\] \[-v\]]
  
  CommandDescription [This command does nothing useful.  It merely serves as a
  template for the implementation of new commands.<p>

  Command options:<p>  

  <dl>
  <dt> -h
  <dd> Print the command usage.
  </dl>

  <dt> -v
  <dd> Verbose mode.
  </dl>
  ]

  SideEffects []

******************************************************************************/
static int
CommandDebug(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int            c;
  int            verbose = 0;              /* default value */

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
    switch(c) {
      case 'v':
        verbose = 1;
        break;
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }

  if (verbose) {
    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
  }

  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
  printf("** DEBUG MODE **\n");
  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
  printf("model : %s\n", Hrc_NodeReadModelName(n));

  mdd_t * safe   = getSafe(fsm);
  mdd_t * forbid = getForbidden(fsm);
  mdd_t * reach  = getReach(fsm);
  
  if(safe == NIL(mdd_t))
  {
	printf("call command set_safe before\n");
	return 1;
  }
  if(forbid == NIL(mdd_t))
  {
	printf("call command set_forbidden before\n");
	return 1;
  }

  FILE*  oFile;
  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);

  mdd_t * EFState = mdd_and(reach,safe,1,1);
//  mdd_t * errorState = mdd_and(reach,forbid,1,1);

  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
  array_t *careStatesArray = array_alloc(mdd_t *, 0);
  array_insert(mdd_t *, careStatesArray, 0,mddOne);

  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
		   EFState,
           fsm->fairnessInfo.states,
           careStatesArray,
		   0,
           McDcLevelNone_c);

  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);

  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
		   EXEFState,
           fsm->fairnessInfo.states,
           careStatesArray,
		   0,
           McDcLevelNone_c);
  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
		   andState,
           fsm->fairnessInfo.states,
           careStatesArray,
		   0,
           McDcLevelNone_c);
  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
  andState =  mdd_xor(EXEFState2,andState);
  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
		   andState,
           fsm->fairnessInfo.states,
           careStatesArray,
		   0,
           McDcLevelNone_c);
  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
  andState =  mdd_xor(EXEFState2,andState);
  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);



  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
  //mdd_GetState_Values(mddManager , EFState, stdout);
  fclose(oFile);





  return 0;		/* normal exit */

  usage:
  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
  return 1;		/* error exit */
}

/******************************************/
/* function that build a bdd for the      */
/* simple example :                       */
/*     (state = 0) -> !(state = 1)        */
/******************************************/
mdd_t * buildDummyBdd(mdd_manager   *mddManager)
{
/** state0 = 0 **/
 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
 mdd_t * state0 =  mdd_one(mddManager);
 state0 = mdd_and(s0,s1,1,1);
/** state1 = 1 **/
 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
 mdd_t * state1 =  mdd_one(mddManager);
 state1 = mdd_and(ns0,ns1,1,1);
/** state = 0) -> !(state = 1) **/
 mdd_t * rel =  mdd_one(mddManager);
 rel =  mdd_or(state0,state1,0,0);
 
 return rel;
}


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

  Synopsis    [Implements the transtion command.]

  CommandName [_transition]

  CommandSynopsis [compute new transition relation]

  CommandArguments [\[-h\] \[-v\]]
  
  CommandDescription [This command create a new transition relation that is a
  and of the Bdd of the old one and an other bdd.
  <p>

  Command options:<p>  

  <dl>
  <dt> -h
  <dd> Print the command usage.
  </dl>

  <dt> -v
  <dd> Verbose mode.
  </dl>
  ]

  SideEffects [Change the fsm]

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

static int 
CommandTransition (Hrc_Manager_t ** hmgr,
		   int  argc, char ** argv){
int            c;
int            verbose = 0;              /* default value */

/*
 * Parse command line options.
 */
util_getopt_reset();
while ((c = util_getopt(argc, argv, "vh")) != EOF) {
  switch(c) {
    case 'v':
      verbose = 1;
      break;
    case 'h':
      goto usage;
    default:
      goto usage;
  }
}

if (verbose) {
  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
}

Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
Ntk_Network_t  *network      = NIL(Ntk_Network_t);
mdd_manager    *mddManager; 
mdd_t          *rel          = NIL(mdd_t);
graph_t        *partition;
int            i;
/******************/
network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if(network == NIL(Ntk_Network_t))
	return 1;
fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
if(fsm ==  NIL(Fsm_Fsm_t))
	return 1;
mddManager   = Fsm_FsmReadMddManager(fsm);



/**********   Build cex  ***********/
/* Here add the function           */
/* that build the Bdd to and       */
/* with the transtion relation     */
/***********************************/
rel = buildDummyBdd(mddManager);
if(rel == NIL(mdd_t))
{
	fprintf(vis_stdout,"Problem when building the new relation bdd");
	return 1;
}

/** Get image_info **/
Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
/**** The complete transtion relation ****/
// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
/*****************************************/
/*** For each latch rebuild the transition function ***/
/*** mvf table is composed of mdd for each possible ***/
/*** value of the latch                             ***/
ImgFunctionData_t * functionData = &(imageInfo->functionData);
array_t *roots = functionData->roots;
array_t *rangeVarMddIdArray = functionData->rangeVars;
char * nodeName;
arrayForEachItem(char *, roots, i, nodeName) {
	/* The new relation */ 
	vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
    int mddId = array_fetch(int, rangeVarMddIdArray, i);
	mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
	mdd_t * n_relation = mdd_and(relation,rel,1,1);
    /* Build for each possible value */
	int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
	int v ;
	Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
	for(v = 0; v<nbValue;v++)
	{
		 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
		 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
		 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
		 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);

	}
	/* Replace the function for the latch */
	Part_VertexSetFunction(vertex, newMvf);
//	printf("vertex %s changed % d\n",PartVertexReadName(vertex));
	Mvf_FunctionFree(mvf);
}

/** Change the fsm **/
fsm = Fsm_FsmCreateFromNetworkWithPartition(network, partition);
mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
Fsm_FsmComputeReachableStates(fsm,0,verbose,
				      0,0, 0,
				      0, 0, Fsm_Rch_Default_c,
				      0,1, NIL(array_t),
				      (verbose > 0),  NIL(array_t));
if(verbose)
	Fsm_FsmReachabilityPrintResults(fsm,3, 0);
/** Change Image Info **/
Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
					  (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
					  (void *) partition);


return 0;		/* normal exit */

usage:
(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
return 1;		/* error exit */

}