Module Term.Watch1
val dummy : t
val make : Mc2_core__.Solver_types.term list -> t
val make_a : Mc2_core__.Solver_types.term array -> t
owns the array
val iter : t -> Mc2_core__.Solver_types.term Iter.t
owns the array
current watch(es)
val init : t -> Mc2_core__.Solver_types.term -> on_all_set:(unit -> unit) -> unit
init w t ~on_all_set
initializesw
(the watchlist) for termt
, by finding an unassigned term in the watchlist and registeringt
to it. If all terms are set, then it watches the one with the highest level and callon_all_set ()
val 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
updatesw
afterwatch
has been assigned. It looks for another term inw
fort
to watch. If all terms are set, then it callson_all_set ()