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