module Fcl_stak:sig
..end
This module provides functions to control the execution of the goal
stack, as well as backtrackable references, i.e. mutable data
structures restored on backtracking. Nota: the module name
Stak
lacks a 'c
' because of a possible clash with the OCaml
standard library module Stack
.
type
level
Type of a level in the stack.
val older : level -> level -> bool
older l1 l2
true if level l1
precedes l2
.
val size : unit -> int
Size of the stack, i.e. number of trailings.
val depth : unit -> int
Depth of the stack, i.e. number of active levels.
val level : unit -> level
Returns the current level.
val levels : unit -> level list
Returns the current active levels.
val nb_choice_points : unit -> int
Access to a global counter incremented at each choice point. Useful to implement search strategies such as Limited Discrepancy Search
exception Level_not_found of level
Raised by cut
.
val cut : level -> unit
cut l
cuts the choice points left on the stack until level l
.
Raise Level_not_found
if level is not reached and stack is empty.
exception Fail of string
Raised during solving whenever a failure occurs. The string argument is informative.
val fail : string -> 'a
fail x
equivalent to raise (Fail x)
.
type 'a
ref
Backtrackable reference of type 'a
. I.e. type of mutable
data structures restored on backtracking.
val ref : 'a -> 'a ref
Returns a reference whose modifications will be trailed during the solving of a goal.
val set : 'a ref -> 'a -> unit
Sets a backtrackable reference.
val get : 'a ref -> 'a
Dereference.