Changeset 41 for vis_dev/vis-2.3/src/debug/debugAbnormal.c

Timestamp:

Jan 10, 2012, 6:51:23 PM (12 years ago)

Author:

cecile

Message:

new command generate cnf from network

File:

• vis_dev/vis-2.3/src/debug/debugAbnormal.c (modified) (3 diffs)

vis_dev/vis-2.3/src/debug/debugAbnormal.c

@@ -138 +138 @@
          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;
@@ -158 +160 @@
          array_free(abn->abnormal);
          array_free(abn->freeInputs);
+     array_free(abn->abnCnfIndexArray);
+     array_free(abn->abnAigArray);
          FREE(abn);
 }       
@@ -267 +271 @@
         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;
+}