- Timestamp:
- Jul 19, 2012, 2:45:31 PM (12 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
vis_dev/vis-2.3/src/bmc/bmcCmd.c
r102 r103 1270 1270 #endif 1271 1271 1272 /**Function******************************************************************** 1273 1274 Synopsis [write_cnf] 1275 1276 Description [] 1277 1278 CommandName [write_cnf] 1279 1280 CommandSynopsis [Generate the CNF form of a design] 1281 1282 CommandArguments [\[-h\] \[-f <ltl_filename>\] 1283 \[-o <out_filename;\] 1284 \[-k <number of steps;\] 1285 1286 1287 CommandDescription [Generate the CNF form of the network and the ltl specification if mentionned. 1288 <p> 1289 <dt> -o <code><output_filename></code> 1290 <dd> Specify the output filename to save the satisfying assignments and 1291 the statistics of SAT solving. 1292 <p> 1293 <dt> -f <code><ltl_filename></code> 1294 <dd> Specify the ltl filename that will be generate with. 1295 <p> 1296 <dt> -k <code><value;</code> 1297 <dd> Specify the number of step unrolled (by default = 0) 1298 <p> 1299 1300 ] 1301 1302 SideEffects [] 1303 1304 SeeAlso [] 1305 1306 ******************************************************************************/ 1272 1307 1273 1308 int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv)
Note: See TracChangeset
for help on using the changeset viewer.