package mc2

  1. Overview
  2. Docs
type t
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_unit:(Mc2_core__.Solver_types.term -> unit) -> 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 exactly one term u is not set, then it calls on_unit u. If all terms are set, then it watches the one with the highest level and call on_all_set ()

val update : t -> Mc2_core__.Solver_types.term -> watch:Mc2_core__.Solver_types.term -> on_unit:(Mc2_core__.Solver_types.term -> unit) -> 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 exactly one term u is not set, then it calls on_unit u. If all terms are set, then it calls on_all_set ()

OCaml

Innovation. Community. Security.