-
BddEnc.c
- Implementaion of class 'BddEnc'
-
BddEncBddPrintWff.c
- Bdd to Well Formed Formulas conversions/printout
-
BddEncCache.c
- The BddEncCache class implementation. This class is
intended to be used exclusively by the class BddEnc.
BddEnc.c
Implementaion of class 'BddEnc'
By: Roberto Cavada
See AlsoBddEnc.h
BddEncBddPrintWff.c
Bdd to Well Formed Formulas conversions/printout
By: Marco Pensallorto
This module exports functions to generate or print a
Bdd as an optimized Well Formed Formula.
-
()
- A shorthand to ease reading of bdd_enc_bdd_to_wff_rec
-
BddEnc_print_formula_info()
- Prints statistical information of a formula.
-
BddEnc_print_bdd_wff()
- Prints a BDD as a Well Formed Formula using optional
sharing
-
BddEnc_bdd_to_wff()
- Converts a bdd into a Well Formed Formula representing
it.
-
bdd_enc_hash_free_bdd_counted()
- Used to deref bdds in the sharing hashtable
-
bdd_enc_get_scalar_essentials()
- Compute scalar essentials of a bdd.
-
bdd_enc_get_preprocessed_vars()
- Preprocesses variables list, as part of the
bdd_enc_bdd_to_wff implementation.
-
bdd_enc_debug_bdd_to_wff()
- Debug code for BddEnc_bdd_to_wff
-
bdd_enc_bdd_to_wff_rec()
- Recursively build a sexp representing a formula encoded as
a BDD
BddEncCache.c
The BddEncCache class implementation. This class is
intended to be used exclusively by the class BddEnc.
By: Roberto Cavada
See AlsoBddEncCache.h
-
BddEncCache_create()
- Class constructor
-
BddEncCache_destroy()
- Class destructor
-
BddEncCache_new_constant()
- Call to associate given constant to the relative add
-
BddEncCache_remove_constant()
- Removes the given constant from the internal hash
-
BddEncCache_is_constant_encoded()
- Returns true whether the given constant has been 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_remove_boolean_var()
- Removes the given variable from the internal hash
-
BddEncCache_is_boolean_var_encoded()
- Returns true whether the given boolean variable has
been encoded
-
BddEncCache_lookup_boolean_var()
- Retrieves the add associated with the given boolean
variable, if previously encoded.
-
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.
-
BddEncCache_remove_evaluation()
- This method is used to remove the result of evaluation
of an expression
-
BddEncCache_get_evaluation()
- Retrieve the evaluation of a given symbol,
as an array of ADD
-
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
-
bdd_enc_cache_init()
- Private initializer
-
bdd_enc_cache_deinit()
- Private deinitializer
-
hash_free_add()
- Private micro function used when destroying caches of
adds
-
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
Last updated on 2012/11/18 14h:16