blob: 00d2034a14cf18d3dc951407c87fd1a3bdbd166f (
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
|
(**************************************************************************)
(* *)
(* 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 SatParser
open SmtCertif
open SmtTrace
let _CL = "CL:"
let _INF = "<="
let _VAR = "VAR:"
let _L = "L:"
let _V = "V:"
let _A = "A:"
let _LITS = "Lits:"
let _CONF = "CONF:"
let _EQ = "=="
(** Parsing of zchaff proof *)
let alloc_res last c1 c2 tail =
let c = mkRes c1 c2 tail in
link last c;
c
let rec parse_tailres reloc lb =
if is_start_int lb then
let cl_id = Hashtbl.find reloc (input_int lb) in
cl_id :: parse_tailres reloc lb
else []
let parse_resolution reloc lb last =
let id = input_blank_int lb in
blank_match_string lb _INF;
let c1 = Hashtbl.find reloc (input_blank_int lb) in
let c2 = Hashtbl.find reloc (input_blank_int lb) in
let tl = parse_tailres reloc lb in
let c = alloc_res last c1 c2 tl in
Hashtbl.add reloc id c;
c
let parse_CL reloc lb last =
let last = ref last in
while blank_check_string lb _CL do
last := parse_resolution reloc lb !last
done;
!last
(* Parsing of the VAR and CONF part *)
(* let var_of_lit l = l lsr 1 *)
type var_key =
| Var of int
| Level of int
type 'hform var_decl = {
var : int;
ante : 'hform clause;
ante_val : int list;
mutable vclause : 'hform clause option
}
type 'hform parse_var_info = (var_key, 'hform var_decl) Hashtbl.t
let var_of_lit l = l lsr 1
let parse_zclause lb =
let zc = ref [var_of_lit (input_blank_int lb)] in
while is_start_int lb do
zc := var_of_lit (input_int lb) :: !zc;
done;
!zc
let parse_VAR_CONF reloc lb last =
let max_level = ref (-1) in
let vartbl = Hashtbl.create 100 in
(* parsing of the VAR part *)
while blank_check_string lb _VAR do
let x = input_blank_int lb in
blank_match_string lb _L;
let lv = input_blank_int lb in
blank_match_string lb _V;
let _ = input_blank_int lb in
blank_match_string lb _A;
let ante = Hashtbl.find reloc (input_blank_int lb) in
blank_match_string lb _LITS;
let ante_val = parse_zclause lb in
max_level := max !max_level lv;
let vd = { var = x; ante = ante; ante_val = ante_val; vclause = None } in
Hashtbl.add vartbl (Var x) vd;
Hashtbl.add vartbl (Level lv) vd;
done;
(* Adding the resolution *)
let rec build_res0 l =
match l with
| [] -> []
| y :: l ->
let yd =
try Hashtbl.find vartbl (Var y)
with Not_found ->
Printf.printf "Var %i not found.\n" y;raise Not_found in
match yd.vclause with
| Some cy -> cy :: build_res0 l
| _ -> assert false in
let rec build_res1 x l =
match l with
| [] -> assert false
| y :: l ->
if x = y then build_res0 l
else
let yd =
try Hashtbl.find vartbl (Var y)
with Not_found ->
Printf.printf "Var %i not found.\n" y;raise Not_found in
match yd.vclause with
| Some cy -> cy :: build_res1 x l
| _ -> assert false in
let last = ref last in
for lv = 0 to !max_level do
try
let vd = Hashtbl.find vartbl (Level lv) in
let c =
match build_res1 vd.var vd.ante_val with
| [] -> vd.ante
| c2::tl ->
last := alloc_res !last vd.ante c2 tl; !last in
vd.vclause <- Some c;
with Not_found -> ()
done;
(* parsing of the CONF *)
blank_match_string lb _CONF;
let conf =
let id = input_blank_int lb in
Hashtbl.find reloc id in
blank_match_string lb _EQ;
let conf_val = parse_zclause lb in
match build_res0 conf_val with
| [] -> assert false
| c2::tl -> alloc_res !last conf c2 tl
let parse_proof reloc filename last =
let lb = open_file "Proof" filename in
let last = parse_CL reloc lb last in
let last = parse_VAR_CONF reloc lb last in
close lb;
last
|
