1 (*open satCommonTools dimacsTools;; *)
3 (* parse minisat proof log into array cl.
4 array elements are either root clauses or
5 resolution chains for deriving the learnt clauses.
6 Last chain derives empty clause *)
9 Rthm of thm * Litset.t * term * thm
10 | Ll of term * Litset.t
14 | Chain of (int * int) list * int (* var, cl index list and the length of that list *)
16 | Learnt of thm * Litset.t (* clause thm, lits as nums set *)
18 let sat_fileopen s = open_in_bin s
20 let sat_fileclose is = close_in is
22 let sat_getChar is = Int32.of_int(input_byte is)
24 (* copied from Minisat-p_v1.14::File::getUInt*)
25 (* this is technically able to parse int32's but no *)
26 (* point since we return int's always *)
27 (* FIXME: no idea what will happen on a 64-bit arch *)
29 let (land) = Int32.logand in
30 let (lor) = Int32.logor in
31 let (lsl) = Int32.shift_left in
32 let (lsr) = Int32.shift_right in
33 let byte0 = sat_getChar is in
34 if ((byte0 land (0x80l))=(0x0l)) (* 8 *)
35 then Int32.to_int(byte0)
37 match Int32.to_int((byte0 land (0x60l)) lsr 5) with
39 let byte1 = sat_getChar is in
40 Int32.to_int(((byte0 land (0x1Fl)) lsl 8) lor byte1) (* 16 *)
42 let byte1 = sat_getChar is in
43 let byte2 = sat_getChar is in
44 Int32.to_int( (((byte0 land (0x1Fl)) lsl 16) lor (byte1 lsl 8)) lor byte2)
46 let byte1 = sat_getChar is in
47 let byte2 = sat_getChar is in
48 let byte3 = sat_getChar is in
49 Int32.to_int(((((byte0 land (0x1Fl)) lsl 24) lor (byte1 lsl 16))
50 lor (byte2 lsl 8)) lor byte3)
51 (* default case is only where int64 is needed since we do a lsl 32*)
53 let byte0 = sat_getChar is in
54 let byte1 = sat_getChar is in
55 let byte2 = sat_getChar is in
56 let byte3 = sat_getChar is in
57 let byte4 = sat_getChar is in
58 let byte5 = sat_getChar is in
59 let byte6 = sat_getChar is in
60 let byte7 = sat_getChar is in
61 Int32.to_int((((byte0 lsl 24) lor (byte1 lsl 16) lor (byte2 lsl 8) lor byte3) lsl 32)
62 lor ((byte4 lsl 24) lor (byte5 lsl 16) lor (byte6 lsl 8) lor byte7))
64 let isRootClauseIdx cl ci =
65 match Array.get cl ci with
70 (* this mapping allows shadow ac-normalisation which keeps the lits for a given var together *)
71 (* the -1 is because literalToInt returns HolSatLib var numbers (base 1) *)
73 let (sign,vnum) = literalToInt p in
74 2*(vnum-1)+(if sign then 1 else 0)
77 let (sign,vnum) = literalToInt p in
80 (* parse a root clause *)
81 let getIntRoot fin idx =
82 let rec loop idx' acc =
83 let v = sat_getint fin in
85 then idx::(List.rev acc)
86 else loop (idx'+v) ((idx'+v)::acc) in
87 let res = loop idx [] in
90 (*l1 and l2 are number reps of lits. Are they complements? *)
91 let is_compl l1 l2 = (abs(l2-l1)=1) && (l1 mod 2 = 0)
93 (*il is clause input from minisat proof trace,
94 sl is internal clause sorted and unduped, with diff in var numbering account for *)
95 (* thus if il and sl are not exactly the same,
96 then the clause represented by sl was skipped *)
97 let isSameClause (il,sl) = (Pervasives.compare il sl = 0)
99 let rec getNextRootClause scl vc cc lr il rcv =
100 let rc = Array.get rcv lr in
101 let rcl = disjuncts rc in
102 let lnl = List.map literalToInt3 rcl in
104 List.fold_left (fun s e -> Litset.add e s)
106 let slnl = (* FIXME: speed this up*)
107 List.sort Pervasives.compare
109 (List.map (fun (isn,vi) ->
113 if isSameClause(il,slnl)
114 then (Array.set scl lr cc;(lr,(rc,lns)))
115 else getNextRootClause scl vc cc (lr+1) il rcv
117 (* this advances the file read pointer but we pick up the
118 actual clause from the list of clauses we already have
119 this is because minisatp removes duplicate literals
120 and sorts the literals so I can't efficiently find the
121 corresponding clause term in HOL.
122 assert: minisatp logs the root clauses in order of input*)
123 let addClause scl vc cc lr rcv fin sr lit1 =
124 let l = getIntRoot fin (lit1 lsr 1) in
127 [] -> failwith ("addClause:Failed parsing clause "^(string_of_int (cc))^"\n")
130 getNextRootClause scl vc cc lr l rcv in
131 (cc+1,lr+1,(Root (Ll (t,lns)))::sr) in
134 (* parse resolve chain *)
135 let getIntBranch fin id h =
136 let rec loop acc len =
137 (*-1 is purely a decoding step *)
138 (* (i.e. not translating b/w HolSat and ms)*)
139 let v = (sat_getint fin)-1 in
141 then ((v,h)::(List.rev acc),len+1)
143 let ci = id-(sat_getint fin) in
144 loop ((v,ci)::acc) (len+1) in
145 let res = loop [] 0 in
148 let addBranch fin sr cc id tc =
150 getIntBranch fin id (id-(tc lsr 1)) in
152 if brl=1 (*(tl br = []) *)
153 then (cc,false,sr) (* delete *)
154 else (cc+1,true,(Chain (br,brl))::sr) (* resolve *) in
157 (*this is modelled on MiniSat::Proof::traverse,
158 except we first read in everything then resolve backwards *)
159 (*sr is stack for originally reading in the clauses *)
160 (*lr is unskipped root clause count. *)
161 (*cc is clause count (inc learnt) *)
163 let rec readTrace_aux scl vc cc lr rcv fin sr id =
164 let tmp,eof = try sat_getint fin,false with End_of_file -> 42,true in
165 if eof then (cc,sr) else
169 addClause scl vc cc lr rcv fin sr tmp in
170 readTrace_aux scl vc cc lr rcv fin sr (id+1)
173 addBranch fin sr cc id tmp in
175 then readTrace_aux scl vc cc lr rcv fin sr' (id+1) (* chain *)
176 else readTrace_aux scl vc cc lr rcv fin sr' id (* deletion *)
179 (*fill in the root clause and chain array*)
180 let parseTrace nr fname vc rcv =
182 let fin = sat_fileopen fname in
183 let scl = Array.make nr (-1) in (*cl[scl[i]]=rcv[i] or scl[i]=~1 if rcv[i] was trivial *)
184 let (cc,sr) = readTrace_aux scl vc 0 0 rcv fin [] 0 in
185 let _ = sat_fileclose fin in
187 with Sys_error _ -> None
189 let getChain = function
190 Chain (vcl,vcll) -> vcl
191 | _ -> failwith("getChain: not a Chain")
193 (*make backwards pass through cl, returning only the chains actually used in deriving F*)
194 let rec mk_sk cl ca ci =
195 let ch = List.fold_left
197 if (Array.get ca cci) or (isRootClauseIdx cl cci)
199 else (mk_sk cl ca cci)::ch)
200 [] (getChain (Array.get cl ci)) in
201 (Array.set ca ci true;ci::(List.concat ch))
203 let parseMinisatProof nr fname vc rcv =
204 match parseTrace nr fname vc rcv with
206 let srl = List.length sr in
207 (*stores clauses as root clauses, learnt clauses or unresolved chains *)
208 let cl = Array.make srl Blank in
209 let _ = List.fold_left (fun i c -> (Array.set cl (i-1) c;i-1)) cc sr in
210 let sk = mk_sk cl (Array.make srl false) (cc-1) in
211 Some (cl,sk,scl,srl,cc)