Changeset 15911

Timestamp:

11/23/08 14:29:29 (5 years ago)

Author:

grochulla

Message:

checker.ml with eprove

File:

• src/typechecker/checker_e.ml (modified) (5 diffs)

src/typechecker/checker_e.ml

@@ -33 +33 @@
 
 let arg_list_counter = ref 1
-
-let proof_number = ref 1
-
-let get_proof_number () = let r = string_of_int !proof_number in
-        incr proof_number; r
 
 let get_x_name () = let r = "x" ^ (string_of_int !arg_list_counter) in
@@ -95 +90 @@
         | ZKFormuli -> insert_zkformuli ()) t
 
-let check_spass (gamma, left, right) t = 
+let check_spass (gamma, left, right) t proof_number = 
         let t' = List.map (fun a -> match a with
-        Proofnumber -> Default(get_proof_number ())
+  | Proofnumber -> Default(string_of_int proof_number)
         | Tfc -> let b = Buffer.create 100 in
                 (
@@ -121 +116 @@
         close_out cout;
         Logmanager.log (Printf.sprintf "%s\n" outfile) ~loglevel:1;
-        let ret = Unix.system ("dfg2tptp " ^ outfile ^ " " ^ outfile ^ "tptp && eprover -xAuto -tAuto --tstp-format " ^ outfile ^ "tptp | grep -q \"# Proof found!\"") in
+ let ret = Unix.system ("dfg2tptp " ^ outfile ^ " " ^ outfile ^ "tptp && eprover -xAuto -tAuto --tstp-format " ^ outfile ^ "tptp | grep -q \"# Proof found!\"") in
         match ret with
         Unix.WEXITED i -> let r = (i = 0) in
                 if r then
                 (
-                        Logmanager.log (Printf.sprintf "exited with %d\n" i) ~loglevel:0; 
+Logmanager.log (Printf.sprintf "exited with %d\n" i) ~loglevel:0; 
                         Unix.unlink outfile;
                         Unix.unlink (outfile ^ "tptp");
@@ -157 +152 @@
         let template' = parse_template () in
         let template = insert_statics filename template' in
-        Logmanager.log (Printf.sprintf "spass check results in %b\n"
-                (List.fold_right (fun b a -> check_spass b template && a) (get_proof_obligations ()) true)) ~loglevel:0;
-        Logmanager.log (Printf.sprintf "%d formulas discharged\n" (List.length (get_proof_obligations ()))) ~loglevel:0
+        let (b, nn) = List.fold_right (fun b (a,n) -> ((check_spass b template n) && a, n+1)) (get_proof_obligations ()) (true,1) in
+        Logmanager.log (Printf.sprintf "eprover check results in %b\n" b) ~loglevel:0;
+        Logmanager.log (Printf.sprintf "%d formulas discharged\n" nn ) ~loglevel:0
 )
 
@@ -186 +181 @@
                 let template' = parse_template () in
                 let template = insert_statics "kind" template' in
-                check_spass (f, (formulas f), c) template
+                check_spass (f, (formulas f), c) template (-1)