diff options
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 |