module Man: sig
.. end
type
d
Indicates that a CUDD manager manipulates standard ADDs with leaves of type C double
type
v
Indicates that a CUDD manager manipulates ``custom'' ADDs with leaves of type an
OCaml
value, see modules
Cudd.Mtbdd
and
Cudd.Mtbddc
. A manager cannot manipulate the two types of ADDs (for garbage collection reasons)
type 'a
t
Type of CUDD managers, where 'a
is either d
or v
type
reorder =
| |
REORDER_SAME |
| |
REORDER_NONE |
| |
REORDER_RANDOM |
| |
REORDER_RANDOM_PIVOT |
| |
REORDER_SIFT |
| |
REORDER_SIFT_CONVERGE |
| |
REORDER_SYMM_SIFT |
| |
REORDER_SYMM_SIFT_CONV |
| |
REORDER_WINDOW2 |
| |
REORDER_WINDOW3 |
| |
REORDER_WINDOW4 |
| |
REORDER_WINDOW2_CONV |
| |
REORDER_WINDOW3_CONV |
| |
REORDER_WINDOW4_CONV |
| |
REORDER_GROUP_SIFT |
| |
REORDER_GROUP_SIFT_CONV |
| |
REORDER_ANNEALING |
| |
REORDER_GENETIC |
| |
REORDER_LINEAR |
| |
REORDER_LINEAR_CONVERGE |
| |
REORDER_LAZY_SIFT |
| |
REORDER_EXACT |
Reordering method.
type
aggregation =
| |
NO_CHECK |
| |
GROUP_CHECK |
| |
GROUP_CHECK2 |
| |
GROUP_CHECK3 |
| |
GROUP_CHECK4 |
| |
GROUP_CHECK5 |
| |
GROUP_CHECK6 |
| |
GROUP_CHECK7 |
| |
GROUP_CHECK8 |
| |
GROUP_CHECK9 |
Type of aggregation methods.
type
lazygroup =
| |
LAZY_NONE |
| |
LAZY_SOFT_GROUP |
| |
LAZY_HARD_GROUP |
| |
LAZY_UNGROUP |
Group type for lazy sifting.
type
vartype =
| |
VAR_PRIMARY_INPUT |
| |
VAR_PRESENT_STATE |
| |
VAR_NEXT_STATE |
Variable type. Currently used only in lazy sifting.
type
mtr =
| |
MTR_DEFAULT |
| |
MTR_FIXED |
Is variable order inside group fixed or not ?
type
error =
| |
NO_ERROR |
| |
MEMORY_OUT |
| |
TOO_MANY_NODES |
| |
MAX_MEM_EXCEEDED |
| |
INVALID_ARG |
| |
INTERNAL_ERROR |
Type of error when CUDD raises an exception.
type
dt = d t
type
vt = v t
Shortcuts
type
tbool =
val string_of_reorder : reorder -> string
val string_of_error : error -> string
Printing functions
Global settings
val print_limit : int Pervasives.ref
Parameter for printing functions: specify the maximum number of minterms to
be printed. Above this numbers, only statistics on the BDD is printed.
val set_gc : int -> (unit -> unit) -> (unit -> unit) -> unit
set_gc max gc reordering
performs several things:
- It sets the ratio used/max for BDDs abstract values to
1/max
(see
the OCaml manual for details). 1 000 000 is a good value.
- It also sets for all the future managers that will be created the hook
function to be called before a CUDD garbage collection, and the hook
function to be called before a CUDD reordering. You may typically specify
a OCaml garbage collection function for both hooks, in order to make
OCaml dereference unused nodes, thus allowing CUDD to remove
them. Default values are
Gc.full_major()
for both hooks.
val srandom : int -> unit
Managers
val _make : bool -> int -> int -> int -> int -> int -> 'a t
Internal, do not use !
val make_d : ?numVars:int ->
?numVarsZ:int ->
?numSlots:int ->
?cacheSize:int -> ?maxMemory:int -> unit -> d t
val make_v : ?numVars:int ->
?numVarsZ:int ->
?numSlots:int ->
?cacheSize:int -> ?maxMemory:int -> unit -> v t
Variation of
Cudd_Init
.
make_d ~numVars ~numVarsZ ~numSlots ~cacheSize ~maxMemory ()
creates a manager with the
given parameters. make_d ()
is OK. In addition, the function sets a hook
function to be called whenever a CUDD garbage collection occurs, and a
(dummy) hook function to be called whenever a CUDD reordering occurs. The defaults can be modified with Cudd.Man.set_gc
.
val debugcheck : 'a t -> bool
Cudd_DebugCheck
.
Returns
false
if it is OK,
true
if there is a problem, and throw
a
Failure
exception in case of
OUT_OF_MEM
.
val check_keys : 'a t -> int
Variables, Reordering and Mapping
val level_of_var : 'a t -> int -> int
Cudd_ReadPerm
. Returns the level of the variable (its order in the BDD)
val var_of_level : 'a t -> int -> int
val reduce_heap : 'a t -> reorder -> int -> unit
Cudd_ReduceHeap
. Main reordering function, that applies the given heuristic. The provided integer is a bound below which no reordering takes place.
val shuffle_heap : 'a t -> int array -> unit
val garbage_collect : 'a t -> int
val flush : 'a t -> unit
val enable_autodyn : 'a t -> reorder -> unit
val disable_autodyn : 'a t -> unit
val autodyn_status : 'a t -> reorder option
val group : 'a t -> int -> int -> mtr -> unit
Cudd_MakeTreeNode
.
group man low size typ
creates a new variable group, ranging from index
low
to index
low+size-1
, in which
typ
specifies if reordering is allowed inside the group.
val ungroupall : 'a t -> unit
val set_varmap : 'a t -> int array -> unit
Parameters
RDDs
val get_background : dt -> float
val set_background : dt -> float -> unit
val get_epsilon : dt -> float
val set_epsilon : dt -> float -> unit
Cache related
val get_min_hit : 'a t -> int
val set_min_hit : 'a t -> int -> unit
val get_max_cache_hard : 'a t -> int
val set_max_cache_hard : 'a t -> int -> unit
Manager
val get_looseupto : 'a t -> int
val set_looseupto : 'a t -> int -> unit
val get_max_live : 'a t -> int
val set_max_live : 'a t -> int -> unit
val get_max_mem : 'a t -> int
val set_max_mem : 'a t -> int -> unit
Reordering methods
val get_sift_max_swap : 'a t -> int
val set_sift_max_swap : 'a t -> int -> unit
val get_sift_max_var : 'a t -> int
val set_sift_max_var : 'a t -> int -> unit
val get_groupcheck : 'a t -> aggregation
val set_groupcheck : 'a t -> aggregation -> unit
val get_arcviolation : 'a t -> int
val set_arcviolation : 'a t -> int -> unit
val get_crossovers : 'a t -> int
val set_crossovers : 'a t -> int -> unit
val get_population : 'a t -> int
val set_population : 'a t -> int -> unit
val get_recomb : 'a t -> int
val set_recomb : 'a t -> int -> unit
(Cudd_SetRecomb
.
val get_symmviolation : 'a t -> int
val set_symmviolation : 'a t -> int -> unit
Dynamic reordering
val get_max_growth : 'a t -> float
val set_max_growth : 'a t -> int -> unit
val get_max_growth_alt : 'a t -> float
val set_max_growth_alt : 'a t -> float -> unit
val get_reordering_cycle : 'a t -> int
val set_reordering_cycle : 'a t -> int -> unit
val get_next_autodyn : 'a t -> int
val set_next_autodyn : 'a t -> int -> unit
Statistics
val get_cache_hits : 'a t -> float
val get_cache_lookups : 'a t -> float
val get_cache_slots : 'a t -> int
val get_cache_used_slots : 'a t -> float
val get_dead : 'a t -> int
val get_error : 'a t -> error
val get_gc_time : 'a t -> int
val get_gc_nb : 'a t -> int
val get_keys : 'a t -> int
val get_linear : 'a t -> int -> int -> int
val get_max_cache : 'a t -> int
val get_min_dead : 'a t -> int
val get_node_count : 'a t -> int
val get_node_count_peak : 'a t -> int
val get_reordering_time : 'a t -> int
val get_reordering_nb : 'a t -> int
val get_bddvar_nb : 'a t -> int
val get_zddvar_nb : 'a t -> int
val get_slots : 'a t -> int
val get_used_slots : 'a t -> float
val get_swap_nb : 'a t -> float
val print_info : 'a t -> unit