Changeset 15911


Ignore:
Timestamp:
11/23/08 14:29:29 (5 years ago)
Author:
grochulla
Message:

checker.ml with eprove

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/typechecker/checker_e.ml

    r15903 r15911  
    3333 
    3434let arg_list_counter = ref 1 
    35  
    36 let proof_number = ref 1 
    37  
    38 let get_proof_number () = let r = string_of_int !proof_number in 
    39         incr proof_number; r 
    4035 
    4136let get_x_name () = let r = "x" ^ (string_of_int !arg_list_counter) in 
     
    9590        | ZKFormuli -> insert_zkformuli ()) t 
    9691 
    97 let check_spass (gamma, left, right) t =  
     92let check_spass (gamma, left, right) t proof_number =  
    9893        let t' = List.map (fun a -> match a with 
    99         Proofnumber -> Default(get_proof_number ()) 
     94  | Proofnumber -> Default(string_of_int proof_number) 
    10095        | Tfc -> let b = Buffer.create 100 in 
    10196                ( 
     
    121116        close_out cout; 
    122117        Logmanager.log (Printf.sprintf "%s\n" outfile) ~loglevel:1; 
    123         let ret = Unix.system ("dfg2tptp " ^ outfile ^ " " ^ outfile ^ "tptp && eprover -xAuto -tAuto --tstp-format " ^ outfile ^ "tptp | grep -q \"# Proof found!\"") in 
     118 let ret = Unix.system ("dfg2tptp " ^ outfile ^ " " ^ outfile ^ "tptp && eprover -xAuto -tAuto --tstp-format " ^ outfile ^ "tptp | grep -q \"# Proof found!\"") in 
    124119        match ret with 
    125120        Unix.WEXITED i -> let r = (i = 0) in 
    126121                if r then 
    127122                ( 
    128                         Logmanager.log (Printf.sprintf "exited with %d\n" i) ~loglevel:0;  
     123Logmanager.log (Printf.sprintf "exited with %d\n" i) ~loglevel:0;  
    129124                        Unix.unlink outfile; 
    130125                        Unix.unlink (outfile ^ "tptp"); 
     
    157152        let template' = parse_template () in 
    158153        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:0 
     154        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 
    162157) 
    163158 
     
    186181                let template' = parse_template () in 
    187182                let template = insert_statics "kind" template' in 
    188                 check_spass (f, (formulas f), c) template 
     183                check_spass (f, (formulas f), c) template (-1) 
    189184 
Note: See TracChangeset for help on using the changeset viewer.