Previous  Up  Next

Module Cudd.Man


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 =
| False
| True
| Top (*Ternary Boolean type, used to defines minterms where Top means True or False*) 
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: 
val srandom : int -> unit
Cudd_Srandom. Initializes the seed for the CUDD rnadom number generator (used in a number of functions, like Cudd.Bdd.pick_cubes_on_support.

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
Cudd_CheckKeys.

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
Cudd_ReadInvPerm. Returns the variable associated to the given level.
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
Cudd_ShuffleHeap. Reorder variables according to the given permutation.
val garbage_collect : 'a t -> int
cuddGarbageCollect. Force a garbage collection (with cache clearing)
val flush : 'a t -> unit
cuddCacheFlush. Clear the global cache
val enable_autodyn : 'a t -> reorder -> unit
Cudd_AutodynEnable. Enables dynamic reordering with the given heuristics.
val disable_autodyn : 'a t -> unit
Cudd_AutodynDisable. Disables dynamic reordering.
val autodyn_status : 'a t -> reorder option
Cudd_ReorderingStatus. Returns None if dynamic reordering is disables, Some(heuristic) otherwise.
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
Cudd_FreeTree. Removes all the groups in the manager.
val set_varmap : 'a t -> int array -> unit
Cuddaux_SetVarMap/Cudd_SetVarMap. Initializes the global mapping table, used by functions Cudd.Bdd.varmap, Cudd.Vdd.varmap, Cudd.Mtbdd.varmap, Cudd.Mtbddc.varmap,... Convenient when the same mapping is applied several times, because the the different calls reuse the same cache.

Parameters



RDDs


val get_background : dt -> float
Cudd_ReadBackground.
val set_background : dt -> float -> unit
Variation of Cudd_SetBackground.
val get_epsilon : dt -> float
Cudd_ReadEpsilon.
val set_epsilon : dt -> float -> unit
Cudd_SetEpsilon.

Cache related


val get_min_hit : 'a t -> int
Cudd_ReadMinHit.
val set_min_hit : 'a t -> int -> unit
Cudd_SetMinHit.
val get_max_cache_hard : 'a t -> int
Cudd_ReadMaxCacheHard.
val set_max_cache_hard : 'a t -> int -> unit
Cudd_SetMaxCacheHard.

Manager


val get_looseupto : 'a t -> int
Cudd_ReadLooseUpTo.
val set_looseupto : 'a t -> int -> unit
Cudd_SetLooseUpTo.
val get_max_live : 'a t -> int
Cudd_ReadMaxLive.
val set_max_live : 'a t -> int -> unit
Cudd_SetMaxLive.
val get_max_mem : 'a t -> int
Cudd_ReadMaxMemory.
val set_max_mem : 'a t -> int -> unit
Cudd_SetMaxMemory.

Reordering methods


val get_sift_max_swap : 'a t -> int
Cudd_ReadSiftMaxSwap.
val set_sift_max_swap : 'a t -> int -> unit
Cudd_SetSiftMaxSwap.
val get_sift_max_var : 'a t -> int
Cudd_ReadSiftMaxVar.
val set_sift_max_var : 'a t -> int -> unit
Cudd_SetSiftMaxVar.
val get_groupcheck : 'a t -> aggregation
Cudd_ReadGroupcheck.
val set_groupcheck : 'a t -> aggregation -> unit
Cudd_SetGroupcheck.
val get_arcviolation : 'a t -> int
Cudd_ReadArcviolation.
val set_arcviolation : 'a t -> int -> unit
Cudd_SetArcviolation.
val get_crossovers : 'a t -> int
Cudd_ReadNumberXovers.
val set_crossovers : 'a t -> int -> unit
Cudd_SetNumberXovers.
val get_population : 'a t -> int
Cudd_ReadPopulationSize.
val set_population : 'a t -> int -> unit
Cudd_SetPopulationSize.
val get_recomb : 'a t -> int
Cudd_ReadRecomb.
val set_recomb : 'a t -> int -> unit
(Cudd_SetRecomb.
val get_symmviolation : 'a t -> int
Cudd_ReadSymmviolation.
val set_symmviolation : 'a t -> int -> unit
Cudd_SetSymmviolation.

Dynamic reordering


val get_max_growth : 'a t -> float
Cudd_ReadMaxGrowth.
val set_max_growth : 'a t -> int -> unit
Cudd_SetMaxGrowth.
val get_max_growth_alt : 'a t -> float
Cudd_ReadMaxGrowthAlternate.
val set_max_growth_alt : 'a t -> float -> unit
Cudd_SetMaxGrowthAlternate.
val get_reordering_cycle : 'a t -> int
Cudd_ReadReorderingCycle.
val set_reordering_cycle : 'a t -> int -> unit
Cudd_SetReorderingCycle.
val get_next_autodyn : 'a t -> int
Cudd_ReadNextReordering.
val set_next_autodyn : 'a t -> int -> unit
Cudd_SetNextReordering.

Statistics


val get_cache_hits : 'a t -> float
Cudd_ReadCacheHits.
val get_cache_lookups : 'a t -> float
Cudd_ReadCacheLookUps.
val get_cache_slots : 'a t -> int
Cudd_ReadCacheSlots.
val get_cache_used_slots : 'a t -> float
Cudd_ReadCacheUsedSlots.
val get_dead : 'a t -> int
Cudd_ReadDead.
val get_error : 'a t -> error
Cudd_ReadErrorCode.
val get_gc_time : 'a t -> int
Cudd_ReadGarbageCollectionTime.
val get_gc_nb : 'a t -> int
Cudd_ReadGarbageCollections.
val get_keys : 'a t -> int
Cudd_ReadKeys.
val get_linear : 'a t -> int -> int -> int
Cudd_ReadLinear.
val get_max_cache : 'a t -> int
Cudd_ReadMaxCache.
val get_min_dead : 'a t -> int
Cudd_ReadMinDead.
val get_node_count : 'a t -> int
Cudd_ReadNodeCount.
val get_node_count_peak : 'a t -> int
Cudd_ReadPeakNodeCount.
val get_reordering_time : 'a t -> int
Cudd_ReadReorderingTime.
val get_reordering_nb : 'a t -> int
Cudd_ReadReorderings.
val get_bddvar_nb : 'a t -> int
Cudd_ReadSize.
val get_zddvar_nb : 'a t -> int
Cudd_ReadZddSize.
val get_slots : 'a t -> int
Cudd_ReadSlots.
val get_used_slots : 'a t -> float
Cudd_ReadUsedSlots.
val get_swap_nb : 'a t -> float
Cudd_ReadSwapSteps.
val print_info : 'a t -> unit
Cudd_PrintInfo.