print_hybrid_options - print information about the hybrid image computation options currently in use _________________________________________________________________ print_hybrid_options [-h] [-H] Prints information about the current hybrid image computation options. Command options: -h Print the command usage. -H Print the hybrid image computation set command usage. Set parameters: The hybrid image computation options are specified with the set command. hybrid_mode Specify a mode how to start hybrid computation. mode must be one of the following: 0 : start with only transition function and build transition relation on demand 1 : start with both transition function and relation (default) 2 : start with only transition relation. Only this mode can deal with nondeterminism. hybrid_tr_split_method Specify a method to choose a splitting variable in hybrid mode = 2. method must be one of the following: 0 : use support (default) 1 : use estimate BDD size hybrid_build_partial_tr Specify whether to build full or partial transition relation in hybrid mode = 2. This option is used to use less memory. When we use partial transition relation, for the variables excluded in the transition relation, we build each bit transition relation on demand. When nondeterminism exists in the circuit, this can not be used. method must be one of the following: yes : build partial transition relation no : build full transition relation (default) hybrid_partial_num_vars Specify how many variables are going to be excluded in building partial transition relation. The default is 8. hybrid_partial_method Specify a method to choose variables to be excluded in building partial transition relation. method must be one of the following: 0 : use BDD size (default) 1 : use support hybrid_delayed_split Specify a method whether to split transition relation immediately or just all at once before AndExist. method must be one of the following: yes : apply splitting to transition relation at once no : do not apply (default) hybrid_split_min_depth Specify the minimum depth to apply dynamic hybrid method. If a depth is smaller than this minimum depth, just split. The default is 1. hybrid_split_max_depth Specify the maximum depth to apply dynamic hybrid method. If a depth is bigger than this maximum depth, just conjoin. The default is 5. hybrid_pre_split_min_depth Specify the minimum depth to apply dynamic hybrid method in preimage computation. If a depth is smaller than this minimum depth, just split. The default is 0. hybrid_pre_split_max_depth Specify the maximum depth to apply dynamic hybrid method in preimage computation. If a depth is bigger than this maximum depth, just conjoin. The default is 4. hybrid_lambda_threshold Specify a threshold in floating between 0.0 and 1.0 to determine to split or to conjoin after computing variable lifetime lambda for image computation. If lambda is equal or smaller than this threshold, we conjoin. Otherwise we split. The default is 0.6 hybrid_pre_lambda_threshold Specify a threshold in floating between 0.0 and 1.0 to determine to split or to conjoin after computing variable lifetime lambda for preimage computation. If lambda is equal or smaller than this threshold, we conjoin. Otherwise we split. The default is 0.65 hybrid_conjoin_vector_size If the number of components in transition function vector is equal or smaller than this threshold, we just conjoin. This check is performed before computing lambda. The default is 10. hybrid_conjoin_relation_size If the number of clusters in transition relation is equal or smaller than this threshold, we just conjoin. This check is performed before computing lambda. The default is 2. hybrid_conjoin_relation_bdd_size If the shared BDD size of transition relation is equal or smaller than this threshold, we conjoin. This check is performed before computing lambda. The default is 200. hybrid_improve_lambda When variable lifetime lambda is bigger than lambda threshold, if the difference between previous and current lambda is equal or smaller than this threshold, then we conjoin. The default is 0.1. hybrid_improve_vector_size When variable lifetime lambda is bigger than lambda threshold, if the difference between the previous and current number of components in transition function vector is equal or smaller than this threshold, then we conjoin. The default is 3. hybrid_improve_vector_bdd_size When variable lifetime lambda is bigger than lambda threshold, if the difference between the previous and current shared BDD size of transition function vector is equal or smaller than this threshold, then we conjoin. The default is 30.0. hybrid_decide_mode Specify a method to decide whether to split or to conjoin. method must be one of the following: 0 : use only lambda 1 : use lambda and also special checks to conjoin 2 : use lambda and also improvement 3 : use all (default) hybrid_reorder_with_from Specify a method to reorder transition relation to conjoin in image computation, whether to include from set in the computation. method must be one of the following: yes : reorder relation array with from to conjoin (default) no : reorder relation array without from to conjoin hybrid_pre_reorder_with_from Specify a method to reorder transition relation to conjoin in preimage computation, whether to include from set in the computation. method must be one of the following: yes : reorder relation array with from to conjoin no : reorder relation array without from to conjoin (default) hybrid_lambda_mode Specify a method to decide which variable lifetime to be used for image computation. method must be one of the following: 0 : total lifetime with ps/pi variables (default) 1 : active lifetime with ps/pi variables 2 : total lifetime with ps/ns/pi variables hybrid_pre_lambda_mode Specify a method to decide which variable lifetime to be used for preimage computation. method must be one of the following: 0 : total lifetime with ns/pi variables 1 : active lifetime with ps/pi variables 2 : total lifetime with ps/ns/pi variables (default) 3 : total lifetime with ps/pi variables hybrid_lambda_with_from Specify a method to compute variable lifetime lambda, whether to include from set in the computation. method must be one of the following: yes : include from set in lambda computation (default) no : do not include hybrid_lambda_with_tr Specify a method to compute variable lifetime lambda, whether to use transition relation or transition function vector, when both exist. method must be one of the following: yes : use transition relation (default) no : use transition function vector hybrid_lambda_with_clustering Specify a method whether to include clustering to compute variable lifetime lambda. method must be one of the following: yes : compute lambda after clustering no : do not cluster (default) hybrid_synchronize_tr Specify a method to keep transition relation. This option is only for when hybrid mode is 1. method must be one of the following: yes : rebuild transition relation from function vector whenever the function vector changes no : do not rebuild (default) hybrid_img_keep_pi Specify a method to build forward transition relation. method must be one of the following: yes : keep all primary input variables in forward transition relation. no : quantify out local primary input variables from the transition relation. (default) hybrid_pre_keep_pi Specify a method to build backward transition relation. method must be one of the following: yes : keep all primary input variables in backward transition relation and preimages. no : quantify out local primary input variables from the transition relation. (default) hybrid_pre_canonical Specify a method whether to canonicalize the function vector for preimage computation. method must be one of the following: yes : canonicalize the function vector no : do not canonicalize (default) hybrid_tr_method lt;methodgt; Specify an image method for AndExist operation in hybrid method. method must be one of the following: iwls95 (default) mlp _________________________________________________________________ Last updated on 20100410 00h02