Source file eq_encode.ml
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
(** {1 Applicative Encoding} *)
open Logtk
open Libzipperposition
let section = Util.Section.make ~parent:Const.section "eq_encode"
let mode_ : [ `None | `Extensional | `Intensional ] ref = ref `None
module T = TypedSTerm
let enabled_ = ref false
let refl_ = ref true
let symm_ = ref true
let trans_ = ref false
let (==>) = T.Ty.(==>)
let decl id ty = Statement.ty_decl ~proof:Proof.Step.trivial id ty
let eq_id = ID.make "$_eq_proxy"
let eq_type =
let alpha = Var.make ~ty:T.tType (ID.make "alpha") in
let body = [T.var alpha; T.var alpha] ==> T.Ty.prop in
T.Ty.close_forall body
let eq_term = T.const ~ty:eq_type eq_id
let eq_clone_tydecl = decl eq_id eq_type
(** Type declarations for these new symbols *)
let ty_decls =
Iter.singleton eq_clone_tydecl
let eq_properties () =
let alpha_var = Var.make ~ty:T.tType (ID.make "alpha") in
let alpha = T.var alpha_var in
let x = T.var (Var.make ~ty:alpha (ID.make "X")) in
let y = T.var (Var.make ~ty:alpha (ID.make "Y")) in
let z = T.var (Var.make ~ty:alpha (ID.make "Y")) in
let app_eq args = T.app ~ty:T.Ty.prop eq_term (alpha::args) in
let refl =
[SLiteral.atom_true (app_eq [x; x])] in
let symm =
[SLiteral.atom_false (app_eq [x; y]);
SLiteral.atom_true (app_eq [y; x])] in
let trans =
[SLiteral.atom_false (app_eq [x; y]);
SLiteral.atom_false (app_eq [y; z]);
SLiteral.atom_true (app_eq [x; z])] in
Iter.of_list ((if !refl_ then [refl] else [])
@ (if !symm_ then [symm] else [])
@ (if !trans_ then [trans] else []) )
(** Encode a literal *)
let eq_encode_lit lit =
Util.debugf ~section 2 "# Encoding Literal %a" (fun k -> k (SLiteral.pp T.pp) lit);
match lit with
| SLiteral.Eq(lhs, rhs) | SLiteral.Neq(lhs, rhs) ->
let sign = match lit with SLiteral.Eq _ -> true | _ -> false in
let ty = T.ty_exn lhs in
let encoded = T.app ~ty:T.Ty.prop eq_term [ty; lhs; rhs] in
SLiteral.atom encoded sign
| _ -> lit
(** Encode a clause *)
let eq_encode_lits lits = List.map eq_encode_lit lits
exception E_i of ((T.t SLiteral.t) list, T.t, T.t) Statement.t
let pp_in pp_f pp_t pp_ty = function
| Output_format.O_zf -> Statement.ZF.pp pp_f pp_t pp_ty
| Output_format.O_tptp -> Statement.TPTP.pp pp_f pp_t pp_ty
| Output_format.O_normal -> Statement.pp pp_f pp_t pp_ty
| Output_format.O_none -> CCFormat.silent
let pp_clause_in o =
let pp_t = T.pp_in o in
pp_in (Util.pp_list ~sep:" ∨ " (SLiteral.pp_in o pp_t)) pp_t pp_t o
let res_tc =
Proof.Result.make_tc
~of_exn:(function E_i c -> Some c | _ -> None)
~to_exn:(fun i -> E_i i)
~compare:compare
~pp_in:pp_clause_in
~is_stmt:true
~name:Statement.name
~to_form:(fun ~ctx st ->
let conv_c (c:(T.t SLiteral.t) list) : _ =
c
|> List.map SLiteral.to_form
|> T.Form.or_
in
Statement.Seq.forms st
|> Iter.map conv_c
|> Iter.to_list
|> T.Form.and_)
()
(** encode a statement *)
let eq_encode_stmt stmt =
let as_proof = Proof.S.mk (Statement.proof_step stmt) (Proof.Result.make res_tc stmt) in
let proof = Proof.Step.esa ~rule:(Proof.Rule.mk "eq_encode") [as_proof |> Proof.Parent.from] in
match Statement.view stmt with
| Statement.Data _ -> failwith "Not implemented: Data"
| Statement.Lemma _ -> failwith "Not implemented: Lemma"
| Statement.Goal lits -> failwith "Not implemented: Goal"
| Statement.Def _ | Statement.Rewrite _ | Statement.TyDecl _ -> stmt
| Statement.NegatedGoal (skolems,clauses) ->
Statement.neg_goal ~proof ~skolems (List.map eq_encode_lits clauses)
| Statement.Assert lits -> Statement.assert_ ~proof (eq_encode_lits lits)
let extension =
let modifier seq =
if !enabled_ then (
let seq = Iter.map eq_encode_stmt seq in
Util.debug ~section 2 "Start eq encoding";
let axioms =
Iter.map (Statement.assert_ ~proof:Proof.Step.trivial) (eq_properties ()) in
let seq = Iter.append ty_decls (Iter.append axioms seq) in
Util.debug ~section 2 "Finished eq encoding";
seq
) else seq
in
Extensions.(
{ default with name="eq_encode"; post_cnf_modifiers=[modifier]; }
)
let () =
Options.add_opts
[ "--eq-encode", Arg.Bool ((:=) enabled_), " enable/disable replacing equality by proxies";
"--eq-encode-refl", Arg.Bool ((:=) refl_), " enable/disable eq proxy reflexivity axiom";
"--eq-encode-symm", Arg.Bool ((:=) symm_), " enable/disable eq proxy symmetry axiom";
"--eq-encode-trans", Arg.Bool ((:=) trans_), " enable/disable eq proxy transitivity axiom";]