BddEncCache_clean_evaluation_about()
Cleans those hashed entries that are about a symbol that is being removed
BddEncCache_clean_evaluation()
Cleans up the cache from all the evaluated expressions
BddEncCache_create()
Class constructor
BddEncCache_destroy()
Class destructor
BddEncCache_get_evaluation()
Retrieve the evaluation of a given symbol, as an array of ADD
BddEncCache_is_boolean_var_encoded()
Returns true whether the given boolean variable has been encoded
BddEncCache_is_constant_encoded()
Returns true whether the given constant has been encoded
BddEncCache_lookup_boolean_var()
Retrieves the add associated with the given boolean variable, if previously encoded.
BddEncCache_lookup_constant()
Returns the ADD corresponding to the given constant, or NULL if not defined
BddEncCache_new_boolean_var()
Call this to insert the encoding for a given boolean variable
BddEncCache_new_constant()
Call to associate given constant to the relative add
BddEncCache_remove_boolean_var()
Removes the given variable from the internal hash
BddEncCache_remove_constant()
Removes the given constant from the internal hash
BddEncCache_remove_evaluation()
This method is used to remove the result of evaluation of an expression
BddEncCache_set_evaluation()
This method is used to remember the result of evaluation, i.e. to keep the association between the expression in node_ptr form and its ADD representation.
BddEnc_bdd_to_wff()
Converts a bdd into a Well Formed Formula representing it.
BddEnc_print_bdd_wff()
Prints a BDD as a Well Formed Formula using optional sharing
BddEnc_print_formula_info()
Prints statistical information of a formula.
bdd_enc_bdd_to_wff_rec()
Recursively build a sexp representing a formula encoded as a BDD
bdd_enc_cache_deinit()
Private deinitializer
bdd_enc_cache_init()
Private initializer
bdd_enc_debug_bdd_to_wff()
Debug code for BddEnc_bdd_to_wff
bdd_enc_get_preprocessed_vars()
Preprocesses variables list, as part of the bdd_enc_bdd_to_wff implementation.
bdd_enc_get_scalar_essentials()
Compute scalar essentials of a bdd.
bdd_enc_hash_free_bdd_counted()
Used to deref bdds in the sharing hashtable
hash_free_add_array()
Private micro function used when destroying caches of adds
hash_free_add_counted()
Private micro function used when destroying caches of adds
hash_free_add()
Private micro function used when destroying caches of adds
()
A shorthand to ease reading of bdd_enc_bdd_to_wff_rec

Last updated on 2012/11/18 14h:16