dolmen.class
Make.S
Signature used by the Response class, which parses prover responses, i.e. SAT/UNSAT answers (with option certificates).
dolmen
dolmen.ae
dolmen.dimacs
dolmen.icnf
dolmen.intf
dolmen.line
dolmen.smtlib2
dolmen.std
dolmen.tptp
dolmen.zf
dolmen_smtlib2_poly
dolmen_smtlib2_v6
dolmen_smtlib2_v6_response
dolmen_smtlib2_v6_script
dolmen_tptp_v6_3_0
type t
The type of statements.
val error : ?loc:L.t -> string -> t
Create an `ERROR` answer.
val unsat : ?loc:L.t -> unit -> t
Create an `UNSAT` answer.
type defs
Definition for model values
val fun_def : ?loc:L.t -> I.t -> T.t list -> T.t list -> T.t -> T.t -> defs
Defines a new function. fun_def f args ret body is such that applications of f are equal to body (module substitution of the arguments), which should be of type ret.
fun_def f args ret body
f
body
ret
val funs_def_rec : ?loc:L.t -> (I.t * T.t list * T.t list * T.t * T.t) list -> defs
Defines a list of mutually recursive functions.
val sat : ?loc:L.t -> defs list option -> t
Create a `SAT` answer with an (optional) model.