dolmen 0.1 · OCaml Package

type t

type id

type term

type location

val annot : ?loc:location -> term -> term list -> term

val include_ : ?loc:location -> string -> id list -> t

val clause : ?loc:location -> term list -> t

val pop : ?loc:location -> int -> t

val push : ?loc:location -> int -> t

val assert_ : ?loc:location -> term -> t

val check_sat : ?loc:location -> unit -> t

val set_logic : ?loc:location -> string -> t

val get_info : ?loc:location -> string -> t

val set_info : ?loc:location -> (string * term option) -> t

val get_option : ?loc:location -> string -> t

val set_option : ?loc:location -> (string * term option) -> t

val type_decl : ?loc:location -> id -> int -> t

val type_def : ?loc:location -> id -> id list -> term -> t

val fun_decl : ?loc:location -> id -> term list -> term -> t

val fun_def : ?loc:location -> id -> term list -> term -> term -> t

val get_proof : ?loc:location -> unit -> t

val get_unsat_core : ?loc:location -> unit -> t

val get_value : ?loc:location -> term list -> t

val get_assignment : ?loc:location -> unit -> t

val get_assertions : ?loc:location -> unit -> t

val exit : ?loc:location -> unit -> t

val tpi : ?loc:location -> ?annot:term -> id -> string -> term -> t

val thf : ?loc:location -> ?annot:term -> id -> string -> term -> t

val tff : ?loc:location -> ?annot:term -> id -> string -> term -> t

val fof : ?loc:location -> ?annot:term -> id -> string -> term -> t

val cnf : ?loc:location -> ?annot:term -> id -> string -> term -> t

val inductive : ?loc:location -> id -> term list -> (id * term list) list -> t

val data : ?loc:location -> t list -> t

val decl : ?loc:location -> id -> term -> t

val definition : ?loc:location -> id -> term -> term -> t

val goal : ?loc:location -> ?attr:term -> term -> t

val assume : ?loc:location -> ?attr:term -> term -> t

val rewrite : ?loc:location -> ?attr:term -> term -> t

package dolmen