module Env:sig
..end
exception Bddindex
type'a
typdef =[ `Benum of 'a array ]
'a
is the type of symbols (typically, string
).type'a
typ =[ `Benum of 'a | `Bint of bool * int | `Bool ]
'a
is the type of symbols (typically, string
.type 'a
symbol = {
|
compare : |
(* | Total order | *) |
|
marshal : |
(* | Conversion to string. The generated strings SHOULD NOT contain NULL character, as they may be converted to C strings. | *) |
|
unmarshal : |
(* | Conversion from string | *) |
|
mutable print : |
(* | Printing | *) |
DO NOT USE Marshal.to_string
and Marshal.from_string
, as
they generate strings with NULL character, which is not
handled properly when converted to C strings.
You may use instead Bdd.Env.marshal
and Bdd.Env.unmarshal
.
type ('a, 'b, 'c, 'd, 'e)
t0 = {
|
mutable cudd : |
(* | CUDD manager | *) |
|
mutable typdef : |
(* | Named types definitions | *) |
|
mutable vartyp : |
(* | Associate to a var/label its type | *) |
|
mutable bddindex0 : |
(* | First index for finite-type variables | *) |
|
mutable bddsize : |
(* | Number of indices dedicated to finite-type variables | *) |
|
mutable bddindex : |
(* | Next free index in BDDs used by self#add_var . | *) |
|
mutable bddincr : |
(* | Increment used by add_var for incrementing
bddindex | *) |
|
mutable idcondvar : |
(* | Associates to a BDD index the variable involved by it | *) |
|
mutable vartid : |
(* | (Sorted) array of BDD indices associated to finite-type variables. | *) |
|
mutable varset : |
(* | Associates to enumerated variable the (care)set of possibled values. | *) |
|
mutable print_external_idcondb : |
(* | Printing conditions not managed by the environment..
By default, pp_print_int . | *) |
|
mutable ext : |
|||
|
symbol : |
|||
|
copy_ext : |
'a
is the type of symbols;'b
is the type of variables type;'c
is the type of type definitions;'d
is the type of CUDD managers and BDDs (Cudd.Man.d
or Cudd.Man.v
);'e
is the type of "extension"module O:sig
..end
type('a, 'd)
t =('a, 'a typ, 'a typdef, 'd, unit) O.t
val print_typ : (Format.formatter -> 'a -> unit) ->
Format.formatter -> [> 'a typ ] -> unit
Print a type
val print_typdef : (Format.formatter -> 'a -> unit) ->
Format.formatter -> [> 'a typdef ] -> unit
val print_tid : Format.formatter -> int array -> unit
val print_idcondb : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
Format.formatter -> int * bool -> unit
val print_order : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
Format.formatter -> unit
val print : Format.formatter ->
('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> unit
val marshal : 'a -> string
(Based on Marshal.to_string
with Marshal.No_sharing
option.)
val unmarshal : string -> 'a
val make_symbol : ?compare:('a -> 'a -> int) ->
?marshal:('a -> string) ->
?unmarshal:(string -> 'a) ->
(Format.formatter -> 'a -> unit) -> 'a symbol
Pervasives.compare
, Bdd.Env.marshal
and Bdd.Env.unmarshal
.
DO NOT USE Marshal.to_string
and Marshal.from_string
, as they
generate strings with NULL character, which is not handled
properly when converted to C strings.
val string_symbol : string symbol
string
val make : symbol:'a symbol ->
?bddindex0:int ->
?bddsize:int -> ?relational:bool -> 'd Cudd.Man.t -> ('a, 'd) t
symbol
is the manager for manipulating symbols;bddindex0
: starting index in BDDs for finite-type variables;bddsize
: number of indices booked for finite-type
variables. If at some point, there is no such
available index, a Failure
exception is raised.relational
: if true, primed indices (unprimed
indices plus one) are booked together with unprimed
indices. bddincr
is initialized to 1 if
relational=false
, 2 otherwise.bddindex0,bddsize,relational
are
0,100,false
.val make_string : ?bddindex0:int ->
?bddsize:int -> ?relational:bool -> 'd Cudd.Man.t -> (string, 'd) t
make_string XXX = make ~symbol:string_symbol XXX
val copy : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a, 'b, 'c, 'd, 'e) O.t
val mem_typ : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a -> bool
val mem_var : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a -> bool
val mem_label : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a -> bool
val typdef_of_typ : ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd, 'e) O.t ->
'a -> 'b
val typ_of_var : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd, 'e) O.t ->
'a -> 'b
val vars : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a PSette.t
val labels : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a PSette.t
val add_typ_with : ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd, 'e) O.t ->
'a -> 'b -> unit
val add_vars_with : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd, 'e) O.t ->
('a * 'b) list -> int array option
val remove_vars_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a list -> int array option
val rename_vars_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
('a * 'a) list -> int array option
val add_typ : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> 'a -> 'c -> ('a, 'b, 'c, 'd, 'e) O.t
val add_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a * 'b) list -> ('a, 'b, 'c, 'd, 'e) O.t
val remove_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> 'a list -> ('a, 'b, 'c, 'd, 'e) O.t
val rename_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a * 'a) list -> ('a, 'b, 'c, 'd, 'e) O.t
val add_var_with : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd, 'e) O.t ->
'a -> 'b -> unit
val iter_ordered : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
('a -> int array -> unit) -> unit
val is_leq : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> bool
val is_eq : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> bool
val shift : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> int -> ('a, 'b, 'c, 'd, 'e) O.t
val lce : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t ->
('a, 'b, 'c, 'd, 'e) O.t -> ('a, 'b, 'c, 'd, 'e) O.t
val permutation12 : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> int array
val permutation21 : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> int array
type 'a
change = {
|
intro : |
(* | Permutation to apply for making space for new BDD variables | *) |
|
remove : |
(* | BDD variables to existentially quantify out, and permutation to apply | *) |
val compute_change : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> 'd change
val notfound : ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
type ('a, 'b)
value = {
|
env : |
|
val0 : |
(environment, value)
val make_value : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> 'f -> (('a, 'b, 'c, 'd, 'e) O.t, 'f) value
val get_env : ('a, 'b) value -> 'a
val get_val0 : ('a, 'b) value -> 'b
val extend_environment : ('f -> int array -> 'f) ->
(('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t, 'f)
value ->
('a, 'b, 'c, 'd, 'e) O.t ->
(('a, 'b, 'c, 'd, 'e) O.t, 'f) value
extend_environment permute value env
embed value
in
the new (super)environment env
, by computing the
permutation transformation and using permute
to apply it
to the value.val compare_idb : int * bool -> int * bool -> int
val permutation : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
int array
val permute_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
int array -> unit
val normalize_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
int array
val check_normalized : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> bool
false
if not normalizedval compose_permutation : int array -> int array -> int array
val compose_opermutation : int array option -> int array option -> int array option
val permutation_of_offset : int -> int -> int array
val check_var : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a -> unit
val check_lvar : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a list -> unit
val check_value : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> (('a, 'b, 'c, 'd, 'e) O.t, 'f) value -> unit
val check_value2 : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t, 'f)
value -> (('a, 'b, 'c, 'd, 'e) O.t, 'g) value -> unit
val check_value3 : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t, 'f)
value ->
(('a, 'b, 'c, 'd, 'e) O.t, 'g) value ->
(('a, 'b, 'c, 'd, 'e) O.t, 'h) value -> unit
val check_lvarvalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t ->
('a * (('a, 'b, 'c, 'd, 'e) O.t, 'f) value) list ->
('a * 'f) list
val check_lvalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t ->
(('a, 'b, 'c, 'd, 'e) O.t, 'f) value list -> 'f list
val check_ovalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t ->
(('a, 'b, 'c, 'd, 'e) O.t, 'f) value option -> 'f option
val mapunop : ('f -> 'g) ->
(('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t, 'f)
value -> (('a, 'b, 'c, 'd, 'e) O.t, 'g) value
val mapbinop : ('f -> 'g -> 'h) ->
(('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t, 'f)
value ->
(('a, 'b, 'c, 'd, 'e) O.t, 'g) value ->
(('a, 'b, 'c, 'd, 'e) O.t, 'h) value
val mapbinope : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> 'f -> 'g -> 'h) ->
(('a, 'b, 'c, 'd, 'e) O.t, 'f) value ->
(('a, 'b, 'c, 'd, 'e) O.t, 'g) value ->
(('a, 'b, 'c, 'd, 'e) O.t, 'h) value
val mapterop : ('f -> 'g -> 'h -> 'i) ->
(('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t, 'f)
value ->
(('a, 'b, 'c, 'd, 'e) O.t, 'g) value ->
(('a, 'b, 'c, 'd, 'e) O.t, 'h) value ->
(('a, 'b, 'c, 'd, 'e) O.t, 'i) value