blob: 6a5fca8005d34134b352326c5d794acf4183bc59 (
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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
open SmtMisc
module type ATOM =
sig
type t
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 -> logic
end
type fop =
| Ftrue
| Ffalse
| Fand
| For
| Fxor
| Fimp
| Fiff
| Fite
| Fnot2 of int
| Fforall of (string * SmtBtype.btype) list
type ('a,'f) gen_pform =
| Fatom of 'a
| Fapp of fop * 'f array
| FbbT of 'a * 'f list
module type FORM =
sig
type hatom
type t
type pform = (hatom, t) gen_pform
val pform_true : pform
val pform_false : pform
val equal : t -> t -> bool
val to_lit : t -> int
val index : t -> int
val pform : t -> pform
val neg : t -> t
val is_pos : t -> bool
val is_neg : t -> bool
val to_smt : ?debug:bool ->
Format.formatter -> t -> unit
val logic : t -> logic
(* Building formula from positive formula *)
exception NotWellTyped of pform
type reify
val create : unit -> reify
val clear : reify -> unit
val get : ?declare:bool -> reify -> pform -> t
(** Given a coq term, build the corresponding formula *)
val of_coq : (CoqInterface.constr -> hatom) -> reify -> CoqInterface.constr -> t
val hash_hform : (hatom -> hatom) -> reify -> t -> t
(** Flattening of [Fand] and [For], removing of [Fnot2] *)
val flatten : reify -> t -> t
(** Turn n-ary [Fand] and [For] into their right-associative
counter-parts *)
val right_assoc : reify -> t -> t
(** Producing Coq terms *)
val to_coq : t -> CoqInterface.constr
val pform_tbl : reify -> pform array
val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
val interp_tbl : reify -> CoqInterface.constr * CoqInterface.constr
val nvars : reify -> int
(* Producing a Coq term corresponding to the interpretation
of a formula *)
(* [interp_atom] map [hatom] to coq term, it is better if it produce
shared terms. *)
val interp_to_coq :
(hatom -> CoqInterface.constr) -> (int, CoqInterface.constr) Hashtbl.t ->
t -> CoqInterface.constr
(* Unstratified terms *)
type atom_form_lit =
| Atom of hatom
| Form of pform
| Lit of t
val lit_of_atom_form_lit : reify -> bool * atom_form_lit -> t
end
module Make (Atom:ATOM) : FORM with type hatom = Atom.t
|
