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 2011/06/16 12h:15