From de9c46d059ddd38c0c1922d91cb788c3d550d488 Mon Sep 17 00:00:00 2001 From: ckeller Date: Sat, 30 Jul 2022 16:42:50 +0200 Subject: Extraction for Coq 8.13 (#109) Extraction is back! Some new features: * Not only an executable is generated, but the ZChaff and veriT checkers are available through a package called Smtcoq_extr * The command-line arguments are better handled * The veriT checker is now the default --- src/extraction/zchaff_checker.ml | 127 ++++++++++++++++++++------------------- 1 file changed, 64 insertions(+), 63 deletions(-) (limited to 'src/extraction/zchaff_checker.ml') diff --git a/src/extraction/zchaff_checker.ml b/src/extraction/zchaff_checker.ml index a53526b..77e6ca1 100644 --- a/src/extraction/zchaff_checker.ml +++ b/src/extraction/zchaff_checker.ml @@ -10,34 +10,41 @@ (**************************************************************************) -open SmtCertif -open SmtForm -open SatAtom -open SmtTrace -open Zchaff -open Sat_checker +open Smtcoq_plugin -let mkInt = ExtrNative.of_int -let mkArray = ExtrNative.of_array +let mkInt = Uint63.of_int +(* From trace/coqTerms.ml *) +let mkArray a = + let l = (Array.length a) - 1 in + snd (Array.fold_left (fun (i,acc) c -> + let acc' = + if i = l then + acc + else + Sat_checker.set acc (mkInt i) c in + (i+1,acc') + ) (0, Sat_checker.make (mkInt l) a.(l)) a) + +(* From zchaff/zchaff.ml *) let make_roots first last = - let roots = Array.make (last.id + 2) (mkArray (Array.make 1 (mkInt 0))) in + let roots = Array.make (last.SmtCertif.id + 2) (mkArray (Array.make 1 (mkInt 0))) in let mk_elem l = - let x = match Form.pform l with + let x = match SatAtom.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 + mkInt (if SatAtom.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 + while !r.SmtCertif.id < last.SmtCertif.id do + let root = Array.of_list (SmtTrace.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 + r := SmtTrace.next !r done; - let root = Array.of_list (get_val !r) in + let root = Array.of_list (SmtTrace.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; @@ -45,71 +52,65 @@ let make_roots first last = 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, cHole) confl = +(* From trace/coqInterface.ml *) +(* WARNING: side effect on r! *) +let mkTrace step_to_coq next size def_step r = + let rec mkTrace s = + if s = size then + Sat_checker.Nil + else ( + r := next !r; + let st = step_to_coq !r in + Sat_checker.Cons (st, mkTrace (s+1)) + ) in + (mkTrace 0, def_step) + + +(* From trace/smtTrace.ml *) +let to_coq cRes confl = + let step_to_coq c = - match c.kind with - | Res res -> + match c.SmtCertif.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); + args.(0) <- mkInt (SmtTrace.get_pos res.rc1); + args.(1) <- mkInt (SmtTrace.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); + | c::tl -> + args.(i) <- mkInt (SmtTrace.get_pos c); l := tl - | _ -> assert false + | _ -> 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 + cRes (mkInt (SmtTrace.get_pos c), mkArray args) + | Other other -> assert false + | _ -> assert false + in + + let def_step = cRes (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; + while not (SmtTrace.isRoot !r.SmtCertif.kind) do r := SmtTrace.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 res = + mkTrace step_to_coq SmtTrace.next !nc def_step r + in + (res, last_root) let checker fdimacs ftrace = SmtTrace.clear (); - let _,first,last,reloc = import_cnf fdimacs in + let _,first,last,reloc = Zchaff.import_cnf fdimacs in let d = make_roots first last in - let max_id, confl = import_cnf_trace reloc ftrace first last in + let max_id, confl = Zchaff.import_cnf_trace reloc ftrace first last in let (tres,_) = - to_coq (fun _ -> assert false) certif_ops confl in + to_coq (fun (pos, args) -> Sat_checker.Sat_Checker.Res (pos, args)) confl + in let certif = - Sat_Checker.Certif (mkInt (max_id + 1), tres, mkInt (get_pos confl)) in + Sat_checker.Sat_Checker.Certif (mkInt (max_id + 1), tres, mkInt (SmtTrace.get_pos confl)) + in - Sat_Checker.checker d certif + Sat_checker.Sat_Checker.checker d certif -- cgit