-
Erwan Jahier authored
Parent-Version: 0.22 Version-Log: Add a bdd-based boolean solver to draw inside formula. Also remove several module opening and use explicit module qualification instead lurette.ml: env_state.ml: Define a function in env.ml to get the list of input and outputs var names and use it in lurette.ml env_state.ml: Add several fields to the env_state structure: * node_to_file_name: to be able to retrieve the list of vars that ougth to be generated from a list of nodes (Indeed, some vars that should be tossed up do no necessarily appear in formula; and once the whole bdd has been traversed for the draw, we need to be able to know what variable are still to be drawn). * var_name_to_index and index_to_var_name: to index output and local variable names. Indeed, the bdd library we use manipulates var as int, not string. * bdd_tbl: be cause transforming a formula into a bdd is expensive, we store the result of this transformation in a table. Define the var_names field as an Hashtbl instead of a list for homogeneity. Define functions that retrieve the list of input (resp output and local) vars from env_state to avois code duplication. env.ml: Initialize the new fields of env_state. util.ml: util.mli: Add a new function that computes the intersection of 2 lists. solver.ml: Implement a real boolean solver using bdds. Project-Description: Lurette
010423f4