blob: 47fbd8c9bebde2940d2f86adac3aacbd0f35d635 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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
|
