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

'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

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.

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.

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