Slothrop/checker.ml at master · iwehrman/Slothrop · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
open Debug
open Tptp
open Terms
open Print
open Unix
open Status
open Learning

module type External_checker =
sig
  val name : string
  val default_cmd : string
  val get_handle : string -> in_channel * out_channel
  val tell : in_channel * out_channel -> string -> unit
  val ask : in_channel * out_channel -> checker_status
  val shutdown : unit -> unit
end
;;

(* FIXME : I have no idea how modules work *)

module AProVE = ( Aprove : External_checker );;
module TPA = ( Tpa : External_checker );;


type checker_t = APROVE | TPA;;

let string_of_checker = function
    APROVE -> AProVE.name
  | TPA -> TPA.name
;;

let checker = ref APROVE;;
let checker_cmd = ref "aprove";;

let use_aprove() = checker_cmd := AProVE.default_cmd; checker := APROVE;;
let use_tpa() = checker_cmd := TPA.default_cmd; checker := TPA;;

let checker_name() = string_of_checker !checker;;

let get_handle cmd =
  match !checker with
      APROVE -> AProVE.get_handle cmd
    | TPA -> TPA.get_handle cmd
;;

let tell handle msg =
  match !checker with
      APROVE -> AProVE.tell handle msg
    | TPA -> TPA.tell handle msg
;;

let ask handle =
  match !checker with
      APROVE -> AProVE.ask handle
    | TPA -> TPA.ask handle
;;

let shutdown () =
  match !checker with
      APROVE -> AProVE.shutdown ()
    | TPA -> TPA.shutdown ()
;;


let call_count = ref 0;;
let call_time = ref 0.;;
let max_call_time = ref 0.;;
let min_call_time = ref max_float;;
let total_yes_time = ref 0.;;
let max_yes_time = ref 0.;;
let yes_count = ref 0;;
let no_count = ref 0;;
let maybe_count = ref 0;;
let orientations = ref 0;;
let duplicates = ref 0;;

let is_terminating all_rules vars =
  match all_rules with
      r::rs ->
        let vars_msg = string_of_vars_tpdb vars in
        let rules_msg = string_of_trs_tpdb all_rules in
        let handle = get_handle !checker_cmd in
          incr call_count;
          debug_if_l TRACE (!debug_checker)
            (lazy ("tell: " ^ (string_of_int !call_count)));
          List.iter (tell handle) [vars_msg;rules_msg];
          let start_t = gettimeofday() in
          let status = ask handle in
          let stop_t = gettimeofday() in
          let this_call_time = stop_t -. start_t in
            call_time := !call_time +. this_call_time;
            if (compare this_call_time !max_call_time) > 0 then
              max_call_time := this_call_time;
            if (compare this_call_time !min_call_time) < 0 then
              min_call_time := this_call_time;
            debug_if_l TRACE (!debug_checker)
              (lazy ("ask: " ^ (string_of_int !call_count) ^ " " ^
                       (string_of_checker_status status) ^ " " ^
                       (string_of_float this_call_time)));
            begin
              match status with
                  TERM_YES ->
                    incr yes_count;
                    total_yes_time := !total_yes_time +. this_call_time;
                    if this_call_time > !max_yes_time then
                      max_yes_time := this_call_time;
                    register_terminating_trs all_rules;
                    true
                | TERM_NO ->
                    incr no_count;
                    register_nonterminating_trs all_rules;
                    false
                | TERM_UNKNOWN ->
                    incr maybe_count;
                    false
            end
    | [] -> failwith "Testing empty TRS for termination"
;;


(* always shutdown checker on exit *)
at_exit (fun () -> shutdown ());;