module Stak: sig .. end
Global Stack of Goals, Backtrackable Operations
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.
Access
type
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
Control
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).
Backtrackable References
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.