blob: ba9be04e42d5fe7e196b03ce88545f79f94d61bd (
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
26
27
28
29
30
31
32
33
34
35
36
37
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2021 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
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
|
