[11] | 1 | |
---|
| 2 | print_hybrid_options - print information about the hybrid image computation |
---|
| 3 | options currently in use |
---|
| 4 | _________________________________________________________________ |
---|
| 5 | |
---|
| 6 | print_hybrid_options [-h] [-H] |
---|
| 7 | |
---|
| 8 | Prints information about the current hybrid image computation options. |
---|
| 9 | |
---|
| 10 | Command options: |
---|
| 11 | |
---|
| 12 | -h |
---|
| 13 | Print the command usage. |
---|
| 14 | |
---|
| 15 | -H |
---|
| 16 | Print the hybrid image computation set command usage. |
---|
| 17 | |
---|
| 18 | Set parameters: The hybrid image computation options are specified |
---|
| 19 | with the set command. |
---|
| 20 | |
---|
| 21 | hybrid_mode <mode> |
---|
| 22 | Specify a mode how to start hybrid computation. |
---|
| 23 | |
---|
| 24 | mode must be one of the following: |
---|
| 25 | |
---|
| 26 | 0 : start with only transition function and build transition |
---|
| 27 | relation on demand |
---|
| 28 | |
---|
| 29 | 1 : start with both transition function and relation (default) |
---|
| 30 | |
---|
| 31 | 2 : start with only transition relation. Only this mode can |
---|
| 32 | deal with nondeterminism. |
---|
| 33 | |
---|
| 34 | hybrid_tr_split_method <method> |
---|
| 35 | Specify a method to choose a splitting variable in hybrid mode |
---|
| 36 | = 2. |
---|
| 37 | |
---|
| 38 | method must be one of the following: |
---|
| 39 | |
---|
| 40 | 0 : use support (default) |
---|
| 41 | |
---|
| 42 | 1 : use estimate BDD size |
---|
| 43 | |
---|
| 44 | hybrid_build_partial_tr <method> |
---|
| 45 | Specify whether to build full or partial transition relation in |
---|
| 46 | hybrid mode = 2. This option is used to use less memory. When |
---|
| 47 | we use partial transition relation, for the variables excluded |
---|
| 48 | in the transition relation, we build each bit transition |
---|
| 49 | relation on demand. When nondeterminism exists in the circuit, |
---|
| 50 | this can not be used. |
---|
| 51 | method must be one of the following: |
---|
| 52 | |
---|
| 53 | yes : build partial transition relation |
---|
| 54 | |
---|
| 55 | no : build full transition relation (default) |
---|
| 56 | |
---|
| 57 | hybrid_partial_num_vars <number> |
---|
| 58 | Specify how many variables are going to be excluded in building |
---|
| 59 | partial transition relation. The default is 8. |
---|
| 60 | |
---|
| 61 | hybrid_partial_method <method> |
---|
| 62 | Specify a method to choose variables to be excluded in building |
---|
| 63 | partial transition relation. |
---|
| 64 | |
---|
| 65 | method must be one of the following: |
---|
| 66 | |
---|
| 67 | 0 : use BDD size (default) |
---|
| 68 | |
---|
| 69 | 1 : use support |
---|
| 70 | |
---|
| 71 | hybrid_delayed_split <method> |
---|
| 72 | Specify a method whether to split transition relation |
---|
| 73 | immediately or just all at once before AndExist. |
---|
| 74 | |
---|
| 75 | method must be one of the following: |
---|
| 76 | |
---|
| 77 | yes : apply splitting to transition relation at once |
---|
| 78 | |
---|
| 79 | no : do not apply (default) |
---|
| 80 | |
---|
| 81 | hybrid_split_min_depth <number> |
---|
| 82 | Specify the minimum depth to apply dynamic hybrid method. If a |
---|
| 83 | depth is smaller than this minimum depth, just split. The |
---|
| 84 | default is 1. |
---|
| 85 | |
---|
| 86 | hybrid_split_max_depth <number> |
---|
| 87 | Specify the maximum depth to apply dynamic hybrid method. If a |
---|
| 88 | depth is bigger than this maximum depth, just conjoin. The |
---|
| 89 | default is 5. |
---|
| 90 | |
---|
| 91 | hybrid_pre_split_min_depth <number> |
---|
| 92 | Specify the minimum depth to apply dynamic hybrid method in |
---|
| 93 | preimage computation. If a depth is smaller than this minimum |
---|
| 94 | depth, just split. The default is 0. |
---|
| 95 | |
---|
| 96 | hybrid_pre_split_max_depth <number> |
---|
| 97 | Specify the maximum depth to apply dynamic hybrid method in |
---|
| 98 | preimage computation. If a depth is bigger than this maximum |
---|
| 99 | depth, just conjoin. The default is 4. |
---|
| 100 | |
---|
| 101 | hybrid_lambda_threshold <number> |
---|
| 102 | Specify a threshold in floating between 0.0 and 1.0 to |
---|
| 103 | determine to split or to conjoin after computing variable |
---|
| 104 | lifetime lambda for image computation. If lambda is equal or |
---|
| 105 | smaller than this threshold, we conjoin. Otherwise we split. |
---|
| 106 | The default is 0.6 |
---|
| 107 | |
---|
| 108 | hybrid_pre_lambda_threshold <number> |
---|
| 109 | Specify a threshold in floating between 0.0 and 1.0 to |
---|
| 110 | determine to split or to conjoin after computing variable |
---|
| 111 | lifetime lambda for preimage computation. If lambda is equal or |
---|
| 112 | smaller than this threshold, we conjoin. Otherwise we split. |
---|
| 113 | The default is 0.65 |
---|
| 114 | |
---|
| 115 | hybrid_conjoin_vector_size <number> |
---|
| 116 | If the number of components in transition function vector is |
---|
| 117 | equal or smaller than this threshold, we just conjoin. This |
---|
| 118 | check is performed before computing lambda. The default is 10. |
---|
| 119 | |
---|
| 120 | hybrid_conjoin_relation_size <number> |
---|
| 121 | If the number of clusters in transition relation is equal or |
---|
| 122 | smaller than this threshold, we just conjoin. This check is |
---|
| 123 | performed before computing lambda. The default is 2. |
---|
| 124 | |
---|
| 125 | hybrid_conjoin_relation_bdd_size <number> |
---|
| 126 | If the shared BDD size of transition relation is equal or |
---|
| 127 | smaller than this threshold, we conjoin. This check is |
---|
| 128 | performed before computing lambda. The default is 200. |
---|
| 129 | |
---|
| 130 | hybrid_improve_lambda <number> |
---|
| 131 | When variable lifetime lambda is bigger than lambda threshold, |
---|
| 132 | if the difference between previous and current lambda is equal |
---|
| 133 | or smaller than this threshold, then we conjoin. The default is |
---|
| 134 | 0.1. |
---|
| 135 | |
---|
| 136 | hybrid_improve_vector_size <number> |
---|
| 137 | When variable lifetime lambda is bigger than lambda threshold, |
---|
| 138 | if the difference between the previous and current number of |
---|
| 139 | components in transition function vector is equal or smaller |
---|
| 140 | than this threshold, then we conjoin. The default is 3. |
---|
| 141 | |
---|
| 142 | hybrid_improve_vector_bdd_size <number> |
---|
| 143 | When variable lifetime lambda is bigger than lambda threshold, |
---|
| 144 | if the difference between the previous and current shared BDD |
---|
| 145 | size of transition function vector is equal or smaller than |
---|
| 146 | this threshold, then we conjoin. The default is 30.0. |
---|
| 147 | |
---|
| 148 | hybrid_decide_mode <method> |
---|
| 149 | Specify a method to decide whether to split or to conjoin. |
---|
| 150 | |
---|
| 151 | method must be one of the following: |
---|
| 152 | |
---|
| 153 | 0 : use only lambda |
---|
| 154 | |
---|
| 155 | 1 : use lambda and also special checks to conjoin |
---|
| 156 | |
---|
| 157 | 2 : use lambda and also improvement |
---|
| 158 | |
---|
| 159 | 3 : use all (default) |
---|
| 160 | |
---|
| 161 | hybrid_reorder_with_from <method> |
---|
| 162 | Specify a method to reorder transition relation to conjoin in |
---|
| 163 | image computation, whether to include from set in the |
---|
| 164 | computation. |
---|
| 165 | |
---|
| 166 | method must be one of the following: |
---|
| 167 | |
---|
| 168 | yes : reorder relation array with from to conjoin (default) |
---|
| 169 | |
---|
| 170 | no : reorder relation array without from to conjoin |
---|
| 171 | |
---|
| 172 | hybrid_pre_reorder_with_from <method> |
---|
| 173 | Specify a method to reorder transition relation to conjoin in |
---|
| 174 | preimage computation, whether to include from set in the |
---|
| 175 | computation. |
---|
| 176 | |
---|
| 177 | method must be one of the following: |
---|
| 178 | |
---|
| 179 | yes : reorder relation array with from to conjoin |
---|
| 180 | |
---|
| 181 | no : reorder relation array without from to conjoin (default) |
---|
| 182 | |
---|
| 183 | hybrid_lambda_mode <method> |
---|
| 184 | Specify a method to decide which variable lifetime to be used |
---|
| 185 | for image computation. |
---|
| 186 | |
---|
| 187 | method must be one of the following: |
---|
| 188 | |
---|
| 189 | 0 : total lifetime with ps/pi variables (default) |
---|
| 190 | |
---|
| 191 | 1 : active lifetime with ps/pi variables |
---|
| 192 | |
---|
| 193 | 2 : total lifetime with ps/ns/pi variables |
---|
| 194 | |
---|
| 195 | hybrid_pre_lambda_mode <method> |
---|
| 196 | Specify a method to decide which variable lifetime to be used |
---|
| 197 | for preimage computation. |
---|
| 198 | |
---|
| 199 | method must be one of the following: |
---|
| 200 | |
---|
| 201 | 0 : total lifetime with ns/pi variables |
---|
| 202 | |
---|
| 203 | 1 : active lifetime with ps/pi variables |
---|
| 204 | |
---|
| 205 | 2 : total lifetime with ps/ns/pi variables (default) |
---|
| 206 | |
---|
| 207 | 3 : total lifetime with ps/pi variables |
---|
| 208 | |
---|
| 209 | hybrid_lambda_with_from <method> |
---|
| 210 | Specify a method to compute variable lifetime lambda, whether |
---|
| 211 | to include from set in the computation. |
---|
| 212 | |
---|
| 213 | method must be one of the following: |
---|
| 214 | |
---|
| 215 | yes : include from set in lambda computation (default) |
---|
| 216 | |
---|
| 217 | no : do not include |
---|
| 218 | |
---|
| 219 | hybrid_lambda_with_tr <method> |
---|
| 220 | Specify a method to compute variable lifetime lambda, whether |
---|
| 221 | to use transition relation or transition function vector, when |
---|
| 222 | both exist. |
---|
| 223 | |
---|
| 224 | method must be one of the following: |
---|
| 225 | |
---|
| 226 | yes : use transition relation (default) |
---|
| 227 | |
---|
| 228 | no : use transition function vector |
---|
| 229 | |
---|
| 230 | hybrid_lambda_with_clustering <method> |
---|
| 231 | Specify a method whether to include clustering to compute |
---|
| 232 | variable lifetime lambda. |
---|
| 233 | |
---|
| 234 | method must be one of the following: |
---|
| 235 | |
---|
| 236 | yes : compute lambda after clustering |
---|
| 237 | |
---|
| 238 | no : do not cluster (default) |
---|
| 239 | |
---|
| 240 | hybrid_synchronize_tr <method> |
---|
| 241 | Specify a method to keep transition relation. This option is |
---|
| 242 | only for when hybrid mode is 1. |
---|
| 243 | |
---|
| 244 | method must be one of the following: |
---|
| 245 | |
---|
| 246 | yes : rebuild transition relation from function vector whenever |
---|
| 247 | the function vector changes |
---|
| 248 | |
---|
| 249 | no : do not rebuild (default) |
---|
| 250 | |
---|
| 251 | hybrid_img_keep_pi <method> |
---|
| 252 | Specify a method to build forward transition relation. |
---|
| 253 | |
---|
| 254 | method must be one of the following: |
---|
| 255 | |
---|
| 256 | yes : keep all primary input variables in forward transition |
---|
| 257 | relation. |
---|
| 258 | |
---|
| 259 | no : quantify out local primary input variables from the |
---|
| 260 | transition relation. (default) |
---|
| 261 | |
---|
| 262 | hybrid_pre_keep_pi <method> |
---|
| 263 | Specify a method to build backward transition relation. |
---|
| 264 | |
---|
| 265 | method must be one of the following: |
---|
| 266 | |
---|
| 267 | yes : keep all primary input variables in backward transition |
---|
| 268 | relation and preimages. |
---|
| 269 | |
---|
| 270 | no : quantify out local primary input variables from the |
---|
| 271 | transition relation. (default) |
---|
| 272 | |
---|
| 273 | hybrid_pre_canonical <method> |
---|
| 274 | Specify a method whether to canonicalize the function vector |
---|
| 275 | for preimage computation. |
---|
| 276 | |
---|
| 277 | method must be one of the following: |
---|
| 278 | |
---|
| 279 | yes : canonicalize the function vector |
---|
| 280 | |
---|
| 281 | no : do not canonicalize (default) |
---|
| 282 | |
---|
| 283 | hybrid_tr_method lt;methodgt; |
---|
| 284 | Specify an image method for AndExist operation in hybrid |
---|
| 285 | method. |
---|
| 286 | |
---|
| 287 | method must be one of the following: |
---|
| 288 | |
---|
| 289 | iwls95 (default) |
---|
| 290 | |
---|
| 291 | mlp |
---|
| 292 | _________________________________________________________________ |
---|
| 293 | |
---|
| 294 | Last updated on 20050519 10h16 |
---|