blob: fdc9bafc4ea274b7412da5a0aae60acb909ddb2f (
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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
(**
Signature to implement to build a converter of LFSC proofs.
See {!Converter.Make}, {!Tosmtcoq} and {!VeritPrinter}.
*)
open Ast
open Format
(** The type of destination rules that are currently supported by the
converter *)
type rule =
| Reso
| Weak
| Or
| Orp
| Imp
| Impp
| Nand
| Andn
| Nimp1
| Nimp2
| Impn1
| Impn2
| Nor
| Orn
| And
| Andp
| Equ1
| Equ2
| Nequ1
| Nequ2
| Equp1
| Equp2
| Equn1
| Equn2
| Xor1
| Xor2
| Xorp1
| Xorp2
| Xorn1
| Xorn2
| Nxor1
| Nxor2
| Itep1
| Itep2
| Iten1
| Iten2
| Ite1
| Ite2
| Nite1
| Nite2
| Eqtr
| Eqcp
| Eqco
| Eqre
| Lage
| Flat
| Hole
| True
| Fals
| Bbva
| Bbconst
| Bbeq
| Bbdis
| Bbop
| Bbadd
| Bbmul
| Bbult
| Bbslt
| Bbshl
| Bbshr
| Bbnot
| Bbneg
| Bbconc
| Bbextr
| Bbzext
| Bbsext
| Row1
| Row2
| Exte
(** Signature for translators *)
module type S = sig
(** The type of literal depends on the chosen tranlation, it is abstract *)
type lit
(** Clauses are lists of the aforementioned literals *)
type clause = lit list
(** Transform a term in LFSC to the chosen clause representation. (This
eliminates top-level dijunctions and implications.) *)
val to_clause : term -> clause
(** Print a clause (for debugging purposes) *)
val print_clause : formatter -> clause -> unit
(** Manually resgister a clause with an integer identifier *)
val register_clause_id : clause -> int -> unit
(** Create a new clause as the result of a rule application with a list of
intgeger arguments. These can be either previously defined clause
identifiers or an arbitrary positive integer depending on the rule. It
returns the identifier of the newly created resulting clause. The
optional arguemnt [reuse] ([true] by default) says if we should reuse
clauses that were previously deduced, in this case the rule application
will not be created and it returns the identifier of this pre-existing
clause. *)
val mk_clause : ?reuse:bool -> rule -> clause -> int list -> int
(** Same as {!mk_clause} but with an hybrid representation for clauses. This
is just used to avoid creating unecessary terms for these clauses when
they are built by hand. *)
val mk_clause_cl : ?reuse:bool -> rule -> term list -> int list -> int
(** Create an input unit clause. It is given an identifier that is not
returned. *)
val mk_input : Hstring.t -> term -> unit
val mk_admit_preproc : Hstring.t -> term -> unit
(** [register_prop_abstr v p] register the term [v] as being a propositional
abstraction of the term [p]. *)
val register_prop_abstr : term -> term -> unit
(** Returns the identifier of a previously deduced clause. *)
val get_clause_id : clause -> int
(** Returns the identifier of a unit input clause given its name, as
intoduced by the proprocessor of CVC4 in the LFSC proof. *)
val get_input_id : Hstring.t -> int
val register_decl : Hstring.t -> term -> unit
val register_decl_id : Hstring.t -> int -> unit
(** register an alias name for a term *)
val register_alias : Hstring.t -> term -> unit
(* (\** register a term as an alias for another term *\) *)
(* val register_termalias : term -> term -> unit *)
(** Clear and reset global tables and values. *)
val clear : unit -> unit
end
|
