glpk/glpk_link.ml

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Linear Programming Link                                                                  *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-05-19                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  10 This file contains material that does not depend on the details of the LP.
  11   list processing functions,
  12   IO operations,
  13   glpk function calls.
  14 *)
  15
  16 module Glpk_link  = struct
  17
  18 (*
  19
  20 needs new mktop on platforms that do not support dynamic loading of Str.
  21
  22 ocamlmktop unix.cma nums.cma str.cma -o ocampl
  23 ./ocampl
  24
  25 glpk needs to be installed, and glpsol needs to be found in the path.
  26
  27 needs lib.ml from HOL Light and flyspeck_lib.hl from Flyspeck.
  28 *)
  29
  30
  31 open Str;;
  32 open List;;
  33 let sprintf = Printf.sprintf;;
  34
  35 let (nextc,resetc) =
  36   let counter = ref 0 in
  37   ((fun () ->
  38     counter:= !counter + 1;
  39     !counter),(fun () -> (counter :=0)));;
  40
  41
  42 (* list operations *)
  43 let maxlist0 xs = fold_right max xs 0;; (* NB: value is always at least 0 *)
  44
  45 let get_values key xs =
  46   map snd (find_all (function k,_ -> (k=key)) xs);;
  47
  48 (*
  49 let rec sort cmp lis =  (* from HOL Light lib.ml *)
  50   match lis with
  51     [] -> []
  52   | piv::rest ->
  53       let r,l = partition (cmp piv) rest in
  54       (sort cmp l) @ (piv::(sort cmp r));;
  55 *)
  56
  57 let sort = Lib.sort;;
  58
  59 let (--) = Lib.(--);;
  60
  61 (*
  62 let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);; (* from HOL Light lib.ml *)
  63 *)
  64
  65 let up i = 0 -- (i-1);;
  66
  67 let rec rotateL i xs =
  68   if i=0 then xs
  69   else match xs with
  70     | x::xss -> rotateL ((i-1) mod length xs) (xss @ [x])
  71     | [] -> [];;
  72
  73 let rotateR i = rotateL (-i);;
  74
  75 let rotation xs =
  76   let maxsz = maxlist0 (map length xs) in
  77   flatten (map (fun i -> map (rotateL i) xs) (up maxsz));;
  78
  79
  80 (*
  81    zip from Harrison's lib.ml.
  82    List.combine causes a stack overflow :
  83    let tt = up 30000 in combine tt tt;;
  84    Stack overflow during evaluation (looping recursion?).
  85
  86 let rec zip l1 l2 =
  87   match (l1,l2) with
  88         ([],[]) -> []
  89       | (h1::t1,h2::t2) -> (h1,h2)::(zip t1 t2)
  90       | _ -> failwith "zip";;
  91 *)
  92
  93 let zip = Lib.zip;;
  94
  95 let enumerate xs = zip (up (length xs)) xs;;
  96
  97 let whereis i xs =
  98   let (p,_) = find (function _,j -> j=i) (enumerate xs) in
  99     p;;
 100
 101 let wheremod xs x =
 102   let ys = rotation xs in
 103    (whereis x ys) mod (length xs);;
 104
 105 (* example *)
 106 wheremod [[0;1;2];[3;4;5];[7;8;9]] [8;9;7];;  (* 2 *)
 107
 108
 109 let unsplit = Flyspeck_lib.unsplit;;
 110
 111 let nub = Flyspeck_lib.nub;;
 112
 113 let join_lines = Flyspeck_lib.join_lines;;
 114
 115 (*
 116 let rec nub = function
 117   | [] -> []
 118   | x::xs -> x::filter ((!=) x) (nub xs);;
 119
 120 let unsplit d f = function
 121   | (x::xs) ->  fold_left (fun s t -> s^d^(f t)) (f x) xs
 122   | [] -> "";;
 123
 124 let join_lines  = unsplit "\n" (fun x-> x);;
 125 *)
 126
 127
 128 (* read and write *)
 129
 130 (*
 131 let load_and_close_channel do_close ic =
 132   let rec lf ichan a =
 133     try
 134       lf ic (Pervasives.input_line ic::a)
 135     with End_of_file -> a in
 136     let rs = lf ic [] in
 137       if do_close then Pervasives.close_in ic else ();
 138       rev rs;;
 139
 140 let load_file filename =
 141   let ic = Pervasives.open_in filename in load_and_close_channel true ic;;
 142
 143 *)
 144
 145 let load_and_close_channel = Flyspeck_lib.load_and_close_channel;;
 146
 147 let load_file = Flyspeck_lib.load_file;;
 148
 149 let save_stringarray filename xs =
 150   let oc = open_out filename in
 151     for i=0 to length xs -1
 152     do
 153       Pervasives.output_string oc (nth xs i ^ "\n");
 154       done;
 155     close_out oc;;
 156
 157 let strip_archive filename =  (* strip // comments, blank lines, quotation marks etc. *)
 158   let (ic,oc) = Unix.open_process(sprintf "cat %s | grep -v '=' | grep -v 'list' | grep -v '^//' | grep -v '^$' | grep '^[^a-z/-]' | sed 's/\"[,;]*//g' | sed 's/_//g' " filename) in
 159   let s = load_and_close_channel false ic in
 160   let _ = Unix.close_process (ic,oc) in
 161     s;;
 162
 163 (* example of java style string from hypermap generator. *)
 164 let pentstring = "13_150834109178 18 3 0 1 2 3 3 2 7 3 3 0 2 4 5 4 0 3 4 6 1 0 4 3 7 2 8 3 8 2 1 4 8 1 6 9 3 9 6 10 3 10 6 4 3 10 4 5 4 5 3 7 11 3 10 5 11 3 11 7 12 3 12 7 8 3 12 8 9 3 9 10 11 3 11 12 9 ";;
 165
 166 (* conversion to list.  e.g. convert_to_list pentstring *)
 167
 168 let convert_to_list  =
 169   let split_sp=  Str.split (regexp " +") in
 170   let strip_ = global_replace (regexp "_") "" in
 171   let rec movelist n (x,a) =
 172     if n=0 then (x,a) else match x with y::ys -> movelist (n-1) (ys, y::a) in
 173   let getone (x,a) = match x with
 174     | [] -> ([],a)
 175     | y::ys -> let (u,v) = movelist y (ys,[]) in (u,v::a) in
 176   let rec getall (x,a) =
 177     if (x=[]) then (x,a) else getall (getone (x,a)) in
 178   fun s ->
 179     let h::ss = (split_sp (strip_ s)) in
 180     let _::ns = map int_of_string ss in
 181     let (_,a) = getall (ns,[]) in
 182      (h,rev (map rev a));;
 183
 184
 185 (* Linear programming *)
 186
 187 let display_ampl ampl_datafile ampl_of_bb bb = (* for debugging *)
 188   let outs = open_out ampl_datafile in
 189   let _ = ampl_of_bb outs bb in
 190   let _ = close_out outs in
 191     Sys.command(sprintf "cat %s" ampl_datafile);;
 192
 193 (* model should name the optimal value "optival" *)
 194
 195 let solve_counter=ref 0;;
 196
 197 let solve com model glpk_outfile varname ampl_of_bb bb =
 198   let (ic,oc) = Unix.open_process(com) in
 199   let _ = ampl_of_bb oc bb in
 200   let _ = close_out oc in
 201   let _ = (solve_counter := !solve_counter + 1) in
 202   let inp = load_and_close_channel false ic in
 203   let _ = Unix.close_process (ic,oc) in
 204   (* test for no feasible solution.  There are two different messages. *)
 205 (*  let _ = Sys.command("cat "^ glpk_outfile) in (* debug *) *)
 206   let com2 = sprintf "grep \"PROBLEM HAS NO.*FEASIBLE SOLUTION\" %s" glpk_outfile in
 207   let (ic,oc)  =Unix.open_process(com2) in
 208   let inp2 = load_and_close_channel false ic in
 209   let _ = Unix.close_process(ic,oc) in
 210     (inp2,inp);;
 211
 212 let solve_branch_f model glpk_outfile varname ampl_of_bb bb =
 213   let com = sprintf "glpsol -m %s -d /dev/stdin | tee %s | grep '^%s' | sed 's/.val//' | sed 's/%s = //' "  model glpk_outfile varname varname in
 214   solve com model glpk_outfile varname ampl_of_bb bb;;
 215
 216 let solve_dual_f model glpk_outfile varname ampl_of_bb bb =
 217   let com = sprintf "glpsol -m %s -d /dev/stdin --simplex --exact --dual -w /tmp/dual.out --output /tmp/output.out | tee %s | grep '^%s' | sed 's/.val//' | sed 's/%s = //' "  model glpk_outfile varname varname in
 218   solve com model glpk_outfile varname ampl_of_bb bb;;
 219
 220 let display_lp model ampl_datafile glpk_outfile ampl_of_bb bb =
 221   let oc = open_out ampl_datafile in
 222   let _ = ampl_of_bb oc bb in
 223   let _ = close_out oc in
 224   let com = sprintf "glpsol -m %s -d %s | tee %s" model ampl_datafile glpk_outfile in
 225   let _ = Sys.command(com) in
 226     ();;
 227
 228 let cpx_branch model cpxfile ampl_of_bb bb = (* debug *)
 229   let com = sprintf "glpsol -m %s --wcpxlp %s -d /dev/stdin | grep '^opti' | sed 's/optival = //' "  model cpxfile in
 230   let (ic,oc) = Unix.open_process(com) in
 231   let _ = ampl_of_bb oc bb in
 232   let _ = close_out oc in
 233   let _ = load_and_close_channel false ic in
 234   let _ = Unix.close_process (ic,oc) in
 235   sprintf "cplex file created of lp: %s" cpxfile;;
 236
 237 (* for debugging: reading optimal variables values from the glpk_outfile *)
 238
 239 let get_dumpvar glpk_outfile s = (* read variables from glpk_outfile *)
 240   let com = sprintf "grep '%s' %s | sed 's/^.*= //'  " s glpk_outfile in
 241   let (ic,oc) = Unix.open_process(com) in
 242   let _ = close_out oc in
 243   let inp = load_and_close_channel false ic in
 244   let _ = Unix.close_process(ic,oc) in
 245   inp;;
 246 (* get_dumpvar "yn.0.*=";; *)
 247
 248 end;;