diff options
Diffstat (limited to 'src/verit')
| -rw-r--r-- | src/verit/verit.ml | 20 | ||||
| -rw-r--r-- | src/verit/veritParser.mly | 2 | ||||
| -rw-r--r-- | src/verit/veritSyntax.ml | 10 | ||||
| -rw-r--r-- | src/verit/veritSyntax.mli | 4 |
4 files changed, 18 insertions, 18 deletions
diff --git a/src/verit/verit.ml b/src/verit/verit.ml index 39f60c0..fbc04e3 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -55,7 +55,7 @@ open SmtCertif * done; * Format.fprintf fmt "@."; close_out out_channel *) -let import_trace ra' rf' filename first lsmt = +let import_trace ra_quant rf_quant filename first lsmt = let chan = open_in filename in let lexbuf = Lexing.from_channel chan in let confl_num = ref (-1) in @@ -78,7 +78,7 @@ let import_trace ra' rf' filename first lsmt = close_in chan; let cfirst = ref (VeritSyntax.get_clause !first_num) in let confl = ref (VeritSyntax.get_clause !confl_num) in - let re_hash = Form.hash_hform (Atom.hash_hatom ra') rf' in + let re_hash = Form.hash_hform (Atom.hash_hatom ra_quant) rf_quant in begin match first with | None -> () | Some _ -> @@ -114,10 +114,10 @@ let import_all fsmt fproof = let ro = Op.create () in let ra = VeritSyntax.ra in let rf = VeritSyntax.rf in - 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 = Smtlib2_genConstr.import_smtlib2 rt ro ra rf fsmt in - let (max_id, confl) = import_trace ra' rf' fproof None [] in + let (max_id, confl) = import_trace ra_quant rf_quant fproof None [] in (rt, ro, ra, rf, roots, max_id, confl) @@ -169,7 +169,7 @@ let export out_channel rt ro lsmt = exception Unknown -let call_verit _ rt ro ra' rf' first lsmt = +let call_verit _ rt ro ra_quant rf_quant first lsmt = let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in export outchan rt ro lsmt; close_out outchan; @@ -206,7 +206,7 @@ let call_verit _ rt ro ra' rf' first lsmt = try if exit_code <> 0 then Structures.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); raise_warnings_errors (); - let res = import_trace ra' rf' logfilename (Some first) lsmt in + let res = import_trace ra_quant rf_quant logfilename (Some first) lsmt in close_in win; Sys.remove wname; res with x -> close_in win; Sys.remove wname; match x with @@ -223,8 +223,8 @@ let tactic_gen vm_cast lcpl lcepl = let ro = Op.create () in let ra = VeritSyntax.ra in let rf = VeritSyntax.rf in - let ra' = VeritSyntax.ra' in - let rf' = VeritSyntax.rf' in - SmtCommands.tactic call_verit verit_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl + let ra_quant = VeritSyntax.ra_quant in + let rf_quant = VeritSyntax.rf_quant in + SmtCommands.tactic call_verit verit_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl let tactic = tactic_gen vm_cast_true let tactic_no_check = tactic_gen (fun _ -> vm_cast_true_no_check) diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly index 08c5cb3..c46b7c3 100644 --- a/src/verit/veritParser.mly +++ b/src/verit/veritParser.mly @@ -272,7 +272,7 @@ term: /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean i | VAR args { let f = $1 in let a = $2 in match find_opt_qvar f with | Some bt -> let op = dummy_indexed_op (Rel_name f) [||] bt in false, Form.Atom (Atom.get ~declare:false ra (Aapp (op, Array.of_list (snd (list_dec a))))) | None -> let dl, l = list_dec $2 in dl, Form.Atom (Atom.get ra ~declare:dl (Aapp (SmtMaps.get_fun f, Array.of_list l))) } /* Both */ - | EQ name_term name_term { let t1 = $2 in let t2 = $3 in match t1,t2 with | (decl1, Form.Atom h1), (decl2, Form.Atom h2) when (match Atom.type_of h1 with | SmtBtype.Tbool -> false | _ -> true) -> let decl = decl1 && decl2 in decl, Form.Atom (Atom.mk_eq ra ~declare:decl (Atom.type_of h1) h1 h2) | (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|Form.lit_of_atom_form_lit rf (decl1, t1); Form.lit_of_atom_form_lit rf (decl2, t2)|])) } + | EQ name_term name_term { let t1 = $2 in let t2 = $3 in match t1,t2 with | (decl1, Form.Atom h1), (decl2, Form.Atom h2) when (match Atom.type_of h1 with | SmtBtype.Tbool -> false | _ -> true) -> let decl = decl1 && decl2 in decl, Form.Atom (Atom.mk_eq_sym ra ~declare:decl (Atom.type_of h1) h1 h2) | (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|Form.lit_of_atom_form_lit rf (decl1, t1); Form.lit_of_atom_form_lit rf (decl2, t2)|])) } | EQ nlit lit { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|t1; t2|])) } | EQ name_term nlit { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|Form.lit_of_atom_form_lit rf (decl1, t1); t2|])) } | LET LPAR bindlist RPAR name_term { $3; $5 } diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index b1a6304..422c6f5 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -555,7 +555,7 @@ let init_index lsmt re_hash = List.iter (fun h -> Format.fprintf fmt "%a\n" (Form.to_smt ~debug:true) (re_hash h)) lsmt; Format.fprintf fmt "\n%a\n@." (Form.to_smt ~debug:true) re_hf; flush oc; close_out oc; - failwith "not found: log available" + failwith "Input not found: log available in /tmp/input_not_found.log" let qf_to_add lr = let is_forall l = match Form.pform l with @@ -570,8 +570,8 @@ let qf_to_add lr = let ra = Atom.create () let rf = Form.create () -let ra' = Atom.create () -let rf' = Form.create () +let ra_quant = Atom.create () +let rf_quant = Form.create () let hlets : (string, Form.atom_form_lit) Hashtbl.t = Hashtbl.create 17 @@ -586,6 +586,6 @@ let clear () = clear_solver (); Atom.clear ra; Form.clear rf; - Atom.clear ra'; - Form.clear rf'; + Atom.clear ra_quant; + Form.clear rf_quant; Hashtbl.clear hlets diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli index 7a325a6..bd98ba6 100644 --- a/src/verit/veritSyntax.mli +++ b/src/verit/veritSyntax.mli @@ -52,8 +52,8 @@ val qf_to_add : SmtAtom.Form.t SmtCertif.clause list -> (SmtAtom.Form.t SmtCerti val ra : SmtAtom.Atom.reify_tbl val rf : SmtAtom.Form.reify -val ra' : SmtAtom.Atom.reify_tbl -val rf' : SmtAtom.Form.reify +val ra_quant : SmtAtom.Atom.reify_tbl +val rf_quant : SmtAtom.Form.reify val hlets : (string, Form.atom_form_lit) Hashtbl.t |