1 files changed, 103 insertions, 0 deletions
diff --git a/src/extraction/zchaff_checker.ml b/src/extraction/zchaff_checker.ml
new file mode 100644
index 0000000..79e87cc
--- /dev/null
+++ b/src/extraction/zchaff_checker.ml
@@ -0,0 +1,103 @@
+open SmtCertif
+open SmtForm
+open SatAtom
+open SmtTrace
+open Zchaff
+open Sat_checker
+
+
+let mkInt = ExtrNative.of_int
+let mkArray = ExtrNative.of_array
+
+
+let make_roots first last =
+  let roots = Array.make (last.id + 2) (mkArray (Array.make 1 (mkInt 0))) in
+  let mk_elem l =
+    let x = match Form.pform l with
+      | Fatom x -> x + 2
+      | _ -> assert false  in
+    mkInt (if Form.is_pos l then x lsl 1 else (x lsl 1) lxor 1) in
+  let r = ref first in
+  while !r.id < last.id do
+    let root = Array.of_list (get_val !r) in
+    let croot = Array.make (Array.length root + 1) (mkInt 0) in
+    Array.iteri (fun i l -> croot.(i) <- mk_elem l) root;
+    roots.(!r.id) <- mkArray croot;
+    r := next !r
+  done;
+  let root = Array.of_list (get_val !r) in
+  let croot = Array.make (Array.length root + 1) (mkInt 0) in
+  Array.iteri (fun i l -> croot.(i) <- mk_elem l) root;
+  roots.(!r.id) <- mkArray croot;
+
+  mkArray roots
+
+
+let to_coq to_lit (cstep,
+                   cRes, cImmFlatten,
+                   cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj,
+                   cImmBuildProj,cImmBuildDef,cImmBuildDef2,
+                   cEqTr, cEqCgr, cEqCgrP,
+                   cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim) confl =
+  let step_to_coq c =
+    match c.kind with
+      | Res res ->
+	let size = List.length res.rtail + 3 in
+	let args = Array.make size (mkInt 0) in
+	args.(0) <- mkInt (get_pos res.rc1);
+	args.(1) <- mkInt (get_pos res.rc2);
+	let l = ref res.rtail in
+	for i = 2 to size - 2 do
+	  match !l with
+	    | c::tl ->
+	      args.(i) <- mkInt (get_pos c);
+	      l := tl
+	    | _ -> assert false
+	done;
+	Sat_Checker.Res (mkInt (get_pos c), mkArray args)
+      | _ -> assert false in
+  let def_step =
+    Sat_Checker.Res (mkInt 0, mkArray [|mkInt 0|]) in
+  let r = ref confl in
+  let nc = ref 0 in
+  while not (isRoot !r.kind) do r := prev !r; incr nc done;
+  let last_root = !r in
+  let size = !nc in
+  let max = (Parray.trunc_size (Uint63.of_int 4194303)) - 1 in
+  let q,r1 = size / max, size mod max in
+
+  let trace =
+    let len = if r1 = 0 then q + 1 else q + 2 in
+    Array.make len (mkArray [|def_step|]) in
+  for j = 0 to q - 1 do
+    let tracej = Array.make (Parray.trunc_size (Uint63.of_int 4194303)) def_step in
+    for i = 0 to max - 1 do
+      r := next !r;
+      tracej.(i) <- step_to_coq !r;
+    done;
+    trace.(j) <- mkArray tracej
+  done;
+  if r1 <> 0 then begin
+    let traceq = Array.make (r1 + 1) def_step in
+    for i = 0 to r1-1 do
+      r := next !r;
+      traceq.(i) <- step_to_coq !r;
+    done;
+    trace.(q) <- mkArray traceq
+  end;
+
+  (mkArray trace, last_root)
+
+
+let checker fdimacs ftrace =
+  SmtTrace.clear ();
+  let _,first,last,reloc = import_cnf fdimacs in
+  let d = make_roots first last in
+
+  let max_id, confl = import_cnf_trace reloc ftrace first last in
+  let (tres,_) =
+    to_coq (fun _ -> assert false) certif_ops confl in
+  let certif =
+    Sat_Checker.Certif (mkInt (max_id + 1), tres, mkInt (get_pos confl)) in
+
+  Sat_Checker.checker d certif