blob: 118ecf57e828ff00a63a4e49012f22c4c96e08c7 (
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
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2015 *)
(* *)
(* Michaël Armand *)
(* Benjamin Grégoire *)
(* Chantal Keller *)
(* *)
(* Inria - École Polytechnique - MSR-Inria Joint Lab *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
module type ATOM =
sig
type t
val index : t -> int
val equal : t -> t -> bool
val is_bool_type : t -> bool
end
type fop =
| Ftrue
| Ffalse
| Fand
| For
| Fxor
| Fimp
| Fiff
| Fite
| Fnot2 of int
type ('a,'f) gen_pform =
| Fatom of 'a
| Fapp of fop * 'f array
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 : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
(* Building formula from positive formula *)
exception NotWellTyped of pform
type reify
val create : unit -> reify
val clear : reify -> unit
val get : reify -> pform -> t
(** Given a coq term, build the corresponding formula *)
val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
(** Flattening of [Fand] and [For], removing of [Fnot2] *)
val flatten : reify -> t -> t
(** Producing Coq terms *)
val to_coq : t -> Term.constr
val pform_tbl : reify -> pform array
val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
val interp_tbl : reify -> Term.constr * Term.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 -> Term.constr) -> (int, Term.constr) Hashtbl.t ->
t -> Term.constr
end
module Make (Atom:ATOM) : FORM with type hatom = Atom.t
|
