Module Inf.Const

module Const: sig .. end

type obs = Inf.ConstBasic.obs 

Type of the observer

val add : Inf.ConstBasic.t -> unit

add obs adds the basic constraint obs to the global constraint set.

val is_false : string -> unit

is_false str adds the constraint False (Some s) to the global constraint set and removes all other constraints from the set. It also empties the work list.

val remove : Inf.ConstBasic.t -> unit

remove obs removes the basic constraint obs from the global constraint set.

val add_wl : obs -> unit

add_wl obs adds the observer obs to the working list. This ensures that the solve function will visit the observer obs if the solving procedure did not deduce an False before. If the observer is already part of the work list it is not added a second time.

val solve : unit -> unit

solve () starts the solving of the global constraint set. This means going throw the work list and call for each basic constraint the function fire. Before the fire function is called the basic constraint is removed from the work list. So if a basic constraints needs more than one visit it can add them self to the list again using add_wl.

val string_of : unit -> string

This returns a string representation of the global constraint. The string do not contain information about the work list.

val reset : unit -> unit

This function resets the global constraint. This results in the constraint true and an empty work list.

val full_visit : unit -> unit

Calling of full_visit adds all constraints that are part of the global constraint set to the work list.