void 
BddEncCache_clean_evaluation_about(
  BddEncCache_ptr  self, 
  NodeList_ptr  symbs 
)
This is called by the BddEnc class when a layer is begin removed and the cache has to be cleaned up

Defined in BddEncCache.c

void 
BddEncCache_clean_evaluation(
  BddEncCache_ptr  self 
)
Note that hashed encoding of boolean variables and constants (added by BddEncCache_new_boolean_var and BddEncCache_new_constant, resp.) remains intact.

Defined in BddEncCache.c

BddEncCache_ptr 
BddEncCache_create(
  SymbTable_ptr  symb_table, 
  DdManager* dd 
)
Class constructor

Defined in BddEncCache.c

void 
BddEncCache_destroy(
  BddEncCache_ptr  self 
)
Class destructor

Defined in BddEncCache.c

AddArray_ptr 
BddEncCache_get_evaluation(
  BddEncCache_ptr  self, 
  node_ptr  expr 
)
If given symbol has not been evaluated, NULL is returned. If the evaluation is in the process, BDD_ENC_EVALUATING is returned. Otherwise an array of ADD is returned. The returned array must be destroyed by the invoker! NB: For all expressions except of the Word type the returned array can contain only one element. NB: If NuSMV option enable_sexp2bdd_caching is unset to 0 then the hash may be empty.

Defined in BddEncCache.c

boolean 
BddEncCache_is_boolean_var_encoded(
  const BddEncCache_ptr  self, 
  node_ptr  var_name 
)
Returns true whether the given boolean variable has been encoded

Defined in BddEncCache.c

boolean 
BddEncCache_is_constant_encoded(
  const BddEncCache_ptr  self, 
  node_ptr  constant 
)
Returns true whether the given constant has been encoded

Defined in BddEncCache.c

add_ptr 
BddEncCache_lookup_boolean_var(
  const BddEncCache_ptr  self, 
  node_ptr  var_name 
)
Returned add is referenced. NULL is returned if the variable is not encoded.

Defined in BddEncCache.c

add_ptr 
BddEncCache_lookup_constant(
  const BddEncCache_ptr  self, 
  node_ptr  constant 
)
Returned ADD is referenced, NULL is returned if the given constant is not currently encoded

Defined in BddEncCache.c

void 
BddEncCache_new_boolean_var(
  BddEncCache_ptr  self, 
  node_ptr  var_name, 
  add_ptr  var_add 
)
Call this to insert the encoding for a given boolean variable

Defined in BddEncCache.c

void 
BddEncCache_new_constant(
  BddEncCache_ptr  self, 
  node_ptr  constant, 
  add_ptr  constant_add 
)
This methods adds the given constant only if it does not exist already, otherwise it only increments a reference counter, to be used when the constant is removed later.

Defined in BddEncCache.c

void 
BddEncCache_remove_boolean_var(
  BddEncCache_ptr  self, 
  node_ptr  var_name 
)
Removes the given variable from the internal hash

Defined in BddEncCache.c

void 
BddEncCache_remove_constant(
  BddEncCache_ptr  self, 
  node_ptr  constant 
)
Removes the given constant from the internal hash

Defined in BddEncCache.c

void 
BddEncCache_remove_evaluation(
  BddEncCache_ptr  self, 
  node_ptr  expr 
)
If a given node_ptr is associated already with some AddArray then the array is freed. Otherwise nothing happens

Defined in BddEncCache.c

void 
BddEncCache_set_evaluation(
  BddEncCache_ptr  self, 
  node_ptr  expr, 
  AddArray_ptr  add_array 
)
The provided array of ADD will belong to "self" and will be freed during destruction of the class or setting a new value for the same node_ptr. NOTE: if NuSMV option "enable_sexp2bdd_caching" is unset to 0 then no result is kept and the provided add_array is immediately freed

Defined in BddEncCache.c

node_ptr 
BddEnc_bdd_to_wff(
  BddEnc_ptr  self, 
  bdd_ptr  bdd, 
  NodeList_ptr  vars variables
)
A new expression is built, that represents the formula given as the input bdd. The list of variables is used to compute the scalar essentials. Note that only the following kinds of variables are allowed in this list. 1. Pure booleans (i.e. not part of an encoding) 2. Finite scalars (both ranged and words). State, frozen and input variables are all allowed, no NEXT. (It will be part of this function's responsibility to add state variables' NEXTs as needed. SideEffects [none

See Also Bddenc_print_wff_bdd
Defined in BddEncBddPrintWff.c

void 
BddEnc_print_bdd_wff(
  BddEnc_ptr  self, 
  bdd_ptr  bdd, 
  NodeList_ptr  vars, 
  boolean  do_sharing, 
  boolean  do_indent, 
  int  start_at_column, 
  FILE* out the stream to write to
)
The bdd representing the formula to be printed is first converted to a wff. If sharing is required optimizations are performed on the printout. If indentation is required, the start_at_column integer offset is used to determine the starting indenting offset to print the expression.

Side Effects prints the expression on the given stream.

See Also BddEnc_bdd_to_wff
Defined in BddEncBddPrintWff.c

void 
BddEnc_print_formula_info(
  BddEnc_ptr  self, 
  Expr_ptr  formula, 
  boolean  print_models, 
  boolean  print_formula, 
  FILE* out 
)
Prints statistical information about a given formula. It is computed taking care of the encoding and of the indifferent variables in the encoding.

Defined in BddEncBddPrintWff.c

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
Defined in BddEncBddPrintWff.c

static void 
bdd_enc_cache_deinit(
  BddEncCache_ptr  self 
)
Private deinitializer, called by the destructor

See Also bdd_enc_cache_init
Defined in BddEncCache.c

static void 
bdd_enc_cache_init(
  BddEncCache_ptr  self, 
  SymbTable_ptr  symb_table, 
  DdManager* dd 
)
Private initializer, called by the constructor

See Also bdd_enc_cache_deinit
Defined in BddEncCache.c

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
Defined in BddEncBddPrintWff.c

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
Defined in BddEncBddPrintWff.c

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
Defined in BddEncBddPrintWff.c

assoc_retval 
bdd_enc_hash_free_bdd_counted(
  char* key, 
  char* data, 
  char* arg 
)
Used to deref bdds in the sharing hashtable

Defined in BddEncBddPrintWff.c

static assoc_retval 
hash_free_add_array(
  char* key, 
  char* data, 
  char* arg 
)
Called when pushing the status, and during deinitialization

Defined in BddEncCache.c

static assoc_retval 
hash_free_add_counted(
  char* key, 
  char* data, 
  char* arg 
)
Called when pushing the status, and during deinitialization. The kind of nodes that must be removed here is CONS(integer, add). Of course it is the add that must be freed.

Defined in BddEncCache.c

static assoc_retval 
hash_free_add(
  char* key, 
  char* data, 
  char* arg 
)
Called when pushing the status, and during deinitialization

Defined in BddEncCache.c

 
(
    
)
Builds a node representing the Bool casting of a single word bit.

Side Effects none

Defined in BddEncBddPrintWff.c

Last updated on 2011/06/16 12h:15