- auto-generated mli files for future documentation

- new Makefiles to handle these mli

1 files changed, 88 insertions, 0 deletions

diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli
new file mode 100644
index 0000000..ff0fe51
--- /dev/null
+++ b/src/zchaff/zchaff.mli
@@ -0,0 +1,88 @@
+val is_trivial : SatAtom.Form.t list -> bool
+val string_of_op : SmtForm.fop -> string
+val pp_form : Format.formatter -> SatAtom.Form.t -> unit
+val pp_sign : Format.formatter -> SatAtom.Form.t -> unit
+val pp_pform : Format.formatter -> SatAtom.Form.pform -> unit
+val pp_value : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit
+val pp_kind : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit
+val pp_trace : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit
+val import_cnf :
+  string ->
+  int * SatAtom.Form.t SmtCertif.clause * SatAtom.Form.t SmtCertif.clause *
+  (int, SatAtom.Form.t SmtCertif.clause) Hashtbl.t
+val import_cnf_trace :
+  (int, 'a SmtCertif.clause) Hashtbl.t ->
+  string ->
+  SatAtom.Form.t SmtCertif.clause ->
+  'a SmtCertif.clause -> int * 'a SmtCertif.clause
+val make_roots :
+  SatAtom.Form.t SmtCertif.clause -> 'a SmtCertif.clause -> Term.constr
+val interp_roots :
+  SatAtom.Form.t SmtCertif.clause -> 'a SmtCertif.clause -> Term.constr
+val sat_checker_modules : string list list
+val parse_certif :
+  Names.identifier -> Names.identifier -> string -> string -> unit
+val cdimacs : Term.constr lazy_t
+val ctheorem_checker : Term.constr lazy_t
+val cchecker : Term.constr lazy_t
+val theorems :
+  (Term.constr ->
+   SatAtom.Form.t SmtCertif.clause ->
+   SatAtom.Form.t SmtCertif.clause -> Term.constr) ->
+  Names.identifier -> string -> string -> unit
+val theorem : Names.identifier -> string -> string -> unit
+val theorem_abs : Names.identifier -> string -> string -> unit
+val checker : string -> string -> unit
+val export_clause : Format.formatter -> SatAtom.Form.t list -> unit
+val export :
+  out_channel ->
+  int ->
+  SatAtom.Form.t SmtCertif.clause ->
+  (int, SatAtom.Form.t SmtCertif.clause) Hashtbl.t *
+  SatAtom.Form.t SmtCertif.clause
+val call_zchaff :
+  int ->
+  SatAtom.Form.t SmtCertif.clause ->
+  (int, SatAtom.Form.t SmtCertif.clause) Hashtbl.t * string * string *
+  SatAtom.Form.t SmtCertif.clause
+val cnf_checker_modules : string list list
+val certif_ops :
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t
+val ccertif : Term.constr lazy_t
+val cCertif : Term.constr lazy_t
+val cchecker_b_correct : Term.constr lazy_t
+val cchecker_b : Term.constr lazy_t
+val cchecker_eq_correct : Term.constr lazy_t
+val cchecker_eq : Term.constr lazy_t
+val build_body :
+  SatAtom.Atom.reify_tbl ->
+  SatAtom.Form.reify ->
+  Term.constr ->
+  Term.constr ->
+  int * SatAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr
+val build_body_eq :
+  SatAtom.Atom.reify_tbl ->
+  SatAtom.Form.reify ->
+  Term.constr ->
+  Term.constr ->
+  Term.constr ->
+  int * SatAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr
+val get_arguments : Term.constr -> Term.constr * Term.constr
+exception Sat of int list
+exception Finished
+val input_int : in_channel -> int
+val check_unsat : string -> unit
+val make_proof :
+  (int, 'a) SmtForm.gen_pform array ->
+  Term.constr array ->
+  Environ.env ->
+  SatAtom.Form.reify ->
+  SatAtom.Form.t -> int * SatAtom.Form.t SmtCertif.clause
+val core_tactic : Environ.env -> 'a -> Term.types -> Proof_type.tactic
+val tactic : unit -> Proof_type.tactic