package mc2

  1. Overview
  2. Docs

Module Term.Watch1Source

Sourcetype t
Sourceval dummy : t
Sourceval make : Mc2_core__.Solver_types.term list -> t
Sourceval make_a : Mc2_core__.Solver_types.term array -> t

owns the array

Sourceval iter : t -> Mc2_core__.Solver_types.term Iter.t

owns the array

current watch(es)

Sourceval init : t -> Mc2_core__.Solver_types.term -> on_all_set:(unit -> unit) -> unit

init w t ~on_all_set initializes w (the watchlist) for term t, by finding an unassigned term in the watchlist and registering t to it. If all terms are set, then it watches the one with the highest level and call on_all_set ()

Sourceval update : t -> Mc2_core__.Solver_types.term -> watch:Mc2_core__.Solver_types.term -> on_all_set:(unit -> unit) -> Mc2_core__.Solver_types.watch_res

update w t ~watch ~on_all_set updates w after watch has been assigned. It looks for another term in w for t to watch. If all terms are set, then it calls on_all_set ()