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_bdd_cache 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_bdd_cache" 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