- Timestamp:
- Jul 19, 2012, 2:40:12 PM (12 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
vis_dev/vis-2.3/src/bmc/bmcCmd.c
r15 r102 48 48 /*static*/ BmcOption_t * ParseBmcOptions(int argc, char **argv); 49 49 static int CommandBmc(Hrc_Manager_t ** hmgr, int argc, char ** argv); 50 static int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv); 50 51 static void TimeOutHandle(void); 51 52 static void DispatchBmcCommand(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray, BmcOption_t *options); … … 74 75 75 76 Cmd_CommandAdd("cnf_sat", CommandCnfSat, /* doesn't change network */ 0); 77 Cmd_CommandAdd("write_cnf", CommandWriteCnf, /* doesn't change network */ 0); 76 78 } 77 79 … … 1267 1269 }/* CommandBddSat() */ 1268 1270 #endif 1271 1272 1273 int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv) 1274 { 1275 Ntk_Network_t *network; 1276 bAig_Manager_t *manager; 1277 array_t *formulaArray; 1278 array_t *LTLformulaArray; 1279 char * outFileName = NIL(char); 1280 char * ltlFileName = NIL(char); 1281 FILE * ltlFile; 1282 FILE * outFile; 1283 int c,i; 1284 int maxK = 0; 1285 st_table *allLatches; 1286 BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t); 1287 1288 1289 outFile = vis_stdout ; 1290 // Parse option 1291 util_getopt_reset(); 1292 while ((c = util_getopt(argc, argv, "f:o:k:h")) != EOF) { 1293 switch(c) { 1294 case 'h': 1295 goto usage; 1296 case 'o' : 1297 outFileName = strdup(util_optarg); 1298 outFile = Cmd_FileOpen(outFileName, "w", NIL(char *), 0); 1299 break; 1300 case 'f' : 1301 ltlFileName = strdup(util_optarg); 1302 break; 1303 case 'k': 1304 for (i = 0; i < strlen(util_optarg); i++) { 1305 if (!isdigit((int)util_optarg[i])) { 1306 goto usage; 1307 } 1308 } 1309 maxK = atoi(util_optarg); 1310 break; 1311 1312 break; 1313 default: 1314 goto usage; 1315 } 1316 } 1317 network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); 1318 if (network == NIL(Ntk_Network_t)) { 1319 (void) fprintf(vis_stdout, "** bmc error: No network\n"); 1320 return 1; 1321 } 1322 manager = Ntk_NetworkReadMAigManager(network); 1323 if (manager == NIL(mAig_Manager_t)) { 1324 (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n"); 1325 return 1; 1326 } 1327 1328 // Create a clause database 1329 1330 cnfClauses = BmcCnfClausesAlloc(); 1331 // Gnerate clauses for an initialized path of length k 1332 // nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph 1333 st_table* nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); 1334 assert(nodeToMvfAigTable != NIL(st_table)); 1335 allLatches = st_init_table(st_ptrcmp, st_ptrhash); 1336 1337 // Get all the latches of the network 1338 lsGen gen ; 1339 Ntk_Node_t *node; 1340 Ntk_NetworkForEachNode(network,gen, node){ 1341 if (Ntk_NodeTestIsLatch(node)){ 1342 st_insert(allLatches, (char *) node, (char *) 0); 1343 } 1344 } 1345 1346 1347 BmcCnfGenerateClausesForPath(network, 0, maxK, BMC_INITIAL_STATES, 1348 cnfClauses, nodeToMvfAigTable, allLatches); 1349 1350 // If ltl file exists 1351 if(ltlFileName != NIL(char)) 1352 { 1353 ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0); 1354 formulaArray = Ctlsp_FileParseFormulaArray(ltlFile); 1355 if (formulaArray == NIL(array_t)) { 1356 (void) fprintf(vis_stderr, 1357 "** bmc error: error in parsing ltl Fromula from file\n"); 1358 return 1; 1359 } 1360 LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray); 1361 for (i = 0; i < array_n(LTLformulaArray); i++) { 1362 Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, 1363 LTLformulaArray, i); 1364 BmcGenerateCnfForLtl(network, ltlFormula, 0, maxK, 0, cnfClauses); 1365 } 1366 } 1367 1368 1369 // Write Clauses 1370 1371 st_generator *stGen; 1372 char *name; 1373 int cnfIndex,k; 1374 1375 st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) { 1376 fprintf(outFile, "c %s %d\n",name, cnfIndex); 1377 } 1378 (void) fprintf(outFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1, 1379 cnfClauses->noOfClauses); 1380 if (cnfClauses->clauseArray != NIL(array_t)) { 1381 for (i = 0; i < cnfClauses->nextIndex; i++) { 1382 k = array_fetch(int, cnfClauses->clauseArray, i); 1383 (void) fprintf(outFile, "%d%c", k, (k == 0) ? '\n' : ' '); 1384 } 1385 } 1386 if(outFileName != NIL(char)) 1387 fclose(outFile); 1388 1389 return 1; 1390 1391 usage: 1392 (void) fprintf(vis_stderr, "usage: write_cnf [-h] [-f ltl file] [-o outfile] [k]\n"); 1393 (void) fprintf(vis_stderr, " -h \tprint the command usage\n"); 1394 (void) fprintf(vis_stderr, " -f <filename> \tto add a ltlfile\n"); 1395 (void) fprintf(vis_stderr, " -o <filename> \twrite output in outputfile\n"); 1396 (void) fprintf(vis_stderr, " -k <value> \tnumber of unroll steps\n"); 1397 return 1; 1398 1399 }
Note: See TracChangeset
for help on using the changeset viewer.