Module Stak

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.


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).

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