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/verit_checker.ml | 444 +++++++++++++++++++++++++++------------- 1 file changed, 304 insertions(+), 140 deletions(-) (limited to 'src/extraction/verit_checker.ml') diff --git a/src/extraction/verit_checker.ml b/src/extraction/verit_checker.ml index 796ae54..c8b2a2f 100644 --- a/src/extraction/verit_checker.ml +++ b/src/extraction/verit_checker.ml @@ -10,25 +10,40 @@ (**************************************************************************) -open SmtMisc -open SmtCertif -open SmtCommands -open SmtForm -open SmtAtom -open SmtTrace -open Verit -open Smtlib2_ast -open Smtlib2_genConstr -(* open Smt_checker *) +open Smtcoq_plugin -module Mc = Structures.Micromega_plugin_Certificate.Mc +let error_hole = "The proof contains a hole, which is not supported by the current version of the extracted checker; in a future version, a warning will be output but the remaining of the proof will be checked" +let error_quant = "The current version of the extracted checker does not support quantifiers" -let mkInt = ExtrNative.of_int -let mkArray = ExtrNative.of_array +module Mc = CoqInterface.Micromega_plugin_Certificate.Mc +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 + Smt_checker.set acc (mkInt i) c in + (i+1,acc') + ) (0, Smt_checker.make (mkInt l) a.(l)) a) + + +(* Generate a list *) +let rec dump_list dump_elt l = + match l with + | [] -> Smt_checker.Nil + | e :: l -> Smt_checker.Cons (dump_elt e, dump_list dump_elt l) + + +(* Correspondance between the Micromega representation of objects and + the one that has been extracted *) let rec dump_nat x = match x with | Mc.O -> Smt_checker.O @@ -71,222 +86,321 @@ let dump_psatz e = dump_cone e -let rec dump_list dump_elt l = - match l with - | [] -> Smt_checker.Nil - | e :: l -> Smt_checker.Cons (dump_elt e, dump_list dump_elt l) - - let rec dump_proof_term = function - | Micromega.DoneProof -> Smt_checker.DoneProof - | Micromega.RatProof(cone,rst) -> + | CoqInterface.Micromega_plugin_Micromega.DoneProof -> Smt_checker.DoneProof + | CoqInterface.Micromega_plugin_Micromega.RatProof(cone,rst) -> Smt_checker.RatProof (dump_psatz cone, dump_proof_term rst) - | Micromega.CutProof(cone,prf) -> + | CoqInterface.Micromega_plugin_Micromega.CutProof(cone,prf) -> Smt_checker.CutProof (dump_psatz cone, dump_proof_term prf) - | Micromega.EnumProof(c1,c2,prfs) -> + | CoqInterface.Micromega_plugin_Micromega.EnumProof(c1,c2,prfs) -> Smt_checker.EnumProof (dump_psatz c1, dump_psatz c2, dump_list dump_proof_term prfs) + | CoqInterface.Micromega_plugin_Micromega.ExProof(p,prf) -> + Smt_checker.ExProof (dump_positive p, dump_proof_term prf) +(* 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 + Smt_checker.Nil + else ( + r := next !r; + let st = step_to_coq !r in + Smt_checker.Cons (st, mkTrace (s+1)) + ) in + (mkTrace 0, def_step) + + +(* From trace/smtTrace.ml *) +let to_coq to_lit + (cRes, cWeaken, cImmFlatten, + cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj, + cImmBuildProj,cImmBuildDef,cImmBuildDef2, + cEqTr, cEqCgr, cEqCgrP, + cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim, + cBBVar, cBBConst, cBBOp, cBBNot, cBBEq, cBBDiseq, + cBBNeg, cBBAdd, cBBMul, cBBUlt, cBBSlt, cBBConc, + cBBExtr, cBBZextn, cBBSextn, + cBBShl, cBBShr, + cRowEq, cRowNeq, cExt, + cHole, cForallInst) confl = -let to_coq to_lit confl = let out_f f = to_lit f in - let out_c c = mkInt (get_pos c) in + let out_c c = mkInt (SmtTrace.get_pos c) in + let out_cl cl = List.fold_right (fun f l -> Smt_checker.Cons (out_f f, l)) cl Smt_checker.Nil in let step_to_coq c = - match c.kind with + 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); + args.(i) <- mkInt (SmtTrace.get_pos c); l := tl | _ -> assert false done; - Smt_checker.Euf_Checker.Res (mkInt (get_pos c), mkArray args) + cRes (mkInt (SmtTrace.get_pos c), mkArray args) | Other other -> begin match other with - | ImmFlatten (c',f) -> Smt_checker.Euf_Checker.ImmFlatten (out_c c, out_c c', out_f f) - | True -> Smt_checker.Euf_Checker.CTrue (out_c c) - | False -> Smt_checker.Euf_Checker.CFalse (out_c c) - | BuildDef f -> Smt_checker.Euf_Checker.BuildDef (out_c c, out_f f) - | BuildDef2 f -> Smt_checker.Euf_Checker.BuildDef2 (out_c c, out_f f) - | BuildProj (f, i) -> Smt_checker.Euf_Checker.BuildProj (out_c c, out_f f, mkInt i) - | ImmBuildDef c' -> Smt_checker.Euf_Checker.ImmBuildDef (out_c c, out_c c') - | ImmBuildDef2 c' -> Smt_checker.Euf_Checker.ImmBuildDef2 (out_c c, out_c c') - | ImmBuildProj(c', i) -> Smt_checker.Euf_Checker.ImmBuildProj (out_c c, out_c c',mkInt i) + | Weaken (c',l') -> cWeaken (out_c c, out_c c', out_cl l') + | ImmFlatten (c',f) -> cImmFlatten (out_c c, out_c c', out_f f) + | True -> cTrue (out_c c) + | False -> cFalse (out_c c) + | BuildDef f -> cBuildDef (out_c c, out_f f) + | BuildDef2 f -> cBuildDef2 (out_c c, out_f f) + | BuildProj (f, i) -> cBuildProj (out_c c, out_f f, mkInt i) + | ImmBuildDef c' -> cImmBuildDef (out_c c, out_c c') + | ImmBuildDef2 c' -> cImmBuildDef2 (out_c c, out_c c') + | ImmBuildProj(c', i) -> cImmBuildProj (out_c c, out_c c', mkInt i) | EqTr (f, fl) -> let res = List.fold_right (fun f l -> Smt_checker.Cons (out_f f, l)) fl Smt_checker.Nil in - Smt_checker.Euf_Checker.EqTr (out_c c, out_f f, res) + cEqTr (out_c c, out_f f, res) | EqCgr (f, fl) -> let res = List.fold_right (fun f l -> Smt_checker.Cons ((match f with | Some f -> Smt_checker.Some (out_f f) | None -> Smt_checker.None), l)) fl Smt_checker.Nil in - Smt_checker.Euf_Checker.EqCgr (out_c c, out_f f, res) + cEqCgr (out_c c, out_f f, res) | EqCgrP (f1, f2, fl) -> let res = List.fold_right (fun f l -> Smt_checker.Cons ((match f with | Some f -> Smt_checker.Some (out_f f) | None -> Smt_checker.None), l)) fl Smt_checker.Nil in - Smt_checker.Euf_Checker.EqCgrP (out_c c, out_f f1, out_f f2, res) + cEqCgrP (out_c c, out_f f1, out_f f2, res) | LiaMicromega (cl,d) -> let cl' = List.fold_right (fun f l -> Smt_checker.Cons (out_f f, l)) cl Smt_checker.Nil in let c' = List.fold_right (fun f l -> Smt_checker.Cons (dump_proof_term f, l)) d Smt_checker.Nil in - Smt_checker.Euf_Checker.LiaMicromega (out_c c, cl', c') - | LiaDiseq l -> Smt_checker.Euf_Checker.LiaDiseq (out_c c, out_f l) + cLiaMicromega (out_c c, cl', c') + | LiaDiseq l -> cLiaDiseq (out_c c, out_f l) | SplArith (orig,res,l) -> let res' = out_f res in let l' = List.fold_right (fun f l -> Smt_checker.Cons (dump_proof_term f, l)) l Smt_checker.Nil in - Smt_checker.Euf_Checker.SplArith (out_c c, out_c orig, res', l') - | SplDistinctElim (c',f) -> Smt_checker.Euf_Checker.SplDistinctElim (out_c c, out_c c', out_f f) + cSplArith (out_c c, out_c orig, res', l') + | SplDistinctElim (c',f) -> cSplDistinctElim (out_c c, out_c c', out_f f) + | BBVar res -> cBBVar (out_c c, out_f res) + | BBConst res -> cBBConst (out_c c, out_f res) + | BBOp (c1,c2,res) -> + cBBOp (out_c c, out_c c1, out_c c2, out_f res) + | BBNot (c1,res) -> + cBBNot (out_c c, out_c c1, out_f res) + | BBNeg (c1,res) -> + cBBNeg (out_c c, out_c c1, out_f res) + | BBAdd (c1,c2,res) -> + cBBAdd (out_c c, out_c c1, out_c c2, out_f res) + | BBMul (c1,c2,res) -> + cBBMul (out_c c, out_c c1, out_c c2, out_f res) + | BBUlt (c1,c2,res) -> + cBBUlt (out_c c, out_c c1, out_c c2, out_f res) + | BBSlt (c1,c2,res) -> + cBBSlt (out_c c, out_c c1, out_c c2, out_f res) + | BBConc (c1,c2,res) -> + cBBConc (out_c c, out_c c1, out_c c2, out_f res) + | BBExtr (c1,res) -> + cBBExtr (out_c c, out_c c1, out_f res) + | BBZextn (c1,res) -> + cBBZextn (out_c c, out_c c1, out_f res) + | BBSextn (c1,res) -> + cBBSextn (out_c c, out_c c1, out_f res) + | BBShl (c1,c2,res) -> + cBBShl (out_c c, out_c c1, out_c c2, out_f res) + | BBShr (c1,c2,res) -> + cBBShr (out_c c, out_c c1, out_c c2, out_f res) + | BBEq (c1,c2,res) -> + cBBEq (out_c c, out_c c1, out_c c2, out_f res) + | BBDiseq (res) -> cBBDiseq (out_c c, out_f res) + | RowEq (res) -> cRowEq (out_c c, out_f res) + | RowNeq (cl) -> + let out_cl cl = + List.fold_right (fun f l -> Smt_checker.Cons (out_f f, l)) cl Smt_checker.Nil + in + cRowNeq (out_c c, out_cl cl) + | Ext (res) -> cExt (out_c c, out_f res) + | Hole (prem_id, concl) -> failwith error_hole + | Forall_inst (cl, concl) | Qf_lemma (cl, concl) -> failwith error_quant end | _ -> assert false in let def_step = - Smt_checker.Euf_Checker.Res (mkInt 0, mkArray [|mkInt 0|]) in + 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 btype_to_coq = function - | TZ -> Smt_checker.Typ.TZ - | Tbool -> Smt_checker.Typ.Tbool - | Tpositive -> Smt_checker.Typ.Tpositive - | Tindex i -> Smt_checker.Typ.Tindex (mkInt (SmtAtom.indexed_type_index i)) + (* Be careful, step_to_coq makes a side effect on cuts so it needs to be called first *) + let res = mkTrace step_to_coq SmtTrace.next !nc def_step r in + (res, last_root) + + +(* Map OCaml integers to the extracted version of N *) +(* From trace/coqTerms.ml *) +let rec mkNat = function + | 0 -> Smt_checker.O + | i -> Smt_checker.S (mkNat (i-1)) + +let rec mkPositive = function + | 1 -> Smt_checker.XH + | i -> + let c = + if (i mod 2) = 0 then + fun c -> Smt_checker.XO c + else + fun c -> Smt_checker.XI c + in + c (mkPositive (i / 2)) + +let mkN = function + | 0 -> Smt_checker.N0 + | i -> Smt_checker.Npos (mkPositive i) + + +(* Correspondance between the SMTCoq representation of objects and the + one that has been extracted *) +let rec btype_to_coq = function + | SmtBtype.TZ -> Smt_checker.Typ.TZ + | SmtBtype.Tbool -> Smt_checker.Typ.Tbool + | SmtBtype.Tpositive -> Smt_checker.Typ.Tpositive + | SmtBtype.TBV i -> Smt_checker.Typ.TBV (mkN i) + | SmtBtype.TFArray (k, v) -> Smt_checker.Typ.TFArray (btype_to_coq k, btype_to_coq v) + | SmtBtype.Tindex i -> Smt_checker.Typ.Tindex (mkN (SmtBtype.indexed_type_index i)) let c_to_coq = function - | CO_xH -> Smt_checker.Atom.CO_xH - | CO_Z0 -> Smt_checker.Atom.CO_Z0 + | SmtAtom.CO_xH -> Smt_checker.Atom.CO_xH + | SmtAtom.CO_Z0 -> Smt_checker.Atom.CO_Z0 + | SmtAtom.CO_BV bv -> + Smt_checker.Atom.CO_BV (dump_list (fun x -> x) bv, mkN (List.length bv)) let u_to_coq = function - | UO_xO -> Smt_checker.Atom.UO_xO - | UO_xI -> Smt_checker.Atom.UO_xI - | UO_Zpos -> Smt_checker.Atom.UO_Zpos - | UO_Zneg -> Smt_checker.Atom.UO_Zneg - | UO_Zopp -> Smt_checker.Atom.UO_Zopp + | SmtAtom.UO_xO -> Smt_checker.Atom.UO_xO + | SmtAtom.UO_xI -> Smt_checker.Atom.UO_xI + | SmtAtom.UO_Zpos -> Smt_checker.Atom.UO_Zpos + | SmtAtom.UO_Zneg -> Smt_checker.Atom.UO_Zneg + | SmtAtom.UO_Zopp -> Smt_checker.Atom.UO_Zopp + | SmtAtom.UO_BVbitOf (s, i) -> Smt_checker.Atom.UO_BVbitOf (mkN s, mkNat i) + | SmtAtom.UO_BVnot s -> Smt_checker.Atom.UO_BVnot (mkN s) + | SmtAtom.UO_BVneg s -> Smt_checker.Atom.UO_BVneg (mkN s) + | SmtAtom.UO_BVextr (s1, s2, s3) -> Smt_checker.Atom.UO_BVextr (mkN s1, mkN s2, mkN s3) + | SmtAtom.UO_BVzextn (s1, s2) -> Smt_checker.Atom.UO_BVzextn (mkN s1, mkN s2) + | SmtAtom.UO_BVsextn (s1, s2) -> Smt_checker.Atom.UO_BVsextn (mkN s1, mkN s2) let b_to_coq = function - | BO_Zplus -> Smt_checker.Atom.BO_Zplus - | BO_Zminus -> Smt_checker.Atom.BO_Zminus - | BO_Zmult -> Smt_checker.Atom.BO_Zmult - | BO_Zlt -> Smt_checker.Atom.BO_Zlt - | BO_Zle -> Smt_checker.Atom.BO_Zle - | BO_Zge -> Smt_checker.Atom.BO_Zge - | BO_Zgt -> Smt_checker.Atom.BO_Zgt - | BO_eq t -> Smt_checker.Atom.BO_eq (btype_to_coq t) + | SmtAtom.BO_Zplus -> Smt_checker.Atom.BO_Zplus + | SmtAtom.BO_Zminus -> Smt_checker.Atom.BO_Zminus + | SmtAtom.BO_Zmult -> Smt_checker.Atom.BO_Zmult + | SmtAtom.BO_Zlt -> Smt_checker.Atom.BO_Zlt + | SmtAtom.BO_Zle -> Smt_checker.Atom.BO_Zle + | SmtAtom.BO_Zge -> Smt_checker.Atom.BO_Zge + | SmtAtom.BO_Zgt -> Smt_checker.Atom.BO_Zgt + | SmtAtom.BO_eq t -> Smt_checker.Atom.BO_eq (btype_to_coq t) + | SmtAtom.BO_BVand s -> Smt_checker.Atom.BO_BVand (mkN s) + | SmtAtom.BO_BVor s -> Smt_checker.Atom.BO_BVor (mkN s) + | SmtAtom.BO_BVxor s -> Smt_checker.Atom.BO_BVxor (mkN s) + | SmtAtom.BO_BVadd s -> Smt_checker.Atom.BO_BVadd (mkN s) + | SmtAtom.BO_BVmult s -> Smt_checker.Atom.BO_BVmult (mkN s) + | SmtAtom.BO_BVult s -> Smt_checker.Atom.BO_BVult (mkN s) + | SmtAtom.BO_BVslt s -> Smt_checker.Atom.BO_BVslt (mkN s) + | SmtAtom.BO_BVconcat (s1, s2) -> Smt_checker.Atom.BO_BVconcat (mkN s1, mkN s2) + | SmtAtom.BO_BVshl s -> Smt_checker.Atom.BO_BVshl (mkN s) + | SmtAtom.BO_BVshr s -> Smt_checker.Atom.BO_BVshr (mkN s) + | SmtAtom.BO_select (k ,v) -> Smt_checker.Atom.BO_select (btype_to_coq k, btype_to_coq v) + | SmtAtom.BO_diffarray (k ,v) -> Smt_checker.Atom.BO_diffarray (btype_to_coq k, btype_to_coq v) + + +let t_to_coq = function + | SmtAtom.TO_store (k ,v) -> Smt_checker.Atom.TO_store (btype_to_coq k, btype_to_coq v) let n_to_coq = function - | NO_distinct t -> btype_to_coq t + | SmtAtom.NO_distinct t -> btype_to_coq t let i_to_coq i = mkInt (SmtAtom.indexed_op_index i) +let hatom_to_coq h = mkInt (SmtAtom.Atom.index h) + let a_to_coq a = - let to_coq h = mkInt (Atom.index h) in match a with - | Acop op -> Smt_checker.Atom.Acop (c_to_coq op) - | Auop (op,h) -> Smt_checker.Atom.Auop (u_to_coq op, to_coq h) - | Abop (op,h1,h2) -> - Smt_checker.Atom.Abop (b_to_coq op, to_coq h1, to_coq h2) - | Anop (op,ha) -> + | SmtAtom.Acop op -> Smt_checker.Atom.Acop (c_to_coq op) + | SmtAtom.Auop (op,h) -> Smt_checker.Atom.Auop (u_to_coq op, hatom_to_coq h) + | SmtAtom.Abop (op,h1,h2) -> + Smt_checker.Atom.Abop (b_to_coq op, hatom_to_coq h1, hatom_to_coq h2) + | SmtAtom.Atop (op,h1,h2,h3) -> + Smt_checker.Atom.Atop (t_to_coq op, hatom_to_coq h1, hatom_to_coq h2, hatom_to_coq h3) + | SmtAtom.Anop (op,ha) -> let cop = n_to_coq op in - let cargs = Array.fold_right (fun h l -> Smt_checker.Cons (to_coq h, l)) ha Smt_checker.Nil in + let cargs = Array.fold_right (fun h l -> Smt_checker.Cons (hatom_to_coq h, l)) ha Smt_checker.Nil in Smt_checker.Atom.Anop (cop, cargs) - | Aapp (op,args) -> + | SmtAtom.Aapp (op,args) -> let cop = i_to_coq op in - let cargs = Array.fold_right (fun h l -> Smt_checker.Cons (to_coq h, l)) args Smt_checker.Nil in + let cargs = Array.fold_right (fun h l -> Smt_checker.Cons (hatom_to_coq h, l)) args Smt_checker.Nil in Smt_checker.Atom.Aapp (cop, cargs) let atom_interp_tbl reify = - let t = Atom.to_array reify (Smt_checker.Atom.Acop Smt_checker.Atom.CO_xH) a_to_coq in + let t = SmtAtom.Atom.to_array reify (Smt_checker.Atom.Acop Smt_checker.Atom.CO_xH) a_to_coq in mkArray t -let form_to_coq hf = mkInt (Form.to_lit hf) +let form_to_coq hf = mkInt (SmtAtom.Form.to_lit hf) let args_to_coq args = let cargs = Array.make (Array.length args + 1) (mkInt 0) in Array.iteri (fun i hf -> cargs.(i) <- form_to_coq hf) args; mkArray cargs -let pf_to_coq = function - | Fatom a -> Smt_checker.Form.Fatom (mkInt (Atom.index a)) - | Fapp(op,args) -> - match op with - | Ftrue -> Smt_checker.Form.Ftrue - | Ffalse -> Smt_checker.Form.Ffalse - | Fand -> Smt_checker.Form.Fand (args_to_coq args) - | For -> Smt_checker.Form.For (args_to_coq args) - | Fimp -> Smt_checker.Form.Fimp (args_to_coq args) - | Fxor -> if Array.length args = 2 then Smt_checker.Form.Fxor (form_to_coq args.(0), form_to_coq args.(1)) else assert false - | Fiff -> if Array.length args = 2 then Smt_checker.Form.Fiff (form_to_coq args.(0), form_to_coq args.(1)) else assert false - | Fite -> if Array.length args = 3 then Smt_checker.Form.Fite (form_to_coq args.(0), form_to_coq args.(1), form_to_coq args.(2)) else assert false - | Fnot2 i -> Smt_checker.Form.Fnot2 (mkInt i, form_to_coq args.(0)) +let pf_to_coq pf = + match pf with + | SmtForm.Fatom a -> Smt_checker.Form.Fatom (hatom_to_coq a) + | SmtForm.Fapp(op,args) -> + (match op with + | SmtForm.Ftrue -> Smt_checker.Form.Ftrue + | SmtForm.Ffalse -> Smt_checker.Form.Ffalse + | SmtForm.Fand -> Smt_checker.Form.Fand (args_to_coq args) + | SmtForm.For -> Smt_checker.Form.For (args_to_coq args) + | SmtForm.Fxor -> if Array.length args = 2 then Smt_checker.Form.Fxor (form_to_coq args.(0), form_to_coq args.(1)) else assert false + | SmtForm.Fimp -> Smt_checker.Form.Fimp (args_to_coq args) + | SmtForm.Fiff -> if Array.length args = 2 then Smt_checker.Form.Fiff (form_to_coq args.(0), form_to_coq args.(1)) else assert false + | SmtForm.Fite -> if Array.length args = 3 then Smt_checker.Form.Fite (form_to_coq args.(0), form_to_coq args.(1), form_to_coq args.(2)) else assert false + | SmtForm.Fnot2 i -> Smt_checker.Form.Fnot2 (mkInt i, form_to_coq args.(0)) + | SmtForm.Fforall _ -> failwith error_quant + ) + | SmtForm.FbbT (a, args) -> Smt_checker.Form.FbbT (hatom_to_coq a, dump_list form_to_coq args) let form_interp_tbl reify = - let (_,t) = Form.to_array reify Smt_checker.Form.Ftrue pf_to_coq in + let (_,t) = SmtAtom.Form.to_array reify Smt_checker.Form.Ftrue pf_to_coq in mkArray t (* Importing from SMT-LIB v.2 without generating section variables *) - +(* From smtlib2/smtlib2_genConstr.ml *) let count_btype = ref 0 let count_op = ref 0 let declare_sort sym = - let s = string_of_symbol sym in - let res = Tindex (dummy_indexed_type !count_btype) in + let s = Smtlib2_genConstr.string_of_symbol sym in + let res = SmtBtype.Tindex (SmtBtype.dummy_indexed_type !count_btype) in incr count_btype; - VeritSyntax.add_btype s res; + SmtMaps.add_btype s res; res let declare_fun sym arg cod = - let s = string_of_symbol sym in - let tyl = List.map sort_of_sort arg in - let ty = sort_of_sort cod in - let op = dummy_indexed_op !count_op (Array.of_list (List.map fst tyl)) (fst ty) in + let s = Smtlib2_genConstr.string_of_symbol sym in + let tyl = List.map Smtlib2_genConstr.sort_of_sort arg in + let ty = Smtlib2_genConstr.sort_of_sort cod in + let op = SmtAtom.dummy_indexed_op (SmtAtom.Index !count_op) (Array.of_list tyl) ty in incr count_op; - VeritSyntax.add_fun s op; + SmtMaps.add_fun s op; op let declare_commands ra rf acc = function - | CDeclareSort (_,sym,_) -> let _ = declare_sort sym in acc - | CDeclareFun (_,sym, (_, arg), cod) -> let _ = declare_fun sym arg cod in acc - | CAssert (_, t) -> (make_root ra rf t)::acc + | Smtlib2_ast.CDeclareSort (_,sym,_) -> let _ = declare_sort sym in acc + | Smtlib2_ast.CDeclareFun (_,sym, (_, arg), cod) -> let _ = declare_fun sym arg cod in acc + | Smtlib2_ast.CAssert (_, t) -> (Smtlib2_genConstr.make_root ra rf t)::acc | _ -> acc @@ -309,29 +423,79 @@ let this_clear_all () = count_op := 0 +let certif_ops = + ((fun (a, b) -> Smt_checker.Checker_Ext.Res (a, b)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.Weaken (a, b, c)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.ImmFlatten (a, b, c)), + (fun a -> Smt_checker.Checker_Ext.CTrue a), + (fun a -> Smt_checker.Checker_Ext.CFalse a), + (fun (a, b) -> Smt_checker.Checker_Ext.BuildDef (a, b)), + (fun (a, b) -> Smt_checker.Checker_Ext.BuildDef2 (a, b)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.BuildProj (a, b, c)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.ImmBuildProj (a, b, c)), + (fun (a, b) -> Smt_checker.Checker_Ext.ImmBuildDef (a, b)), + (fun (a, b) -> Smt_checker.Checker_Ext.ImmBuildDef2 (a, b)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.EqTr (a, b, c)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.EqCgr (a, b, c)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.EqCgrP (a, b, c, d)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.LiaMicromega (a, b, c)), + (fun (a, b) -> Smt_checker.Checker_Ext.LiaDiseq (a, b)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.SplArith (a, b, c, d)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.SplDistinctElim (a, b, c)), + (fun (a, b) -> Smt_checker.Checker_Ext.BBVar (a, b)), + (fun (a, b) -> Smt_checker.Checker_Ext.BBConst (a, b)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.BBOp (a, b, c, d)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.BBNot (a, b, c)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.BBEq (a, b, c, d)), + (fun (a, b) -> Smt_checker.Checker_Ext.BBDiseq (a, b)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.BBNeg (a, b, c)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.BBAdd (a, b, c, d)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.BBMul (a, b, c, d)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.BBUlt (a, b, c, d)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.BBSlt (a, b, c, d)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.BBConcat (a, b, c, d)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.BBExtract (a, b, c)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.BBZextend (a, b, c)), + (fun (a, b, c) -> Smt_checker.Checker_Ext.BBSextend (a, b, c)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.BBShl (a, b, c, d)), + (fun (a, b, c, d) -> Smt_checker.Checker_Ext.BBShr (a, b, c, d)), + (fun (a, b) -> Smt_checker.Checker_Ext.RowEq (a, b)), + (fun (a, b) -> Smt_checker.Checker_Ext.RowNeq (a, b)), + (fun (a, b) -> Smt_checker.Checker_Ext.Ext (a, b)), + (fun () -> failwith error_hole), + (fun () -> failwith error_quant)) + + +(* From verit/verit.ml and trace/smtCommands.ml *) let checker fsmt fproof = this_clear_all (); let ra = VeritSyntax.ra in let rf = VeritSyntax.rf in + let ra_quant = VeritSyntax.ra_quant in + let rf_quant = VeritSyntax.rf_quant in let roots = import_smtlib2 ra rf fsmt in - let (max_id, confl) = import_trace fproof None in - let (tres,last_root) = to_coq (fun i -> mkInt (SmtAtom.Form.to_lit i)) confl in + let (max_id, confl) = Verit.import_trace ra_quant rf_quant fproof None [] in + + let (tres,last_root) = to_coq (fun i -> mkInt (SmtAtom.Form.to_lit i)) certif_ops confl in let certif = - Smt_checker.Euf_Checker.Certif (mkInt (max_id + 1), tres, mkInt (get_pos confl)) in - let used_roots = compute_roots roots last_root in + Smt_checker.Checker_Ext.Certif (mkInt (max_id + 1), tres, mkInt (SmtTrace.get_pos confl)) + in + let used_roots = SmtCommands.compute_roots roots last_root in let used_rootsCstr = let l = List.length used_roots in let res = Array.make (l + 1) (mkInt 0) in let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - Smt_checker.Some (mkArray res) in + Smt_checker.Some (mkArray res) + in let rootsCstr = let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (SmtAtom.Form.to_lit j); incr i) roots; - mkArray res in + mkArray res + in let t_atom = atom_interp_tbl ra in let t_form = form_interp_tbl rf in - Smt_checker.Euf_Checker.checker_ext t_atom t_form rootsCstr used_rootsCstr certif + Smt_checker.Checker_Ext.checker_ext t_atom t_form rootsCstr used_rootsCstr certif -- cgit