Changeset 41 for vis_dev/vis-2.3/src/debug/debugUtilities.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/debugUtilities.c (modified) (1 diff)

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

@@ -87 +87 @@
   return;
 }
+/**Function********************************************************************
+ 
+  Synopsis    [Performs the sat call]
+
+  Description [Retrun the result of SAT call, avec positionnement des options]
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+
+int Dbg_SatCheck(char * forceAssigName, char * cnfFileName
+)
+{
+ satManager_t *cm;
+ cm = sat_InitManager(0);
+ cm->comment = ALLOC(char, 2);
+ cm->comment[0] = ' ';
+ cm->comment[1] = '\0';
+ cm->stdOut = stdout;
+ cm->stdErr = stderr;
+
+ 
+  satOption_t  *satOption;
+  array_t      *result = NIL(array_t);
+  int          maxSize;
+
+  satOption = sat_InitOption();
+  satOption->verbose = 2;
+  //satOption->unsatCoreFileName = "Ucore.txt";
+  satOption->clauseDeletionHeuristic = 0;
+  //satOption->coreGeneration = 1 ;
+  //satOption->minimizeConflictClause = 1;
+  if(forceAssigName != NULL)
+    satOption->forcedAssignArr = sat_ReadForcedAssignment(forceAssigName);
+   cm->option = satOption;
+   cm->each = sat_InitStatistics();
+
+  cm->unitLits = sat_ArrayAlloc(16);
+  cm->pureLits = sat_ArrayAlloc(16);
+
+  maxSize = 1024 << 8;
+  cm->nodesArray = ALLOC(long, maxSize);
+  cm->maxNodesArraySize = maxSize;
+  cm->nodesArraySize = satNodeSize;
+
+  sat_AllocLiteralsDB(cm);
+
+   sat_ReadCNF(cm,cnfFileName);
+   sat_Main(cm);
+
+   if(cm->status == SAT_UNSAT) {
+    if(cm->option->forcedAssignArr)
+      fprintf(cm->stdOut, "%s UNSAT under given assignment\n",
+              cm->comment);
+    fprintf(cm->stdOut, "%s UNSATISFIABLE\n", cm->comment);
+    fflush(cm->stdOut);
+    sat_ReportStatistics(cm, cm->each);
+    sat_FreeManager(cm);
+  }
+  else if(cm->status == SAT_SAT) {
+    fprintf(cm->stdOut, "%s SATISFIABLE\n", cm->comment);
+    fflush(cm->stdOut);
+    sat_PrintSatisfyingAssignment(cm);
+    sat_ReportStatistics(cm, cm->each);
+    sat_FreeManager(cm);
+  }
+return cm->status;
+}
+/**Function********************************************************************
+ 
+  Synopsis    [Generate a CNF of the network]
+
+  Description [Generate the set of clauses of the unroll network for a given 
+  length and for a given cone of influence]
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+BmcCnfClauses_t*
+Dbg_GenerateCNF(Ntk_Network_t * network, 
+BmcOption_t * options,
+st_table  *CoiTable
+){
+st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
+BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
+/*
+ *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));
+/*
+ * 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);
+return cnfClauses;
+
+}