ocaml-buddy 0.6.1 · OCaml Package

type bdd

type bddpair

type var = int

type value =

| False
| True
| Unknown

type solution =

| SAT
| UNSAT
| UNKNOWN

val value_of_var : var -> value

val string_of_value : value -> string

type reorder_strategy =

| Win2
| Win2ite
| Win3
| Win3ite
| Sift
| Siftite
| Random

val bdd_compare : bdd -> bdd -> int

val bdd_init : ?nodenum:int -> ?cachesize:int -> unit -> unit

val bdd_done : unit -> unit

val bdd_setvarnum : int -> unit

val bdd_varnum : unit -> int

val bdd_newvar : unit -> var

val bdd_pos : var -> bdd

val bdd_neg : var -> bdd

val bdd_true : bdd

val bdd_false : bdd

val bdd_not : bdd -> bdd

val bdd_and : bdd -> bdd -> bdd

val bdd_or : bdd -> bdd -> bdd

val bdd_xor : bdd -> bdd -> bdd

val bdd_imp : bdd -> bdd -> bdd

val bdd_biimp : bdd -> bdd -> bdd

val bdd_ite : bdd -> bdd -> bdd -> bdd

val bdd_bigor : bdd list -> bdd

val bdd_bigand : bdd list -> bdd

val bdd_allsat : ((var * value) list -> unit) -> bdd -> unit

val bdd_satone : bdd -> bdd

val bdd_satoneset : ?pol:bool -> bdd -> var list -> bdd

val bdd_makeset : var list -> bdd

val bdd_simplify : bdd -> bdd -> bdd

val bdd_var : bdd -> var

val bdd_high : bdd -> bdd

val bdd_low : bdd -> bdd

val bdd_restrict : bdd -> bdd -> bdd

val bdd_support : bdd -> bdd

val bdd_nodecount : bdd -> int

val bdd_newpair : unit -> bddpair

val bdd_setpair : bddpair -> int -> int -> int

val bdd_replace : bdd -> bddpair -> bdd

val bdd_varblockall : unit -> unit

val bdd_addvarblock : bdd -> int -> int

val bdd_intaddvarblock : int -> int -> int -> int

val bdd_reorder : ?strategy:reorder_strategy -> unit -> unit

val bdd_autoreorder : ?strategy:reorder_strategy -> unit -> unit

val bdd_setvarorder : int list -> unit

val bdd_enable_reorder : unit -> unit

val bdd_disable_reorder : unit -> unit

val bdd_reorder_verbose : int -> int

val bdd_fprintorder : out_channel -> unit

val bdd_level2var : int -> int

val bdd_var2level : int -> int

val bdd_setmaxincrease : int -> int

val bdd_setcacheratio : int -> int

val bdd_fprinttable : out_channel -> bdd -> unit

val bdd_fprintdot : out_channel -> bdd -> unit

val bdd_fprintset : out_channel -> bdd -> unit

val bdd_load : in_channel -> bdd

val bdd_save : out_channel -> bdd -> unit

val bdd_createset : (int -> bool) -> bdd

val bdd_relprod : (int -> bool) -> bdd -> bdd -> bdd

exception EmptyBdd

val bdd_setfold : (int -> 'a -> 'a) -> bdd -> 'a -> 'a

package ocaml-buddy