Module Bdd.Env

module Env: sig .. end


Types


exception Bddindex
type 'a typdef = [ `Benum of 'a array ] 
Type defintions. 'a is the type of symbols (typically, string).
type 'a typ = [ `Benum of 'a | `Bint of bool * int | `Bool ] 
Types. 'a is the type of symbols (typically, string.
type 'a symbol = {
   compare :'a -> 'a -> int; (*Total order*)
   marshal :'a -> string; (*Conversion to string. The generated strings SHOULD NOT contain NULL character, as they may be converted to C strings.*)
   unmarshal :string -> 'a; (*Conversion from string*)
   mutable print :Format.formatter -> 'a -> unit; (*Printing*)
}
Manager for manipulating symbols.

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 :'d Cudd.Man.t; (*CUDD manager*)
   mutable typdef :('a, 'c) PMappe.t; (*Named types definitions*)
   mutable vartyp :('a, 'b) PMappe.t; (*Associate to a var/label its type*)
   mutable bddindex0 :int; (*First index for finite-type variables*)
   mutable bddsize :int; (*Number of indices dedicated to finite-type variables*)
   mutable bddindex :int; (*Next free index in BDDs used by self#add_var.*)
   mutable bddincr :int; (*Increment used by add_var for incrementing bddindex*)
   mutable idcondvar :(int, 'a) PMappe.t; (*Associates to a BDD index the variable involved by it*)
   mutable vartid :('a, int array) PMappe.t; (*(Sorted) array of BDD indices associated to finite-type variables.*)
   mutable varset :('a, 'd Cudd.Bdd.t) PMappe.t; (*Associates to enumerated variable the (care)set of possibled values.*)
   mutable print_external_idcondb :Format.formatter -> int * bool -> unit; (*Printing conditions not managed by the environment.. By default, pp_print_int.*)
   mutable ext :'e;
   symbol :'a symbol;
   copy_ext :'e -> 'e;
}
Environment


module O: sig .. end
Opened signature
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

Printing

Print a type

val print_typdef : (Format.formatter -> 'a -> unit) ->
Format.formatter -> [> 'a typdef ] -> unit
Print a type definition
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
Print the BDD variable ordering
val print : Format.formatter ->
('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> unit
Print an environment

Constructors


val marshal : 'a -> string
Safe marshalling function, generating strings without NULL characters.

(Based on Marshal.to_string with Marshal.No_sharing option.)

val unmarshal : string -> 'a
Companion unmarshalling function
val make_symbol : ?compare:('a -> 'a -> int) ->
?marshal:('a -> string) ->
?unmarshal:(string -> 'a) ->
(Format.formatter -> 'a -> unit) -> 'a symbol
Generic function for creating a manager for symbols. Default values are 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
Standard manager for symbols of type string
val make : symbol:'a symbol ->
?bddindex0:int ->
?bddsize:int -> ?relational:bool -> 'd Cudd.Man.t -> ('a, 'd) t
Create a new environment.

Default values for 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
Copy

Accessors


val mem_typ : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a -> bool
Is the type defined in the database ?
val mem_var : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a -> bool
Is the label/var defined in the database ?
val mem_label : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a -> bool
Is the label a label defined in the database ?
val typdef_of_typ : ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd, 'e) O.t ->
'a -> 'b
Return the definition of the type
val typ_of_var : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd, 'e) O.t ->
'a -> 'b
Return the type of the label/variable
val vars : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a PSette.t
Return the list of variables (not labels)
val labels : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a PSette.t
Return the list of labels (not variables)

Adding types and variables


val add_typ_with : ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd, 'e) O.t ->
'a -> 'b -> unit
Declaration of a new type
val add_vars_with : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd, 'e) O.t ->
('a * 'b) list -> int array option
Add the set of variables, possibly normalize the environment and return the applied permutation (that should also be applied to expressions defined in this environment)
val remove_vars_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
'a list -> int array option
Remove the set of variables, and possibly normalize the environment and return the applied permutation.
val rename_vars_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
('a * 'a) list -> int array option
Rename the variables, possibly normalize the environment and return the applied permutation.
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
Functional versions of the previous functions
val add_var_with : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd, 'e) O.t ->
'a -> 'b -> unit
Addition without normalization (internal)

Operations


val iter_ordered : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
('a -> int array -> unit) -> unit
Iter on all finite-state variables declared in the database
val is_leq : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> bool
Test inclusion of environments in terms of types and variables (but not in term of indexes)
val is_eq : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> bool
Test equality of environments in terms of types and variables (but not in term of indexes)
val shift : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> int -> ('a, 'b, 'c, 'd, 'e) O.t
Shift all the indices by the offset
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
Least common environment
val permutation12 : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> int array
Permutation for going from a subenvironment to a superenvironment
val permutation21 : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e)
O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> int array
Permutation from a superenvironment to a subenvironment

Precomputing change of environments


type 'a change = {
   intro :int array option; (*Permutation to apply for making space for new BDD variables*)
   remove :('a Cudd.Bdd.t * int array) option; (*BDD variables to existentially quantify out, and permutation to apply*)
}
Contain the computed information to switch from one environment to another one.
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

Utilities


val notfound : ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
type ('a, 'b) value = {
   env :'a;
   val0 :'b;
}
Type of pairs (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
Constructor
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.

Internal functions


val compare_idb : int * bool -> int * bool -> int
Comparison

Normalisation


val permutation : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
int array
Compute the permutation for normalizing the environment
val permute_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
int array -> unit
Apply the given permutation to the environment
val normalize_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t ->
int array
Combine the two previous functions, and return the permutation
val check_normalized : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> bool
Prints error message and returns false if not normalized

Permutations


val 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

Used by level1 APIs


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