Changeset 103 for vis_dev/vis-2.3

Timestamp:

Jul 19, 2012, 2:45:31 PM (12 years ago)

Author:

cecile

Message:

add write_cnf comments

File:

• vis_dev/vis-2.3/src/bmc/bmcCmd.c (modified) (1 diff)

vis_dev/vis-2.3/src/bmc/bmcCmd.c

@@ -1270 +1270 @@
 #endif
 
+/**Function********************************************************************
+
+  Synopsis    [write_cnf]
+
+  Description []
+  
+  CommandName [write_cnf]
+
+  CommandSynopsis [Generate the CNF form of a design]
+
+  CommandArguments [\[-h\] \[-f <ltl_filename>\] 
+                    \[-o <out_filename;\] 
+                    \[-k <number of steps;\] 
+                    
+
+  CommandDescription [Generate the CNF form of the network and the ltl specification if mentionned.
+  <p>
+  <dt> -o  <code>&lt;output_filename&gt;</code>
+  <dd> Specify the output filename to save the satisfying assignments and 
+  the statistics of SAT solving.
+  <p>
+  <dt> -f  <code>&lt;ltl_filename&gt;</code>
+  <dd> Specify the ltl filename that will be generate with.
+  <p>
+  <dt> -k  <code>&lt;value;</code>
+  <dd> Specify the number of step unrolled (by default = 0)
+  <p>
+
+  ]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
 
 int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv)