Index: vis_dev/vis-2.3/src/debug/debug.c
===================================================================
--- vis_dev/vis-2.3/src/debug/debug.c	(revision 40)
+++ vis_dev/vis-2.3/src/debug/debug.c	(revision 41)
@@ -65,4 +65,5 @@
 static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
 static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
+static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
 
 
@@ -94,4 +95,5 @@
   Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
   Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
+  Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 0);
 
 }
@@ -176,27 +178,4 @@
 
 ******************************************************************************/
-static int
-checkIndex(
-  int             index,
-  BmcCnfClauses_t *cnfClauses)
-{
-  int     rtnValue = -1; /* it is not TRUE or FALSE*/
-
-  if (index == 0){ /* TRUE or FALSE*/
-    if (cnfClauses->emptyClause){   /* last added clause was empty = FALSE*/
-      rtnValue = 0; /* FALSE */
-    } else {
-      /*
-	if (cnfClauses->noOfClauses == 0)
-	rtnValue = 1;
-	}
-      */
-      rtnValue = 1; /* TRUE */
-    }
-  }
-  return rtnValue;
-}
-
-
 static int 
 CommandSatDebug(
@@ -206,145 +185,71 @@
 int            c,i;
 int            verbose = 0;              /* default value */
-BmcOption_t  *options = BmcOptionAlloc();
-Ntk_Network_t * network;
-bAig_Manager_t    *manager;
-array_t           *formulaArray;
-array_t           *LTLformulaArray;
-char *ltlFileName     = NIL(char);
+BmcOption_t      * options = BmcOptionAlloc();
+Ntk_Network_t    * network;
+bAig_Manager_t   * manager;
+array_t          * formulaArray;
+array_t          * LTLformulaArray;
+char             * ltlFileName     = NIL(char);
+
 
 /*
  * Parse command line options.
  */
-util_getopt_reset();
-while ((c = util_getopt(argc, argv, "vhp: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;
-    case 'p':
-      ltlFileName     = util_strsav(util_optarg);
-    break;
-
-    default:
-      goto usage;
-  }
-}
+if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
+     return 1;
+}
+
+
 printf("MAX K %d", options->maxK);
- 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)){
+/*
+ *  Read the network
+ */
+network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+if (network == NIL(Ntk_Network_t)) {
+  (void) fprintf(vis_stdout, "** _sat_debug error: No network\n");
   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;
-    }
-  }
+manager = Ntk_NetworkReadMAigManager(network);
+if (manager == NIL(mAig_Manager_t)) {
+  (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n");
+  BmcOptionFree(options);
+  return 1;
+}
+
 Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
-printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
-/*
- * Read the formula
- */
- /* Read LTL Formulae */
-  if (!ltlFileName) 
-      goto usage;
-
-  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
-  if (options->ltlFile == NIL(FILE)) {
-    (void) fprintf(vis_stdout,"** _sat_debug error: Cannot open the file %s\n", ltlFileName);
-    FREE(ltlFileName);
-    BmcOptionFree(options);
-  }
-  FREE(ltlFileName);
-
- formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
-  if (formulaArray == NIL(array_t)) {
-    (void) fprintf(vis_stderr,
-		   "** bmc error: error in parsing CTL* Fromula from file\n");
-    BmcOptionFree(options);
-    return 1;
-  }
-  if (array_n(formulaArray) == 0) {
-    (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
-    BmcOptionFree(options);
-    Ctlsp_FormulaArrayFree(formulaArray);
-    return 1;
-  }
-  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
+if(abn == NIL(Dbg_Abnormal_t)){
+  (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n");
+  return 1;
+}
+if(verbose)
+  printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
+
+
+formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
+if (formulaArray == NIL(array_t)) {
+  (void) fprintf(vis_stderr,
+  	   "** bmc error: error in parsing CTL* Fromula from file\n");
+  BmcOptionFree(options);
+  return 1;
+}
+if (array_n(formulaArray) == 0) {
+  (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
+  BmcOptionFree(options);
   Ctlsp_FormulaArrayFree(formulaArray);
-  if (LTLformulaArray ==  NIL(array_t)){
-    (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
-    BmcOptionFree(options);
-    return 1;
-  }
-    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
+  return 1;
+}
+LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
+Ctlsp_FormulaArrayFree(formulaArray);
+if (LTLformulaArray ==  NIL(array_t)){
+  (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
+  BmcOptionFree(options);
+  return 1;
+}
+Ctlsp_Formula_t *ltlFormula  = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
 
 
@@ -353,4 +258,5 @@
     Compute the cone of influence 
 	here : a list of state variables (latches)
+    TODO refine to COI of the property
   */
 	st_table        *CoiTable =  generateAllLatches(network);
@@ -359,33 +265,12 @@
       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)
+  	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
-     */
-    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
-     fprintf(vis_stdout, "\n");
-    BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
-				 cnfClauses, nodeToMvfAigTable, CoiTable);
+    BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
+
 
     //Generate ltl CNF
@@ -393,4 +278,6 @@
     // aprÃšs il faut ajouter l'objectif de l'index avec boucle ou pas ...
     // cf. BmcLtlVerifyGeneralLtl
+    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
+    fprintf(vis_stdout, "\n");
     int k = options->maxK;
     int l;
@@ -398,6 +285,5 @@
     int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
    
-    int leftValue   = checkIndex(noLoopIndex, cnfClauses);
-    printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue); 
+
 	array_t           *objClause = NIL(array_t);
 	objClause = array_alloc(int, 0);   
@@ -406,10 +292,33 @@
     array_free(objClause);
 
-	
-//TODO Add abnormal formula 
-
-
-
-
+	//Add Abnormal
+    st_table * nodeToMvfAigTable =  NIL(st_table);
+    nodeToMvfAigTable =
+(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
+assert(nodeToMvfAigTable != NIL(st_table));
+
+    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);
+
+      //loop abnormal
+    int aIndex;
+    Ntk_Node_t * abnNode;
+     Dbg_ForEachAbnormal(abn,aIndex,abnNode){
+     if(aIndex<=0){
+     //set abnormal
+      int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex);
+      bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
+      int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses);
+      array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
+
+      FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
+      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
+      fclose(cnfFile);
+
+      //SAT procedure 
+      int res = Dbg_SatCheck("assig",options->cnfFileName);
+
+        array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
+        }
+     }
 
 	 if(verbose)
@@ -417,22 +326,150 @@
 		latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
    	
- Ctlsp_FormulaArrayFree(LTLformulaArray);    
-	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
-fclose(cnfFile);
+Ctlsp_FormulaArrayFree(LTLformulaArray);    
 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] [-p ltl_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");  
+ 
+}
+/**Function********************************************************************
+
+  Synopsis    [Implements the generate_network_cnf.]
+
+  CommandName [generate_network_cnf]
+
+  CommandSynopsis [generate a CNF view of the network]
+
+  CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
+  
+  CommandDescription [This command geerate a CNF of the network in DMACS form.
+  The network may be unroll within k steps.
+  <p>
+
+  Command options:<p>  
+
+  <dl>
+  <dt> -h
+  <dd> Print the command usage.
+  </dl>
+
+  <dt> -v
+  <dd> Verbose mode.
+  </dl>
+
+  <dt> -k
+  <dd> number of steps (default 1).
+  </dl>
+  ]
+
+  SideEffects []
+
+******************************************************************************/
+
+static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
+{
+  BmcOption_t  *options = BmcOptionAlloc();
+  int c;
+  unsigned int i;
+  Ntk_Network_t * network;
+  bAig_Manager_t   * manager;
+  char *  outName = NIL(char);
+   FILE *cnfFile;
+  if (!options){
+    return 1;
+  }
+  options->dbgOut = 0;
+  /*
+   * Parse command line options.
+   */
+  util_getopt_reset();
+  while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
+    switch(c) {
+    case 'h':
+      goto usage;
+    case 'k':
+      options->maxK = atoi(util_optarg);
+      break;
+    case 'v':
+      for (i = 0; i < strlen(util_optarg); i++) {
+	if (!isdigit((int)util_optarg[i])) {
+	  goto usage;
+	}
+      }
+      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
+      break;
+    default:
+      goto usage;
+    }
+  }
+   if (argc - util_optind != 0)
+   {
+      outName  = util_strsav(argv[util_optind]);
+      /* create SAT Solver input file */
+     options->cnfFileName= outName;
+    options->satInFile = options->cnfFileName;
+    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
+  }
+  
+ 
+/*
+ *  Read the network
+ */
+network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+if (network == NIL(Ntk_Network_t)) {
+  (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
+  BmcOptionFree(options);
+  return 1;
+}
+manager = Ntk_NetworkReadMAigManager(network);
+if (manager == NIL(mAig_Manager_t)) {
+  (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
+  BmcOptionFree(options);
+  return 1;
+}
+
+ /*
+    Compute the cone of influence 
+	here : a list of state variables (latches)
+  */
+st_table        *CoiTable =  generateAllLatches(network);
+
+if(options->verbosityLevel)
+{	
+	(void) fprintf(vis_stdout, "------      COI       ----\n");
+	printLatch(CoiTable);
+	(void) fprintf(vis_stdout, "--------------------------\n");
+}
+BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
+  if(outName != NIL(char))
+  {
+    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
+    fclose(cnfFile);
+  }
+  else
+     BmcWriteClauses(manager, vis_stdout, cnfClauses, options);
+
+if(options->verbosityLevel)
+{	
+	(void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
+    (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
+    st_count(CoiTable));
+} 
+    
+BmcOptionFree(options);
+ return 0;
+ usage:
+  (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n");
+  (void) fprintf(vis_stderr, "   -h \tprint the command usage\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 debug instance\n");  
-  (void) fprintf(vis_stderr, "   -p <ltl_file> contains the ltl formula\n");  
-  return 1;		/* error exit */
-
-}
+  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
+  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
+  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
+  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
+  (void) fprintf(vis_stderr, "   <cnf_file> The output file containing CNF of the network.\n");
+
+  BmcOptionFree(options);
+  return 1;
+}
+
 /**Function********************************************************************
 
