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/trace/smtCnf.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/trace/smtCnf.mli')
-rw-r--r-- | src/trace/smtCnf.mli | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/trace/smtCnf.mli b/src/trace/smtCnf.mli new file mode 100644 index 0000000..47fbd8c --- /dev/null +++ b/src/trace/smtCnf.mli @@ -0,0 +1,25 @@ +module MakeCnf : + functor (Form : SmtForm.FORM) -> + sig + type form_info = Immediate of bool | Done | Todo + val info : (int, form_info) Hashtbl.t + val init_last : Form.t SmtCertif.clause + val last : Form.t SmtCertif.clause ref + val cnf_todo : Form.t array list ref + val clear : unit -> unit + val push_cnf : Form.t array -> unit + val get_info : Form.t -> form_info + val set_done : Form.t -> unit + val set_immediate : Form.t -> unit + val test_immediate : Form.t -> bool + val check_trivial : Form.t list -> bool + val link_Other : Form.t SmtCertif.rule -> Form.t list -> unit + val both_lit : Form.t -> Form.t * Form.t + val or_of_imp : Form.t array -> Form.t array + val cnf : Form.t -> unit + exception Cnf_done + val imm_link_Other : Form.t SmtCertif.rule -> Form.t -> unit + val imm_cnf : Form.t SmtCertif.clause -> unit + val make_cnf : + Form.reify -> Form.t SmtCertif.clause -> Form.t SmtCertif.clause + end |