diff options
author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-11-24 18:06:20 +0100 |
---|---|---|
committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-11-24 18:06:20 +0100 |
commit | a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0 (patch) | |
tree | 4a934a82dc23b9fa8d0089dc2a95cbbe820733ca /src/zchaff/zchaffParser.mli | |
parent | 6566176e1f87838bada8c04ba80e608e8c7e958f (diff) | |
download | smtcoq-a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0.tar.gz smtcoq-a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0.zip |
- auto-generated mli files for future documentation
- new Makefiles to handle these mli
Diffstat (limited to 'src/zchaff/zchaffParser.mli')
-rw-r--r-- | src/zchaff/zchaffParser.mli | 36 |
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 |