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