formal_lp/hypermap/main/lp_certificate.hl

   1 module Lp_certificate = struct
   2
   3 (* inequality id, indices of inequalities, coefficients *)
   4 type constraint_type = string * int list * int64 list;;
   5
   6 type terminal_case = {
   7   precision : int;
   8   infeasible: bool;
   9   constraints : constraint_type list;
  10   target_variables : constraint_type list;
  11   variable_bounds : constraint_type list;
  12 };;
  13
  14 (* For testing *)
  15 let empty_terminal = {
  16   precision = 0;
  17   infeasible = false;
  18   constraints = [];
  19   target_variables = [];
  20   variable_bounds = [];
  21 };;
  22
  23 type split_case = {
  24   split_type : string;
  25   split_face : int list;
  26 };;
  27
  28 type lp_certificate_case =
  29     Lp_terminal of terminal_case
  30   | Lp_split of split_case * lp_certificate_case list;;
  31
  32 type lp_certificate = {
  33   hypermap_string : string;
  34   root_case : lp_certificate_case;
  35 };;
  36
  37 type lp_certificate_info = {
  38   terminals : int;
  39   infeasibles: int;
  40   precision_table: (int * int)list;
  41   split_table: (string * int)list;
  42 };;
  43
  44 (* Counts the number of terminal cases *)
  45 let rec count_terminals lp_case =
  46   match lp_case with
  47     | Lp_terminal _ -> 1
  48     | Lp_split (_, cs) -> itlist (+) (map count_terminals cs) 0;;
  49
  50
  51 let case_info lp_case =
  52   let terminals = ref 0 and
  53       infs = ref 0 and
  54       precision = Hashtbl.create 5 and
  55       split = Hashtbl.create 10 in
  56   let add_precision p =
  57     try
  58       let n = Hashtbl.find precision p in
  59         Hashtbl.replace precision p (n + 1)
  60     with Not_found ->
  61       Hashtbl.add precision p 1 in
  62   let add_split name =
  63     try
  64       let n = Hashtbl.find split name in
  65         Hashtbl.replace split name (n + 1)
  66     with Not_found ->
  67       Hashtbl.add split name 1 in
  68   let rec count case =
  69     match case with
  70       | Lp_terminal t ->
  71           let _ = terminals := !terminals + 1 in
  72           let _ = infs := !infs + if t.infeasible then 1 else 0 in
  73             add_precision t.precision
  74       | Lp_split (info, cs) ->
  75           let _ = add_split info.split_type in
  76           let _ = map count cs in
  77             () in
  78   let _ = count lp_case in
  79     {
  80       terminals = !terminals; infeasibles = !infs;
  81       precision_table = Hashtbl.fold (fun key v list -> (key,v) :: list) precision [];
  82       split_table = Hashtbl.fold (fun key v list -> (key,v) :: list) split [];
  83     };;
  84
  85
  86 let certificate_info cert = case_info cert.root_case;;
  87
  88
  89 (* Writes a certificate into a binary file *)
  90 let write_lp_certificates fname (certificates : lp_certificate list) =
  91   let out = open_out_bin fname in
  92   let _ = Marshal.to_channel out certificates [] in
  93     close_out out;;
  94
  95 (* Reads a certificate from a binary file *)
  96 let read_lp_certificates fname =
  97   let input = open_in_bin fname in
  98   let certificates = (Marshal.from_channel input : lp_certificate list) in
  99   let _ = close_in input in
 100     certificates;;
 101
 102 (******************)
 103 (* Test functions *)
 104 (******************)
 105
 106 type test_split = Dummy | Info of string * int list * (test_split list);;
 107
 108 let rec build_test_split case =
 109   match case with
 110     | Lp_terminal _ -> Dummy
 111     | Lp_split (info, cs) ->
 112           Info (info.split_type, info.split_face, map build_test_split cs);;
 113
 114 end;;