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


Last updated on 2010/11/04 13h:34