1
2structure minisatParse =
3struct
4
5local
6
7open Globals Parse HolKernel boolSyntax boolTheory (* HOL4 term parsers etc *)
8open Array (* ML *)
9open satCommonTools minisatResolve SatSolvers
10
11
12in
13
14fun sat_fileopen s = BinIO.openIn s
15
16fun sat_fileclose is = BinIO.closeIn is
17
18local open Word in
19
20(*read in the next byte*)
21fun sat_getChar is =
22    let val v = BinIO.input1 is
23    in if isSome v
24       then Word8.toLargeWord(valOf v)
25       else raise Domain end
26
27infix orb
28infix andb
29infix <<
30infix >>
31
32(* adapted from Minisat-p_v1.14::File::getUInt*)
33(* reads the next int, which may be encoded in 8, 16, 32 or 64 bits*)
34(* FIXME: Currently this is untested and will likely crash on 64 bit archs*)
35fun sat_getint is =
36 let val  byte0 = sat_getChar is
37 in  if ((byte0 andb (0wx80))=(0wx0)) (* 8 *)
38        then toInt(byte0)
39        else
40        case toInt((byte0 andb (0wx60)) >> (Word.fromInt 5)) of
41         0 => let val byte1 = sat_getChar is
42              in toInt(((byte0 andb (0wx1F)) << (Word.fromInt 8)) orb byte1)
43              end (* 16 *)
44        | 1 => let val byte1 = sat_getChar is
45                   val byte2 = sat_getChar is
46               in  toInt((((byte0 andb (0wx1F)) << (Word.fromInt 16))
47                            orb (byte1 << (Word.fromInt 8))) orb byte2)
48               end
49        | 2 => let val byte1 = sat_getChar is
50                   val byte2 = sat_getChar is
51                   val byte3 = sat_getChar is
52               in toInt(((((byte0 andb (0wx1F)) << (Word.fromInt 24))
53                            orb (byte1 << (Word.fromInt 16)))
54                           orb (byte2 << (Word.fromInt 8))) orb byte3)
55               end
56        (* default case is only place where int64 is needed since we
57           do a << 32*)
58        | _ => let val byte0 = sat_getChar is
59                   val byte1 = sat_getChar is
60                   val byte2 = sat_getChar is
61                   val byte3 = sat_getChar is
62                   val byte4 = sat_getChar is
63                   val byte5 = sat_getChar is
64                   val byte6 = sat_getChar is
65                   val byte7 = sat_getChar is
66               in toInt((((byte0 << (Word.fromInt 24))
67                              orb (byte1 << (Word.fromInt 16))
68                              orb (byte2 << (Word.fromInt 8))
69                              orb byte3) << (Word.fromInt 32))
70                            orb ((byte4 << (Word.fromInt 24))
71                                     orb (byte5 << (Word.fromInt 16))
72                                     orb (byte6 << (Word.fromInt 8)) orb byte7))
73            end
74        end
75end
76
77(* bitwise rightshift by 1 bit*)
78fun rshift w = Word.toInt((op Word.>>) (Word.fromInt w,Word.fromInt 1))
79
80(* parse resolution chain *)
81fun getIntBranch fin id h =
82    let
83        fun loop acc len =
84            let val v = (sat_getint fin)-1
85              (*-1 is purely a decoding step (i.e. not translating b/w HolSat
86                and ms)*)
87            in if v=(~1) then ((v,h)::(rev acc),len+1)
88               else let val ci = id-(sat_getint fin)
89                    in loop ((v,ci)::acc) (len+1) end
90            end
91        val res = loop [] 0
92     in res  end
93
94(* parse and resolve a chain : assumes all dependencies already calculated *)
95(* the var component of the first pair is a dummy value ~1 *)
96fun addBranch lfn cl sva fin tc id =
97    let val (br,brl) = getIntBranch fin id (id-(rshift tc))
98        val res = if brl=1 (*(tl br = []) *)
99                  then false (* delete *)
100                  else
101                      ((*print "\nB ";print( (int_to_string id)^": ");
102                       List.app (fn (i,j) =>
103                                    print (int_to_string i ^ "," ^
104                                           int_to_string j ^" ")) br; *)
105                      resolveChain lfn sva cl (br,brl) id; true) (* resolve *)
106    in res end
107
108(* Parse a root clause. Final result is int list of literals *)
109fun getIntRoot fin idx =
110    let
111        fun loop idx' acc =
112            let val v = sat_getint fin
113            in if v=0 then idx::(rev acc) else loop (idx'+v) ((idx'+v)::acc) end
114        val res = loop idx []
115     in res  end
116
117(* Parse a root clause and add it to the sr stack
118   This advances the file read pointer
119        but we pick up the actual clause term from the vector
120        of clauses we already have, using the orc value.
121   This is because minisat-p removes duplicate literals and sorts the
122   literals so I can't efficiently find the corresponding clause term in HOL
123
124   So this is faster (time and space) than building the clause term from the
125   proof log.
126*)
127fun addClause lfn cl  sva vc clauseth fin lit1 id =
128    let val orc = (rshift lit1)-1
129          (*-1 because right now orc's in proof log start at 1*)
130        val l = getIntRoot fin (sat_getint fin)
131          (*val _ = (print "\nR ";
132                     print(int_to_string orc ^ "~" ^ int_to_string id)^ ": ");
133                     List.app (fn i => print (int_to_string i ^ " ")) l) *)
134    in case l of
135           []  => failwith
136                    ("addClause:Failed parsing clause "^Int.toString id^"\n")
137         | _ => prepareRootClause lfn orc clauseth cl id
138    end
139
140(* SML equivalent of  C-style eval of v&1=0 *)
141fun isRoot v =
142    Word.compare(Word.andb(Word.fromInt v,Word.fromInt 1),(Word.fromInt 0)) =
143    EQUAL
144
145fun readTrace lfn cl sva vc clauseth fin id =
146    if BinIO.endOfStream fin then id
147    else
148      let val tmp = sat_getint fin
149      in
150        if isRoot tmp then
151          let val _ = addClause lfn cl sva vc clauseth fin tmp id
152          in readTrace lfn cl  sva vc clauseth fin (id+1) end
153        else
154          let val isch = addBranch lfn cl sva fin tmp id
155          in if isch then readTrace lfn cl sva vc clauseth fin (id+1) (* chain*)
156             else readTrace lfn cl sva vc clauseth fin id
157          end (* deletion *)
158        end
159
160exception Trivial
161
162(*build the clause/chain list *)
163fun parseTrace cl sva nr fname solver vc clauseth lfn proof =
164    let
165        val fin = sat_fileopen (if isSome proof then valOf proof
166                                else fname^"."^(getSolverName solver)^".proof")
167        val id = readTrace lfn cl sva vc clauseth fin 0
168        val _ = sat_fileclose fin
169     in SOME id end
170handle Io _ => NONE
171
172(*
173nr: number of root clauses
174fname: filename of proof log
175vc: number of variables (includes variables added by def CNF conversion)
176clauseth: root clause vector. clauseth[i] is i'th root clause from original
177          problem
178*)
179fun replayProof sva nr fname solver vc clauseth lfn proof =
180    let val _ = (minisatResolve.counter:=0)
181        val cl = Dynarray.array((Array.length clauseth) * 2,TRUTH)
182    in case parseTrace cl sva nr fname solver vc clauseth lfn proof of
183           SOME id => SOME (Dynarray.sub(cl,id-1))
184         | NONE => NONE
185    end
186
187end
188end
189