1 files changed, 161 insertions, 0 deletions
diff --git a/src/zchaff/zchaffParser.ml b/src/zchaff/zchaffParser.ml
new file mode 100644
index 0000000..c5bcb09
--- /dev/null
+++ b/src/zchaff/zchaffParser.ml
@@ -0,0 +1,161 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+open SatParser
+open SmtForm
+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
+