package alt-ergo-lib

  1. Overview
  2. Docs
type t
val init : unit -> unit
val decision : int -> string -> unit
val assume : int -> unit
val query : unit -> unit
val instantiation : int -> unit
val instances : 'a list -> unit
val bool_conflict : unit -> unit
val theory_conflict : unit -> unit
val bcp_conflict : bool -> bool -> unit
val red : bool -> unit
val elim : bool -> unit
val reset_dlevel : int -> unit
val reset_ilevel : int -> unit
val new_instance_of : string -> Expr.t -> Loc.t -> bool -> unit
val conflicting_instance : string -> Loc.t -> unit
val register_produced_terms : string -> Loc.t -> Expr.Set.t -> Expr.Set.t -> Expr.Set.t -> Expr.Set.t -> unit
val print : bool -> int -> Timers.t -> Format.formatter -> unit
val switch : Format.formatter -> unit