print_hybrid_options - print information about the hybrid image computation options currently in use

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.

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

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

Specify how many variables are going to be excluded in building partial transition relation. The default is 8.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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