Module Invariant


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.