package dolmen

  1. Overview
  2. Docs
type t
val annot : ?loc:L.t -> T.t -> T.t list -> T.t
val include_ : ?loc:L.t -> string -> I.t list -> t
val clause : ?loc:L.t -> T.t list -> t
val pop : ?loc:L.t -> int -> t
val push : ?loc:L.t -> int -> t
val assert_ : ?loc:L.t -> T.t -> t
val check_sat : ?loc:L.t -> unit -> t
val set_logic : ?loc:L.t -> string -> t
val get_info : ?loc:L.t -> string -> t
val set_info : ?loc:L.t -> (string * T.t option) -> t
val get_option : ?loc:L.t -> string -> t
val set_option : ?loc:L.t -> (string * T.t option) -> t
val type_decl : ?loc:L.t -> I.t -> int -> t
val type_def : ?loc:L.t -> I.t -> I.t list -> T.t -> t
val fun_decl : ?loc:L.t -> I.t -> T.t list -> T.t -> t
val fun_def : ?loc:L.t -> I.t -> T.t list -> T.t -> T.t -> t
val get_proof : ?loc:L.t -> unit -> t
val get_unsat_core : ?loc:L.t -> unit -> t
val get_value : ?loc:L.t -> T.t list -> t
val get_assignment : ?loc:L.t -> unit -> t
val get_assertions : ?loc:L.t -> unit -> t
val exit : ?loc:L.t -> unit -> t
val tpi : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val thf : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val tff : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val fof : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val cnf : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val inductive : ?loc:L.t -> I.t -> T.t list -> (I.t * T.t list) list -> t
val data : ?loc:L.t -> t list -> t
val decl : ?loc:L.t -> I.t -> T.t -> t
val definition : ?loc:L.t -> I.t -> T.t -> T.t -> t
val goal : ?loc:L.t -> ?attr:T.t -> T.t -> t
val assume : ?loc:L.t -> ?attr:T.t -> T.t -> t
val rewrite : ?loc:L.t -> ?attr:T.t -> T.t -> t
OCaml

Innovation. Community. Security.