Index: vis_dev/vis-2.3/src/debug/debug.c
===================================================================
--- vis_dev/vis-2.3/src/debug/debug.c	(revision 30)
+++ vis_dev/vis-2.3/src/debug/debug.c	(revision 35)
@@ -7,5 +7,5 @@
   Synopsis    [Debug package initialization, ending, and the command debug]
 
-  Author      [Originated from SIS.]
+  Author      [Cecile B.]
 
   Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
@@ -61,6 +61,8 @@
 /*---------------------------------------------------------------------------*/
 
+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);
 
 
@@ -88,6 +90,8 @@
    * 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,      0);
+  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);
 
 }
@@ -122,4 +126,279 @@
 /*---------------------------------------------------------------------------*/
 
+
+static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
+{
+  Ntk_Network_t * ntk;
+  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+  if (ntk == NIL(Ntk_Network_t)) {
+	(void) fprintf(vis_stdout, "** abn error: No network\n");
+	return 1;
+  }
+  lsGen gen;
+  Ntk_Node_t* node;
+
+  (void) fprintf(vis_stdout, "** NODE **\n");
+  Ntk_NetworkForEachNode(ntk,gen,node){
+	  if(Ntk_NodeTestIsCombinational(node)){
+		if(Ntk_NodeReadNumFanins(node) > 1 && Ntk_NodeReadNumFanouts(node)> 0)
+		{
+		  if(strcmp(Ntk_NodeReadName(node),"_n2")==0)
+		  {
+			char * nodeName = util_strsav(Ntk_NodeReadName(node));
+	        printf("%s \n",  nodeName); 
+			(void) fprintf(vis_stdout, "** read table\n");
+			Tbl_Table_t    *table =  Ntk_NodeReadTable(node);
+
+			Tbl_TableWriteBlifMvToFile(table,2,vis_stdout);
+			// Build new variables abnormal  and  input
+			//abn
+			char * abnName = (char *) malloc(strlen(nodeName) + 5);
+			sprintf(abnName,"abn_%s",Ntk_NodeReadName(node));
+			Var_Variable_t * abn = Var_VariableAlloc(NIL(Hrc_Node_t),abnName);
+			Ntk_Node_t * newNode = Ntk_NodeCreateInNetwork(ntk, abnName,abn);
+			Ntk_NodeDeclareAsPrimaryInput(newNode);
+			//new free inputs
+			char * iName = (char *) malloc(strlen(nodeName) + 3);
+			sprintf(iName,"i_%s",Ntk_NodeReadName(node));
+			Var_Variable_t * i = Var_VariableAlloc(NIL(Hrc_Node_t),iName);
+			Ntk_Node_t * newNode2 = Ntk_NodeCreateInNetwork(ntk, iName, i);
+			Ntk_NodeDeclareAsPrimaryInput(newNode2);
+			//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);
+
+			//For each row already there in the table
+			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);
+				printf("entry : colNum %d \n",colNum);
+				if(colNum == abnIndex || colNum == iIndex)
+					Tbl_EntrySetValue(entry,1,1);
+				else
+					Tbl_EntrySetValue(entry,0,1);
+			    Tbl_TableSetEntry(table, entry, r, colNum, 0);
+			}
+			for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){
+				Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
+				Tbl_EntrySetValue(entry,1,1);
+			    Tbl_TableSetEntry(table, entry, r, colNum, 1);
+			}
+			 printf("---------------\n");
+			 Tbl_TablePrintStats(table, vis_stdout);
+			 Tbl_TableWriteBlifMvToFile(table,0,vis_stdout);
+			 free(abnName);
+			 free(iName);
+		  }
+		}
+	 }
+  }
+  // TODO
+  //Remplacer l'ancien network par le nouveau 
+}
+/**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********************************************************************
 
