diff options
Diffstat (limited to 'src/verit/verit.ml')
| -rw-r--r-- | src/verit/verit.ml | 77 |
1 files changed, 58 insertions, 19 deletions
diff --git a/src/verit/verit.ml b/src/verit/verit.ml index 16968cc..6406500 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -1,13 +1,9 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2016 *) +(* Copyright (C) 2011 - 2019 *) (* *) -(* Michaël Armand *) -(* Benjamin Grégoire *) -(* Chantal Keller *) -(* *) -(* Inria - École Polytechnique - Université Paris-Sud *) +(* See file "AUTHORS" for the list of authors *) (* *) (* This file is distributed under the terms of the CeCILL-C licence *) (* *) @@ -38,7 +34,32 @@ exception Import_trace of int let get_val = function Some a -> a | None -> assert false - + +(* For debugging certif processing : <add_scertif> <select> <occur> <alloc> *) +let print_certif c where= + let r = ref c in + let out_channel = open_out where in + let fmt = Format.formatter_of_out_channel out_channel in + let continue = ref true in + while !continue do + let kind = to_string (!r.kind) in + let id = !r.id in + let pos = match !r.pos with + | None -> "None" + | Some p -> string_of_int p in + let used = !r.used in + Format.fprintf fmt "id:%i kind:%s pos:%s used:%i value:" id kind pos used; + begin match !r.value with + | None -> Format.fprintf fmt "None" + | Some l -> List.iter (fun f -> Form.to_smt Atom.to_smt fmt f; + Format.fprintf fmt " ") l end; + Format.fprintf fmt "\n"; + match !r.next with + | None -> continue := false + | Some n -> r := n + done; + Format.fprintf fmt "@."; close_out out_channel + let import_trace ra' rf' filename first lsmt = let chan = open_in filename in let lexbuf = Lexing.from_channel chan in @@ -105,9 +126,17 @@ let import_all fsmt fproof = 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) + SmtCommands.parse_certif t_i t_func t_atom t_form root used_root trace + (import_all fsmt fproof) + +let checker_debug fsmt fproof = + SmtCommands.checker_debug (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) @@ -137,15 +166,17 @@ let export out_channel rt ro lsmt = ) (Op.to_list ro); List.iter (fun u -> Format.fprintf fmt "(assert "; - Form.to_smt Atom.to_string fmt u; + Form.to_smt Atom.to_smt fmt u; Format.fprintf fmt ")\n") lsmt; Format.fprintf fmt "(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 ra' rf' first lsmt = - let filename, outchan = Filename.open_temp_file "verit_coq" ".smt2" in +let call_verit _ rt ro ra' rf' first lsmt = + let (_, l') = first in + let fl' = Form.flatten rf' l' in + let lsmt = fl'::lsmt in + let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in export outchan rt ro lsmt; close_out outchan; let logfilename = Filename.chop_extension filename ^ ".vtlog" in @@ -157,8 +188,10 @@ let call_verit rt ro ra' rf' first lsmt = let exit_code = Sys.command command in let t1 = Sys.time () in Format.eprintf "Verit = %.5f@." (t1-.t0); + + (* TODO: improve readability: remove the three nested try *) let win = open_in wname in - try + try if exit_code <> 0 then failwith ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); @@ -167,13 +200,17 @@ let call_verit rt ro ra' rf' first lsmt = Structures.error "veriT returns 'unknown'" with End_of_file -> try - let res = import_trace ra' rf' logfilename first lsmt in + let res = import_trace ra' rf' logfilename (Some first) lsmt in close_in win; Sys.remove wname; res with - | VeritSyntax.Sat -> Structures.error "veriT found a counter-example" + | VeritSyntax.Sat -> Structures.error "veriT found a counter-example" with x -> close_in win; Sys.remove wname; raise x -let tactic lcpl lcepl = + +let verit_logic = + SL.of_list [LUF; LLia] + +let tactic_gen vm_cast lcpl lcepl = clear_all (); let rt = SmtBtype.create () in let ro = Op.create () in @@ -181,4 +218,6 @@ let tactic lcpl lcepl = let rf = VeritSyntax.rf in let ra' = VeritSyntax.ra' in let rf' = VeritSyntax.rf' in - SmtCommands.tactic call_verit rt ro ra rf ra' rf' lcpl lcepl + SmtCommands.tactic call_verit verit_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl +let tactic = tactic_gen vm_cast_true +let tactic_no_check = tactic_gen (fun _ -> vm_cast_true_no_check) |