Module Bddapron.Env

module Env: sig .. end

Types

type 'a typdef = 'a Bdd.Env.typdef

Type definitions. 'a is the type of symbols (typically, string).

type 'a typ = [ `Benum of 'a | `Bint of bool * int | `Bool | `Int | `Real ]

Types. 'a is the type of symbols (typically, string).

type 'a symbol = 'a Bdd.Env.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 Bddapron.Env.marshal and Bddapron.Env.unmarshal.

type ('a, 'b) ext = {

	`mutable table :'a Bddapron.Apronexpr.t Cudd.Mtbdd.table;`
	`mutable eapron :Apron.Environment.t;`
	`mutable aext :'b;`

}

Environment extension. 'a is the type of symbols, 'b is the type of further extension.

type ('a, 'b, 'c, 'd) t0 = ('a, 'b, 'c, Cudd.Man.v, ('a, 'd) ext) Bdd.Env.t0

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 further extension

See Bdd.Env.t0 for more (internal) details.

module O: sig .. end

Opened signature

type 'a t = ('a, 'a typ, 'a typdef, unit) O.t

Printing

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

Print a type definition

val print_idcondb : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> Format.formatter -> int * bool -> unit

val print_order : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> Format.formatter -> unit

Print the BDD variable ordering

val print : Format.formatter ->
       ('a, [> 'a typ ], [> 'a typdef ], 'd)
       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, Bddapron.Env.marshal and Bddapron.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 -> Cudd.Man.vt -> 'a 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 -> Cudd.Man.vt -> string t

make_string XXX = make ~symbol:string_symbol XXX

val copy : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t -> ('a, 'b, 'c, 'd) O.t

Copy

Accessors

val mem_typ : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> 'a -> bool

Is the type defined in the database ?

val mem_var : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> 'a -> bool

Is the label/var defined in the database ?

val mem_label : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       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)
       O.t -> 'a -> 'b

Return the definition of the type

val typ_of_var : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd)
       O.t -> 'a -> 'b

Return the type of the label/variable

val vars : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> 'a PSette.t

Return the list of variables (not labels)

val labels : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> 'a PSette.t

Return the list of labels (not variables)

val apron : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> Apron.Environment.t

return the APRON sub-environment

Adding types and variables

val add_typ_with : ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd)
       O.t -> 'a -> 'b -> unit

Declaration of a new type

val add_vars_with : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd)
       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)
       O.t -> 'a list -> int array option

Remove the set of variables, as well as all constraints, and possibly normalize the environment and return the applied permutation.

val rename_vars_with : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t ->
       ('a * 'a) list -> int array option * Apron.Dim.perm option

Rename the variables, and remove all constraints,possibly normalize the environment and return the applied permutation.

val add_typ : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t -> 'a -> 'c -> ('a, 'b, 'c, 'd) O.t

val add_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t -> ('a * 'b) list -> ('a, 'b, 'c, 'd) O.t

val remove_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t -> 'a list -> ('a, 'b, 'c, 'd) O.t

val rename_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t -> ('a * 'a) list -> ('a, 'b, 'c, 'd) O.t

Functional versions of the previous functions

Operations

val is_leq : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t -> ('a, 'b, 'c, 'd) 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)
       O.t -> ('a, 'b, 'c, 'd) O.t -> bool

Test equality of environments in terms of types and variables (but not in term of indexes)

val lce : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t ->
       ('a, 'b, 'c, 'd) O.t -> ('a, 'b, 'c, 'd) O.t

Least common environment

Precomputing change of environments

type change = {

	`cbdd :Cudd.Man.v Bdd.Env.change;`
	`capron :Apron.Dim.change2;`

}

val compute_change : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t -> ('a, 'b, 'c, 'd) O.t -> change

Utilities

type ('a, 'b) value = ('a, 'b) Bdd.Env.value = {

	`env :'a;`
	`val0 :'b;`

}

Type of pairs (environment, value)

val make_value : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t ->
       'e -> (('a, 'b, 'c, 'd) O.t, 'e) value

Constructor

val get_env : ('a, 'b) value -> 'a

val get_val0 : ('a, 'b) value -> 'b

val check_var : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> 'a -> unit

val check_lvar : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> 'a list -> unit

val check_value : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t ->
       (('a, 'b, 'c, 'd) O.t, 'e) value -> unit

val check_value2 : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
        O.t, 'e)
       value ->
       (('a, 'b, 'c, 'd) O.t, 'f) value -> unit

val check_value3 : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
        O.t, 'e)
       value ->
       (('a, 'b, 'c, 'd) O.t, 'f) value ->
       (('a, 'b, 'c, 'd) O.t, 'g) value -> unit

val check_lvarvalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t ->
       ('a * (('a, 'b, 'c, 'd) O.t, 'e) value) list ->
       ('a * 'e) list

val check_lvalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t ->
       (('a, 'b, 'c, 'd) O.t, 'e) value list -> 'e list

val check_ovalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
       O.t ->
       (('a, 'b, 'c, 'd) O.t, 'e) value option ->
       'e option

val mapunop : ('e -> 'f) ->
       (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
        O.t, 'e)
       value ->
       (('a, 'b, 'c, 'd) O.t, 'f) value

val mapbinop : ('e -> 'f -> 'g) ->
       (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
        O.t, 'e)
       value ->
       (('a, 'b, 'c, 'd) O.t, 'f) value ->
       (('a, 'b, 'c, 'd) O.t, 'g) value

val mapbinope : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
        O.t -> 'e -> 'f -> 'g) ->
       (('a, 'b, 'c, 'd) O.t, 'e) value ->
       (('a, 'b, 'c, 'd) O.t, 'f) value ->
       (('a, 'b, 'c, 'd) O.t, 'g) value

val mapterop : ('e -> 'f -> 'g -> 'h) ->
       (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd)
        O.t, 'e)
       value ->
       (('a, 'b, 'c, 'd) O.t, 'f) value ->
       (('a, 'b, 'c, 'd) O.t, 'g) value ->
       (('a, 'b, 'c, 'd) O.t, 'h) value

val var_of_aprondim : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> Apron.Dim.t -> 'a

val aprondim_of_var : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> 'a -> Apron.Dim.t

val string_of_aprondim : ('a, [> 'a typ ], [> 'a typdef ], 'd)
       O.t -> Apron.Dim.t -> string