Changeset 15911
 Timestamp:
 11/23/08 14:29:29 (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/typechecker/checker_e.ml
r15903 r15911 33 33 34 34 let arg_list_counter = ref 1 35 36 let proof_number = ref 137 38 let get_proof_number () = let r = string_of_int !proof_number in39 incr proof_number; r40 35 41 36 let get_x_name () = let r = "x" ^ (string_of_int !arg_list_counter) in … … 95 90  ZKFormuli > insert_zkformuli ()) t 96 91 97 let check_spass (gamma, left, right) t =92 let check_spass (gamma, left, right) t proof_number = 98 93 let t' = List.map (fun a > match a with 99 Proofnumber > Default(get_proof_number ())94  Proofnumber > Default(string_of_int proof_number) 100 95  Tfc > let b = Buffer.create 100 in 101 96 ( … … 121 116 close_out cout; 122 117 Logmanager.log (Printf.sprintf "%s\n" outfile) ~loglevel:1; 123 118 let ret = Unix.system ("dfg2tptp " ^ outfile ^ " " ^ outfile ^ "tptp && eprover xAuto tAuto tstpformat " ^ outfile ^ "tptp  grep q \"# Proof found!\"") in 124 119 match ret with 125 120 Unix.WEXITED i > let r = (i = 0) in 126 121 if r then 127 122 ( 128 123 Logmanager.log (Printf.sprintf "exited with %d\n" i) ~loglevel:0; 129 124 Unix.unlink outfile; 130 125 Unix.unlink (outfile ^ "tptp"); … … 157 152 let template' = parse_template () in 158 153 let template = insert_statics filename template' in 159 Logmanager.log (Printf.sprintf "spass check results in %b\n"160 (List.fold_right (fun b a > check_spass b template && a) (get_proof_obligations ()) true)) ~loglevel:0;161 Logmanager.log (Printf.sprintf "%d formulas discharged\n" (List.length (get_proof_obligations ()))) ~loglevel:0154 let (b, nn) = List.fold_right (fun b (a,n) > ((check_spass b template n) && a, n+1)) (get_proof_obligations ()) (true,1) in 155 Logmanager.log (Printf.sprintf "eprover check results in %b\n" b) ~loglevel:0; 156 Logmanager.log (Printf.sprintf "%d formulas discharged\n" nn ) ~loglevel:0 162 157 ) 163 158 … … 186 181 let template' = parse_template () in 187 182 let template = insert_statics "kind" template' in 188 check_spass (f, (formulas f), c) template 183 check_spass (f, (formulas f), c) template (1) 189 184
Note: See TracChangeset
for help on using the changeset viewer.