diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-02 17:31:47 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-02 17:31:47 +0100 |
commit | 37f297b89f04155124237acf3d7f220a9dcd1544 (patch) | |
tree | b5d89abd09f0093d070efdf7658b24d932d70986 | |
parent | 607c758e0220d8ba91eaf0e9e96b5ea71c5c6fd2 (diff) | |
download | smtcoq-37f297b89f04155124237acf3d7f220a9dcd1544.tar.gz smtcoq-37f297b89f04155124237acf3d7f220a9dcd1544.zip |
Code refactoring
-rw-r--r-- | src/Make | 7 | ||||
-rw-r--r-- | src/Makefile | 7 | ||||
-rw-r--r-- | src/smtlib2/smtlib2_genConstr.ml | 13 | ||||
-rw-r--r-- | src/trace/smtAtom.ml | 13 | ||||
-rw-r--r-- | src/trace/smtAtom.mli | 4 | ||||
-rw-r--r-- | src/trace/smtCommands.ml | 256 | ||||
-rw-r--r-- | src/verit/verit.ml | 364 |
7 files changed, 304 insertions, 360 deletions
@@ -36,7 +36,7 @@ -custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli" -custom "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "ml" --custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "trace/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)" +-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "trace/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)" -custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)" CMXA = trace/smtcoq.cmxa @@ -52,16 +52,17 @@ trace/smtAtom.ml trace/smtAtom.mli trace/smtCertif.ml trace/smtCnf.ml +trace/smtCommands.ml trace/smtForm.ml trace/smtForm.mli trace/smtMisc.ml trace/smt_tactic.ml4 trace/smtTrace.ml +smtlib2/smtlib2_parse.ml +smtlib2/smtlib2_lex.ml smtlib2/smtlib2_ast.ml smtlib2/smtlib2_genConstr.ml -smtlib2/smtlib2_lex.ml -smtlib2/smtlib2_parse.ml smtlib2/smtlib2_util.ml verit/veritParser.ml diff --git a/src/Makefile b/src/Makefile index d81ee84..5a796a0 100644 --- a/src/Makefile +++ b/src/Makefile @@ -164,13 +164,14 @@ MLFILES:=lia/lia.ml\ verit/veritLexer.ml\ verit/veritParser.ml\ smtlib2/smtlib2_util.ml\ - smtlib2/smtlib2_parse.ml\ - smtlib2/smtlib2_lex.ml\ smtlib2/smtlib2_genConstr.ml\ smtlib2/smtlib2_ast.ml\ + smtlib2/smtlib2_lex.ml\ + smtlib2/smtlib2_parse.ml\ trace/smtTrace.ml\ trace/smtMisc.ml\ trace/smtForm.ml\ + trace/smtCommands.ml\ trace/smtCnf.ml\ trace/smtCertif.ml\ trace/smtAtom.ml\ @@ -252,7 +253,7 @@ beautify: $(VFILES:=.beautified) $(CMXS): $(CMXA) $(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^ -$(CMXA): trace/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx +$(CMXA): trace/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx trace/smt_tactic.cmx $(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^ ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index f11d650..533f139 100644 --- a/src/smtlib2/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -224,3 +224,16 @@ let declare_commands rt ro ra rf acc = function let _ = declare_fun rt ro sym arg cod in acc | CAssert (_, t) -> (make_root ra rf t)::acc | _ -> acc + + +(* Import function *) + +let import_smtlib2 rt ro ra rf filename = + let chan = open_in filename in + let lexbuf = Lexing.from_channel chan in + let commands = Smtlib2_parse.main Smtlib2_lex.token lexbuf in + close_in chan; + match commands with + | None -> [] + | Some (Smtlib2_ast.Commands (_,(_,res))) -> + List.rev (List.fold_left (declare_commands rt ro ra rf) [] res) diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 392ef2e..80c012f 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -746,3 +746,16 @@ module Atom = module Form = SmtForm.Make(Atom) module Trace = SmtTrace.MakeOpt(Form) + + +(* Interpretation tables *) + +let mk_ftype cod dom = + let typeb = Lazy.force ctype in + let typea = mklApp clist [|typeb|] in + let a = Array.fold_right (fun bt acc -> mklApp ccons [|typeb; Btype.to_coq bt; acc|]) cod (mklApp cnil [|typeb|]) in + let b = Btype.to_coq dom in + mklApp cpair [|typea;typeb;a;b|] + +let make_t_i rt = Btype.interp_tbl rt +let make_t_func ro t_i = Op.interp_tbl (mklApp ctval [|t_i|]) (fun cod dom value -> mklApp cTval [|t_i; mk_ftype cod dom; value|]) ro diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index 8eadb49..9b8a613 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -173,3 +173,7 @@ module Form : SmtForm.FORM with type hatom = hatom module Trace : sig val share_prefix : Form.t SmtCertif.clause -> int -> unit end + + +val make_t_i : Btype.reify_tbl -> Term.constr +val make_t_func : Op.reify_tbl -> Term.constr -> Term.constr diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml new file mode 100644 index 0000000..1941065 --- /dev/null +++ b/src/trace/smtCommands.ml @@ -0,0 +1,256 @@ +open Entries +open Declare +open Decl_kinds + +open SmtMisc +open CoqTerms +open SmtForm +open SmtAtom +open SmtTrace +open SmtCertif + + +let euf_checker_modules = [ ["SMTCoq";"Trace";"Euf_Checker"] ] +let certif_ops = CoqTerms.make_certif_ops euf_checker_modules +let cCertif = gen_constant euf_checker_modules "Certif" +let ccertif = gen_constant euf_checker_modules "certif" +let cchecker = gen_constant euf_checker_modules "checker" +let cchecker_correct = gen_constant euf_checker_modules "checker_correct" +let cchecker_b_correct = + gen_constant euf_checker_modules "checker_b_correct" +let cchecker_b = gen_constant euf_checker_modules "checker_b" +let cchecker_eq_correct = + gen_constant euf_checker_modules "checker_eq_correct" +let cchecker_eq = gen_constant euf_checker_modules "checker_eq" + + +(* Given an SMT-LIB2 file and a certif, build the corresponding objects *) + +let compute_roots roots last_root = + let r = ref last_root in + while (has_prev !r) do + r := prev !r + done; + + let rec find_root i root = function + | [] -> assert false + | t::q -> if Form.equal t root then (i,q) else find_root (i+1) root q in + + let rec used_roots acc i roots r = + if isRoot r.kind then + match r.value with + | Some [root] -> + let (j,roots') = find_root i root roots in + used_roots (j::acc) (j+1) roots' (next r) + | _ -> assert false + else + acc in + + used_roots [] 0 roots !r + + +let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, roots, max_id, confl) = + let (tres, last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in + let certif = + mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in + let ce4 = Structures.mkConst certif in + let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in + let used_roots = compute_roots roots last_root in + let roots = + let res = Array.make (List.length roots + 1) (mkInt 0) in + let i = ref 0 in + List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; + Structures.mkArray (Lazy.force cint, res) in + let used_roots = + 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; + mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in + let ce3 = Structures.mkConst roots in + let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in + let ce3' = Structures.mkConst used_roots in + let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in + let t_i' = make_t_i rt in + let t_func' = make_t_func ro t_i' in + let ce5 = Structures.mkConst t_i' in + let _ = declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition) in + let ce6 = Structures.mkConst t_func' in + let _ = declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition) in + let ce1 = Structures.mkConst (Atom.interp_tbl ra) in + let _ = declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition) in + let ce2 = Structures.mkConst (snd (Form.interp_tbl rf)) in + let _ = declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition) in + () + + +(* Given an SMT-LIB2 file and a certif, build the corresponding theorem *) + +let interp_roots roots = + let interp = Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17) in + match roots with + | [] -> Lazy.force ctrue + | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots + +let build_certif (rt, ro, ra, rf, roots, max_id, confl) = + let (tres,last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in + let certif = + mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in + let used_roots = 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; + mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, 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 (Form.to_lit j); incr i) roots; + Structures.mkArray (Lazy.force cint, res) in + + let t_atom = Atom.interp_tbl ra in + let t_form = snd (Form.interp_tbl rf) in + let t_i = make_t_i rt in + let t_func = make_t_func ro t_i in + + (rootsCstr, used_rootsCstr, certif, t_atom, t_form, t_i, t_func) + +let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) = + let (rootsCstr, used_rootsCstr, certif, t_atom, t_form, t_i, t_func) = build_certif p in + + let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots roots|]|] in + let theorem_proof = + Term.mkLetIn (mkName "used_roots", used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], (*7*) + Term.mkLetIn (mkName "t_atom", t_atom, mklApp carray [|Lazy.force catom|], (*6*) + Term.mkLetIn (mkName "t_form", t_form, mklApp carray [|Lazy.force cform|], (*5*) + Term.mkLetIn (mkName "d", rootsCstr, mklApp carray [|Lazy.force cint|], (*4*) + Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, (*3*) + Term.mkLetIn (mkName "t_i", t_i, mklApp carray [|Lazy.force ctyp_eqb|], (*2*) + Term.mkLetIn (mkName "t_func", t_func, mklApp carray [|mklApp ctval [|t_i|]|], (*1*) + mklApp cchecker_correct + [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3; + vm_cast_true + (mklApp cchecker [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3|])|]))))))) in + let ce = Structures.mkConst theorem_proof in + let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in + () + + +(* Given an SMT-LIB2 file and a certif, call the checker *) + +let checker ((rt, ro, ra, rf, roots, max_id, confl) as p) = + let (rootsCstr, used_rootsCstr, certif, t_atom, t_form, t_i, t_func) = build_certif p in + + let tm = mklApp cchecker [|t_i; t_func; t_atom; t_form; rootsCstr; used_rootsCstr; certif|] in + + let res = Vnorm.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in + Format.eprintf " = %s\n : bool@." + (if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then + "true" else "false") + + +(* Tactic *) + +let build_body rt ro ra rf l b (max_id, confl) = + let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in + let certif = + mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in + + let t_atom = Atom.interp_tbl ra in + let t_form = snd (Form.interp_tbl rf) in + let t_i = make_t_i rt in + let t_func = make_t_func ro t_i in + + let ntatom = mkName "t_atom" in + let ntform = mkName "t_form" in + let nc = mkName "c" in + let nti = mkName "t_i" in + let ntfunc = mkName "t_func" in + + let vtatom = Term.mkRel 5 in + let vtform = Term.mkRel 4 in + let vc = Term.mkRel 3 in + let vti = Term.mkRel 2 in + let vtfunc = Term.mkRel 1 in + + Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + Term.mkLetIn (nc, certif, Lazy.force ccertif, + Term.mkLetIn (nti, Term.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], + Term.mkLetIn (ntfunc, Term.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], + mklApp cchecker_b_correct + [|vti;vtfunc;vtatom; vtform; l; b; vc; + vm_cast_true (mklApp cchecker_b [|vti;vtfunc;vtatom;vtform;l;b;vc|])|]))))) + + +let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) = + let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in + let certif = + mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in + + let t_atom = Atom.interp_tbl ra in + let t_form = snd (Form.interp_tbl rf) in + let t_i = make_t_i rt in + let t_func = make_t_func ro t_i in + + let ntatom = mkName "t_atom" in + let ntform = mkName "t_form" in + let nc = mkName "c" in + let nti = mkName "t_i" in + let ntfunc = mkName "t_func" in + + let vtatom = Term.mkRel 5 in + let vtform = Term.mkRel 4 in + let vc = Term.mkRel 3 in + let vti = Term.mkRel 2 in + let vtfunc = Term.mkRel 1 in + + Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + Term.mkLetIn (nc, certif, Lazy.force ccertif, + Term.mkLetIn (nti, Term.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], + Term.mkLetIn (ntfunc, Term.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], + mklApp cchecker_eq_correct + [|vti;vtfunc;vtatom; vtform; l1; l2; l; vc; + vm_cast_true (mklApp cchecker_eq [|vti;vtfunc;vtatom;vtform;l1;l2;l;vc|])|]))))) + + +let get_arguments concl = + let f, args = Term.decompose_app concl in + match args with + | [ty;a;b] when f = Lazy.force ceq && ty = Lazy.force cbool -> a, b + | [a] when f = Lazy.force cis_true -> a, Lazy.force ctrue + | _ -> failwith ("Verit.tactic: can only deal with equality over bool") + + +let make_proof call_solver rt ro rf l = + let fl = Form.flatten rf l in + let root = SmtTrace.mkRootV [l] in + call_solver rt ro fl (root,l) + + +let tactic call_solver rt ro ra rf gl = + let env = Tacmach.pf_env gl in + let sigma = Tacmach.project gl in + let t = Tacmach.pf_concl gl in + + let (forall_let, concl) = Term.decompose_prod_assum t in + let env = Environ.push_rel_context forall_let env in + let a, b = get_arguments concl in + let body = + if (b = Lazy.force ctrue || b = Lazy.force cfalse) then + let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in + let l' = if b = Lazy.force ctrue then Form.neg l else l in + let max_id_confl = make_proof call_solver rt ro rf l' in + build_body rt ro ra rf (Form.to_coq l) b max_id_confl + else + let l1 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in + let l2 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf b in + let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in + let max_id_confl = make_proof call_solver rt ro rf l in + build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in + let compose_lam_assum forall_let body = + List.fold_left (fun t rd -> Term.mkLambda_or_LetIn rd t) body forall_let in + let res = compose_lam_assum forall_let body in + Tactics.exact_no_check res gl diff --git a/src/verit/verit.ml b/src/verit/verit.ml index cb670c4..3a1abc0 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -29,36 +29,10 @@ open SmtAtom let debug = false -(* Interpretation tables *) - -let mk_ftype cod dom = - let typeb = Lazy.force ctype in - let typea = mklApp clist [|typeb|] in - let a = Array.fold_right (fun bt acc -> mklApp ccons [|typeb; Btype.to_coq bt; acc|]) cod (mklApp cnil [|typeb|]) in - let b = Btype.to_coq dom in - mklApp cpair [|typea;typeb;a;b|] - -let make_t_i rt = Btype.interp_tbl rt -let make_t_func ro t_i = Op.interp_tbl (mklApp ctval [|t_i|]) (fun cod dom value -> mklApp cTval [|t_i; mk_ftype cod dom; value|]) ro - - (******************************************************************************) -(** Given a SMT-LIB2 file and a verit trace build *) -(* the corresponding object *) +(* Given a verit trace build the corresponding certif and theorem *) (******************************************************************************) - -let import_smtlib2 rt ro ra rf filename = - let chan = open_in filename in - let lexbuf = Lexing.from_channel chan in - let commands = Smtlib2_parse.main Smtlib2_lex.token lexbuf in - close_in chan; - match commands with - | None -> [] - | Some (Smtlib2_ast.Commands (_,(_,res))) -> - List.rev (List.fold_left (Smtlib2_genConstr.declare_commands rt ro ra rf) [] res) - - let import_trace filename first = let chan = open_in filename in let lexbuf = Lexing.from_channel chan in @@ -100,237 +74,27 @@ let import_trace filename first = | Parsing.Parse_error -> failwith ("Verit.import_trace: parsing error line "^(string_of_int !line)) -let euf_checker_modules = [ ["SMTCoq";"Trace";"Euf_Checker"] ] - -let certif_ops = CoqTerms.make_certif_ops euf_checker_modules -let cCertif = gen_constant euf_checker_modules "Certif" - - let clear_all () = SmtTrace.clear (); VeritSyntax.clear () -let compute_roots roots last_root = - let r = ref last_root in - while (has_prev !r) do - r := prev !r - done; - - let rec find_root i root = function - | [] -> assert false - | t::q -> if Form.equal t root then (i,q) else find_root (i+1) root q in - - let rec used_roots acc i roots r = - if isRoot r.kind then - match r.value with - | Some [root] -> - let (j,roots') = find_root i root roots in - used_roots (j::acc) (j+1) roots' (next r) - | _ -> assert false - else - acc in - - used_roots [] 0 roots !r - - -let parse_certif t_i t_func t_atom t_form root used_root trace fsmt fproof = +let import_all fsmt fproof = clear_all (); let rt = Btype.create () in let ro = Op.create () in let ra = VeritSyntax.ra in let rf = VeritSyntax.rf in - let roots = import_smtlib2 rt ro ra rf fsmt in + let roots = Smtlib2_genConstr.import_smtlib2 rt ro ra rf fsmt in let (max_id, confl) = import_trace fproof None in - let (tres, last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in - let certif = - mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - let ce4 = Structures.mkConst certif in - let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in - let used_roots = compute_roots roots last_root in - let roots = - let res = Array.make (List.length roots + 1) (mkInt 0) in - let i = ref 0 in - List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - Structures.mkArray (Lazy.force cint, res) in - let used_roots = - 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; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in - let ce3 = Structures.mkConst roots in - let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in - let ce3' = Structures.mkConst used_roots in - let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in - let t_i' = make_t_i rt in - let t_func' = make_t_func ro t_i' in - let ce5 = Structures.mkConst t_i' in - let _ = declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition) in - let ce6 = Structures.mkConst t_func' in - let _ = declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition) in - let ce1 = Structures.mkConst (Atom.interp_tbl ra) in - let _ = declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition) in - let ce2 = Structures.mkConst (snd (Form.interp_tbl rf)) in - let _ = declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition) in - () - - -let ccertif = gen_constant euf_checker_modules "certif" -let cchecker = gen_constant euf_checker_modules "checker" -let cchecker_correct = gen_constant euf_checker_modules "checker_correct" + (rt, ro, ra, rf, roots, max_id, confl) -let interp_roots roots = - let interp = Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17) in - match roots with - | [] -> Lazy.force ctrue - | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots -let theorem name fsmt fproof = - clear_all (); - let rt = Btype.create () in - let ro = Op.create () in - let ra = VeritSyntax.ra in - let rf = VeritSyntax.rf in - let roots = import_smtlib2 rt ro ra rf fsmt in - let (max_id, confl) = import_trace fproof None in - let (tres,last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in - let certif = - mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - let used_roots = 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; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, 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 (Form.to_lit j); incr i) roots; - Structures.mkArray (Lazy.force cint, res) in - - let t_atom = Atom.interp_tbl ra in - let t_form = snd (Form.interp_tbl rf) in - let t_i = make_t_i rt in - let t_func = make_t_func ro t_i in - - let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots roots|]|] in - let theorem_proof = - Term.mkLetIn (mkName "used_roots", used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], (*7*) - Term.mkLetIn (mkName "t_atom", t_atom, mklApp carray [|Lazy.force catom|], (*6*) - Term.mkLetIn (mkName "t_form", t_form, mklApp carray [|Lazy.force cform|], (*5*) - Term.mkLetIn (mkName "d", rootsCstr, mklApp carray [|Lazy.force cint|], (*4*) - Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, (*3*) - Term.mkLetIn (mkName "t_i", t_i, mklApp carray [|Lazy.force ctyp_eqb|], (*2*) - Term.mkLetIn (mkName "t_func", t_func, mklApp carray [|mklApp ctval [|t_i|]|], (*1*) - mklApp cchecker_correct - [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3; - vm_cast_true - (mklApp cchecker [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3|])|]))))))) in - let ce = Structures.mkConst theorem_proof in - let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in - () - - -let checker fsmt fproof = - let t1 = Unix.time () in (* for debug *) - clear_all (); - let t2 = Unix.time () in (* for debug *) - let rt = Btype.create () in - let ro = Op.create () in - let ra = VeritSyntax.ra in - let rf = VeritSyntax.rf in - let t3 = Unix.time () in (* for debug *) - let roots = import_smtlib2 rt ro ra rf fsmt in - let t4 = Unix.time () in (* for debug *) - let (max_id, confl) = import_trace fproof None in - let t5 = Unix.time () in (* for debug *) - let (tres,last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in - let t6 = Unix.time () in (* for debug *) - let certif = - mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - let t7 = Unix.time () in (* for debug *) - let used_roots = compute_roots roots last_root in - let t8 = Unix.time () in (* for debug *) - 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; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in - let t9 = Unix.time () in (* for debug *) - 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 (Form.to_lit j); incr i) roots; - Structures.mkArray (Lazy.force cint, res) in - let t10 = Unix.time () in (* for debug *) - - let t_i = make_t_i rt in - let t11 = Unix.time () in (* for debug *) - let t_func = make_t_func ro t_i in - let t12 = Unix.time () in (* for debug *) - let t_atom = Atom.interp_tbl ra in - let t13 = Unix.time () in (* for debug *) - let t_form = snd (Form.interp_tbl rf) in - let t14 = Unix.time () in (* for debug *) - - let tm = mklApp cchecker [|t_i; t_func; t_atom; t_form; rootsCstr; used_rootsCstr; certif|] in - let t15 = Unix.time () in (* for debug *) - - let res = Vnorm.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in - let t16 = Unix.time () in (* for debug *) - Format.eprintf " = %s\n : bool@." - (if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then - "true" else "false"); - let t17 = Unix.time () in (* for debug *) - - (* let expr = Constrextern.extern_constr true Environ.empty_env tm in *) - (* let t16 = Unix.time () in (\* for debug *\) *) - (* let res_aux1 = Glob_term.CbvVm None in *) - (* let t17 = Unix.time () in (\* for debug *\) *) - (* let res_aux2 = Vernacexpr.VernacCheckMayEval(Some res_aux1, None, expr) in *) - (* let t18 = Unix.time () in (\* for debug *\) *) - (* Vernacentries.interp res_aux2; *) - (* let t19 = Unix.time () in (\* for debug *\) *) +let parse_certif t_i t_func t_atom t_form root used_root trace fsmt fproof = + SmtCommands.parse_certif t_i t_func t_atom t_form root used_root trace (import_all fsmt fproof) +let theorem name fsmt fproof = SmtCommands.theorem name (import_all fsmt fproof) +let checker fsmt fproof = SmtCommands.checker (import_all fsmt fproof) - if debug then ( - Printf.printf"Clear: %f -Create hashtables: %f -Import SMT-LIB: %f -Import trace: %f -Compute trace: %f -Build certif: %f -Build roots: %f -Compute used roots: %f -Build used roots: %f -Build t_i: %f -Build t_func: %f -Build t_atom: %f -Build t_form: %f -Build checker call: %f -Compute checker call: %f -Print result: %f\n" (t2-.t1) (t3-.t2) (t4-.t3) (t5-.t4) (t6-.t5) (t7-.t6) (t8-.t7) (t9-.t8) (t10-.t9) (t11-.t10) (t12-.t11) (t13-.t12) (t14-.t13) (t15-.t14) (t16-.t15) (t17-.t16); -(* Printf.printf"Clear: %f *) -(* Create hashtables: %f *) -(* Import SMT-LIB: %f *) -(* Import trace: %f *) -(* Compute trace: %f *) -(* Build certif: %f *) -(* Build roots: %f *) -(* Compute used roots: %f *) -(* Build used roots: %f *) -(* Build t_i: %f *) -(* Build t_func: %f *) -(* Build t_atom: %f *) -(* Build t_form: %f *) -(* Build checker call: %f *) -(* Build constr: %f *) -(* Build conclusion1: %f *) -(* Build conclusion2: %f *) -(* Build conclusion: %f\n" (t2-.t1) (t3-.t2) (t4-.t3) (t5-.t4) (t6-.t5) (t7-.t6) (t8-.t7) (t9-.t8) (t10-.t9) (t11-.t10) (t12-.t11) (t13-.t12) (t14-.t13) (t15-.t14) (t16-.t15) (t17-.t16) (t18-.t17) (t19-.t18); *) - flush stdout) (******************************************************************************) @@ -363,6 +127,7 @@ let export out_channel rt ro l = Format.fprintf fmt ")@\n(check-sat)@\n(exit)@." +(* val call_verit : Btype.reify_tbl -> Op.reify_tbl -> Form.t -> (Form.t clause * Form.t) -> (int * Form.t clause) *) let call_verit rt ro fl root = let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in export outchan rt ro fl; @@ -384,119 +149,10 @@ let call_verit rt ro fl root = | VeritSyntax.Sat -> Structures.error "veriT can't prove this" -let cchecker_b_correct = - gen_constant euf_checker_modules "checker_b_correct" -let cchecker_b = gen_constant euf_checker_modules "checker_b" -let cchecker_eq_correct = - gen_constant euf_checker_modules "checker_eq_correct" -let cchecker_eq = gen_constant euf_checker_modules "checker_eq" - - -let build_body rt ro ra rf l b (max_id, confl) = - let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in - let certif = - mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - - let t_atom = Atom.interp_tbl ra in - let t_form = snd (Form.interp_tbl rf) in - let t_i = make_t_i rt in - let t_func = make_t_func ro t_i in - - let ntatom = mkName "t_atom" in - let ntform = mkName "t_form" in - let nc = mkName "c" in - let nti = mkName "t_i" in - let ntfunc = mkName "t_func" in - - let vtatom = Term.mkRel 5 in - let vtform = Term.mkRel 4 in - let vc = Term.mkRel 3 in - let vti = Term.mkRel 2 in - let vtfunc = Term.mkRel 1 in - - Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, Lazy.force ccertif, - Term.mkLetIn (nti, Term.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], - Term.mkLetIn (ntfunc, Term.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], - mklApp cchecker_b_correct - [|vti;vtfunc;vtatom; vtform; l; b; vc; - vm_cast_true (mklApp cchecker_b [|vti;vtfunc;vtatom;vtform;l;b;vc|])|]))))) - - -let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) = - let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in - let certif = - mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - - let t_atom = Atom.interp_tbl ra in - let t_form = snd (Form.interp_tbl rf) in - let t_i = make_t_i rt in - let t_func = make_t_func ro t_i in - - let ntatom = mkName "t_atom" in - let ntform = mkName "t_form" in - let nc = mkName "c" in - let nti = mkName "t_i" in - let ntfunc = mkName "t_func" in - - let vtatom = Term.mkRel 5 in - let vtform = Term.mkRel 4 in - let vc = Term.mkRel 3 in - let vti = Term.mkRel 2 in - let vtfunc = Term.mkRel 1 in - - Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, Lazy.force ccertif, - Term.mkLetIn (nti, Term.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], - Term.mkLetIn (ntfunc, Term.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], - mklApp cchecker_eq_correct - [|vti;vtfunc;vtatom; vtform; l1; l2; l; vc; - vm_cast_true (mklApp cchecker_eq [|vti;vtfunc;vtatom;vtform;l1;l2;l;vc|])|]))))) - - -let get_arguments concl = - let f, args = Term.decompose_app concl in - match args with - | [ty;a;b] when f = Lazy.force ceq && ty = Lazy.force cbool -> a, b - | [a] when f = Lazy.force cis_true -> a, Lazy.force ctrue - | _ -> failwith ("Verit.tactic: can only deal with equality over bool") - - -let make_proof rt ro rf l = - let fl = Form.flatten rf l in - let root = SmtTrace.mkRootV [l] in - call_verit rt ro fl (root,l) - - let tactic gl = clear_all (); let rt = Btype.create () in let ro = Op.create () in let ra = VeritSyntax.ra in let rf = VeritSyntax.rf in - - let env = Tacmach.pf_env gl in - let sigma = Tacmach.project gl in - let t = Tacmach.pf_concl gl in - - let (forall_let, concl) = Term.decompose_prod_assum t in - let env = Environ.push_rel_context forall_let env in - let a, b = get_arguments concl in - let body = - if (b = Lazy.force ctrue || b = Lazy.force cfalse) then - let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in - let l' = if b = Lazy.force ctrue then Form.neg l else l in - let max_id_confl = make_proof rt ro rf l' in - build_body rt ro ra rf (Form.to_coq l) b max_id_confl - else - let l1 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in - let l2 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf b in - let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in - let max_id_confl = make_proof rt ro rf l in - build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in - let compose_lam_assum forall_let body = - List.fold_left (fun t rd -> Term.mkLambda_or_LetIn rd t) body forall_let in - let res = compose_lam_assum forall_let body in - Tactics.exact_no_check res gl + SmtCommands.tactic call_verit rt ro ra rf gl |