4 files changed, 170 insertions, 0 deletions
diff --git a/src/zchaff/cnfParser.mli b/src/zchaff/cnfParser.mli
new file mode 100644
index 0000000..4e2e079
--- /dev/null
+++ b/src/zchaff/cnfParser.mli
@@ -0,0 +1,13 @@
+val skip_comment : SatParser.lex_buff -> unit
+val parse_p_cnf : SatParser.lex_buff -> int
+val mklit : int -> SatAtom.Form.reify -> int -> SatAtom.Form.t
+val parse_clause :
+  int -> SatAtom.Form.reify -> SatParser.lex_buff -> SatAtom.Form.t list
+val parse_clauses :
+  int ->
+  SatAtom.Form.reify ->
+  SatParser.lex_buff ->
+  SatAtom.Form.t SmtCertif.clause -> SatAtom.Form.t SmtCertif.clause
+val parse_cnf :
+  string ->
+  int * SatAtom.Form.t SmtCertif.clause * SatAtom.Form.t SmtCertif.clause
diff --git a/src/zchaff/satParser.mli b/src/zchaff/satParser.mli
new file mode 100644
index 0000000..ad5385b
--- /dev/null
+++ b/src/zchaff/satParser.mli
@@ -0,0 +1,33 @@
+type lex_buff = {
+  buff : string;
+  mutable curr_char : int;
+  mutable buff_end : int;
+  in_ch : in_channel;
+}
+val buff_length : int
+val open_file : string -> string -> lex_buff
+val close : lex_buff -> unit
+val eof : lex_buff -> bool
+val curr_char : lex_buff -> char
+val refill : lex_buff -> unit
+val is_space : char -> bool
+val is_space_ret : char -> bool
+val skip : (char -> bool) -> lex_buff -> unit
+val skip_space : lex_buff -> unit
+val skip_blank : lex_buff -> unit
+val skip_string : lex_buff -> string -> bool
+val match_string : lex_buff -> string -> unit
+val aux_buff : bytes
+val aux_be : int ref
+val aux_pi : int ref
+val aux_cc : int ref
+val save_lb : lex_buff -> unit
+val restore_lb : lex_buff -> unit
+val check_string : lex_buff -> string -> bool
+val blank_check_string : lex_buff -> string -> bool
+val blank_match_string : lex_buff -> string -> unit
+val is_digit : char -> bool
+val is_start_int : lex_buff -> bool
+val input_int : lex_buff -> int
+val input_blank_int : lex_buff -> int
+val skip_line : lex_buff -> unit
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
diff --git a/src/zchaff/zchaffParser.mli b/src/zchaff/zchaffParser.mli
new file mode 100644
index 0000000..a512f48
--- /dev/null
+++ b/src/zchaff/zchaffParser.mli
@@ -0,0 +1,36 @@
+val _CL : string
+val _INF : string
+val _VAR : string
+val _L : string
+val _V : string
+val _A : string
+val _LITS : string
+val _CONF : string
+val _EQ : string
+val alloc_res :
+  'a SmtCertif.clause ->
+  'a SmtCertif.clause ->
+  'a SmtCertif.clause -> 'a SmtCertif.clause list -> 'a SmtCertif.clause
+val parse_tailres : (int, 'a) Hashtbl.t -> SatParser.lex_buff -> 'a list
+val parse_resolution :
+  (int, 'a SmtCertif.clause) Hashtbl.t ->
+  SatParser.lex_buff -> 'a SmtCertif.clause -> 'a SmtCertif.clause
+val parse_CL :
+  (int, 'a SmtCertif.clause) Hashtbl.t ->
+  SatParser.lex_buff -> 'a SmtCertif.clause -> 'a SmtCertif.clause
+type var_key = Var of int | Level of int
+type 'hform var_decl = {
+  var : int;
+  ante : 'hform SmtCertif.clause;
+  ante_val : int list;
+  mutable vclause : 'hform SmtCertif.clause option;
+}
+type 'hform parse_var_info = (var_key, 'hform var_decl) Hashtbl.t
+val var_of_lit : int -> int
+val parse_zclause : SatParser.lex_buff -> int list
+val parse_VAR_CONF :
+  (int, 'a SmtCertif.clause) Hashtbl.t ->
+  SatParser.lex_buff -> 'a SmtCertif.clause -> 'a SmtCertif.clause
+val parse_proof :
+  (int, 'a SmtCertif.clause) Hashtbl.t ->
+  string -> 'a SmtCertif.clause -> 'a SmtCertif.clause