node_ptr
bdd_enc_bdd_to_wff_rec(
BddEnc_ptr self,
NodeList_ptr vars,
bdd_ptr bdd,
hash_ptr cache memoization hashtable for DAG traversal
)
- This function accepts a list of variables as part of
its inputs.The present algorithm assumes that a variable in vars list
is a boolean only in two distinct cases:
1. Pure booleans
2. Boolean
variables belonging to words (i.e. Boolean variables belonging to a
scalar encoding are _not_ allowed in the input list of this
function. This would invariably cause this implementation to
fail). This assumptions are enforced by its public top-level caller.
- Side Effects none
- See Also
BddEnc_bdd_to_wff
void
bdd_enc_debug_bdd_to_wff(
BddEnc_ptr self,
bdd_ptr bdd,
node_ptr expr
)
- Debug code for BddEnc_bdd_to_wff
- Side Effects Halts NuSMV if the expression is not a correct
representation of bdd.
- See Also
BddEnc_bdd_to_wff
NodeList_ptr
bdd_enc_get_preprocessed_vars(
BddEnc_ptr self,
NodeList_ptr vars variables to be preprocessed
)
- This function is used to preprocess variables list to
provide to bddenc_print_wff_bdd. As the algorithm implemented in the
latter does not support word variables, word variables (if any)
shall be substituted with their bit variables
representatives. Moreover, this function takes care of adding NEXT
variables for state variables. For this reason no NEXT nor BITS are
allowed as input to this function.
The result NodeList must be destroyed by the caller.
- Side Effects none
- See Also
BddEnc_bdd_to_wff
bdd_ptr
bdd_enc_get_scalar_essentials(
BddEnc_ptr self,
bdd_ptr bdd,
NodeList_ptr vars variables
)
- Computes the scalar essentials of a bdd, picking
identifiers from the variables in vars list. Used as part of
bdd_enc_bdd_to_wff_rec implementation.
- See Also
bdd_enc_bdd_to_wff
assoc_retval
bdd_enc_hash_free_bdd_counted(
char* key,
char* data,
char* arg
)
- Used to deref bdds in the sharing hashtable