-
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 2011/04/06 21h:13