1 files changed, 36 insertions, 0 deletions
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