Module Fcl_invariant

module Fcl_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 : Stdlib.out_channel ->
       ?printer:(Stdlib.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 = Fcl_var.Fd.t
  and type elt = Fcl_var.Fd.elt

Module for accessing finite integer domain variables with BIRs.

module SetFd: FD 
with
   type fd = Fcl_var.SetFd.t
   and type elt = Fcl_var.SetFd.elt

Module for accessing set domain variables with BIRs.