module Invariant: sig
.. end
Backtrackable Invariant References
This module provides types and functions to create
and handle Backtrackable Invariant References (noted BIR in the sequel).
BIRs are single-valued variables whose values are restored
upon backtracks and which are linked by "one-way" constraints.
They maintain functional dependencies between "source" setable
BIRs (initialized with their creation value) and unsetable BIRs
built upon them. BIRs may be convenient to automatically handle
heuristic criteria or the data structures of local search
algorithms . Note that circular dependencies
are not allowed by the typing policy.
type ('a, 'b)
t
type
setable
type
unsetable
type 'a
setable_t = ('a, setable) t
type 'a
unsetable_t = ('a, unsetable) t
Type of BIRs. Parameter 'a
stands for the
type of the value of the BIR. Parameter 'b
is setable
if the BIR
can be assigned, unsetable
if not. setable_t
and unsetable_t
are
shortcuts.
val create : ?name:string -> 'a -> 'a setable_t
create ~name:"" v
returns a setable BIR with initial content v
.
An optional string can be given to name the BIR.
val constant : ?name:string -> 'a -> 'a unsetable_t
constant ~name:"" cst
returns an unsetable BIR with initial
content cst
. An optional string can be given to name the BIR.
val set : 'a setable_t -> 'a -> unit
Assignment of a setable BIR.
val get : ('a, 'b) t -> 'a
Access to the content of a BIR.
val id : ('a, 'b) t -> int
id r
returns a unique integer associated to BIR r
.
val name : ('a, 'b) t -> string
name r
returns the name (specified or generated) of BIR r
.
val fprint : Pervasives.out_channel ->
?printer:(Pervasives.out_channel -> 'a -> unit) ->
('a, 'b) t -> unit
fprint c ~printer:(fun _ _ -> ()) r
prints BIR r
on channel c
.
An optional custom printer can be given to display the value of r
.
val unary : ?name:string ->
('a -> 'b) -> ('a, 'c) t -> 'b unsetable_t
unary ~name:"Invariant.unary" f
wraps the unary function f
into
an operator on BIRs. An optional string can be given to name the
operator.
val binary : ?name:string ->
('a -> 'b -> 'c) ->
('a, 'd) t -> ('b, 'e) t -> 'c unsetable_t
binary ~name:"Invariant.binary" f
wraps the binary function f
into an operator on BIRs.
An optional string can be given to name the operator.
val ternary : ?name:string ->
('a -> 'b -> 'c -> 'd) ->
('a, 'e) t ->
('b, 'f) t -> ('c, 'g) t -> 'd unsetable_t
ternary ~name:"Invariant.ternary" f
wraps the ternary function f
into an operator on BIRs.
An optional string can be given to name the operator.
val sum : (int, 'a) t array -> int unsetable_t
sum a
returns a BIR equal to the sum of elements of a
.
val prod : (int, 'a) t array -> int unsetable_t
sum a
returns a BIR equal to the product of elements of a
.
module Array: sig
.. end
module type FD = sig
.. end
Generic signature.
module Fd: FD
with
type fd = Var.Fd.t
and type elt = Var.Fd.elt
Module for accessing finite integer domain variables with BIRs.
module SetFd: FD
with
type fd = Var.SetFd.t
and type elt = Var.SetFd.elt
Module for accessing set domain variables with BIRs.