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/cnfParser.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/cnfParser.mli')
| -rw-r--r-- | src/zchaff/cnfParser.mli | 13 |
1 files changed, 13 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 |