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 |
---|