Minisat/minisat_parse.ml

   1 (*open satCommonTools dimacsTools;; *)
   2
   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  *)
   7
   8 type rootc =
   9     Rthm of thm * Litset.t * term * thm
  10   | Ll of term * Litset.t
  11
  12 type clause =
  13     Blank
  14   | Chain of (int * int) list * int (* var, cl index list and the length of that list *)
  15   | Root of rootc
  16   | Learnt of thm * Litset.t (* clause  thm, lits as nums set *)
  17
  18 let sat_fileopen s = open_in_bin s
  19
  20 let sat_fileclose is = close_in is
  21
  22 let sat_getChar is = Int32.of_int(input_byte is)
  23
  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 *)
  28 let sat_getint is =
  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)
  36   else
  37     match Int32.to_int((byte0 land (0x60l)) lsr 5) with
  38       0 ->
  39         let byte1 = sat_getChar is in
  40         Int32.to_int(((byte0 land (0x1Fl)) lsl 8) lor byte1) (* 16 *)
  41     | 1 ->
  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)
  45     | 2 ->
  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*)
  52     | _ ->
  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))
  63
  64 let isRootClauseIdx cl ci =
  65   match Array.get cl ci with
  66     Root _ -> true
  67   | _      -> false
  68
  69 (* p is a literal *)
  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) *)
  72 let literalToInt2 p =
  73   let (sign,vnum) = literalToInt p in
  74   2*(vnum-1)+(if sign then 1 else 0)
  75
  76 let literalToInt3 p =
  77   let (sign,vnum) = literalToInt p in
  78   (sign,vnum-1)
  79
  80 (* parse a root clause *)
  81 let getIntRoot fin idx =
  82   let rec loop idx' acc =
  83     let v = sat_getint fin in
  84     if v=0
  85     then idx::(List.rev acc)
  86     else loop (idx'+v) ((idx'+v)::acc) in
  87   let res = loop idx [] in
  88   res
  89
  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)
  92
  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)
  98
  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
 103   let lns =
 104     List.fold_left (fun s e -> Litset.add e s)
 105       Litset.empty lnl in
 106   let slnl = (* FIXME: speed this up*)
 107     List.sort Pervasives.compare
 108       (setify
 109          (List.map (fun (isn,vi) ->
 110            if isn
 111            then 2*vi+1
 112            else 2*vi) lnl)) in
 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
 116
 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
 125     let res =
 126       match l with
 127         []  -> failwith ("addClause:Failed parsing clause "^(string_of_int (cc))^"\n")
 128       | _   ->
 129           let (lr,(t,lns)) =
 130             getNextRootClause scl vc cc lr l rcv in
 131           (cc+1,lr+1,(Root (Ll (t,lns)))::sr) in
 132     res
 133
 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
 140     if v=(-1)
 141     then ((v,h)::(List.rev acc),len+1)
 142     else
 143       let ci = id-(sat_getint fin) in
 144       loop ((v,ci)::acc) (len+1) in
 145   let res = loop [] 0 in
 146   res
 147
 148 let addBranch fin sr cc id tc =
 149     let (br,brl) =
 150       getIntBranch fin id (id-(tc lsr 1)) in
 151     let res =
 152       if brl=1 (*(tl br = []) *)
 153       then (cc,false,sr) (* delete *)
 154       else (cc+1,true,(Chain (br,brl))::sr) (* resolve *) in
 155     res
 156
 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) *)
 162
 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
 166   if (tmp land 1)=0
 167   then
 168     let (cc,lr,sr) =
 169       addClause scl vc cc lr rcv fin sr tmp in
 170     readTrace_aux scl vc cc lr rcv fin sr (id+1)
 171   else
 172     let (cc,isch,sr') =
 173       addBranch fin sr cc id tmp in
 174     if isch
 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 *)
 177 ;;
 178
 179 (*fill in the root clause and chain array*)
 180 let parseTrace nr fname vc rcv =
 181     try
 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
 186       Some (cc,sr,scl)
 187     with Sys_error _  -> None
 188
 189 let getChain = function
 190     Chain (vcl,vcll) -> vcl
 191   |  _ ->  failwith("getChain: not a Chain")
 192
 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
 196         (fun ch (v,cci) ->
 197           if (Array.get ca cci) or (isRootClauseIdx cl cci)
 198           then ch
 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))
 202
 203 let parseMinisatProof nr fname vc rcv =
 204     match parseTrace nr fname vc rcv with
 205       Some (cc,sr,scl) ->
 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)
 212     | None -> None