blob: 9f4272cc3c3fdae616a6458d04bd37261f14223b (
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
module Atom : sig
type t = int
val index : t -> int
val equal : t -> t -> bool
val is_bool_type : t -> bool
val is_bv_type : t -> bool
val to_smt : ?debug:bool -> Format.formatter -> t -> unit
val logic : t -> SmtMisc.logic
type reify_tbl = {
mutable count : int;
tbl : (CoqInterface.constr, t) Hashtbl.t;
}
val create : unit -> reify_tbl
val declare : reify_tbl -> CoqInterface.constr -> t
val get : reify_tbl -> CoqInterface.constr -> t
val atom_tbl : reify_tbl -> CoqInterface.constr array
val interp_tbl : reify_tbl -> CoqInterface.constr
end
module Form : SmtForm.FORM with type hatom = Atom.t
module Trace :
sig
val share_prefix : Form.t SmtCertif.clause -> int -> unit
end
module Cnf :
sig
type form_info =
SmtCnf.MakeCnf(Form).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
|
